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