1.1 --- a/src/Tools/isac/Build_Isac.thy	Sat Jul 26 14:26:54 2014 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Jul 28 17:06:16 2014 +0200
     1.3 @@ -120,14 +120,7 @@
     1.4    building a hierarchy of theorems according to (1.2), see (*2*) below.
     1.5  *}
     1.6  ML {*(*1*) Free ("123.456", HOLogic.realT) *}
     1.7 -ML {*(*2*)
     1.8 -val unknown = filter ((curry op= "??.unknown") o fst) isacrlsthms';
     1.9 -unknown |> nth 1 |> snd |> term_to_string''' @{theory};
    1.10 -unknown |> nth 2 |> snd |> term_to_string''' @{theory};
    1.11 -(*but these seem ok:*)
    1.12 -  Thm.get_name_hint @{thm add_0};
    1.13 -  Thm.get_name_hint (num_str @{thm add_0});
    1.14 -*}
    1.15 +
    1.16  subsection {* (4) Improve the efficiency of Isac’s rewrite-engine *}
    1.17  subsection {* (5) Adopt Isabelle/jEdit for Isac *}
    1.18  

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sat Jul 26 14:26:54 2014 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Jul 28 17:06:16 2014 +0200
     2.3 @@ -42,14 +42,10 @@
     2.4  
     2.5  subsubsection {* From rule-sets collect theorems, which have been taken from Isabelle *}
     2.6  ML {*
     2.7 -  val isacrlsthms' =                      (*length = 468*)
     2.8 -    thms_of_rlss (KEStore_Elems.get_rlss knowledge_parent) : (thmID * term) list
     2.9 +  val isacrlsthms =                      (*length = 460*)
    2.10 +    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * term) list
    2.11  
    2.12 -  val isacrlsthms = isacrlsthms'            (*length = 457  DELETE AFTER vvv..TODO*)
    2.13 -  (*|> filter (fn (thyID, _) => "??.unknown" = thyID)   ...INVESTIGATE THESE..TODO  length = 9*)
    2.14 -    |> filter_out (fn (thyID, _) => "??.unknown" = thyID) (*DELETE AFTER ^^^..TODO*)
    2.15 -
    2.16 -  val rlsthmsNOTisac = isacrlsthms          (*length = 49*)
    2.17 +  val rlsthmsNOTisac = isacrlsthms       (*length =  36*)
    2.18      |> filter (fn (deriv, _) => 
    2.19        member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))
    2.20      : (thmID * term) list

     3.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Sat Jul 26 14:26:54 2014 +0200
     3.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jul 28 17:06:16 2014 +0200
     3.3 @@ -42,13 +42,22 @@
     3.4  		      mathauthors=["isac-team"], ord = ord})
     3.5      end;
     3.6  
     3.7 +fun revert_sym thy (Thm (thmID, thm)) =
     3.8 +  if (is_sym o thmID_of_derivation_name) thmID
     3.9 +  then 
    3.10 +    let 
    3.11 +      val thmID' = sym_drop thmID
    3.12 +      val thm' = assoc_thm' thy (thmID',"")
    3.13 +      val thmDeriv' = Thm.get_name_hint thm'
    3.14 +    in Thm (thmDeriv', thm') end
    3.15 +  else Thm (Thm.get_name_hint thm, thm)
    3.16  
    3.17 -fun thms_of_rlss rlss = (rlss : (rls' * (theory' * rls)) list)
    3.18 +fun thms_of_rlss thy rlss = (rlss : (rls' * (theory' * rls)) list)
    3.19    |> map (thms_of_rls o #2 o #2)
    3.20    |> flat
    3.21 -  |> map thm_of_thm
    3.22 -  |> gen_distinct Thm.eq_thm
    3.23 -  |> map (fn a => (Thm.get_name_hint a, prop_of a)) (*term adapts to Theory.axioms_of*)
    3.24 +  |> map (revert_sym thy)
    3.25 +  |> map (fn Thm (thmID, thm) => (thmID, prop_of thm)) (*prop_of adapts to Theory.axioms_of*)
    3.26 +  |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) 
    3.27    : (thmID * term) list                              
    3.28  
    3.29  fun collect_thms part thy =

     4.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Sat Jul 26 14:26:54 2014 +0200
     4.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Mon Jul 28 17:06:16 2014 +0200
     4.3 @@ -25,6 +25,8 @@
     4.4  "----------- collect thydata from Test_Build_Thydata.thy ---------";
     4.5  "----------- correct theIDs for e_rls ----------------------------";
     4.6  "----------- correct theIDs for list_rls -------------------------";
     4.7 +"----------- fun revert_sym --------------------------------------";
     4.8 +"----------- fun thms_of_rlss ------------------------------------";
     4.9  "-----------------------------------------------------------------";
    4.10  "-----------------------------------------------------------------";
    4.11  "-----------------------------------------------------------------";
    4.12 @@ -346,3 +348,48 @@
    4.13                                                     ["IsacScripts", "Tools", "Rulesets", "list_rls"],
    4.14    :*)
    4.15  
    4.16 +"----------- fun revert_sym --------------------------------------";
    4.17 +"----------- fun revert_sym --------------------------------------";
    4.18 +"----------- fun revert_sym --------------------------------------";
    4.19 +val thy = @{theory Isac}
    4.20 +val (Thm (thmID, thm)) =
    4.21 +  revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym})))
    4.22 +;
    4.23 +if thmID = "Delete.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
    4.24 +then () else error "fun revert_sym changed 1";
    4.25 +
    4.26 +val (Thm (thmID, thm)) =
    4.27 +  revert_sym thy (Thm ("real_diff_minus", num_str @{thm real_diff_minus}))
    4.28 +;
    4.29 +if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
    4.30 +then () else error "fun revert_sym changed 2"
    4.31 +
    4.32 +"----------- fun thms_of_rlss ------------------------------------";
    4.33 +"----------- fun thms_of_rlss ------------------------------------";
    4.34 +"----------- fun thms_of_rlss ------------------------------------";
    4.35 +val rlss = 
    4.36 +  [("e_rls" : rls', ("KEStore": theory', e_rls)),
    4.37 +  ("discard_minus" : rls', ("Poly": theory', discard_minus))]
    4.38 +;
    4.39 +val [_, (thmID, term)] = thms_of_rlss thy rlss;
    4.40 +(*
    4.41 +if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
    4.42 +then () else error "thms_of_rlss changed"
    4.43 +*)
    4.44 +;
    4.45 +"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac}, rlss);
    4.46 +val rlss' = (rlss : (rls' * (theory' * rls)) list)
    4.47 +  |> map (thms_of_rls o #2 o #2)
    4.48 +    (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
    4.49 +      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
    4.50 +  |> flat
    4.51 +    (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
    4.52 +      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
    4.53 +  |> map (revert_sym thy)
    4.54 +    (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
    4.55 +      Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
    4.56 +  |> map (fn Thm (thmID, thm) => (thmID, prop_of thm))
    4.57 +    (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
    4.58 +      ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
    4.59 +  |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2)
    4.60 +