1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Tue Apr 14 15:56:15 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Wed Apr 15 10:07:43 2020 +0200
1.3 @@ -17,8 +17,9 @@
1.4 val to_string: Rule_Def.rule -> string
1.5 val to_string_short: Rule_Def.rule -> string
1.6
1.7 + val thm: rule -> thm
1.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.9 - (*NONE*)
1.10 + val thm_id: rule -> string
1.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.12 (*NONE*)
1.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.14 @@ -31,6 +32,7 @@
1.15
1.16 datatype rule = datatype Rule_Def.rule;
1.17 datatype program = datatype Rule_Def.program;
1.18 +type is_as_string = string;
1.19
1.20 type calc = Rule_Def.calc
1.21 type calID = Rule_Def.calID;
1.22 @@ -62,4 +64,9 @@
1.23 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
1.24 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
1.25
1.26 +fun thm_id (Rule_Def.Thm (id, _)) = id
1.27 + | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
1.28 +fun thm (Rule_Def.Thm (_, thm)) = thm
1.29 + | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
1.30 +
1.31 (**)end(**)
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 14 15:56:15 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 10:07:43 2020 +0200
2.3 @@ -96,9 +96,9 @@
2.4 | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
2.5 indt j ^ "<RULE>\n" ^
2.6 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
2.7 - indt (j+i) ^ "<STRING> " ^ ThmC.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
2.8 + indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^
2.9 indt (j+i) ^ "<GUH> " ^
2.10 - Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
2.11 + Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
2.12 indt j ^ "</RULE>\n"
2.13 | rule2xml _ _ (Rule.Num_Calc (_(*termop*), _)) = ""
2.14 (*FIXXXXXXXME.WN060714 in rls make Num_Calc : calc -> rule [add scriptop!]
2.15 @@ -466,7 +466,7 @@
2.16
2.17 fun thm''2xml j (thm : thm) =
2.18 indt j ^ "<THEOREM>\n" ^
2.19 - indt (j+i) ^ "<ID> " ^ ThmC.thmID_of_derivation_name' thm ^ " </ID>\n"^
2.20 + indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^
2.21 term2xml j (Thm.prop_of thm) ^ "\n" ^
2.22 indt j ^ "</THEOREM>\n";
2.23 fun xml_of_thm' (ID, form) =
2.24 @@ -504,7 +504,7 @@
2.25 (XML.Elem (("THEOREM", []), [
2.26 XML.Elem (("ID", []), [XML.Text ID]),
2.27 XML.Elem (("FORMULA", []), [
2.28 - XML.Text term])])) = (ID, ThmC.assoc_thm'' (ThyC.Isac ()) ID)
2.29 + XML.Text term])])) = (ID, ThmC.thm_from_thy (ThyC.Isac ()) ID)
2.30 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
2.31
2.32 fun xml_of_src Rule.EmptyScr =
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Apr 14 15:56:15 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 15 10:07:43 2020 +0200
3.3 @@ -679,7 +679,7 @@
3.4 (#1: (Error_Fill_Def.fillpatID * term * thm * (Selem.subs option) -> Error_Fill_Def.fillpatID))) fillforms of
3.5 (_, fillform, thm, sube_opt) :: _ =>
3.6 let
3.7 - val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.thm''_of_thm thm)
3.8 + val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.of_thm thm)
3.9 fillform (get_loc pt pos) pos pt
3.10 in
3.11 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 14 15:56:15 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 10:07:43 2020 +0200
4.3 @@ -63,7 +63,7 @@
4.4 in
4.5 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
4.6 andalso not (thm contains_one_of fun_ids)
4.7 - andalso not (ThmC.thmID_of_derivation_name' thm = "mono"))
4.8 + andalso not (ThmC.id_of_thm thm = "mono"))
4.9 (* created in Biegelinie by partial_function ^^^^^^*)
4.10 (map snd (Global_Theory.all_thms_of thy false))
4.11 end
4.12 @@ -71,7 +71,7 @@
4.13 (* wrap theory-data into the uniform type thydata *)
4.14
4.15 fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) =
4.16 - let val theID = [part, thyID, "Theorems"] @ [ThmC.thmID_of_derivation_name' thm] : Celem.theID
4.17 + let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Celem.theID
4.18 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
4.19 mathauthors = ["isac-team"], fillpats = [], thm = thm})
4.20 end;
4.21 @@ -95,7 +95,7 @@
4.22 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list)
4.23 |> map (Rtools.thms_of_rls o #2 o #2)
4.24 |> flat
4.25 - |> map (ThmC.revert_sym thy)
4.26 + |> map (ThmC.revert_sym_rule thy)
4.27 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
4.28 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
4.29 : ThmC.T list
4.30 @@ -123,7 +123,7 @@
4.31 (* collect theorems defined in Isabelle *)
4.32 fun collect_isab isa (thmDeriv, thm) =
4.33 let val theID =
4.34 - [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
4.35 + [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
4.36 in
4.37 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID,
4.38 mathauthors = ["Isabelle team, TU Munich"],
5.1 --- a/src/Tools/isac/Build_Isac.thy Tue Apr 14 15:56:15 2020 +0200
5.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 15 10:07:43 2020 +0200
5.3 @@ -18,7 +18,7 @@
5.4 ML_file theoryC.sml
5.5 ML_file unparseC.sml
5.6 ML_file "rule-def.sml"
5.7 - ML_file "thmC-def.sml"
5.8 + ML_file thmC.sml
5.9 ML_file "exec-def.sml"
5.10 ML_file "rewrite-order.sml"
5.11 ML_file rule.sml
6.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Tue Apr 14 15:56:15 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 10:07:43 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', ThmC.sym_rule r, (t, a));
6.8 +fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_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),
6.12 @@ -153,7 +153,7 @@
6.13 let
6.14 val thmDeriv = Thm.get_name_hint thm
6.15 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
6.16 - val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
6.17 + val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
6.18 val fillpats = case Specify.get_the theID of
6.19 Celem.Hthm {fillpats, ...} => fillpats
6.20 | _ => error "get_fillpats: uncovered case of get_the"
7.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Apr 14 15:56:15 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 15 10:07:43 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, ThmC.assoc_thm'' thy tid)) end
7.8 + in (Tactic.Rewrite (tid, ThmC.thm_from_thy 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, ThmC.assoc_thm'' thy tid))) end
7.13 + in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, ThmC.thm_from_thy 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 Tue Apr 14 15:56:15 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 15 10:07:43 2020 +0200
8.3 @@ -175,7 +175,7 @@
8.4 in rew_once (! Celem.lim_deriv) [] tt Noap rs end
8.5
8.6 (*version for reverse rewrite used before 040214*)
8.7 -fun rev_deriv (t, r, (_, a)) = (ThmC.sym_rule r, (t, a));
8.8 +fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
8.9 fun reverse_deriv thy erls rs ro goal t =
8.10 (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
8.11
8.12 @@ -186,7 +186,7 @@
8.13 | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.to_string r1 ^ "' '" ^ Rule.to_string r2 ^ "'")
8.14 fun distinct_Thm r = gen_distinct eq_Thm r
8.15
8.16 -fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC.id_of_thm thm))
8.17 +fun eq_Thms thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
8.18 handle ERROR _ => false
8.19
8.20 fun thy_containing_thm thmDeriv =
8.21 @@ -299,7 +299,7 @@
8.22 Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
8.23 ContThm
8.24 {thyID = ThyC.theory'2thyID thy',
8.25 - thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
8.26 + thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
8.27 applto = f, applat = TermC.empty, reword = ord',
8.28 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
8.29 result = res, resasms = asm, asmrls = Rule_Set.id erls}
8.30 @@ -315,7 +315,7 @@
8.31 ContNOrew
8.32 {thyID = ThyC.theory'2thyID thy',
8.33 thm_rls =
8.34 - Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
8.35 + Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
8.36 applto = f}
8.37 end
8.38 | _ => error "context_thy..Rewrite: uncovered case 2")
8.39 @@ -332,7 +332,7 @@
8.40 ContThmInst
8.41 {thyID = ThyC.theory'2thyID thy',
8.42 thm =
8.43 - Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
8.44 + Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
8.45 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
8.46 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
8.47 result = res, resasms = asm, asmrls = Rule_Set.id erls}
8.48 @@ -352,7 +352,7 @@
8.49 in
8.50 ContNOrewInst
8.51 {thyID = ThyC.theory'2thyID thy',
8.52 - thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
8.53 + thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
8.54 bdvs = subst, thminst = thminst, applto = f}
8.55 end
8.56 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
8.57 @@ -494,7 +494,7 @@
8.58 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
8.59 | _ => error "guh2rewtac: uncovered case"
8.60 in case sect of
8.61 - "Theorems" => Tactic.Rewrite (xstr, ThmC.assoc_thm'' (Celem.assoc_thy thy) xstr)
8.62 + "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (Celem.assoc_thy thy) xstr)
8.63 | "Rulesets" => Tactic.Rewrite_Set xstr
8.64 | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
8.65 end
8.66 @@ -505,7 +505,7 @@
8.67 | _ => error "guh2rewtac: uncovered case"
8.68 in case sect of
8.69 "Theorems" =>
8.70 - Tactic.Rewrite_Inst (subs, (xstr, ThmC.assoc_thm'' (Celem.assoc_thy thy) xstr))
8.71 + Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (Celem.assoc_thy thy) xstr))
8.72 | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr)
8.73 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
8.74 end
9.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Apr 14 15:56:15 2020 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Wed Apr 15 10:07:43 2020 +0200
9.3 @@ -195,7 +195,7 @@
9.4 case rul of
9.5 Rule.Thm (thmid, thm) =>
9.6 (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
9.7 - rls put_asm (ThmC.thm_of_thm rul) ct of
9.8 + rls put_asm (Rule.thm rul) ct of
9.9 NONE => rew_once ruls asm ct apno thms
9.10 | SOME (ct',asm') =>
9.11 rew_once ruls (asm union asm') ct' Appl (rul::thms))
9.12 @@ -231,7 +231,7 @@
9.13 case rul of
9.14 Rule.Thm (thmid, thm) =>
9.15 (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
9.16 - rls put_asm (ThmC.thm_of_thm rul) ct of
9.17 + rls put_asm (Rule.thm rul) ct of
9.18 NONE => rew_once ruls asm ct apno thms
9.19 | SOME (ct',asm') =>
9.20 rew_once ruls (asm union asm') ct' Appl (rul::thms))
10.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Apr 14 15:56:15 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Apr 15 10:07:43 2020 +0200
10.3 @@ -485,15 +485,15 @@
10.4 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
10.5
10.6 fun locate_rule thy eval_rls ro [rs] t r =
10.7 - if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
10.8 + if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
10.9 then
10.10 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
10.11 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
10.12 in
10.13 case ropt of SOME ta => [(r, ta)]
10.14 | NONE => ((*tracing
10.15 - ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) [])
10.16 + ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) [])
10.17 end
10.18 - else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
10.19 + else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
10.20 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
10.21
10.22 fun next_rule thy eval_rls ro [rs] t =
10.23 @@ -546,16 +546,16 @@
10.24 in (t, t'', [rs(*here only _ONE_*)], der) end;
10.25
10.26 fun locate_rule thy eval_rls ro [rs] t r =
10.27 - if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
10.28 + if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
10.29 then
10.30 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
10.31 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
10.32 in
10.33 case ropt of
10.34 SOME ta => [(r, ta)]
10.35 | NONE =>
10.36 - ((*tracing ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
10.37 + ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
10.38 []) end
10.39 - else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
10.40 + else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
10.41 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
10.42
10.43 fun next_rule thy eval_rls ro [rs] t =
11.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Tue Apr 14 15:56:15 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Apr 15 10:07:43 2020 +0200
11.3 @@ -2,7 +2,8 @@
11.4 Author: Walther Neuper
11.5 (c) due to copyright terms
11.6
11.7 -Probably this structure can be dropped due to improved reflection in Isabelle.
11.8 +This structure could be dropped due to improved reflection in Isabelle;
11.9 +but ThmC.sym_thm requires still an identifying string thm_id.
11.10 *)
11.11 signature THEOREM_ISAC =
11.12 sig
11.13 @@ -10,33 +11,25 @@
11.14 type id = ThmC_Def.id;
11.15
11.16 val numerals_to_Free: thm -> thm
11.17 + val thm_from_thy: theory -> ThmC_Def.id -> thm
11.18
11.19 - val id_of_thm: Rule_Def.rule -> string
11.20 - val thmID_of_derivation_name: string -> string
11.21 - val thmID_of_derivation_name': thm -> string
11.22 - val thm''_of_thm: thm -> T
11.23 - val thm_of_thm: Rule_Def.rule -> thm
11.24 + val string_of_thm: thm -> string
11.25 + val string_of_thms: thm list -> string
11.26
11.27 - val assoc_thm'': theory -> ThmC_Def.id -> thm
11.28 + val cut_id: string -> string
11.29 + val id_of_thm: thm -> string
11.30 + val of_thm: thm -> T
11.31
11.32 - val is_sym : id -> bool
11.33 - val sym_drop : id -> id
11.34 - val sym_rule : Rule.rule -> Rule.rule
11.35 - val sym_rls : Rule_Set.T -> Rule_Set.T
11.36 -
11.37 - val revert_sym: theory -> Rule.rule -> Rule.rule
11.38 + val is_sym: id -> bool
11.39 + val revert_sym_rule: theory -> Rule.rule -> Rule.rule
11.40
11.41 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.42 - val thm2str: thm -> string
11.43 - val thms2str : thm list -> string
11.44 - val string_of_thm': theory -> thm -> string
11.45 - val string_of_thm: thm -> string
11.46 - val string_of_thms: thm list -> string
11.47 -(** )
11.48 - val mk_thm: theory -> string -> thm
11.49 -( **)
11.50 + val string_of_thm_in_thy: theory -> thm -> string
11.51 + val id_drop_sym: id -> id
11.52 + val make_sym_rule: Rule.rule -> Rule.rule
11.53 + val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
11.54 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.55 - (*NONE*)
11.56 + val sym_thm: thm -> thm
11.57 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.58 end
11.59
11.60 @@ -47,40 +40,26 @@
11.61
11.62 type T = ThmC_Def.T;
11.63 type id = ThmC_Def.id;
11.64 -type thm' = id * TermC.as_string;
11.65
11.66 -val string_of_thm = ThmC_Def.string_of_thm
11.67 -val string_of_thms = ThmC_Def.string_of_thms
11.68 +val string_of_thm = ThmC_Def.string_of_thm;
11.69 +val string_of_thms = ThmC_Def.string_of_thms;
11.70
11.71 -val numerals_to_Free = ThmC_Def.numerals_to_Free
11.72 +fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into KEStore*)
11.73 +fun id_of_thm thm = (cut_id o Thm.get_name_hint) thm;
11.74 +fun of_thm thm = (id_of_thm thm, thm);
11.75
11.76 +fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm);
11.77
11.78 -(*/------- to ThmC -------\*)
11.79 -fun thm2str thm =
11.80 - let
11.81 - val t = Thm.prop_of thm
11.82 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
11.83 - val ctxt' = Config.put show_markup false ctxt
11.84 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
11.85 -fun thms2str thms = (strs2str o (map thm2str)) thms
11.86
11.87 -fun string_of_thm' thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm)
11.88 +(** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
11.89
11.90 -fun id_of_thm (Rule_Def.Thm (id, _)) = id
11.91 - | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ to_string r *))
11.92 -
11.93 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
11.94 -fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
11.95 -fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm
11.96 - | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ to_string r *))
11.97 -fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : T
11.98 -(*\------- to ThmC -------/*)
11.99 +val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)
11.100
11.101 (*
11.102 "metaview" as seen from programs and from user input;
11.103 both are parsed as terms by the function package.
11.104 *)
11.105 -fun convert_metaview_to_thmid thy thmid =
11.106 +fun id_Isac_to_Isabelle thy thmid = (* Isac uses thmid *)
11.107 let val thmid' = case thmid of
11.108 "add_commute" => "add.commute"
11.109 | "mult_commute" => "mult.commute"
11.110 @@ -90,18 +69,34 @@
11.111 | "mult_assoc" => "mult.assoc"
11.112 | _ => thmid
11.113 in (Global_Theory.get_thm thy) thmid' end;
11.114 +(**)
11.115 +
11.116 +
11.117 +(** handle symmetric equalities, generated by deriving input terms **)
11.118 +
11.119 +fun is_sym id =
11.120 + case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
11.121 + | _ => false;
11.122 +fun id_drop_sym id =
11.123 + case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
11.124 + | _ => id
11.125
11.126 (* get the theorem associated with the xstring-identifier;
11.127 - if the identifier starts with "sym_" then swap lhs = rhs around =
11.128 - (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC.string_of_thm);
11.129 - identifiers starting with "#" come from Num_Calc and
11.130 - get a hand-made theorem (containing numerals only) *)
11.131 -fun assoc_thm'' thy thmid =
11.132 + if the identifier starts with "sym_" then swap lhs = rhs" around "=";
11.133 + in case identifiers starting with "#" come from Num_Calc and
11.134 + get an ad-hoc theorem (containing numerals only) -- rejected here
11.135 +*)
11.136 +fun thm_from_thy thy thmid =
11.137 case Symbol.explode thmid of
11.138 - "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
11.139 - | "s"::"y"::"m"::"_"::id => ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
11.140 - | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
11.141 - | _ => thmid |> convert_metaview_to_thmid thy |> numerals_to_Free
11.142 + "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
11.143 + raise ERROR ("thm_from_thy not impl.for " ^ thmid)
11.144 + | "s" :: "y" :: "m" :: "_" :: id =>
11.145 + ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
11.146 + | "#" :: _ =>
11.147 + raise ERROR ("thm_from_thy not impl.for " ^ thmid)
11.148 + | _ =>
11.149 + (**)thmid |> id_Isac_to_Isabelle thy |> numerals_to_Free(**)
11.150 + (** )thmid |> Global_Theory.get_thm thy |> numerals_to_Free( **)
11.151
11.152 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
11.153 fun sym_thm thm =
11.154 @@ -113,51 +108,42 @@
11.155 val prop' = case TermC.strip_imp_prems' prop of
11.156 NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
11.157 | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
11.158 - in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end
11.159 + in
11.160 + Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop'
11.161 + end
11.162
11.163 -fun sym_drop id =
11.164 - case Symbol.explode id of
11.165 - "s" :: "y" :: "m" :: "_" :: id => implode id
11.166 - | _ => id
11.167 -fun is_sym id =
11.168 - case Symbol.explode id of
11.169 - "s" :: "y" :: "m" :: "_" :: _ => true
11.170 - | _ => false;
11.171 -
11.172 -(*FIXXXXME.040219: detail has to handle Rls id="sym_..."
11.173 - by applying make_deriv, rev_deriv'; see concat_deriv*)
11.174 -fun sym_rls Rule_Set.Empty = Rule_Set.Empty
11.175 - | sym_rls (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
11.176 +fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
11.177 + | make_sym_rule_set (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
11.178 Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
11.179 rules = rules, rew_ord = rew_ord, preconds = preconds}
11.180 - | sym_rls (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
11.181 + | make_sym_rule_set (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
11.182 Rule_Set.Seqence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
11.183 rules = rules, rew_ord = rew_ord, preconds = preconds}
11.184 - | sym_rls (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
11.185 + | make_sym_rule_set (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
11.186 Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
11.187 prepat = prepat, rew_ord = rew_ord}
11.188
11.189 -(* toggles sym_* and keeps "#:" for ad-hoc calculations *)
11.190 -fun sym_rule (Rule.Thm (thmID, thm)) =
11.191 - let
11.192 - val thm' = sym_thm thm
11.193 - val thmID' = case Symbol.explode thmID of
11.194 - "s" :: "y" :: "m" :: "_" :: id => implode id
11.195 - | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
11.196 - | _ => "sym_" ^ thmID
11.197 - in Rule.Thm (thmID', thm') end
11.198 -| sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
11.199 -| sym_rule r = error ("sym_rule: not for " ^ Rule.to_string r)
11.200 +(* toggles sym_* and keeps "#:" for ad-hoc theorems *)
11.201 +fun make_sym_rule (Rule.Thm (thmID, thm)) =
11.202 + let
11.203 + val thm' = sym_thm thm
11.204 + val thmID' = case Symbol.explode thmID of
11.205 + "s" :: "y" :: "m" :: "_" :: id => implode id
11.206 + | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
11.207 + | _ => "sym_" ^ thmID
11.208 + in Rule.Thm (thmID', thm') end
11.209 + | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
11.210 + | make_sym_rule r = error ("make_sym_rule: not for " ^ Rule.to_string r)
11.211
11.212 -fun revert_sym thy (Rule.Thm (thmID, thm)) =
11.213 - if (is_sym o thmID_of_derivation_name) thmID
11.214 +fun revert_sym_rule thy (Rule.Thm (id, thm)) =
11.215 + if is_sym (cut_id id)
11.216 then
11.217 let
11.218 - val thmID' = sym_drop thmID
11.219 - val thm' = assoc_thm'' thy thmID'
11.220 - val thmDeriv' = Thm.get_name_hint thm'
11.221 - in Rule.Thm (thmDeriv', thm') end
11.222 + val id' = id_drop_sym id
11.223 + val thm' = thm_from_thy thy id'
11.224 + val id'' = Thm.get_name_hint thm'
11.225 + in Rule.Thm (id'', thm') end
11.226 else Rule.Thm (Thm.get_name_hint thm, thm)
11.227 - | revert_sym _ rule = raise ERROR ("revert_sym: NOT for " ^ Rule.to_string rule)
11.228 + | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
11.229
11.230 (**)end(**)
12.1 --- a/src/Tools/isac/TODO.thy Tue Apr 14 15:56:15 2020 +0200
12.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 15 10:07:43 2020 +0200
12.3 @@ -23,6 +23,8 @@
12.4 \<close>
12.5 subsection \<open>Current changeset\<close>
12.6 text \<open>
12.7 +(*/------- to -------\*)
12.8 +(*\------- to -------/*)
12.9 \begin{itemize}
12.10 \item type_empty -> typ_empty
12.11 \item Seqence -> Sequence
12.12 @@ -30,7 +32,8 @@
12.13 \item Num_Calc -> Exec, eval_* -> exec_*
12.14 \item xxx
12.15 \item xxx
12.16 - \item xxx
12.17 + \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
12.18 + probably first review calcelems.sml
12.19 \item xxx
12.20 \item xxx
12.21 \item xxx
12.22 @@ -50,7 +53,7 @@
12.23 thmDeriv : type for thy_hierarchy ONLY
12.24 obsolete types : thm' (SEE "ad thm'"), thm''.
12.25 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
12.26 - activate : thmID_of_derivation_name'
12.27 + activate : ThmC.cut_id'
12.28 *)
12.29 \item xxx
12.30 \item use "Exec_Def" for renaming identifiers
13.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 14 15:56:15 2020 +0200
13.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 10:07:43 2020 +0200
13.3 @@ -8,9 +8,9 @@
13.4 "table of contents --------------------------------------";
13.5 "--------------------------------------------------------";
13.6 "-------- Unsynchronized.ref doesn't work any more ------";
13.7 -"-------- fun thmID_of_derivation_name ------------------";
13.8 +"-------- fun ThmC.cut_id ------------------";
13.9 "-------- fun UnparseC.term ----------------------------------";
13.10 -"-------- fun thmID_of_derivation_name 000---------------";
13.11 +"-------- fun ThmC.cut_id 000---------------";
13.12 "-------- fun Rule_Set.merge -----------------------------------------------------";
13.13 "-------- fun update_ptyps --------------------------------------------------";
13.14 "-------- fun subst2str' -----------------------------------------------------------------------";
13.15 @@ -35,15 +35,15 @@
13.16 --- fun insert_errpats ---, see changeset 90f3855dee3b *)
13.17
13.18
13.19 -"-------- fun thmID_of_derivation_name ----------------";
13.20 -"-------- fun thmID_of_derivation_name ----------------";
13.21 -"-------- fun thmID_of_derivation_name ----------------";
13.22 +"-------- fun ThmC.cut_id ----------------";
13.23 +"-------- fun ThmC.cut_id ----------------";
13.24 +"-------- fun ThmC.cut_id ----------------";
13.25 val thm = @{thm radd_0};
13.26 val dn = Thm.derivation_name thm;
13.27 if dn = "Test.radd_0" then ()
13.28 else error "calcelems.sml Thm.derivation_name changed 1";
13.29
13.30 -val thmID = ThmC.thmID_of_derivation_name dn;
13.31 +val thmID = ThmC.cut_id dn;
13.32 val thyID = ThyC.thyID_of_derivation_name dn;
13.33 if thmID = "radd_0" andalso thyID = "Test" then ()
13.34 else error "calcelems.sml Thm.derivation_name changed 2";
13.35 @@ -51,7 +51,7 @@
13.36 "--- thm2 --";
13.37 val thm = @{thm add_divide_distrib}
13.38 val dn = Thm.derivation_name thm;
13.39 -val thmID = thmID_of_derivation_name dn;
13.40 +val thmID = ThmC.cut_id dn;
13.41 val thyID = ThyC.thyID_of_derivation_name dn;
13.42 if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()
13.43 else error "calcelems.sml Thm.derivation_name changed 3";
13.44 @@ -87,15 +87,15 @@
13.45 handle _ => NONE;
13.46 *)
13.47
13.48 -"-------- fun thmID_of_derivation_name 000---------------";
13.49 -"-------- fun thmID_of_derivation_name 000---------------";
13.50 -"-------- fun thmID_of_derivation_name 000---------------";
13.51 +"-------- fun ThmC.cut_id 000---------------";
13.52 +"-------- fun ThmC.cut_id 000---------------";
13.53 +"-------- fun ThmC.cut_id 000---------------";
13.54 val long_id = Thm.get_name_hint @{thm mult_1_left};
13.55 if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
13.56 else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
13.57
13.58 -if ThmC.thmID_of_derivation_name long_id = "mult_1_left" then ()
13.59 -else error "fun thmID_of_derivation_name broken";
13.60 +if ThmC.cut_id long_id = "mult_1_left" then ()
13.61 +else error "fun ThmC.cut_id broken";
13.62
13.63 if ThyC.thyID_of_derivation_name long_id = "Groups" then ()
13.64 else error "fun ThyC.thyID_of_derivation_name broken";
14.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 14 15:56:15 2020 +0200
14.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 10:07:43 2020 +0200
14.3 @@ -20,7 +20,7 @@
14.4 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
14.5 "----------- fun Thm.make_thm ------------------------------------";
14.6 "----------- correct theIDs for Rule_Set.empty -------------------";
14.7 -"----------- fun revert_sym --------------------------------------";
14.8 +"----------- fun revert_sym_rule --------------------------------------";
14.9 "----------- fun thms_of_rlss ------------------------------------";
14.10 "----------- repair thydata2xml for rls --------------------------";
14.11 "-----------------------------------------------------------------";
14.12 @@ -41,13 +41,13 @@
14.13 (*val it =
14.14 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
14.15 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
14.16 -map ThmC.thmID_of_derivation_name' (thms_of thy) =
14.17 +map ThmC.id_of_thm (thms_of thy) =
14.18 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit",
14.19 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
14.20 *)
14.21 val thy = @{theory Biegelinie};
14.22 val thms = thms_of thy;
14.23 -if map ThmC.thmID_of_derivation_name' thms =
14.24 +if map ThmC.id_of_thm thms =
14.25 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
14.26 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
14.27 else error "fun thms_of ...changed";
14.28 @@ -168,21 +168,21 @@
14.29 ["IsacScripts", "KEStore", "Rulesets", "empty"],
14.30 :*)
14.31
14.32 -"----------- fun revert_sym --------------------------------------";
14.33 -"----------- fun revert_sym --------------------------------------";
14.34 -"----------- fun revert_sym --------------------------------------";
14.35 +"----------- fun revert_sym_rule --------------------------------------";
14.36 +"----------- fun revert_sym_rule --------------------------------------";
14.37 +"----------- fun revert_sym_rule --------------------------------------";
14.38 val thy = @{theory Isac_Knowledge}
14.39 -val (Thm (thmID, thm)) = ThmC.revert_sym thy
14.40 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
14.41 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
14.42 ;
14.43 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
14.44 -then () else error "fun revert_sym changed 1";
14.45 +then () else error "fun revert_sym_rule changed 1";
14.46
14.47 -val (Thm (thmID, thm)) = ThmC.revert_sym thy
14.48 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
14.49 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
14.50 ;
14.51 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
14.52 -then () else error "fun revert_sym changed 2"
14.53 +then () else error "fun revert_sym_rule changed 2"
14.54
14.55 "----------- fun thms_of_rlss ------------------------------------";
14.56 "----------- fun thms_of_rlss ------------------------------------";
14.57 @@ -205,7 +205,7 @@
14.58 |> flat
14.59 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.60 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
14.61 - |> map (ThmC.revert_sym thy)
14.62 + |> map (ThmC.revert_sym_rule thy)
14.63 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
14.64 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
14.65 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
15.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Tue Apr 14 15:56:15 2020 +0200
15.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 10:07:43 2020 +0200
15.3 @@ -1099,7 +1099,7 @@
15.4 (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
15.5 val thmDeriv = Thm.get_name_hint thm
15.6 val (part, thyID) = thy_containing_thm thmDeriv
15.7 - val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
15.8 + val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
15.9 val Hthm {fillpats, ...} = get_the theID
15.10 val some = map (get_fillform subst (thm, form) errpatID) fillpats;
15.11
16.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Apr 14 15:56:15 2020 +0200
16.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Apr 15 10:07:43 2020 +0200
16.3 @@ -139,7 +139,7 @@
16.4 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
16.5 val thm_deriv = Thm.get_name_hint thm;
16.6
16.7 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv)
16.8 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
16.9 = "thy_isac_Test-thm-radd_left_commute" then ()
16.10 else error "context_thy mini-subpbl ([2,4], Res) changed";
16.11 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
16.12 @@ -161,7 +161,7 @@
16.13 applicable_in pos pt tac
16.14 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
16.15 val thm_deriv = Thm.get_name_hint thm;
16.16 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv) =
16.17 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
16.18 "thy_isac_Test-thm-risolate_bdv_add" then ()
16.19 else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
16.20 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
17.1 --- a/test/Tools/isac/Knowledge/algein.sml Tue Apr 14 15:56:15 2020 +0200
17.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Apr 15 10:07:43 2020 +0200
17.3 @@ -103,7 +103,7 @@
17.4 val thy = @{theory "Isac_Knowledge"};
17.5 val rew_ord = dummy_ord;
17.6 val erls = Rule_Set.Empty;
17.7 -val thm = assoc_thm'' thy "sym_mult_zero_right";
17.8 +val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
17.9 val t = str2term "0 = (0::real)";
17.10 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
17.11 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
17.12 @@ -118,7 +118,7 @@
17.13 val t'' = subst_atomic subst t';
17.14 UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
17.15
17.16 -val thm = assoc_thm'' thy "sym";
17.17 +val thm = ThmC.thm_from_thy thy "sym";
17.18 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
17.19 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
17.20 *)
18.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Apr 14 15:56:15 2020 +0200
18.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Apr 15 10:07:43 2020 +0200
18.3 @@ -806,7 +806,7 @@
18.4
18.5 if length (hd revsets) = 11 then () else error "length of revset changed";
18.6 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
18.7 - (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.thmID_of_derivation_name)
18.8 + (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
18.9 then () else error "first element of revset changed";
18.10 if
18.11 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
19.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Apr 14 15:56:15 2020 +0200
19.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Apr 15 10:07:43 2020 +0200
19.3 @@ -370,7 +370,7 @@
19.4 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
19.5 val SOME t = parseNEW @{context} "9 is_const";
19.6 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.7 -if str = "#is_const_9_" andalso thm2str thm = "(9 is_const) = True"
19.8 +if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
19.9 then () else error "adhoc_thm 9 is_const changed";
19.10
19.11
19.12 @@ -381,7 +381,7 @@
19.13
19.14 val SOME t = parseNEW @{context} "4 < 4";
19.15 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.16 -if str = "#less_4_4" andalso thm2str thm = "(4 < 4) = False"
19.17 +if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
19.18 then () else error "adhoc_thm 4 < 4 changed";
19.19
19.20 val SOME t = parseNEW @{context} "a < 4";
19.21 @@ -393,14 +393,14 @@
19.22 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
19.23 val SOME t = parseNEW @{context} "1 + 2";
19.24 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.25 -if str = "#: 1 + 2 = 3" andalso thm2str thm = "1 + 2 = 3"
19.26 +if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
19.27 then () else error "adhoc_thm 1 + 2 changed";
19.28
19.29 (*--------------------------------------------------------------------vvvvvvvvvv*)
19.30 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
19.31 val SOME t = parseNEW @{context} "6 / -8";
19.32 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.33 -if str = "#divide_e6_-8" andalso thm2str thm = "6 / -8 = -3 / 4"
19.34 +if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4"
19.35 then () else error "adhoc_thm 1 + 2 changed";
19.36
19.37
19.38 @@ -411,12 +411,12 @@
19.39
19.40 val SOME t = parseNEW @{context} "3 =!= 3";
19.41 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.42 -if str = "#ident_(3)_(3)" andalso thm2str thm = "(3 =!= 3) = True"
19.43 +if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
19.44 then () else error "adhoc_thm (3 =!= 3) changed";
19.45
19.46 val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
19.47 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
19.48 -if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso thm2str thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
19.49 +if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
19.50 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
19.51
19.52 "----------- fun power -------------------------------------------------------------------------";