19 val setup: theory -> theory |
29 val setup: theory -> theory |
20 val get_eqvt_thms: Proof.context -> thm list |
30 val get_eqvt_thms: Proof.context -> thm list |
21 |
31 |
22 end; |
32 end; |
23 |
33 |
24 structure NominalThmDecls: NOMINAL_THMDECLS = |
34 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
25 struct |
35 struct |
26 |
36 |
27 structure Data = Generic_Data |
37 structure EqvtData = Generic_Data |
28 ( |
38 ( |
29 type T = thm list |
39 type T = thm Item_Net.T; |
30 val empty = [] |
40 val empty = Thm.full_rules; |
31 val extend = I |
41 val extend = I; |
32 val merge = Thm.merge_thms |
42 val merge = Item_Net.merge; |
33 ) |
43 ); |
34 |
44 |
35 (* Exception for when a theorem does not conform with form of an equivariance lemma. *) |
45 val content = Item_Net.content o EqvtData.get; |
36 (* There are two forms: one is an implication (for relations) and the other is an *) |
46 val get_eqvt_thms = content o Context.Proof; |
37 (* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *) |
|
38 (* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) |
|
39 (* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) |
|
40 (* be equal to t except that every free variable, say x, is replaced by pi o x. In *) |
|
41 (* the implicational case it is also checked that the variables and permutation fit *) |
|
42 (* together, i.e. are of the right "pt_class", so that a stronger version of the *) |
|
43 (* equality-lemma can be derived. *) |
|
44 exception EQVT_FORM of string |
|
45 |
47 |
46 val perm_boolE = |
48 val add_thm = EqvtData.map o Item_Net.update; |
47 @{lemma "pi \<bullet> P ==> P" by (simp add: permute_bool_def)}; |
49 val del_thm = EqvtData.map o Item_Net.remove; |
48 |
50 |
49 val perm_boolI = |
51 val add_force_thm = EqvtData.map o Item_Net.update; |
50 @{lemma "P ==> pi \<bullet> P" by (simp add: permute_bool_def)}; |
52 val del_force_thm = EqvtData.map o Item_Net.remove; |
51 |
53 |
52 fun prove_eqvt_tac ctxt orig_thm pi pi' = |
54 |
|
55 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
|
56 | dest_perm t = raise TERM("dest_perm", [t]) |
|
57 |
|
58 fun mk_perm p trm = |
53 let |
59 let |
54 val mypi = Thm.cterm_of ctxt pi |
60 val ty = fastype_of trm |
55 val T = fastype_of pi' |
|
56 val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi') |
|
57 val perm_pi_simp = @{thms permute_minus_cancel} |
|
58 in |
61 in |
59 EVERY1 [rtac @{thm iffI}, |
62 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
60 dtac perm_boolE, |
|
61 etac orig_thm, |
|
62 dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm), |
|
63 rtac perm_boolI, |
|
64 full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)] |
|
65 end; |
|
66 |
|
67 fun get_derived_thm ctxt hyp concl orig_thm pi = |
|
68 let |
|
69 val thy = ProofContext.theory_of ctxt; |
|
70 val pi' = Var (pi, @{typ "perm"}); |
|
71 val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; |
|
72 val ([goal_term, pi''], ctxt') = Variable.import_terms false |
|
73 [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt |
|
74 in |
|
75 Goal.prove ctxt' [] [] goal_term |
|
76 (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |> |
|
77 singleton (ProofContext.export ctxt' ctxt) |
|
78 end |
|
79 |
|
80 (* replaces in t every variable, say x, with pi o x *) |
|
81 fun apply_pi trm pi = |
|
82 let |
|
83 fun replace n ty = |
|
84 let |
|
85 val c = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) |
|
86 val v1 = Var (pi, @{typ "perm"}) |
|
87 val v2 = Var (n, ty) |
|
88 in |
|
89 c $ v1 $ v2 |
|
90 end |
|
91 in |
|
92 map_aterms (fn Var (n, ty) => replace n ty | t => t) trm |
|
93 end |
63 end |
94 |
64 |
95 (* returns *the* pi which is in front of all variables, provided there *) |
65 fun eqvt_transform_tac thm = REPEAT o FIRST' |
96 (* exists such a pi; otherwise raises EQVT_FORM *) |
66 [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), |
97 fun get_pi t thy = |
67 rtac (thm RS @{thm trans}), |
98 let fun get_pi_aux s = |
68 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
99 (case s of |
|
100 (Const (@{const_name "permute"} ,typrm) $ |
|
101 (Var (pi,_)) $ |
|
102 (Var (n,ty))) => |
|
103 if (Sign.of_sort thy (ty, @{sort pt})) |
|
104 then [pi] |
|
105 else raise |
|
106 EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt") |
|
107 | Abs (_,_,t1) => get_pi_aux t1 |
|
108 | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 |
|
109 | _ => []) |
|
110 in |
|
111 (* collect first all pi's in front of variables in t and then use distinct *) |
|
112 (* to ensure that all pi's must have been the same, i.e. distinct returns *) |
|
113 (* a singleton-list *) |
|
114 (case (distinct (op =) (get_pi_aux t)) of |
|
115 [pi] => pi |
|
116 | [] => raise EQVT_FORM "No permutations found" |
|
117 | _ => raise EQVT_FORM "All permutation should be the same") |
|
118 end; |
|
119 |
69 |
120 (* Either adds a theorem (orig_thm) to or deletes one from the equivariance *) |
70 (* transform equations into the required form *) |
121 (* lemma list depending on flag. To be added the lemma has to satisfy a *) |
71 fun transform_eq ctxt thm lhs rhs = |
122 (* certain form. *) |
72 let |
|
73 val (p, t) = dest_perm lhs |
|
74 val (c, args) = strip_comb t |
|
75 val (c', args') = strip_comb rhs |
|
76 val eargs = map Envir.eta_contract args |
|
77 val eargs' = map Envir.eta_contract args' |
|
78 val p_str = fst (fst (dest_Var p)) |
|
79 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
|
80 in |
|
81 if c <> c' |
|
82 then error "eqvt lemma is not of the right form (constants do not agree)" |
|
83 else if eargs' <> map (mk_perm p) eargs |
|
84 then error "eqvt lemma is not of the right form (arguments do not agree)" |
|
85 else if args = [] |
|
86 then thm |
|
87 else Goal.prove ctxt [p_str] [] goal |
|
88 (fn _ => eqvt_transform_tac thm 1) |
|
89 end |
123 |
90 |
124 fun eqvt_add_del_aux flag orig_thm context = |
91 fun transform addel_fn thm context = |
125 let |
92 let |
126 val thy = Context.theory_of context |
93 val ctxt = Context.proof_of context |
127 val thms_to_be_added = (case (prop_of orig_thm) of |
94 val trm = HOLogic.dest_Trueprop (prop_of thm) |
128 (* case: eqvt-lemma is of the implicational form *) |
95 in |
129 (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => |
96 case trm of |
130 let |
97 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
131 val pi = get_pi concl thy |
98 addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context |
132 in |
99 | _ => raise (error "no other cases yet implemented") |
133 if (apply_pi hyp pi = concl) |
100 end |
134 then |
|
135 (warning ("equivariance lemma of the relational form"); |
|
136 [orig_thm, |
|
137 get_derived_thm (Context.proof_of context) hyp concl orig_thm pi]) |
|
138 else raise EQVT_FORM "Type Implication" |
|
139 end |
|
140 (* case: eqvt-lemma is of the equational form *) |
|
141 | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ |
|
142 (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) => |
|
143 (if (apply_pi lhs pi) = rhs |
|
144 then [orig_thm] |
|
145 else raise EQVT_FORM "Type Equality") |
|
146 | _ => raise EQVT_FORM "Type unknown") |
|
147 in |
|
148 fold (fn thm => Data.map (flag thm)) thms_to_be_added context |
|
149 end |
|
150 handle EQVT_FORM s => |
|
151 error (Display.string_of_thm (Context.proof_of context) orig_thm ^ |
|
152 " does not comply with the form of an equivariance lemma (" ^ s ^").") |
|
153 |
101 |
154 |
102 |
155 val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm)); |
103 val eqvt_add = Thm.declaration_attribute (transform add_thm); |
156 val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm)); |
104 val eqvt_del = Thm.declaration_attribute (transform del_thm); |
157 |
105 |
158 val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm); |
106 val eqvt_force_add = Thm.declaration_attribute add_force_thm; |
159 val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm); |
107 val eqvt_force_del = Thm.declaration_attribute del_force_thm; |
160 |
|
161 val get_eqvt_thms = Context.Proof #> Data.get; |
|
162 |
108 |
163 val setup = |
109 val setup = |
164 Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) |
110 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
165 "equivariance theorem declaration" |
111 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
166 #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del) |
112 "brought into the form p o c = c"]) #> |
167 "equivariance theorem declaration (without checking the form of the lemma)" |
113 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
168 #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) |
114 (cat_lines ["declaration of equivariance lemmas - they will will be", |
|
115 "added/deleted directly to the eqvt thm-list"]) #> |
|
116 PureThy.add_thms_dynamic (@{binding "eqvt"}, content); |
169 |
117 |
170 |
118 |
171 end; |
119 end; |