1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Apr 13 15:31:23 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Apr 13 18:32:01 2020 +0200
     1.3 @@ -438,7 +438,7 @@
     1.4  
     1.5  (** transform binary numeralsstrings **)
     1.6  val numbers_to_string = ThmC_Def.numbers_to_string
     1.7 -val uminus_to_string = ThmC_Def.numbers_to_string
     1.8 +val uminus_to_string = ThmC_Def.uminus_to_string
     1.9  
    1.10  fun mk_Free (s,T) = Free (s, T);
    1.11  fun mk_free T s =  Free (s, T);

     2.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Apr 13 15:31:23 2020 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Apr 13 18:32:01 2020 +0200
     2.3 @@ -109,23 +109,18 @@
     2.4      case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
     2.5    end;
     2.6  
     2.7 -(** transform binary numeralsstrings **)
     2.8 +(** transform binary numerals to "Free (string, T)" **)
     2.9  
    2.10 -(*Makarius 100308, hacked by WN*)
    2.11 +(* Makarius 100308 *)
    2.12  val numbers_to_string =
    2.13    let
    2.14      fun dest_num t =
    2.15        (case try HOLogic.dest_number t of
    2.16 -        SOME (T, i) =>
    2.17 -          (*if T = @{typ int} orelse T = @{typ real} then WN*)
    2.18 -            SOME (Free (signed_string_of_int i, T))
    2.19 -          (*else NONE  WN*)
    2.20 +        SOME (T, i) => SOME (Free (signed_string_of_int i, T))
    2.21        | NONE => NONE);
    2.22      fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
    2.23        | to_str (t as (u1 $ u2)) =
    2.24 -          (case dest_num t of
    2.25 -            SOME t' => t'
    2.26 -          | NONE => to_str u1 $ to_str u2)
    2.27 +          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
    2.28        | to_str t = perhaps dest_num t;
    2.29    in to_str end
    2.30  val uminus_to_string =

     3.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml	Mon Apr 13 15:31:23 2020 +0200
     3.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml	Mon Apr 13 18:32:01 2020 +0200
     3.3 @@ -14,27 +14,22 @@
     3.4    val term_empty: term
     3.5    val type_empty: typ
     3.6  
     3.7 -  val term: term -> string
     3.8 -(*val term_ctxt: Proof.context -> term -> string*)
     3.9 -  val term_in_ctxt: Proof.context -> term -> string
    3.10 -(*val term_thy: theory -> term -> string*)
    3.11 -  val term_in_thy: theory -> term -> string
    3.12 +  val term: term -> term_as_string
    3.13 +  val term_in_ctxt: Proof.context -> term -> term_as_string
    3.14 +  val term_in_thy: theory -> term -> term_as_string
    3.15  
    3.16 -  val term_opt: term option -> string
    3.17 +  val term_opt: term option -> term_as_string
    3.18  
    3.19 -  val terms_short: term list -> string
    3.20 -(*val terms_thy: theory -> term list -> string*)
    3.21 -  val terms_in_thy: theory -> term list -> string
    3.22 +  val terms_short: term list -> term_as_string
    3.23 +  val terms_in_thy: theory -> term list -> term_as_string
    3.24  
    3.25 -  val typ: typ -> string
    3.26 -(*val typ_thyID: ThyC.thyID -> typ -> string*)
    3.27 -  val typ_by_thyID: ThyC.thyID -> typ -> string
    3.28 +  val typ: typ -> term_as_string
    3.29 +  val typ_by_thyID: ThyC.thyID -> typ -> term_as_string
    3.30  
    3.31  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    3.32 -  val terms: term list -> string
    3.33 -(*val term_thyID: ThyC.thyID -> term -> string*)
    3.34 -  val term_by_thyID: ThyC.thyID -> term -> string
    3.35 -  val terms_to_strings: term list -> string list
    3.36 +  val terms: term list -> term_as_string
    3.37 +  val term_by_thyID: ThyC.thyID -> term -> term_as_string
    3.38 +  val terms_to_strings: term list -> term_as_string list
    3.39  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    3.40    (*NONE*)
    3.41  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

     4.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon Apr 13 15:31:23 2020 +0200
     4.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon Apr 13 18:32:01 2020 +0200
     4.3 @@ -505,7 +505,7 @@
     4.4      (XML.Elem (("THEOREM", []), [
     4.5        XML.Elem (("ID", []), [XML.Text ID]),
     4.6        XML.Elem (("FORMULA", []), [
     4.7 -        XML.Text term])])) = (ID, Rewrite.assoc_thm'' (ThyC.Isac ()) ID)
     4.8 +        XML.Text term])])) = (ID, ThmC.assoc_thm'' (ThyC.Isac ()) ID)
     4.9    | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
    4.10  
    4.11  fun xml_of_src Rule.EmptyScr =

     5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon Apr 13 15:31:23 2020 +0200
     5.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon Apr 13 18:32:01 2020 +0200
     5.3 @@ -42,11 +42,11 @@
     5.4      end;
     5.5  
     5.6  fun revert_sym thy (Rule.Thm (thmID, thm)) =
     5.7 -  if (Rtools.is_sym o ThmC_Def.thmID_of_derivation_name) thmID
     5.8 +  if (ThmC.is_sym o ThmC_Def.thmID_of_derivation_name) thmID
     5.9    then 
    5.10      let 
    5.11 -      val thmID' = Rtools.sym_drop thmID
    5.12 -      val thm' = Rewrite.assoc_thm' thy (thmID',"")
    5.13 +      val thmID' = ThmC.sym_drop thmID
    5.14 +      val thm' = ThmC.assoc_thm' thy (thmID',"")
    5.15        val thmDeriv' = Thm.get_name_hint thm'
    5.16      in Rule.Thm (thmDeriv', thm') end
    5.17    else Rule.Thm (Thm.get_name_hint thm, thm)
    5.18 @@ -58,7 +58,7 @@
    5.19    |> map (revert_sym thy)
    5.20    |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
    5.21    |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) 
    5.22 -  : (ThmC_Def.thmID * thm) list                              
    5.23 +  : (ThmC.thmID * thm) list                              
    5.24  
    5.25  (* collect all thydata defined in in a theory *)
    5.26  
    5.27 @@ -211,7 +211,7 @@
    5.28      val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
    5.29    in (the, theID) end
    5.30  
    5.31 -fun make_thm thy part (thmID : ThmC_Def.thmID, thm) (mathauthors : Celem.authors) =
    5.32 +fun make_thm thy part (thmID : ThmC.thmID, thm) (mathauthors : Celem.authors) =
    5.33    let
    5.34      val guh = Celem.thm2guh (part, ThyC.theory2thyID thy) thmID
    5.35      val theID = Rtools.guh2theID guh

     6.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml	Mon Apr 13 15:31:23 2020 +0200
     6.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml	Mon Apr 13 18:32:01 2020 +0200
     6.3 @@ -66,7 +66,7 @@
     6.4    | dropwhile' _ _ _ = error "dropwhile': uncovered case"
     6.5  
     6.6  (* 040214: version for concat_deriv *)
     6.7 -fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
     6.8 +fun rev_deriv' (t, r, (t', a)) = (t', ThmC.sym_rule r, (t, a));
     6.9  
    6.10  fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 
    6.11        (Tactic.Rewrite (id, thm), 

     7.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Mon Apr 13 15:31:23 2020 +0200
     7.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Mon Apr 13 18:32:01 2020 +0200
     7.3 @@ -71,11 +71,11 @@
     7.4  fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
     7.5      let
     7.6        val tid = HOLogic.dest_string thmID
     7.7 -    in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid)) end
     7.8 +    in (Tactic.Rewrite (tid, ThmC.assoc_thm'' thy tid)) end
     7.9    | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
    7.10      let
    7.11        val tid = HOLogic.dest_string thmID
    7.12 -    in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid))) end
    7.13 +    in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, ThmC.assoc_thm'' thy tid))) end
    7.14    | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
    7.15       (Tactic.Rewrite_Set (HOLogic.dest_string rls))
    7.16    | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =

     8.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Mon Apr 13 15:31:23 2020 +0200
     8.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Mon Apr 13 18:32:01 2020 +0200
     8.3 @@ -25,10 +25,6 @@
     8.4         rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
     8.5       | EContThy
     8.6    val guh2filename : Celem.guh -> Celem.filename
     8.7 -  val is_sym : ThmC_Def.thmID -> bool
     8.8 -  val sym_drop : ThmC_Def.thmID -> ThmC_Def.thmID
     8.9 -  val sym_rls : Rule_Set.T -> Rule_Set.T
    8.10 -  val sym_rule : Rule.rule -> Rule.rule
    8.11    val thms_of_rls : Rule_Set.T -> Rule.rule list
    8.12    val theID2filename : Celem.theID -> Celem.filename
    8.13    val no_thycontext : Celem.guh -> bool
    8.14 @@ -98,18 +94,6 @@
    8.15  fun rtas2str rtas = (strs2str o (map rta2str)) rtas
    8.16  val deri2str = rtas2str
    8.17  
    8.18 -(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
    8.19 -fun sym_thm thm =
    8.20 -  let 
    8.21 -    val (deriv,
    8.22 -      {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 
    8.23 -      prop = prop}) = Thm.rep_thm_G thm
    8.24 -    val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
    8.25 -    val prop' = case TermC.strip_imp_prems' prop of
    8.26 -        NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
    8.27 -      | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
    8.28 -  in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end
    8.29 -
    8.30  (* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
    8.31  fun sym_trm trm =
    8.32    let
    8.33 @@ -190,42 +174,8 @@
    8.34      | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
    8.35    in rew_once (! Celem.lim_deriv) [] tt Noap rs end
    8.36  
    8.37 -fun sym_drop thmID =
    8.38 -  case Symbol.explode thmID of
    8.39 -	  "s" :: "y" :: "m" :: "_" :: id => implode id
    8.40 -  | _ => thmID
    8.41 -fun is_sym thmID =
    8.42 -  case Symbol.explode thmID of
    8.43 -	  "s" :: "y" :: "m" :: "_" :: _ => true
    8.44 -  | _ => false;
    8.45 -
    8.46 -(*FIXXXXME.040219: detail has to handle Rls id="sym_..." 
    8.47 -  by applying make_deriv, rev_deriv'; see concat_deriv*)
    8.48 -fun sym_rls Rule_Set.Empty = Rule_Set.Empty
    8.49 -  | sym_rls (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
    8.50 -    Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 
    8.51 -      rules = rules, rew_ord = rew_ord, preconds = preconds}
    8.52 -  | sym_rls (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
    8.53 -    Rule_Set.Seqence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 
    8.54 -      rules = rules, rew_ord = rew_ord, preconds = preconds}
    8.55 -  | sym_rls (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = 
    8.56 -    Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc,  errpatts = errpatts, erls = erls,
    8.57 -      prepat = prepat, rew_ord = rew_ord}
    8.58 -
    8.59 -(* toggles sym_* and keeps "#:" for ad-hoc calculations *)
    8.60 -fun sym_rule (Rule.Thm (thmID, thm)) =
    8.61 -  let
    8.62 -    val thm' = sym_thm thm
    8.63 -    val thmID' = case Symbol.explode thmID of
    8.64 -      "s" :: "y" :: "m" :: "_" :: id => implode id
    8.65 -    | "#" :: ":" :: _ => "#: " ^ ThmC_Def.string_of_thmI thm'
    8.66 -    | _ => "sym_" ^ thmID
    8.67 -  in Rule.Thm (thmID', thm') end
    8.68 -| sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
    8.69 -| sym_rule r = error ("sym_rule: not for " ^  Rule.to_string r)
    8.70 -
    8.71  (*version for reverse rewrite used before 040214*)
    8.72 -fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
    8.73 +fun rev_deriv (t, r, (_, a)) = (ThmC.sym_rule r, (t, a));
    8.74  fun reverse_deriv thy erls rs ro goal t =
    8.75      (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
    8.76  
    8.77 @@ -544,7 +494,7 @@
    8.78          [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
    8.79        | _ => error "guh2rewtac: uncovered case"
    8.80      in case sect of
    8.81 -      "Theorems" => Tactic.Rewrite (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr)
    8.82 +      "Theorems" => Tactic.Rewrite (xstr, ThmC.assoc_thm'' (Celem.assoc_thy thy) xstr)
    8.83      | "Rulesets" => Tactic.Rewrite_Set xstr
    8.84      | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 
    8.85      end
    8.86 @@ -555,7 +505,7 @@
    8.87        | _ => error "guh2rewtac: uncovered case"
    8.88      in case sect of
    8.89        "Theorems" => 
    8.90 -        Tactic.Rewrite_Inst (subs, (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr))
    8.91 +        Tactic.Rewrite_Inst (subs, (xstr, ThmC.assoc_thm'' (Celem.assoc_thy thy) xstr))
    8.92      | "Rulesets" => Tactic.Rewrite_Set_Inst (subs,  xstr)
    8.93      | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 
    8.94      end

     9.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Apr 13 15:31:23 2020 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Apr 13 18:32:01 2020 +0200
     9.3 @@ -50,12 +50,12 @@
     9.4  subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
     9.5  ML \<open>
     9.6    val isacrlsthms =                      (*length = 460*)
     9.7 -    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC_Def.thmID * thm) list
     9.8 +    thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.thmID * thm) list
     9.9  
    9.10    val rlsthmsNOTisac = isacrlsthms       (*length =  36*)
    9.11      |> filter (fn (deriv, _) => 
    9.12        member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
    9.13 -    : (ThmC_Def.thmID * thm) list
    9.14 +    : (ThmC.thmID * thm) list
    9.15  \<close> 
    9.16  
    9.17  subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>

    10.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 15:31:23 2020 +0200
    10.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 18:32:01 2020 +0200
    10.3 @@ -4,10 +4,6 @@
    10.4  
    10.5  signature REWRITE =
    10.6    sig
    10.7 -(*/------- to ThmC_Def -------\*)
    10.8 -    val assoc_thm': theory -> ThmC_Def.thm' -> thm
    10.9 -    val assoc_thm'': theory -> ThmC_Def.thmID -> thm
   10.10 -(*\------- to ThmC_Def -------/*)
   10.11      val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
   10.12      val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
   10.13      val eval_prog_expr: theory -> Rule_Set.T -> term -> term
   10.14 @@ -31,7 +27,6 @@
   10.15      val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
   10.16      val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
   10.17      val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
   10.18 -    val mk_thm: theory -> string -> thm
   10.19      val trace1: int -> string -> unit
   10.20  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.21    end
   10.22 @@ -277,58 +272,6 @@
   10.23  	   handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
   10.24    end;
   10.25  
   10.26 -(* Thm.make_thm added to Pure/thm.ML *)
   10.27 -fun mk_thm thy str = 
   10.28 -  let
   10.29 -    val t = (Thm.term_of o the o (TermC.parse thy)) str
   10.30 -    val t' = case t of
   10.31 -        Const ("Pure.imp", _) $ _ $ _ => t
   10.32 -      | _ => HOLogic.Trueprop $ t
   10.33 -  in Thm.make_thm (Thm.global_cterm_of thy t') end;
   10.34 -
   10.35 -(*/------- to ThmC_Def -------\*)
   10.36 -(* 
   10.37 -  "metaview" as seen from programs and from user input;
   10.38 -  both are parsed as terms by the function package.
   10.39 -*)
   10.40 -fun convert_metaview_to_thmid thy thmid =
   10.41 -  let val thmid' = case thmid of
   10.42 -      "add_commute" => "add.commute"
   10.43 -    | "mult_commute" => "mult.commute"
   10.44 -    | "add_left_commute" => "add.left_commute"
   10.45 -    | "mult_left_commute" => "mult.left_commute"
   10.46 -    | "add_assoc" => "add.assoc"
   10.47 -    | "mult_assoc" => "mult.assoc"
   10.48 -    | _ => thmid
   10.49 -  in (Global_Theory.get_thm thy) thmid' end;
   10.50 -
   10.51 -(* get the theorem associated with the xstring-identifier;
   10.52 -   if the identifier starts with "sym_" then swap lhs = rhs around =
   10.53 -   (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
   10.54 -   identifiers starting with "#" come from Num_Calc and
   10.55 -   get a hand-made theorem (containing numerals only) *)
   10.56 -fun assoc_thm'' thy thmid =
   10.57 -  case Symbol.explode thmid of
   10.58 -    "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
   10.59 -  | "s"::"y"::"m"::"_"::id => ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
   10.60 -  | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
   10.61 -  | _ => thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
   10.62 -fun assoc_thm' thy (thmid, ct') =
   10.63 -  (case Symbol.explode thmid of
   10.64 -    "s"::"y"::"m"::"_"::id => 
   10.65 -      if hd id = "#" 
   10.66 -      then mk_thm thy ct'
   10.67 -      else ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
   10.68 -  | id =>
   10.69 -    if hd id = "#" 
   10.70 -    then mk_thm thy ct'
   10.71 -    else thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
   10.72 -  ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
   10.73 -    raise ERROR
   10.74 -      ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
   10.75 -(*\------- to ThmC_Def -------/*)
   10.76 -
   10.77 -
   10.78  fun eval_prog_expr thy srls t =
   10.79    let val rew = rewrite_set_ thy false srls t;
   10.80    in case rew of SOME (res,_) => res | NONE => t end;

    11.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Mon Apr 13 15:31:23 2020 +0200
    11.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Mon Apr 13 18:32:01 2020 +0200
    11.3 @@ -6,8 +6,21 @@
    11.4  *)
    11.5  signature THEOREM_ISAC =
    11.6  sig
    11.7 +  type thmID = ThmC_Def.thmID;
    11.8    val numerals_to_Free: thm -> thm
    11.9 +  val assoc_thm': theory -> ThmC_Def.thm' -> thm
   11.10 +  val assoc_thm'': theory -> ThmC_Def.thmID -> thm
   11.11  
   11.12 +  val is_sym : thmID -> bool
   11.13 +  val sym_drop : thmID -> thmID
   11.14 +  val sym_rule : Rule.rule -> Rule.rule
   11.15 +  val sym_rls : Rule_Set.T -> Rule_Set.T
   11.16 +
   11.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   11.18 +  (* NONE *)
   11.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   11.20 +  val mk_thm: theory -> string -> thm
   11.21 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.22  end
   11.23  
   11.24  (**)
   11.25 @@ -20,4 +33,99 @@
   11.26  
   11.27  val numerals_to_Free = ThmC_Def.numerals_to_Free
   11.28  
   11.29 +(* Thm.make_thm added to Pure/thm.ML *)
   11.30 +fun mk_thm thy str = 
   11.31 +  let
   11.32 +    val t = (Thm.term_of o the o (TermC.parse thy)) str
   11.33 +    val t' = case t of
   11.34 +        Const ("Pure.imp", _) $ _ $ _ => t
   11.35 +      | _ => HOLogic.Trueprop $ t
   11.36 +  in Thm.make_thm (Thm.global_cterm_of thy t') end;
   11.37 +
   11.38 +(* 
   11.39 +  "metaview" as seen from programs and from user input;
   11.40 +  both are parsed as terms by the function package.
   11.41 +*)
   11.42 +fun convert_metaview_to_thmid thy thmid =
   11.43 +  let val thmid' = case thmid of
   11.44 +      "add_commute" => "add.commute"
   11.45 +    | "mult_commute" => "mult.commute"
   11.46 +    | "add_left_commute" => "add.left_commute"
   11.47 +    | "mult_left_commute" => "mult.left_commute"
   11.48 +    | "add_assoc" => "add.assoc"
   11.49 +    | "mult_assoc" => "mult.assoc"
   11.50 +    | _ => thmid
   11.51 +  in (Global_Theory.get_thm thy) thmid' end;
   11.52 +
   11.53 +(* get the theorem associated with the xstring-identifier;
   11.54 +   if the identifier starts with "sym_" then swap lhs = rhs around =
   11.55 +   (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
   11.56 +   identifiers starting with "#" come from Num_Calc and
   11.57 +   get a hand-made theorem (containing numerals only) *)
   11.58 +fun assoc_thm'' thy thmid =
   11.59 +  case Symbol.explode thmid of
   11.60 +    "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
   11.61 +  | "s"::"y"::"m"::"_"::id => ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
   11.62 +  | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
   11.63 +  | _ => thmid |> convert_metaview_to_thmid thy |> numerals_to_Free
   11.64 +fun assoc_thm' thy (thmid, ct') =
   11.65 +  (case Symbol.explode thmid of
   11.66 +    "s"::"y"::"m"::"_"::id => 
   11.67 +      if hd id = "#" 
   11.68 +      then mk_thm thy ct'
   11.69 +      else ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
   11.70 +  | id =>
   11.71 +    if hd id = "#" 
   11.72 +    then mk_thm thy ct'
   11.73 +    else thmid |> convert_metaview_to_thmid thy |> numerals_to_Free
   11.74 +  ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
   11.75 +    raise ERROR
   11.76 +      ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
   11.77 +
   11.78 +(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
   11.79 +fun sym_thm thm =
   11.80 +  let 
   11.81 +    val (deriv,
   11.82 +      {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 
   11.83 +      prop = prop}) = Thm.rep_thm_G thm
   11.84 +    val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
   11.85 +    val prop' = case TermC.strip_imp_prems' prop of
   11.86 +        NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
   11.87 +      | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
   11.88 +  in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end
   11.89 +
   11.90 +fun sym_drop thmID =
   11.91 +  case Symbol.explode thmID of
   11.92 +	  "s" :: "y" :: "m" :: "_" :: id => implode id
   11.93 +  | _ => thmID
   11.94 +fun is_sym thmID =
   11.95 +  case Symbol.explode thmID of
   11.96 +	  "s" :: "y" :: "m" :: "_" :: _ => true
   11.97 +  | _ => false;
   11.98 +
   11.99 +(*FIXXXXME.040219: detail has to handle Rls id="sym_..." 
  11.100 +  by applying make_deriv, rev_deriv'; see concat_deriv*)
  11.101 +fun sym_rls Rule_Set.Empty = Rule_Set.Empty
  11.102 +  | sym_rls (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
  11.103 +    Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 
  11.104 +      rules = rules, rew_ord = rew_ord, preconds = preconds}
  11.105 +  | sym_rls (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
  11.106 +    Rule_Set.Seqence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 
  11.107 +      rules = rules, rew_ord = rew_ord, preconds = preconds}
  11.108 +  | sym_rls (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = 
  11.109 +    Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc,  errpatts = errpatts, erls = erls,
  11.110 +      prepat = prepat, rew_ord = rew_ord}
  11.111 +
  11.112 +(* toggles sym_* and keeps "#:" for ad-hoc calculations *)
  11.113 +fun sym_rule (Rule.Thm (thmID, thm)) =
  11.114 +  let
  11.115 +    val thm' = sym_thm thm
  11.116 +    val thmID' = case Symbol.explode thmID of
  11.117 +      "s" :: "y" :: "m" :: "_" :: id => implode id
  11.118 +    | "#" :: ":" :: _ => "#: " ^ ThmC_Def.string_of_thmI thm'
  11.119 +    | _ => "sym_" ^ thmID
  11.120 +  in Rule.Thm (thmID', thm') end
  11.121 +| sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
  11.122 +| sym_rule r = error ("sym_rule: not for " ^  Rule.to_string r)
  11.123 +
  11.124  end

    12.1 --- a/src/Tools/isac/TODO.thy	Mon Apr 13 15:31:23 2020 +0200
    12.2 +++ b/src/Tools/isac/TODO.thy	Mon Apr 13 18:32:01 2020 +0200
    12.3 @@ -24,6 +24,13 @@
    12.4  subsection \<open>Current changeset\<close>
    12.5  text \<open>
    12.6    \begin{itemize}
    12.7 +  \item type_empty -> typ_empty
    12.8 +  \item Seqence -> Sequence
    12.9 +  \item EmptyScr -> Empty_Prog
   12.10 +  \item Num_Calc -> Exec, eval_* -> exec_*
   12.11 +  \item xxx
   12.12 +  \item xxx
   12.13 +  \item xxx
   12.14    \item xxx
   12.15    \item xxx
   12.16    \item xxx

    13.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 13 15:31:23 2020 +0200
    13.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 13 18:32:01 2020 +0200
    13.3 @@ -123,7 +123,7 @@
    13.4    open ContextC;               transfer_asms_from_to;
    13.5    open Tactic;                 (* NONE *)
    13.6    open Model;                  (* NONE *)
    13.7 -  open Rewrite;                mk_thm;
    13.8 +  open Rewrite;
    13.9    open Num_Calc;                   get_pair;
   13.10    open TermC;                  atomt;
   13.11    open Celem;                  e_pbt;