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}, \<^rule_thm_sym>\<open>real_mult_minus1\<close>);
51 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = - 1 * ?z1" then ()
52 else error "input to revert_sym_rule CHANGED";
54 (*if*) is_sym (cut_id id) (*then*);
55 val id' = id_drop_sym id
56 val thm' = thm_from_thy thy id'
57 val id'' = Thm.get_name_hint thm'
59 val thy = @{theory Isac_Knowledge}
60 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy (\<^rule_thm_sym>\<open>real_mult_minus1\<close>)
62 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z"
63 then () else error "fun revert_sym_rule changed 1";
65 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
66 (Thm ("real_diff_minus", @{thm real_diff_minus}))
68 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
69 then () else error "fun revert_sym_rule changed 2"