1.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy	Mon Apr 13 18:37:24 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/KEStore.thy	Tue Apr 14 12:39:26 2020 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  ML_file libraryC.sml
     1.5  ML_file theoryC.sml          (*rename identifiers by use of struct.id*)
     1.6  ML_file unparseC.sml
     1.7 -ML_file "rule-def.sml"       (*rename identifiers by use of struct.id*)
     1.8 +ML_file "rule-def.sml"
     1.9  ML_file "thmC-def.sml"       (*rename identifiers by use of struct.id*)
    1.10  ML_file "exec-def.sml"       (*rename identifiers by use of struct.id*)
    1.11  ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)

     2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml	Mon Apr 13 18:37:24 2020 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml	Tue Apr 14 12:39:26 2020 +0200
     2.3 @@ -71,7 +71,7 @@
     2.4      val lim_deriv: int Unsynchronized.ref
     2.5      val isabthys: unit -> theory list
     2.6      val partID': ThyC.theory' -> string
     2.7 -    val thm2guh: string * ThyC.thyID -> ThmC_Def.thmID -> guh
     2.8 +    val thm2guh: string * ThyC.thyID -> ThmC_Def.id -> guh
     2.9      val rls2guh: string * ThyC.thyID -> Rule_Set.id -> guh
    2.10      val theID2guh: theID -> guh
    2.11      type pbt_ = string * (term * term)

     3.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Mon Apr 13 18:37:24 2020 +0200
     3.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Tue Apr 14 12:39:26 2020 +0200
     3.3 @@ -20,6 +20,7 @@
     3.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     3.5    (*NONE*)
     3.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     3.7 +  (*NONE*)
     3.8  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
     3.9  end
    3.10  

     4.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Apr 13 18:37:24 2020 +0200
     4.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Tue Apr 14 12:39:26 2020 +0200
     4.3 @@ -6,29 +6,24 @@
     4.4  *)
     4.5  signature THEOREM_ISAC_DEF =
     4.6  sig
     4.7 -  type thm'
     4.8 -  type thm''
     4.9 -  eqtype thmID
    4.10 +  type T
    4.11 +  eqtype id
    4.12  
    4.13 -  val id_of_thm: Rule_Def.rule -> string
    4.14    val string_of_thmI: thm -> string
    4.15 -  val thmID_of_derivation_name: string -> string
    4.16 -  val thmID_of_derivation_name': thm -> string
    4.17 -  val thm''_of_thm: thm -> thm''
    4.18 -  val thm_of_thm: Rule_Def.rule -> thm
    4.19 +  val thms2str : thm list -> string
    4.20  
    4.21 -(* required only for ProgLang/ListC *)
    4.22 +(* required for ProgLang/ListC BEFORE definition in ------vvv   *)
    4.23 +  val int_of_str_opt: string -> int option  (* belongs to TermC *)
    4.24    val numerals_to_Free: thm -> thm          (* belongs to ThmC  *)
    4.25 -  val int_of_str_opt: string -> int option  (* belongs to TermC *)
    4.26    val numbers_to_string: term -> term       (* belongs to TermC *)
    4.27    val uminus_to_string: term -> term        (* belongs to TermC *)
    4.28  
    4.29 +  val make_thm: theory -> term -> thm
    4.30 +
    4.31  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    4.32 -  val thm2str: thm -> string
    4.33 -  val thms2str : thm list -> string
    4.34 -  val string_of_thm': theory -> thm -> string
    4.35 +  (*NONE*)
    4.36  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    4.37 -  val string_of_thm: thm -> string
    4.38 +  (*NONE*)
    4.39  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.40  end
    4.41  
    4.42 @@ -37,50 +32,12 @@
    4.43  struct
    4.44  (**)
    4.45  
    4.46 -(* TODO CLEANUP Thm:
    4.47 -Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
    4.48 -                   (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC_Def.string_of_thmI
    4.49 -thmID            : type for data from user input + program
    4.50 -thmDeriv         : type for thy_hierarchy ONLY
    4.51 -obsolete types   : thm' (SEE "ad thm'"), thm''. 
    4.52 -revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
    4.53 -activate         : thmID_of_derivation_name'
    4.54 -*)
    4.55 -type thmID = string;    (* identifier for a thm (the shortest string possible, without points)       *)
    4.56 -(*
    4.57 -  ad thm': there are two kinds of theorems ...
    4.58 -  (1) defined in isabelle
    4.59 -  (2) not known, eg. calc_thm, instantiated rls
    4.60 -      the latter have a thmid "#..."
    4.61 -  and thus outside isa we ALWAYS transport both (thmID, ThmC_Def.string_of_thmI)
    4.62 -  and have a special assoc_thm / assoc_rls in this interface
    4.63 -*)
    4.64 -type thm' = thmID * UnparseC.term_as_string;(*WN060610 deprecated in favour of thm'';
    4.65 -WN180324: used in TODO review:
    4.66 -val thm'2xml : int -> ThmC_Def.thm' -> Celem.xml
    4.67 -val assoc_thm': theory -> ThmC_Def.thm' -> thm
    4.68 -| Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
    4.69 -*)
    4.70 -(* tricky combination of (string, term) for theorems in Isac:
    4.71 -  * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
    4.72 -    by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
    4.73 -  * case 2 "sym_..": Global_Theory.get_thm..RS sym
    4.74 -  * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
    4.75 -    from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
    4.76 -*)
    4.77 -type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
    4.78 +type id = string; (* key into KEStore, without point *)
    4.79 +type T = id * Thm.thm;
    4.80  
    4.81 -fun thm2str thm =
    4.82 -  let
    4.83 -    val t = Thm.prop_of thm
    4.84 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
    4.85 -    val ctxt' = Config.put show_markup false ctxt
    4.86 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    4.87 -fun thms2str thms = (strs2str o (map thm2str)) thms
    4.88  
    4.89 +fun string_of_thm thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
    4.90  (*check for [.] as caused by "fun assoc_thm'"*)
    4.91 -fun string_of_thm thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
    4.92 -fun string_of_thm' thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm)
    4.93  fun string_of_thmI thm =
    4.94    let 
    4.95      val str = (de_quote o string_of_thm) thm
    4.96 @@ -91,14 +48,13 @@
    4.97      | _ => str
    4.98    end
    4.99  
   4.100 -fun id_of_thm (Rule_Def.Thm (id, _)) = id
   4.101 -  | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string r *))
   4.102 -
   4.103 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
   4.104 -fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
   4.105 -fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm
   4.106 -  | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ to_string r *))
   4.107 -fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
   4.108 +fun thm2str thm =
   4.109 +  let
   4.110 +    val t = Thm.prop_of thm
   4.111 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
   4.112 +    val ctxt' = Config.put show_markup false ctxt
   4.113 +  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
   4.114 +fun thms2str thms = (strs2str o (map thm2str)) thms
   4.115  
   4.116  fun int_of_str_opt str = 
   4.117    let
   4.118 @@ -109,10 +65,10 @@
   4.119      case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
   4.120    end;
   4.121  
   4.122 -(** transform binary numerals to "Free (string, T)" **)
   4.123  
   4.124 -(* Makarius 100308 *)
   4.125 -val numbers_to_string =
   4.126 +(** transform Isabelle's binary numerals to "Free (string, T)" **)
   4.127 +
   4.128 +val numbers_to_string = (* Makarius 100308 *)
   4.129    let
   4.130      fun dest_num t =
   4.131        (case try HOLogic.dest_number t of
   4.132 @@ -145,4 +101,6 @@
   4.133      val prop' = numbers_to_string prop;
   4.134    in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end;
   4.135  
   4.136 +fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);
   4.137 +
   4.138  (**)end(**)

     5.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon Apr 13 18:37:24 2020 +0200
     5.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Apr 14 12:39:26 2020 +0200
     5.3 @@ -48,7 +48,6 @@
     5.4      val tac2xml : int -> Tactic.input -> Celem.xml
     5.5      val tacs2xml : int -> Tactic.input list -> Celem.xml
     5.6      val theref2xml : int -> ThyC.thyID -> string -> xstring -> string
     5.7 -    val thm'2xml : int -> ThmC_Def.thm' -> Celem.xml
     5.8      val thm''2xml : int -> thm -> Celem.xml
     5.9      val thmstr2xml : int -> string -> Celem.xml
    5.10    end
    5.11 @@ -97,9 +96,9 @@
    5.12    | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
    5.13        indt j ^ "<RULE>\n" ^
    5.14        indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
    5.15 -      indt (j+i) ^ "<STRING> " ^ ThmC_Def.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
    5.16 +      indt (j+i) ^ "<STRING> " ^ ThmC.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
    5.17        indt (j+i) ^ "<GUH> " ^ 
    5.18 -        Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC_Def.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
    5.19 +        Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
    5.20          indt j ^ "</RULE>\n"
    5.21    | rule2xml _ _ (Rule.Num_Calc (_(*termop*), _)) = ""
    5.22  (*FIXXXXXXXME.WN060714 in rls make Num_Calc : calc -> rule [add scriptop!]
    5.23 @@ -467,7 +466,7 @@
    5.24  
    5.25  fun thm''2xml j (thm : thm) =
    5.26      indt j ^ "<THEOREM>\n" ^
    5.27 -    indt (j+i) ^ "<ID> " ^ ThmC_Def.thmID_of_derivation_name' thm ^ " </ID>\n"^
    5.28 +    indt (j+i) ^ "<ID> " ^ ThmC.thmID_of_derivation_name' thm ^ " </ID>\n"^
    5.29      term2xml j (Thm.prop_of thm) ^ "\n" ^
    5.30      indt j ^ "</THEOREM>\n";
    5.31  fun xml_of_thm' (ID, form) =

     6.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Mon Apr 13 18:37:24 2020 +0200
     6.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Tue Apr 14 12:39:26 2020 +0200
     6.3 @@ -679,7 +679,7 @@
     6.4          (#1: (Error_Fill_Def.fillpatID * term * thm * (Selem.subs option) -> Error_Fill_Def.fillpatID))) fillforms of
     6.5        (_, fillform, thm, sube_opt) :: _ =>
     6.6          let
     6.7 -          val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC_Def.thm''_of_thm thm)
     6.8 +          val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.thm''_of_thm thm)
     6.9              fillform (get_loc pt pos) pos pt
    6.10          in
    6.11            (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)

     7.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon Apr 13 18:37:24 2020 +0200
     7.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 14 12:39:26 2020 +0200
     7.3 @@ -4,6 +4,56 @@
     7.4     (c) isac-team
     7.5  *)
     7.6  
     7.7 +signature THEORY_HIERARCHY =
     7.8 +sig
     7.9 +  val collect_cals: string * ThyC.thyID -> (Celem.theID * Celem.thydata) list
    7.10 +  val collect_isab: string -> string * thm -> Celem.theID * Celem.thydata
    7.11 +  val collect_ords: 'a * ThyC.thyID -> (Celem.theID * Celem.thydata) list
    7.12 +  val collect_part: string -> theory -> theory list -> (Celem.theID * Celem.thydata) list
    7.13 +  val collect_rlss: string -> (Rule_Set.id * (ThyC.thyID * Rule_Set.T)) list -> theory list ->
    7.14 +    (Celem.theID * Celem.thydata) list
    7.15 +  val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list
    7.16 +
    7.17 +  val hierarchy_guh: 'a Celem.ptyp list -> string
    7.18 +  val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->
    7.19 +    Celem.thydata * Celem.theID
    7.20 +
    7.21 +  val makeHcal: string * ThyC.thyID -> string * Rule_Def.calc -> Celem.theID * Celem.thydata
    7.22 +  val makeHord: string * ThyC.thyID -> string * ((term * term) list -> term * term -> bool) ->
    7.23 +    Celem.theID * Celem.thydata
    7.24 +  val makeHrls: string -> Rule_Set.id * (ThyC.thyID * Rule_Def.rule_set) ->
    7.25 +    Celem.theID * Celem.thydata
    7.26 +  val makeHthm: string * ThyC.thyID -> thm -> Celem.theID * Celem.thydata
    7.27 +  val make_cal: theory -> Rule_Def.calc -> Celem.authors -> Celem.thydata * Celem.theID
    7.28 +  val make_isa: theory -> ThyC.theory' * ThyC.theory' -> Celem.authors ->
    7.29 +    Celem.thydata * Celem.theID
    7.30 +  val make_ord: theory -> ((term * term) list -> term * term -> bool) -> Celem.authors ->
    7.31 +    Celem.thydata * Celem.theID
    7.32 +  val make_rls: theory -> Rule_Def.rule_set -> Celem.authors -> Celem.thydata * Celem.theID
    7.33 +  val make_thm: theory -> string -> string * thm -> Celem.authors -> Celem.thydata * Celem.theID
    7.34 +  val make_thy: theory -> Celem.authors -> Celem.thydata * Celem.theID
    7.35 +
    7.36 +  val show_thes: unit -> unit
    7.37 +
    7.38 +  val thes2file: Celem.filepath -> unit
    7.39 +  val thms_of: theory -> thm list
    7.40 +  val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Def.rule_set)) list ->
    7.41 +    (string * thm) list
    7.42 +  val thy_hierarchy2file: Celem.filepath -> unit
    7.43 +  val thydata2file: Celem.filepath -> Pos.pos -> Celem.theID -> Celem.thydata -> unit
    7.44 +  val thydata2xml: Celem.theID * Celem.thydata -> Celem.xml
    7.45 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    7.46 +  (*NONE*)
    7.47 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    7.48 +  val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp -> unit
    7.49 +  val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp list -> unit
    7.50 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    7.51 +end
    7.52 +
    7.53 +(**)
    7.54 +structure Thy_Hierarchy(**): THEORY_HIERARCHY(**) =
    7.55 +struct
    7.56 +(**)
    7.57  open TermC (* allows contains_one_of to be infix *)
    7.58  
    7.59  (* copy from mutabelle_extra.ML, fun thms_of *)
    7.60 @@ -13,7 +63,7 @@
    7.61    in
    7.62      filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
    7.63          andalso not (thm contains_one_of fun_ids)
    7.64 -        andalso not (ThmC_Def.thmID_of_derivation_name' thm = "mono"))
    7.65 +        andalso not (ThmC.thmID_of_derivation_name' thm = "mono"))
    7.66          (* created in Biegelinie by partial_function ^^^^^^*)
    7.67        (map snd (Global_Theory.all_thms_of thy false))
    7.68    end
    7.69 @@ -21,7 +71,7 @@
    7.70  (* wrap theory-data into the uniform type thydata *)
    7.71  
    7.72  fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) =
    7.73 -    let val theID = [part, thyID, "Theorems"] @ [ThmC_Def.thmID_of_derivation_name' thm] : Celem.theID
    7.74 +    let val theID = [part, thyID, "Theorems"] @ [ThmC.thmID_of_derivation_name' thm] : Celem.theID
    7.75      in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], 
    7.76  		     mathauthors = ["isac-team"], fillpats = [], thm = thm})
    7.77      end;
    7.78 @@ -41,24 +91,14 @@
    7.79  		      mathauthors = ["isac-team"], ord = ord})
    7.80      end;
    7.81  
    7.82 -fun revert_sym thy (Rule.Thm (thmID, thm)) =
    7.83 -  if (ThmC.is_sym o ThmC_Def.thmID_of_derivation_name) thmID
    7.84 -  then 
    7.85 -    let 
    7.86 -      val thmID' = ThmC.sym_drop thmID
    7.87 -      val thm' = ThmC.assoc_thm' thy (thmID',"")
    7.88 -      val thmDeriv' = Thm.get_name_hint thm'
    7.89 -    in Rule.Thm (thmDeriv', thm') end
    7.90 -  else Rule.Thm (Thm.get_name_hint thm, thm)
    7.91 -
    7.92  (* get all theorems from the list of rule-sets (defined in Knowledge) *)
    7.93  fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list)
    7.94    |> map (Rtools.thms_of_rls o #2 o #2)
    7.95    |> flat
    7.96 -  |> map (revert_sym thy)
    7.97 +  |> map (ThmC.revert_sym thy)
    7.98    |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
    7.99    |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) 
   7.100 -  : (ThmC.thmID * thm) list                              
   7.101 +  : ThmC.T list                              
   7.102  
   7.103  (* collect all thydata defined in in a theory *)
   7.104  
   7.105 @@ -83,7 +123,7 @@
   7.106  (* collect theorems defined in Isabelle *)
   7.107  fun collect_isab isa (thmDeriv, thm) =
   7.108    let val theID =
   7.109 -    [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
   7.110 +    [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
   7.111    in 
   7.112      (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID, 
   7.113        mathauthors = ["Isabelle team, TU Munich"],
   7.114 @@ -211,7 +251,7 @@
   7.115      val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
   7.116    in (the, theID) end
   7.117  
   7.118 -fun make_thm thy part (thmID : ThmC.thmID, thm) (mathauthors : Celem.authors) =
   7.119 +fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Celem.authors) =
   7.120    let
   7.121      val guh = Celem.thm2guh (part, ThyC.theory2thyID thy) thmID
   7.122      val theID = Rtools.guh2theID guh
   7.123 @@ -249,3 +289,5 @@
   7.124        handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
   7.125    in (hrls', theID) end
   7.126  
   7.127 +(**)end(**)
   7.128 +open Thy_Hierarchy

     8.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Apr 13 18:37:24 2020 +0200
     8.2 +++ b/src/Tools/isac/Build_Isac.thy	Tue Apr 14 12:39:26 2020 +0200
     8.3 @@ -120,9 +120,6 @@
     8.4  (*declare [[ML_print_depth = 999]]*)
     8.5  ML \<open>
     8.6  \<close> ML \<open>
     8.7 -parseNEW @{context} "xxx #> aaa bbb"
     8.8 -\<close> ML \<open>
     8.9 -#> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    8.10  \<close> ML \<open>
    8.11  \<close>
    8.12  ML \<open>Num_Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>

     9.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml	Mon Apr 13 18:37:24 2020 +0200
     9.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml	Tue Apr 14 12:39:26 2020 +0200
     9.3 @@ -21,7 +21,7 @@
     9.4    val check_for :
     9.5      term * term ->
     9.6      term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
     9.7 -  val rule2thm'' : Rule.rule -> ThmC_Def.thm''
     9.8 +  val rule2thm'' : Rule.rule -> ThmC.T
     9.9    val rule2rls' : Rule.rule -> string
    9.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    9.11    (*  NONE *)
    9.12 @@ -153,7 +153,7 @@
    9.13    let
    9.14      val thmDeriv = Thm.get_name_hint thm
    9.15      val (part, thyID) = Rtools.thy_containing_thm thmDeriv
    9.16 -    val theID = [part, thyID, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
    9.17 +    val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
    9.18      val fillpats = case Specify.get_the theID of
    9.19        Celem.Hthm {fillpats, ...} => fillpats
    9.20      | _ => error "get_fillpats: uncovered case of get_the"

    10.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Apr 13 18:37:24 2020 +0200
    10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Tue Apr 14 12:39:26 2020 +0200
    10.3 @@ -47,7 +47,7 @@
    10.4    val trtas2str : (term * Rule.rule * (term * term list)) list -> string
    10.5    val eq_Thm : Rule.rule * Rule.rule -> bool
    10.6    val deriv2str : (term * Rule.rule * (term * term list)) list -> string
    10.7 -  val deriv_of_thm'' : ThmC_Def.thm'' -> string
    10.8 +  val deriv_of_thm'' : ThmC.T -> string
    10.9  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.10  
   10.11  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   10.12 @@ -186,7 +186,7 @@
   10.13    | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.to_string r1 ^ "' '" ^ Rule.to_string r2 ^ "'")
   10.14  fun distinct_Thm r = gen_distinct eq_Thm r
   10.15  
   10.16 -fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC_Def.id_of_thm thm))
   10.17 +fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC.id_of_thm thm))
   10.18    handle ERROR _ => false
   10.19  
   10.20  fun thy_containing_thm thmDeriv =
   10.21 @@ -299,7 +299,7 @@
   10.22        Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
   10.23          ContThm
   10.24           {thyID = ThyC.theory'2thyID thy',
   10.25 -          thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
   10.26 +          thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
   10.27            applto = f, applat  = TermC.empty, reword  = ord',
   10.28            asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
   10.29            result = res, resasms = asm, asmrls  = Rule_Set.id erls}
   10.30 @@ -315,7 +315,7 @@
   10.31             ContNOrew
   10.32              {thyID   = ThyC.theory'2thyID thy',
   10.33               thm_rls = 
   10.34 -               Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
   10.35 +               Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
   10.36               applto  = f}
   10.37  		     end
   10.38       | _ => error "context_thy..Rewrite: uncovered case 2")
   10.39 @@ -332,7 +332,7 @@
   10.40  	         ContThmInst
   10.41  	          {thyID = ThyC.theory'2thyID thy',
   10.42  	           thm = 
   10.43 -	             Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
   10.44 +	             Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
   10.45  	           bdvs = subst, thminst = thminst, applto  = f, applat  = TermC.empty, reword  = ord',
   10.46  	           asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
   10.47  	           result = res, resasms = asm, asmrls  = Rule_Set.id erls}
   10.48 @@ -352,7 +352,7 @@
   10.49           in
   10.50             ContNOrewInst
   10.51              {thyID = ThyC.theory'2thyID thy',
   10.52 -             thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
   10.53 +             thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
   10.54               bdvs = subst, thminst = thminst, applto = f}
   10.55           end
   10.56        | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

    11.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Apr 13 18:37:24 2020 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Apr 14 12:39:26 2020 +0200
    11.3 @@ -50,12 +50,12 @@
    11.4  subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
    11.5  ML \<open>
    11.6    val isacrlsthms =                      (*length = 460*)
    11.7 -    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.thmID * thm) list
    11.8 +    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : ThmC.T list
    11.9  
   11.10    val rlsthmsNOTisac = isacrlsthms       (*length =  36*)
   11.11      |> filter (fn (deriv, _) => 
   11.12        member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
   11.13 -    : (ThmC.thmID * thm) list
   11.14 +    : ThmC.T list
   11.15  \<close> 
   11.16  
   11.17  subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>

    12.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Mon Apr 13 18:37:24 2020 +0200
    12.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Tue Apr 14 12:39:26 2020 +0200
    12.3 @@ -195,7 +195,7 @@
    12.4        case rul of
    12.5  	Rule.Thm (thmid, thm) =>
    12.6  	  (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) 
    12.7 -	     rls put_asm (ThmC_Def.thm_of_thm rul) ct of
    12.8 +	     rls put_asm (ThmC.thm_of_thm rul) ct of
    12.9  	     NONE => rew_once ruls asm ct apno thms
   12.10  	   | SOME (ct',asm') => 
   12.11  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))
   12.12 @@ -231,7 +231,7 @@
   12.13        case rul of
   12.14  	Rule.Thm (thmid, thm) =>
   12.15  	  (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) 
   12.16 -	     rls put_asm (ThmC_Def.thm_of_thm rul) ct of
   12.17 +	     rls put_asm (ThmC.thm_of_thm rul) ct of
   12.18  	     NONE => rew_once ruls asm ct apno thms
   12.19  	   | SOME (ct',asm') => 
   12.20  	     rew_once ruls (asm union asm') ct' Appl (rul::thms))

    13.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Apr 13 18:37:24 2020 +0200
    13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 14 12:39:26 2020 +0200
    13.3 @@ -485,15 +485,15 @@
    13.4    in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
    13.5  
    13.6  fun locate_rule thy eval_rls ro [rs] t r =
    13.7 -    if member op = ((map (ThmC_Def.id_of_thm)) rs) (ThmC_Def.id_of_thm r)
    13.8 +    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
    13.9      then 
   13.10 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC_Def.thm_of_thm r) t;
   13.11 +      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
   13.12        in
   13.13          case ropt of SOME ta => [(r, ta)]
   13.14  	      | NONE => ((*tracing 
   13.15 -	          ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
   13.16 +	          ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
   13.17  			end
   13.18 -    else ((*tracing ("### locate_rule:  " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
   13.19 +    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
   13.20    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
   13.21  
   13.22  fun next_rule thy eval_rls ro [rs] t =
   13.23 @@ -546,16 +546,16 @@
   13.24    in (t, t'', [rs(*here only _ONE_*)], der) end;
   13.25  
   13.26  fun locate_rule thy eval_rls ro [rs] t r =
   13.27 -    if member op = ((map (ThmC_Def.id_of_thm)) rs) (ThmC_Def.id_of_thm r)
   13.28 +    if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
   13.29      then 
   13.30 -      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC_Def.thm_of_thm r) t;
   13.31 +      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
   13.32        in 
   13.33          case ropt of
   13.34            SOME ta => [(r, ta)]
   13.35  	      | NONE => 
   13.36 -	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
   13.37 +	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
   13.38  	        []) end
   13.39 -    else ((*tracing ("### locate_rule:  " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
   13.40 +    else ((*tracing ("### locate_rule:  " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
   13.41    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
   13.42  
   13.43  fun next_rule thy eval_rls ro [rs] t =

    14.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 13 18:37:24 2020 +0200
    14.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Apr 14 12:39:26 2020 +0200
    14.3 @@ -21,7 +21,7 @@
    14.4    | End_Ruleset' of term | End_Intersect' of term | End_Proof''
    14.5  
    14.6    | CAScmd' of term
    14.7 -  | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
    14.8 +  | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
    14.9    | Check_Postcond' of Celem.pblID * term
   14.10    | Check_elementwise' of term * TermC.as_string * Selem.result
   14.11    | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
   14.12 @@ -40,8 +40,8 @@
   14.13    | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
   14.14    | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
   14.15  
   14.16 -  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
   14.17 -  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
   14.18 +  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
   14.19 +  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
   14.20    | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
   14.21    | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
   14.22  
   14.23 @@ -91,8 +91,8 @@
   14.24    | Refine_Problem of Celem.pblID
   14.25    | Refine_Tacitly of Celem.pblID
   14.26  
   14.27 -  | Rewrite of ThmC_Def.thm''
   14.28 -  | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
   14.29 +  | Rewrite of ThmC.T
   14.30 +  | Rewrite_Inst of Selem.subs * ThmC.T
   14.31    | Rewrite_Set of Rule_Set.id
   14.32    | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
   14.33  
   14.34 @@ -183,8 +183,8 @@
   14.35       because there all the thms are present with both (thmID, thm)
   14.36       (where user-views can show both or only one of (thmID, thm)),
   14.37       and thm is created from ThmID by assoc_thm'' when entering isabisac *)
   14.38 -  | Rewrite of ThmC_Def.thm''
   14.39 -  | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
   14.40 +  | Rewrite of ThmC.T
   14.41 +  | Rewrite_Inst of Selem.subs * ThmC.T
   14.42    | Rewrite_Set of Rule_Set.id
   14.43    | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
   14.44  
   14.45 @@ -351,7 +351,7 @@
   14.46    | End_Ruleset' of term | End_Intersect' of term | End_Proof''
   14.47    (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
   14.48    | CAScmd' of term
   14.49 -  | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
   14.50 +  | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
   14.51    | Check_Postcond' of Celem.pblID *
   14.52      term         (* returnvalue of program in solve *)
   14.53    | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
   14.54 @@ -381,8 +381,8 @@
   14.55      ThyC.domID *      (* from new pbt?! filled in specify                                     *)
   14.56      Celem.metID *     (* from new pbt?! filled in specify                                     *)
   14.57      Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
   14.58 -  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
   14.59 -  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
   14.60 +  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
   14.61 +  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
   14.62    | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
   14.63    | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
   14.64  

    15.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Mon Apr 13 18:37:24 2020 +0200
    15.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Tue Apr 14 12:39:26 2020 +0200
    15.3 @@ -6,20 +6,36 @@
    15.4  *)
    15.5  signature THEOREM_ISAC =
    15.6  sig
    15.7 -  type thmID = ThmC_Def.thmID;
    15.8 +  type T = ThmC_Def.T
    15.9 +  type id = ThmC_Def.id;
   15.10    val numerals_to_Free: thm -> thm
   15.11 -  val assoc_thm': theory -> ThmC_Def.thm' -> thm
   15.12 -  val assoc_thm'': theory -> ThmC_Def.thmID -> thm
   15.13  
   15.14 -  val is_sym : thmID -> bool
   15.15 -  val sym_drop : thmID -> thmID
   15.16 +  val id_of_thm: Rule_Def.rule -> string
   15.17 +  val string_of_thmI: thm -> string
   15.18 +  val thmID_of_derivation_name: string -> string
   15.19 +  val thmID_of_derivation_name': thm -> string
   15.20 +  val thm''_of_thm: thm -> T
   15.21 +  val thm_of_thm: Rule_Def.rule -> thm
   15.22 +
   15.23 +  val assoc_thm'': theory -> ThmC_Def.id -> thm
   15.24 +
   15.25 +  val is_sym : id -> bool
   15.26 +  val sym_drop : id -> id
   15.27    val sym_rule : Rule.rule -> Rule.rule
   15.28    val sym_rls : Rule_Set.T -> Rule_Set.T
   15.29  
   15.30 +  val revert_sym: theory -> Rule.rule -> Rule.rule
   15.31 +
   15.32  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   15.33 -  (* NONE *)
   15.34 +  val thm2str: thm -> string
   15.35 +  val thms2str : thm list -> string
   15.36 +  val string_of_thm': theory -> thm -> string
   15.37 +  val string_of_thm: thm -> string
   15.38 +(** )
   15.39 +  val mk_thm: theory -> string -> thm
   15.40 +( **)
   15.41  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   15.42 -  val mk_thm: theory -> string -> thm
   15.43 +  (*NONE*)
   15.44  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   15.45  end
   15.46  
   15.47 @@ -28,19 +44,35 @@
   15.48  struct
   15.49  (**)
   15.50  
   15.51 -type thmID = ThmC_Def.thmID;
   15.52 -type thm' = thmID * TermC.as_string;
   15.53 +type T = ThmC_Def.T;
   15.54 +type id = ThmC_Def.id;
   15.55 +type thm' = id * TermC.as_string;
   15.56  
   15.57  val numerals_to_Free = ThmC_Def.numerals_to_Free
   15.58  
   15.59 -(* Thm.make_thm added to Pure/thm.ML *)
   15.60 -fun mk_thm thy str = 
   15.61 +
   15.62 +(*/------- to ThmC -------\*)
   15.63 +fun thm2str thm =
   15.64    let
   15.65 -    val t = (Thm.term_of o the o (TermC.parse thy)) str
   15.66 -    val t' = case t of
   15.67 -        Const ("Pure.imp", _) $ _ $ _ => t
   15.68 -      | _ => HOLogic.Trueprop $ t
   15.69 -  in Thm.make_thm (Thm.global_cterm_of thy t') end;
   15.70 +    val t = Thm.prop_of thm
   15.71 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
   15.72 +    val ctxt' = Config.put show_markup false ctxt
   15.73 +  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
   15.74 +fun thms2str thms = (strs2str o (map thm2str)) thms
   15.75 +
   15.76 +fun string_of_thm thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
   15.77 +fun string_of_thm' thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm)
   15.78 +val string_of_thmI = ThmC_Def.string_of_thmI
   15.79 +
   15.80 +fun id_of_thm (Rule_Def.Thm (id, _)) = id
   15.81 +  | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string r *))
   15.82 +
   15.83 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
   15.84 +fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
   15.85 +fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm
   15.86 +  | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ to_string r *))
   15.87 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : T
   15.88 +(*\------- to ThmC -------/*)
   15.89  
   15.90  (* 
   15.91    "metaview" as seen from programs and from user input;
   15.92 @@ -68,19 +100,6 @@
   15.93    | "s"::"y"::"m"::"_"::id => ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
   15.94    | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
   15.95    | _ => thmid |> convert_metaview_to_thmid thy |> numerals_to_Free
   15.96 -fun assoc_thm' thy (thmid, ct') =
   15.97 -  (case Symbol.explode thmid of
   15.98 -    "s"::"y"::"m"::"_"::id => 
   15.99 -      if hd id = "#" 
  15.100 -      then mk_thm thy ct'
  15.101 -      else ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
  15.102 -  | id =>
  15.103 -    if hd id = "#" 
  15.104 -    then mk_thm thy ct'
  15.105 -    else thmid |> convert_metaview_to_thmid thy |> numerals_to_Free
  15.106 -  ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
  15.107 -    raise ERROR
  15.108 -      ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
  15.109  
  15.110  (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
  15.111  fun sym_thm thm =
  15.112 @@ -94,12 +113,12 @@
  15.113        | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
  15.114    in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end
  15.115  
  15.116 -fun sym_drop thmID =
  15.117 -  case Symbol.explode thmID of
  15.118 +fun sym_drop id =
  15.119 +  case Symbol.explode id of
  15.120  	  "s" :: "y" :: "m" :: "_" :: id => implode id
  15.121 -  | _ => thmID
  15.122 -fun is_sym thmID =
  15.123 -  case Symbol.explode thmID of
  15.124 +  | _ => id
  15.125 +fun is_sym id =
  15.126 +  case Symbol.explode id of
  15.127  	  "s" :: "y" :: "m" :: "_" :: _ => true
  15.128    | _ => false;
  15.129  
  15.130 @@ -128,4 +147,15 @@
  15.131  | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
  15.132  | sym_rule r = error ("sym_rule: not for " ^  Rule.to_string r)
  15.133  
  15.134 -end
  15.135 +fun revert_sym thy (Rule.Thm (thmID, thm)) =
  15.136 +      if (is_sym o thmID_of_derivation_name) thmID
  15.137 +      then 
  15.138 +        let 
  15.139 +          val thmID' = sym_drop thmID
  15.140 +          val thm' = assoc_thm'' thy thmID'
  15.141 +          val thmDeriv' = Thm.get_name_hint thm'
  15.142 +        in Rule.Thm (thmDeriv', thm') end
  15.143 +      else Rule.Thm (Thm.get_name_hint thm, thm)
  15.144 +  | revert_sym _ rule = raise ERROR ("revert_sym: NOT for " ^ Rule.to_string rule)
  15.145 +
  15.146 +(**)end(**)

    16.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Mon Apr 13 18:37:24 2020 +0200
    16.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Tue Apr 14 12:39:26 2020 +0200
    16.3 @@ -152,16 +152,15 @@
    16.4     apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
    16.5  fun adhoc_thm thy (op_, eval_fn) ct =
    16.6    case get_pair thy op_ eval_fn ct of
    16.7 -    NONE =>  NONE
    16.8 -  | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
    16.9 +    NONE => NONE
   16.10 +  | SOME (thmid, t) => SOME (thmid, ThmC_Def.make_thm thy t);
   16.11  
   16.12  (* get a thm applying an op_ to a term;
   16.13     apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
   16.14  fun adhoc_thm1_ thy (op_, eval_fn) ct =
   16.15 -    case eval_fn op_ ct thy of
   16.16 -	NONE => NONE
   16.17 -      | SOME (thmid,t) =>
   16.18 -	SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
   16.19 +  case eval_fn op_ ct thy of
   16.20 +	  NONE => NONE
   16.21 +  | SOME (thmid,t) => SOME (thmid, ThmC_Def.make_thm thy t);
   16.22  
   16.23  (** for ordered and conditional rewriting **)
   16.24  

    17.1 --- a/src/Tools/isac/Specify/appl.sml	Mon Apr 13 18:37:24 2020 +0200
    17.2 +++ b/src/Tools/isac/Specify/appl.sml	Tue Apr 14 12:39:26 2020 +0200
    17.3 @@ -377,7 +377,7 @@
    17.4          then
    17.5      	    case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
    17.6      	      SOME (f', (id, thm))
    17.7 -    	        => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, ThmC_Def.string_of_thmI thm))))
    17.8 +    	        => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
    17.9      	    | NONE => Notappl ("'calculate "^op_^"' not applicable") 
   17.10          else Notappl msg
   17.11        end

    18.1 --- a/src/Tools/isac/Specify/generate.sml	Mon Apr 13 18:37:24 2020 +0200
    18.2 +++ b/src/Tools/isac/Specify/generate.sml	Tue Apr 14 12:39:26 2020 +0200
    18.3 @@ -24,7 +24,7 @@
    18.4      theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
    18.5    val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
    18.6      Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *)
    18.7 -  val generate_inconsistent_rew : Selem.subs option * ThmC_Def.thm'' -> term -> Istate_Def.T * Proof.context ->
    18.8 +  val generate_inconsistent_rew : Selem.subs option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
    18.9      Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
   18.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   18.11    val tacis2str : taci list -> string

    19.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml	Mon Apr 13 18:37:24 2020 +0200
    19.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml	Tue Apr 14 12:39:26 2020 +0200
    19.3 @@ -43,7 +43,7 @@
    19.4  if dn = "Test.radd_0" then () 
    19.5  else error "calcelems.sml Thm.derivation_name changed 1";
    19.6  
    19.7 -val thmID = ThmC_Def.thmID_of_derivation_name dn;
    19.8 +val thmID = ThmC.thmID_of_derivation_name dn;
    19.9  val thyID = ThyC.thyID_of_derivation_name dn;
   19.10  if thmID = "radd_0" andalso thyID = "Test" then ()
   19.11  else error "calcelems.sml Thm.derivation_name changed 2";
   19.12 @@ -94,7 +94,7 @@
   19.13  if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
   19.14  else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
   19.15  
   19.16 -if ThmC_Def.thmID_of_derivation_name long_id = "mult_1_left" then ()
   19.17 +if ThmC.thmID_of_derivation_name long_id = "mult_1_left" then ()
   19.18  else error "fun thmID_of_derivation_name broken";
   19.19  
   19.20  if ThyC.thyID_of_derivation_name long_id = "Groups" then ()

    20.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon Apr 13 18:37:24 2020 +0200
    20.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Apr 14 12:39:26 2020 +0200
    20.3 @@ -19,7 +19,7 @@
    20.4  "-----------------------------------------------------------------";
    20.5  "-----------------------------------------------------------------";
    20.6  "-----------------------------------------------------------------";
    20.7 -
    20.8 +                          
    20.9  
   20.10  
   20.11  "----------- fun rules2xml ---------------------------------------";
   20.12 @@ -112,7 +112,7 @@
   20.13  import isac.util.tactics.SubProblemTactic
   20.14  import isac.util.tactics.Tactic
   20.15  *)
   20.16 -Rewrite: thm'' -> Tactic.input;
   20.17 +Rewrite: ThmC.T -> Tactic.input;
   20.18  val tac = Rewrite("refl", @{thm refl});
   20.19  if xmlstr 0 (xml_of_tac tac) =
   20.20  (*---xml_of_tac------------------------------------------thm'_to_thm''--------------
   20.21 @@ -142,7 +142,7 @@
   20.22  ". (/THEOREM)\n" ^ 
   20.23  "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
   20.24  
   20.25 -Rewrite_Inst: subs * thm'' -> Tactic.input;
   20.26 +Rewrite_Inst: subs * ThmC.T -> Tactic.input;
   20.27  val tac = Rewrite_Inst(["(''bdv'', x)"], ("refl", @{thm refl}));
   20.28  if xmlstr 0 (xml_of_tac tac) = 
   20.29  "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^ 
   20.30 @@ -289,7 +289,7 @@
   20.31  "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
   20.32  (* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
   20.33  while input in frontend is not yet clear: *)
   20.34 -Rewrite_Inst: subs * thm'' -> Tactic.input;
   20.35 +Rewrite_Inst: subs * ThmC.T -> Tactic.input;
   20.36  Substitute  : sube -> Tactic.input;
   20.37  
   20.38  e_subs: TermC.as_string list;

    21.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon Apr 13 18:37:24 2020 +0200
    21.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 14 12:39:26 2020 +0200
    21.3 @@ -41,13 +41,13 @@
    21.4  (*val it = 
    21.5    ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
    21.6     "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
    21.7 -map ThmC_Def.thmID_of_derivation_name' (thms_of thy) = 
    21.8 +map ThmC.thmID_of_derivation_name' (thms_of thy) = 
    21.9    ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", 
   21.10     "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
   21.11  *)
   21.12  val thy = @{theory Biegelinie};
   21.13  val thms = thms_of thy;
   21.14 -if map ThmC_Def.thmID_of_derivation_name' thms = 
   21.15 +if map ThmC.thmID_of_derivation_name' thms = 
   21.16    ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", 
   21.17     "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
   21.18  else error "fun thms_of ...changed";
   21.19 @@ -144,10 +144,10 @@
   21.20  ;
   21.21  thydata2xml (theID, thydata);
   21.22  
   21.23 -"----------- fun Thm.make_thm ------------------------------------";
   21.24 -"----------- fun Thm.make_thm ------------------------------------";
   21.25 -"----------- fun Thm.make_thm ------------------------------------";
   21.26 -"~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
   21.27 +"----------- fun ThmC_Def.make_thm ------------------------------------";
   21.28 +"----------- fun ThmC_Def.make_thm ------------------------------------";
   21.29 +"----------- fun ThmC_Def.make_thm ------------------------------------";
   21.30 +"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : authors)) =
   21.31    (@{theory "Biegelinie"}, "IsacKnowledge",
   21.32      ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
   21.33  	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
   21.34 @@ -172,14 +172,14 @@
   21.35  "----------- fun revert_sym --------------------------------------";
   21.36  "----------- fun revert_sym --------------------------------------";
   21.37  val thy = @{theory Isac_Knowledge}
   21.38 -val (Thm (thmID, thm)) =
   21.39 -  revert_sym thy (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
   21.40 +val (Thm (thmID, thm)) = ThmC.revert_sym thy
   21.41 +  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
   21.42  ;
   21.43  if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
   21.44  then () else error "fun revert_sym changed 1";
   21.45  
   21.46 -val (Thm (thmID, thm)) =
   21.47 -  revert_sym thy (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
   21.48 +val (Thm (thmID, thm)) = ThmC.revert_sym thy
   21.49 +  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
   21.50  ;
   21.51  if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
   21.52  then () else error "fun revert_sym changed 2"
   21.53 @@ -205,7 +205,7 @@
   21.54    |> flat
   21.55      (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
   21.56        Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
   21.57 -  |> map (revert_sym thy)
   21.58 +  |> map (ThmC.revert_sym thy)
   21.59      (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
   21.60        Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
   21.61    |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))

    22.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml	Mon Apr 13 18:37:24 2020 +0200
    22.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml	Tue Apr 14 12:39:26 2020 +0200
    22.3 @@ -1099,7 +1099,7 @@
    22.4    (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
    22.5          val thmDeriv = Thm.get_name_hint thm
    22.6          val (part, thyID) = thy_containing_thm thmDeriv
    22.7 -        val theID = [part, thyID, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
    22.8 +        val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
    22.9          val Hthm {fillpats, ...} = get_the theID
   22.10          val some = map (get_fillform subst (thm, form) errpatID) fillpats;
   22.11  

    23.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Mon Apr 13 18:37:24 2020 +0200
    23.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Tue Apr 14 12:39:26 2020 +0200
    23.3 @@ -139,7 +139,7 @@
    23.4              val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
    23.5              val thm_deriv = Thm.get_name_hint thm;
    23.6  
    23.7 -if thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv)
    23.8 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv)
    23.9     = "thy_isac_Test-thm-radd_left_commute" then ()
   23.10  else error "context_thy mini-subpbl ([2,4], Res) changed";
   23.11  (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
   23.12 @@ -161,7 +161,7 @@
   23.13    applicable_in pos pt tac
   23.14               val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
   23.15               val thm_deriv = Thm.get_name_hint thm;
   23.16 -if thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv) =
   23.17 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv) =
   23.18    "thy_isac_Test-thm-risolate_bdv_add" then ()
   23.19  else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
   23.20  (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*

    24.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon Apr 13 18:37:24 2020 +0200
    24.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Tue Apr 14 12:39:26 2020 +0200
    24.3 @@ -103,7 +103,7 @@
    24.4  val thy = @{theory "Isac_Knowledge"}; 
    24.5  val rew_ord = dummy_ord;
    24.6  val erls = Rule_Set.Empty;
    24.7 -val thm = assoc_thm' thy ("sym_mult_zero_right","");
    24.8 +val thm = assoc_thm'' thy "sym_mult_zero_right";
    24.9  val t = str2term "0 = (0::real)";
   24.10  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
   24.11  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
   24.12 @@ -118,7 +118,7 @@
   24.13  val t'' = subst_atomic subst t';
   24.14  UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
   24.15  
   24.16 -val thm = assoc_thm' thy ("sym","");
   24.17 +val thm = assoc_thm'' thy "sym";
   24.18  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
   24.19  val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
   24.20  *)

    25.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Mon Apr 13 18:37:24 2020 +0200
    25.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Tue Apr 14 12:39:26 2020 +0200
    25.3 @@ -54,11 +54,11 @@
    25.4    val progthys' =                         (*["Program", "Tools", "ListC", "KEStore"]*)
    25.5      drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
    25.6    val isacrlsthms =                      (*length = 460*)
    25.7 -    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * thm) list
    25.8 +    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
    25.9    val rlsthmsNOTisac = isacrlsthms       (*length =  36*)
   25.10      |> filter (fn (deriv, _) => 
   25.11        member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
   25.12 -    : (thmID * thm) list
   25.13 +    : (ThmC.id * thm) list
   25.14  ;
   25.15  (*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
   25.16  (*val thydata_list = ...*)

    26.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Apr 13 18:37:24 2020 +0200
    26.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Tue Apr 14 12:39:26 2020 +0200
    26.3 @@ -806,7 +806,7 @@
    26.4  
    26.5  if length (hd revsets) = 11 then () else error "length of revset changed";
    26.6  if (revsets |> nth 1 |> nth 1 |> id_of_thm) = 
    26.7 -  (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC_Def.thmID_of_derivation_name)
    26.8 +  (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.thmID_of_derivation_name)
    26.9  then () else error "first element of revset changed";
   26.10  if
   26.11  (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
   26.12 @@ -840,8 +840,8 @@
   26.13  ### Isabelle2009-2 for cancel_ (not cancel_p_):
   26.14  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
   26.15     andalso string_of_thm thm = 
   26.16 -           (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac_Knowledge"})))
   26.17 -               (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
   26.18 +           (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
   26.19 +               (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2"))) then ()
   26.20  else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   26.21  \---------------------------------------------------------------------------------------/*)
   26.22  
   26.23 @@ -859,8 +859,8 @@
   26.24  (* find the next rule to apply *)
   26.25    val SOME (r as (Thm (str, thm))) = nex revsets t;
   26.26  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
   26.27 -   string_of_thm thm = (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac_Knowledge"})))
   26.28 -                (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
   26.29 +   string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
   26.30 +                (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2"))) then ()
   26.31  else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   26.32  
   26.33  (*check the next rule*)

    27.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 18:37:24 2020 +0200
    27.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 14 12:39:26 2020 +0200
    27.3 @@ -17,9 +17,7 @@
    27.4  "----------- fun app_rev, Rrls, -------------------------";
    27.5  "----------- 2011 thms with axclasses -------------------";
    27.6  "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
    27.7 -"----------- fun assoc_thm' -----------------------------";
    27.8  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
    27.9 -"----------- fun mk_thm ------------------------------------------------------------------------";
   27.10  "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
   27.11  "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
   27.12  "--------------------------------------------------------";
   27.13 @@ -682,27 +680,6 @@
   27.14  ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
   27.15  
   27.16  
   27.17 -"----------- fun assoc_thm' -----------------------------";
   27.18 -"----------- fun assoc_thm' -----------------------------";
   27.19 -"----------- fun assoc_thm' -----------------------------";
   27.20 -val thy = @{theory ProgLang}
   27.21 -
   27.22 -val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
   27.23 -if string_of_thm' thy tth = "6 = 2 * 3" then ()
   27.24 -else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
   27.25 -
   27.26 -val tth = assoc_thm' thy ("add_0_left","");
   27.27 -if string_of_thm' thy tth = "0 + ?a = ?a" then ()
   27.28 -else error "assoc_thm' (add_0_left,\"\") changed";
   27.29 -
   27.30 -val tth = assoc_thm' thy ("sym_add_0_left","");
   27.31 -if string_of_thm' thy tth = "?t = 0 + ?t" then ()
   27.32 -else error "assoc_thm' (sym_add_0_left,\"\") changed";
   27.33 -
   27.34 -val tth = assoc_thm' thy ("add_commute","");
   27.35 -if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
   27.36 -else error "assoc_thm' (add_commute,\"\") changed"
   27.37 -
   27.38  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
   27.39  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
   27.40  "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
   27.41 @@ -723,72 +700,6 @@
   27.42  if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
   27.43    else error "Pattern.match CHANGED";
   27.44  
   27.45 -"----------- fun mk_thm ------------------------------------------------------------------------";
   27.46 -"----------- fun mk_thm ------------------------------------------------------------------------";
   27.47 -"----------- fun mk_thm ------------------------------------------------------------------------";
   27.48 -val thy = @{theory Isac_Knowledge}
   27.49 -
   27.50 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
   27.51 -val thm = @{thm realpow_twoI};
   27.52 -val patt_str = "?r ^^^ 2 = ?r * ?r";
   27.53 -val term_str = "r ^^^ 2 = r * r";
   27.54 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
   27.55 -case parse_patt thy patt_str of
   27.56 -  Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
   27.57 -      (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
   27.58 -| _ => error "parse_patt  ?r ^^^ 2 = ?r * ?r  changed";
   27.59 -case parse thy term_str of
   27.60 -  NONE => ()
   27.61 -| _ => writeln "parse does NOT take patterns with '?'";
   27.62 -
   27.63 -val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
   27.64 -if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
   27.65 -
   27.66 -val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
   27.67 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
   27.68 -
   27.69 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
   27.70 -(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
   27.71 -  gives a strange thm*);
   27.72 -(*while this..*) 
   27.73 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
   27.74 -  ..gives another strange thm; but it is used and works with rewriting: *);
   27.75 -
   27.76 -val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
   27.77 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
   27.78 -
   27.79 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
   27.80 -val thm = @{thm real_mult_div_cancel2};
   27.81 -val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
   27.82 -val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
   27.83 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
   27.84 -case parse_patt thy patt_str of
   27.85 -  Const ("Pure.imp", _) $ 
   27.86 -    (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
   27.87 -      (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
   27.88 -        (Const ("HOL.Trueprop", _) $
   27.89 -          (Const ("HOL.eq", _) $ _ $ _ )) => ()
   27.90 -| _ => error "parse_patt  ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n  changed";
   27.91 -case parse thy term_str of
   27.92 -  NONE => ()
   27.93 -| _ => writeln "parse does NOT take patterns with '?'";
   27.94 -
   27.95 -val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
   27.96 -if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
   27.97 -
   27.98 -val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
   27.99 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
  27.100 -
  27.101 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
  27.102 -(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
  27.103 -  gives a strange thm*);
  27.104 -(*while this*) 
  27.105 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
  27.106 -  gives another strange thm; but it is used and words with rewriting: *);
  27.107 -
  27.108 -val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
  27.109 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
  27.110 -
  27.111  "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
  27.112  "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
  27.113  "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";

    28.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 13 18:37:24 2020 +0200
    28.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Tue Apr 14 12:39:26 2020 +0200
    28.3 @@ -18,7 +18,7 @@
    28.4  val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
    28.5  val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
    28.6  ;
    28.7 -Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * thm'' * term * result -> Tactic.T;
    28.8 +Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * result -> Tactic.T;
    28.9  val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
   28.10  ;
   28.11  if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";

    29.1 --- a/test/Tools/isac/Test_Some.thy	Mon Apr 13 18:37:24 2020 +0200
    29.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Apr 14 12:39:26 2020 +0200
    29.3 @@ -43,8 +43,8 @@
    29.4    open ContextC;               transfer_asms_from_to;
    29.5    open Tactic;                 (* NONE *)
    29.6    open Model;                  (* NONE *)
    29.7 -  open Rewrite;                mk_thm;
    29.8 -  open Num_Calc;                   get_pair;
    29.9 +  open Rewrite;
   29.10 +  open Num_Calc;               get_pair;
   29.11    open TermC;                  atomt;
   29.12    open Celem;                  e_pbt;
   29.13    open Rule;