6 Provides the attributes [eqvt] and [eqvt_raw], and the theorem |
6 Provides the attributes [eqvt] and [eqvt_raw], and the theorem |
7 lists eqvts and eqvts_raw. The first attribute will store the |
7 lists eqvts and eqvts_raw. The first attribute will store the |
8 theorem in the eqvts list and also in the eqvts_raw list. For |
8 theorem in the eqvts list and also in the eqvts_raw list. For |
9 the latter the theorem is expected to be of the form |
9 the latter the theorem is expected to be of the form |
10 |
10 |
11 p o (c x1 x2 ...) = c (p o x1) (p o x2) ... |
11 p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1) |
|
12 |
|
13 or |
|
14 |
|
15 c x1 x2 ... ==> c (p o x1) (p o x2) ... (2) |
12 |
16 |
13 and it is stored in the form |
17 and it is stored in the form |
14 |
18 |
15 p o c == c |
19 p o c == c |
16 |
20 |
17 The [eqvt_raw] attribute just adds the theorem to eqvts_raw. |
21 The [eqvt_raw] attribute just adds the theorem to eqvts_raw. |
18 |
22 |
19 TODO: |
23 TODO: In case of the form in (2) one should also |
20 |
24 add the equational form to eqvts |
21 - deal with eqvt-lemmas of the form |
|
22 |
|
23 c x1 x2 ... ==> c (p o x1) (p o x2) .. |
|
24 *) |
25 *) |
25 |
26 |
26 signature NOMINAL_THMDECLS = |
27 signature NOMINAL_THMDECLS = |
27 sig |
28 sig |
28 val eqvt_add: attribute |
29 val eqvt_add: attribute |
54 val merge = Item_Net.merge ); |
52 val merge = Item_Net.merge ); |
55 |
53 |
56 val eqvts = Item_Net.content o EqvtData.get; |
54 val eqvts = Item_Net.content o EqvtData.get; |
57 val eqvts_raw = Item_Net.content o EqvtRawData.get; |
55 val eqvts_raw = Item_Net.content o EqvtRawData.get; |
58 |
56 |
59 val get_eqvts_thms = eqvts o Context.Proof; |
57 val get_eqvts_thms = eqvts o Context.Proof; |
60 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
61 |
59 |
62 val add_thm = EqvtData.map o Item_Net.update; |
60 val add_thm = EqvtData.map o Item_Net.update; |
63 val del_thm = EqvtData.map o Item_Net.remove; |
61 val del_thm = EqvtData.map o Item_Net.remove; |
64 |
62 |
65 fun is_equiv (Const ("==", _) $ _ $ _) = true |
63 fun is_equiv (Const ("==", _) $ _ $ _) = true |
66 | is_equiv _ = false |
64 | is_equiv _ = false |
67 |
65 |
68 fun add_raw_thm thm = |
66 fun add_raw_thm thm = |
69 let |
67 case prop_of thm of |
70 val trm = prop_of thm |
68 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) |
71 in |
69 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
72 if is_equiv trm |
|
73 then (EqvtRawData.map o Item_Net.update) thm |
|
74 else raise THM ("Theorem must be a meta-equality", 0, [thm]) |
|
75 end |
|
76 |
70 |
77 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
71 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
78 |
72 |
79 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
73 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
80 | dest_perm t = raise TERM ("dest_perm", [t]) |
74 | dest_perm t = raise TERM ("dest_perm", [t]) |
102 val eargs' = map Envir.eta_contract args' |
96 val eargs' = map Envir.eta_contract args' |
103 val p_str = fst (fst (dest_Var p)) |
97 val p_str = fst (fst (dest_Var p)) |
104 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
98 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
105 in |
99 in |
106 if c <> c' |
100 if c <> c' |
107 then error "eqvt lemma is not of the right form (constants do not agree)" |
101 then error "Eqvt lemma is not of the right form (constants do not agree)" |
108 else if eargs' <> map (mk_perm p) eargs |
102 else if eargs' <> map (mk_perm p) eargs |
109 then error "eqvt lemma is not of the right form (arguments do not agree)" |
103 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
110 else if args = [] |
104 else if args = [] |
111 then thm |
105 then thm |
112 else Goal.prove ctxt [p_str] [] goal |
106 else Goal.prove ctxt [p_str] [] goal |
113 (fn _ => eqvt_transform_tac thm 1) |
107 (fn _ => eq_transform_tac thm 1) |
114 end |
108 end |
|
109 |
|
110 |
|
111 (* tests whether the lists of pis all agree, and that there is at least one p *) |
|
112 fun is_bad_list [] = true |
|
113 | is_bad_list [_] = false |
|
114 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
|
115 |
|
116 fun mk_minus p = |
|
117 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
|
118 |
|
119 fun imp_transform_tac thy p p' thm = |
|
120 let |
|
121 val cp = Thm.cterm_of thy p |
|
122 val cp' = Thm.cterm_of thy (mk_minus p') |
|
123 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
|
124 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
|
125 in |
|
126 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
|
127 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
|
128 end |
|
129 |
|
130 fun transform_imp ctxt thm = |
|
131 let |
|
132 val thy = ProofContext.theory_of ctxt |
|
133 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
|
134 val (c, prem_args) = strip_comb prem |
|
135 val (c', concl_args) = strip_comb concl |
|
136 val ps = map (fst o dest_perm) concl_args handle TERM _ => [] |
|
137 val p = try hd ps |
|
138 in |
|
139 if c <> c' |
|
140 then error "Eqvt lemma is not of the right form (constants do not agree)" |
|
141 else if is_bad_list ps |
|
142 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
|
143 else if concl_args <> map (mk_perm (the p)) prem_args |
|
144 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
|
145 else |
|
146 let |
|
147 val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem |
|
148 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
|
149 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
|
150 in |
|
151 Goal.prove ctxt' [] [] goal' |
|
152 (fn _ => imp_transform_tac thy (the p) p' thm 1) |
|
153 |> singleton (ProofContext.export ctxt' ctxt) |
|
154 |> transform_eq ctxt |
|
155 end |
|
156 end |
|
157 |
|
158 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
159 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
115 |
160 |
116 fun transform addel_fun thm context = |
161 fun transform addel_fun thm context = |
117 let |
162 let |
118 val ctxt = Context.proof_of context |
163 val ctxt = Context.proof_of context |
119 in |
164 in |
120 case (prop_of thm) of |
165 case (prop_of thm) of |
121 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => |
166 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
122 addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context |
167 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
123 | @{const "==>"} $ _ $ _ => |
168 addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context |
124 error ("not yet implemented") |
169 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
125 | _ => raise (error "only (op=) case implemented yet") |
170 addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context |
|
171 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
126 end |
172 end |
127 |
173 |
128 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
174 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
129 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |
175 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |
130 |
176 |
131 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
177 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
132 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
178 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
133 |
179 |
134 val setup = |
180 val setup = |
135 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
181 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
136 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
182 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
137 "brought into the form p o c = c"]) #> |
183 "brought into the form p o c == c"]) #> |
138 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
184 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
139 (cat_lines ["declaration of equivariance lemmas - no", |
185 (cat_lines ["Declaration of equivariance lemmas - no", |
140 "transformation is performed"]) #> |
186 "transformation is performed"]) #> |
141 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
187 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
142 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
188 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
143 |
189 |
144 |
190 |