1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Apr 18 15:19:49 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Apr 18 18:56:43 2021 +0200
1.3 @@ -88,7 +88,7 @@
1.4 val uminus_to_string: term -> term
1.5
1.6 val var2free: term -> term
1.7 - val vars: term -> term list (* recognises numverals, should replace "fun vars_of" *)
1.8 + val vars: term -> term list (* recognises numerals, should replace "fun vars_of" *)
1.9 val vars': term list -> term list
1.10 val vars_of: term -> term list (* deprecated *)
1.11 val dest_list': term -> term list
2.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Sun Apr 18 15:19:49 2021 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Sun Apr 18 18:56:43 2021 +0200
2.3 @@ -25,12 +25,11 @@
2.4 val is_sym: id -> bool
2.5 val thm_from_thy: theory -> ThmC_Def.id -> thm
2.6
2.7 -
2.8 -
2.9 val revert_sym_rule: theory -> Rule.rule -> Rule.rule
2.10
2.11
2.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.13 + val dest_eq_concl: thm -> term * term
2.14 val string_of_thm_in_thy: theory -> thm -> string
2.15 val id_drop_sym: id -> id
2.16 val make_sym_rule: Rule.rule -> Rule.rule
2.17 @@ -81,7 +80,7 @@
2.18 | _ => id
2.19
2.20 (* get the theorem associated with the xstring-identifier;
2.21 - if the identifier starts with "sym_" then swap lhs = rhs" around "=";
2.22 + if the identifier starts with "sym_" then swap "lhs = rhs" around "=";
2.23 in case identifiers starting with "#" come from Eval and
2.24 get an ad-hoc theorem (containing numerals only) -- rejected here
2.25 *)
2.26 @@ -90,11 +89,11 @@
2.27 "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
2.28 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
2.29 | "s" :: "y" :: "m" :: "_" :: id =>
2.30 - ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
2.31 + ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
2.32 | "#" :: _ =>
2.33 - raise ERROR ("thm_from_thy not impl.for " ^ thmid)
2.34 + raise ERROR ("thm_from_thy not impl.for " ^ thmid)
2.35 | _ =>
2.36 - thmid |> Global_Theory.get_thm thy |> numerals_to_Free
2.37 + thmid |> Global_Theory.get_thm thy |> numerals_to_Free
2.38
2.39 fun dest_eq_concl thm =
2.40 (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
3.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 18 15:19:49 2021 +0200
3.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 18 18:56:43 2021 +0200
3.3 @@ -171,16 +171,16 @@
3.4 "----------- fun thms_of_rlss ------------------------------------";
3.5 "----------- fun thms_of_rlss ------------------------------------";
3.6 "----------- fun thms_of_rlss ------------------------------------";
3.7 +(*GOON* )
3.8 val rlss =
3.9 [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
3.10 - ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]
3.11 -;
3.12 + ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))];
3.13 +
3.14 val [_, (thmID, term)] = thms_of_rlss thy rlss;
3.15 -(*
3.16 -if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
3.17 -then () else error "thms_of_rlss changed"
3.18 -*)
3.19 -;
3.20 +
3.21 +if thmID = "real_mult_minus1" (* WAS "??.unknown" from Pure/more_thm>ML *)
3.22 +then () else error "thms_of_rlss changed";
3.23 +
3.24 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
3.25 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
3.26 |> map (Thy_Present.thms_of_rls o #2 o #2)
3.27 @@ -196,6 +196,7 @@
3.28 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
3.29 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
3.30 |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
3.31 +( *GOON*)
3.32
3.33 "----------- repair thydata2xml for rls --------------------------";
3.34 "----------- repair thydata2xml for rls --------------------------";
4.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Sun Apr 18 15:19:49 2021 +0200
4.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Sun Apr 18 18:56:43 2021 +0200
4.3 @@ -6,12 +6,42 @@
4.4 "-----------------------------------------------------------------------------------------------";
4.5 "table of contents -----------------------------------------------------------------------------";
4.6 "-----------------------------------------------------------------------------------------------";
4.7 +"----------- fun sym_thm -----------------------------------------------------------------------";
4.8 "----------- fun revert_sym_rule ---------------------------------------------------------------";
4.9 "-----------------------------------------------------------------------------------------------";
4.10 "-----------------------------------------------------------------------------------------------";
4.11 "-----------------------------------------------------------------------------------------------";
4.12
4.13
4.14 +"----------- fun sym_thm -----------------------------------------------------------------------";
4.15 +"----------- fun sym_thm -----------------------------------------------------------------------";
4.16 +"----------- fun sym_thm -----------------------------------------------------------------------";
4.17 +"~~~~~ fun sym_thm , args:"; val (thm) = (@{thm real_mult_minus1});
4.18 + val thy = Thm.theory_of_thm thm;
4.19 + val certT = Thm.global_ctyp_of thy: typ -> ctyp;
4.20 + val cert = Thm.global_cterm_of thy: term -> cterm;
4.21 +
4.22 + val (lhs, rhs) = dest_eq_concl thm |> apply2 cert; (*"- 1 * ?z", "- ?z"*)
4.23 + val A = Thm.typ_of_cterm lhs; (* "real"*)
4.24 +
4.25 + val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
4.26 +if ThmC.string_of_thm sym_rule = "?s1 = ?t1 \<Longrightarrow> ?t1 = ?s1" then () else error "sym_thm 1";
4.27 + val (t, s) = dest_eq_concl sym_rule; (*Var (("t", 1), "?'a1"), Var (("s", 1), "?'a1")*)
4.28 +
4.29 + val instT = map (rpair A) (Term.add_tvars t []);
4.30 + (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * typ) list*)
4.31 + val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, []));
4.32 + (* = ( (("t", 1), "real"), (("s", 1), "real") )*)
4.33 +
4.34 + val cinstT = map (apsnd certT) instT;
4.35 + (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * ctyp) list*)
4.36 + val cinst = [(s', lhs), (t', rhs)];
4.37 + (* = [((("s", 1), "real"), "- 1 * ?z"), ((("t", 1), "real"), "- ?z")] *)
4.38 +
4.39 +val res = Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule) thm;
4.40 +if ThmC.string_of_thm res = "- ?z = - 1 * ?z" then () else error "sym_thm - 1 * ?z = - ?z CHANGED"
4.41 +
4.42 +
4.43 "----------- fun revert_sym_rule ---------------------------------------------------------------";
4.44 "----------- fun revert_sym_rule ---------------------------------------------------------------";
4.45 "----------- fun revert_sym_rule ---------------------------------------------------------------";
4.46 @@ -26,7 +56,7 @@
4.47 val id' = id_drop_sym id
4.48 val thm' = thm_from_thy thy id'
4.49 val id'' = Thm.get_name_hint thm'
4.50 -(*GOON*)
4.51 +(*GOON* )
4.52
4.53 val thy = @{theory Isac_Knowledge}
4.54 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
4.55 @@ -40,3 +70,5 @@
4.56 ;
4.57 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
4.58 then () else error "fun revert_sym_rule changed 2"
4.59 +
4.60 +( *GOON*)
5.1 --- a/test/Tools/isac/Test_Some.thy Sun Apr 18 15:19:49 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Sun Apr 18 18:56:43 2021 +0200
5.3 @@ -58,7 +58,7 @@
5.4 ML \<open>
5.5 "~~~~~ fun xxx , args:"; val () = ();
5.6 "~~~~~ and xxx , args:"; val () = ();
5.7 -"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
5.8 +"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
5.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
5.10 "xx"
5.11 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
5.12 @@ -95,17 +95,119 @@
5.13 declare [[ML_exception_trace]]
5.14 \<close>
5.15
5.16 -section \<open>===================================================================================\<close>
5.17 +section \<open>====== ML_file "MathEngBasic/thmC.sml" ============================================\<close>
5.18 ML \<open>
5.19 \<close> ML \<open>
5.20 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
5.21 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
5.22 +"----------- fun revert_sym_rule ---------------------------------------------------------------";
5.23 +"~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
5.24 + (@{theory Isac_Knowledge},
5.25 + Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
5.26 +
5.27 +if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
5.28 +else error "input to revert_sym_rule CHANGED";
5.29 +
5.30 +\<close> ML \<open>
5.31 + (*if*) is_sym (cut_id id) (*then*);
5.32 +\<close> ML \<open>
5.33 + val id' = id_drop_sym id
5.34 +\<close> ML \<open>
5.35 + val thm' = thm_from_thy thy id'
5.36 +\<close> ML \<open>
5.37 + val id'' = Thm.get_name_hint thm'
5.38 +(*GOON*)
5.39 +
5.40 +\<close> ML \<open> (*ERROR "??.unknown"*)
5.41 +val thy = @{theory Isac_Knowledge}
5.42 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
5.43 + (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
5.44 +;
5.45 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
5.46 +then () else error "fun revert_sym_rule changed 1";
5.47 +
5.48 +val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
5.49 + (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
5.50 +;
5.51 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
5.52 +then () else error "fun revert_sym_rule changed 2"
5.53 +\<close> ML \<open>
5.54 +\<close> ML \<open>
5.55 +\<close> ML \<open>
5.56 +\<close> ML \<open>
5.57 +\<close> ML \<open>
5.58 +\<close> ML \<open>
5.59 +\<close> ML \<open>
5.60 \<close> ML \<open>
5.61 \<close> ML \<open>
5.62 \<close>
5.63
5.64 -section \<open>===================================================================================\<close>
5.65 +section \<open>=========== ML_file "BridgeLibisabelle/thy-hierarchy.sml" ======================\<close>
5.66 ML \<open>
5.67 \<close> ML \<open>
5.68 \<close> ML \<open>
5.69 +"----------- fun ThmC_Def.make_thm ------------------------------------";
5.70 +"----------- fun ThmC_Def.make_thm ------------------------------------";
5.71 +"----------- fun ThmC_Def.make_thm ------------------------------------";
5.72 +"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Write.authors)) =
5.73 + (@{theory "Biegelinie"}, "IsacKnowledge",
5.74 + ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
5.75 + ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
5.76 + val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
5.77 + val theID = Thy_Present.guh2theID guh;
5.78 +if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
5.79 + theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
5.80 +then () else error "store_thm: guh | theID changed";
5.81 +
5.82 +\<close> ML \<open> (*ERROR "??.unknown"*)
5.83 +"----------- fun thms_of_rlss ------------------------------------";
5.84 +"----------- fun thms_of_rlss ------------------------------------";
5.85 +"----------- fun thms_of_rlss ------------------------------------";
5.86 +\<close> ML \<open>
5.87 +val rlss =
5.88 + [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
5.89 + ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]:
5.90 + (id * (id * Rule_Def.rule_set)) list
5.91 +;
5.92 +\<close> ML \<open>
5.93 +(*--- fun ThmC_Def.make_thm --- avoids ERROR BELOW Undefined fact: "real_mult_minus1"*)
5.94 +(*+*)thms_of_rlss thy rlss (* = [("??.unknown", "?a - ?b = ?a + -1 * ?b")]: (string * thm) list*)
5.95 +\<close> ML \<open>
5.96 +(*+*)Rule_Set.empty: Rule_Def.rule_set
5.97 +\<close> ML \<open>
5.98 +(*+*)discard_minus: Rule_Def.rule_set
5.99 +\<close> ML \<open>
5.100 +val [_, (thmID, term)] = thms_of_rlss thy rlss;
5.101 +
5.102 +\<close> ML \<open>
5.103 +if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
5.104 +then () else error "thms_of_rlss changed";
5.105 +
5.106 +\<close> ML \<open>
5.107 +"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
5.108 +val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
5.109 + |> map (Thy_Present.thms_of_rls o #2 o #2)
5.110 + (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
5.111 + Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
5.112 + |> flat
5.113 + (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
5.114 + Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
5.115 + |> map (ThmC.revert_sym_rule thy)
5.116 + (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
5.117 + Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
5.118 + |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
5.119 + (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
5.120 + ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
5.121 + |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
5.122 +\<close> ML \<open>
5.123 +\<close> ML \<open>
5.124 +\<close> ML \<open>
5.125 +\<close> ML \<open>
5.126 +\<close> ML \<open>
5.127 +\<close> ML \<open>
5.128 +\<close> ML \<open>
5.129 +\<close> ML \<open>
5.130 +\<close> ML \<open>
5.131 \<close> ML \<open>
5.132 \<close>
5.133