116 rtac (thm RS @{thm trans}), |
116 rtac (thm RS @{thm trans}), |
117 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
117 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
118 end |
118 end |
119 |
119 |
120 fun eqvt_transform_eq ctxt thm = |
120 fun eqvt_transform_eq ctxt thm = |
121 let |
121 let |
122 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
122 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
123 handle TERM _ => error "Equivariance lemma must be an equality." |
123 handle TERM _ => error "Equivariance lemma must be an equality." |
124 val (p, t) = dest_perm lhs |
124 val (p, t) = dest_perm lhs |
125 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
125 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
126 |
126 |
127 val ps = get_perms rhs handle TERM _ => [] |
127 val ps = get_perms rhs handle TERM _ => [] |
128 val (c, c') = (head_of t, head_of rhs) |
128 val (c, c') = (head_of t, head_of rhs) |
129 val msg = "Equivariance lemma is not of the right form " |
129 val msg = "Equivariance lemma is not of the right form " |
130 in |
130 in |
131 if c <> c' |
131 if c <> c' |
132 then error (msg ^ "(constants do not agree).") |
132 then error (msg ^ "(constants do not agree).") |
133 else if is_bad_list (p :: ps) |
133 else if is_bad_list (p :: ps) |
134 then error (msg ^ "(permutations do not agree).") |
134 then error (msg ^ "(permutations do not agree).") |
135 else if not (rhs aconv (put_perm p t)) |
135 else if not (rhs aconv (put_perm p t)) |
136 then error (msg ^ "(arguments do not agree).") |
136 then error (msg ^ "(arguments do not agree).") |
137 else if is_Const t |
137 else if is_Const t |
138 then safe_mk_equiv thm |
138 then safe_mk_equiv thm |
139 else |
139 else |
140 let |
140 let |
141 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
141 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
142 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
142 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
143 in |
143 in |
144 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
144 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
145 |> singleton (ProofContext.export ctxt' ctxt) |
145 |> singleton (ProofContext.export ctxt' ctxt) |
146 |> safe_mk_equiv |
146 |> safe_mk_equiv |
147 |> zero_var_indexes |
147 |> zero_var_indexes |
148 end |
148 end |
149 end |
149 end |
150 |
150 |
151 (* transforms equations into the "p o c == c"-form |
151 (* transforms equations into the "p o c == c"-form |
152 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
152 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
153 |
153 |
154 fun eqvt_transform_imp_tac ctxt p p' thm = |
154 fun eqvt_transform_imp_tac ctxt p p' thm = |
155 let |
155 let |
156 val thy = ProofContext.theory_of ctxt |
156 val thy = ProofContext.theory_of ctxt |
157 val cp = Thm.cterm_of thy p |
157 val cp = Thm.cterm_of thy p |
158 val cp' = Thm.cterm_of thy (mk_minus p') |
158 val cp' = Thm.cterm_of thy (mk_minus p') |
159 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
159 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
160 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
160 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
161 in |
161 in |
162 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
162 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
163 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
163 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
164 end |
164 end |
165 |
165 |
166 fun eqvt_transform_imp ctxt thm = |
166 fun eqvt_transform_imp ctxt thm = |
167 let |
167 let |
168 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
168 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
169 val (c, c') = (head_of prem, head_of concl) |
169 val (c, c') = (head_of prem, head_of concl) |
170 val ps = get_perms concl handle TERM _ => [] |
170 val ps = get_perms concl handle TERM _ => [] |
171 val p = try hd ps |
171 val p = try hd ps |
172 val msg = "Equivariance lemma is not of the right form " |
172 val msg = "Equivariance lemma is not of the right form " |
173 in |
173 in |
174 if c <> c' |
174 if c <> c' |
175 then error (msg ^ "(constants do not agree).") |
175 then error (msg ^ "(constants do not agree).") |
176 else if is_bad_list ps |
176 else if is_bad_list ps |
177 then error (msg ^ "(permutations do not agree).") |
177 then error (msg ^ "(permutations do not agree).") |
178 else if not (concl aconv (put_perm (the p) prem)) |
178 else if not (concl aconv (put_perm (the p) prem)) |
179 then error (msg ^ "(arguments do not agree).") |
179 then error (msg ^ "(arguments do not agree).") |
180 else |
180 else |
181 let |
181 let |
182 val prem' = mk_perm (the p) prem |
182 val prem' = mk_perm (the p) prem |
183 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
183 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
184 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
184 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
185 in |
185 in |
186 Goal.prove ctxt' [] [] goal' |
186 Goal.prove ctxt' [] [] goal' |
187 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
187 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
188 |> singleton (ProofContext.export ctxt' ctxt) |
188 |> singleton (ProofContext.export ctxt' ctxt) |
189 end |
189 end |
190 end |
190 end |
191 |
191 |
192 fun eqvt_transform ctxt thm = |
192 fun eqvt_transform ctxt thm = |
193 case (prop_of thm) of |
193 case (prop_of thm) of |
194 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
194 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
195 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
195 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
196 eqvt_transform_eq ctxt thm |
196 eqvt_transform_eq ctxt thm |
197 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
197 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
198 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
198 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
199 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
199 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
200 |
200 |
201 |
201 |
202 (** attributes **) |
202 (** attributes **) |
203 |
203 |
204 val eqvt_add = Thm.declaration_attribute |
204 val eqvt_add = Thm.declaration_attribute |