169 val gs = map inst pre_gs |
169 val gs = map inst pre_gs |
170 val args = map inst pre_args |
170 val args = map inst pre_args |
171 val rhs = inst pre_rhs |
171 val rhs = inst pre_rhs |
172 |
172 |
173 val cqs = map (cterm_of thy) qs |
173 val cqs = map (cterm_of thy) qs |
174 val ags = map (Thm.assume o cterm_of thy) gs |
174 val (ags, ctxt') = fold_map Thm.assume_hyps (map (cterm_of thy) gs) ctxt |
175 |
175 |
176 val import = fold Thm.forall_elim cqs |
176 val import = fold Thm.forall_elim cqs |
177 #> fold Thm.elim_implies ags |
177 #> fold Thm.elim_implies ags |
178 |
178 |
179 val export = fold_rev (Thm.implies_intr o cprop_of) ags |
179 val export = fold_rev (Thm.implies_intr o cprop_of) ags |
180 #> fold_rev forall_intr_rename (oqnames ~~ cqs) |
180 #> fold_rev forall_intr_rename (oqnames ~~ cqs) |
181 in |
181 in |
182 F ctxt (f, qs, gs, args, rhs) import export |
182 F ctxt' (f, qs, gs, args, rhs) import export |
183 end |
183 end |
184 |
184 |
185 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
185 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
186 import (export : thm -> thm) sum_psimp_eq = |
186 import (export : thm -> thm) sum_psimp_eq = |
187 let |
187 let |
188 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
188 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
189 |
189 |
190 val psimp = import sum_psimp_eq |
190 val psimp = import sum_psimp_eq |
191 val (simp, restore_cond) = |
191 val ((simp, restore_cond), ctxt') = |
192 case cprems_of psimp of |
192 case cprems_of psimp of |
193 [] => (psimp, I) |
193 [] => ((psimp, I), ctxt) |
194 | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
194 | [cond] => |
|
195 let val (asm, ctxt') = Thm.assume_hyps cond ctxt |
|
196 in ((Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end |
195 | _ => raise General.Fail "Too many conditions" |
197 | _ => raise General.Fail "Too many conditions" |
196 in |
198 in |
197 Goal.prove ctxt [] [] |
199 Goal.prove ctxt' [] [] |
198 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
200 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
199 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
201 (fn _ => (Local_Defs.unfold_tac ctxt' all_orig_fdefs) |
200 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
202 THEN EqSubst.eqsubst_tac ctxt' [0] [simp] 1 |
201 THEN (simp_tac ctxt) 1) |
203 THEN (simp_tac ctxt') 1) |
202 |> restore_cond |
204 |> restore_cond |
203 |> export |
205 |> export |
204 end |
206 end |
205 |
207 |
206 val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp} |
208 val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp} |
210 import (export : thm -> thm) sum_psimp_eq = |
212 import (export : thm -> thm) sum_psimp_eq = |
211 let |
213 let |
212 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
214 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
213 |
215 |
214 val psimp = import sum_psimp_eq |
216 val psimp = import sum_psimp_eq |
215 val (cond, simp, restore_cond) = |
217 val ((cond, simp, restore_cond), ctxt') = |
216 case cprems_of psimp of |
218 case cprems_of psimp of |
217 [] => ([], psimp, I) |
219 [] => (([], psimp, I), ctxt) |
218 | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
220 | [cond] => |
|
221 let val (asm, ctxt') = Thm.assume_hyps cond ctxt |
|
222 in (([asm], Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end |
219 | _ => raise General.Fail "Too many conditions" |
223 | _ => raise General.Fail "Too many conditions" |
220 |
224 |
221 val ([p], ctxt') = ctxt |
225 val ([p], ctxt'') = ctxt' |
222 |> fold Variable.declare_term args |
226 |> fold Variable.declare_term args |
223 |> Variable.variant_fixes ["p"] |
227 |> Variable.variant_fixes ["p"] |
224 val p = Free (p, @{typ perm}) |
228 val p = Free (p, @{typ perm}) |
225 |
229 |
226 val simpset = |
230 val simpset = |
227 put_simpset HOL_basic_ss ctxt' addsimps |
231 put_simpset HOL_basic_ss ctxt'' addsimps |
228 @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ |
232 @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ |
229 @{thms Projr.simps Projl.simps} @ |
233 @{thms Projr.simps Projl.simps} @ |
230 [(cond MRS eqvt_thm) RS @{thm sym}] @ |
234 [(cond MRS eqvt_thm) RS @{thm sym}] @ |
231 [inl_perm, inr_perm, simp] |
235 [inl_perm, inr_perm, simp] |
232 val goal_lhs = mk_perm p (list_comb (f, args)) |
236 val goal_lhs = mk_perm p (list_comb (f, args)) |
233 val goal_rhs = list_comb (f, map (mk_perm p) args) |
237 val goal_rhs = list_comb (f, map (mk_perm p) args) |
234 in |
238 in |
235 Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) |
239 Goal.prove ctxt'' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) |
236 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
240 (fn _ => Local_Defs.unfold_tac ctxt'' all_orig_fdefs |
237 THEN (asm_full_simp_tac simpset 1)) |
241 THEN (asm_full_simp_tac simpset 1)) |
238 |> singleton (Proof_Context.export ctxt' ctxt) |
242 |> singleton (Proof_Context.export ctxt'' ctxt) |
239 |> restore_cond |
243 |> restore_cond |
240 |> export |
244 |> export |
241 end |
245 end |
242 |
246 |
243 fun mk_applied_form ctxt caTs thm = |
247 fun mk_applied_form ctxt caTs thm = |