1 (* Title: "BaseDefinitions/thmC.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- fun sym_thm -----------------------------------------------------------------------";
10 "----------- fun revert_sym_rule ---------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
16 "----------- fun sym_thm -----------------------------------------------------------------------";
17 "----------- fun sym_thm -----------------------------------------------------------------------";
18 "----------- fun sym_thm -----------------------------------------------------------------------";
19 "~~~~~ fun sym_thm , args:"; val (thm) = (@{thm real_mult_minus1});
20 val thy = Thm.theory_of_thm thm;
21 val certT = Thm.global_ctyp_of thy: typ -> ctyp;
22 val cert = Thm.global_cterm_of thy: term -> cterm;
24 val (lhs, rhs) = dest_eq_concl thm |> apply2 cert; (*"- 1 * ?z", "- ?z"*)
25 val A = Thm.typ_of_cterm lhs; (* "real"*)
27 val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
28 if ThmC.string_of_thm sym_rule = "?s1 = ?t1 \<Longrightarrow> ?t1 = ?s1" then () else error "sym_thm 1";
29 val (t, s) = dest_eq_concl sym_rule; (*Var (("t", 1), "?'a1"), Var (("s", 1), "?'a1")*)
31 val instT = map (rpair A) (Term.add_tvars t []);
32 (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * typ) list*)
33 val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, []));
34 (* = ( (("t", 1), "real"), (("s", 1), "real") )*)
36 val cinstT = map (apsnd certT) instT;
37 (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * ctyp) list*)
38 val cinst = [(s', lhs), (t', rhs)];
39 (* = [((("s", 1), "real"), "- 1 * ?z"), ((("t", 1), "real"), "- ?z")] *)
41 val res = Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule) thm;
42 if ThmC.string_of_thm res = "- ?z = - 1 * ?z" then () else error "sym_thm - 1 * ?z = - ?z CHANGED"
45 "----------- fun revert_sym_rule ---------------------------------------------------------------";
46 "----------- fun revert_sym_rule ---------------------------------------------------------------";
47 "----------- fun revert_sym_rule ---------------------------------------------------------------";
48 "~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
49 (@{theory Isac_Knowledge},
50 Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
52 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
53 else error "input to revert_sym_rule CHANGED";
55 (*if*) is_sym (cut_id id) (*then*);
56 val id' = id_drop_sym id
57 val thm' = thm_from_thy thy id'
58 val id'' = Thm.get_name_hint thm'
61 val thy = @{theory Isac_Knowledge}
62 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
63 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
65 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
66 then () else error "fun revert_sym_rule changed 1";
68 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
69 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
71 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
72 then () else error "fun revert_sym_rule changed 2"