equal
deleted
inserted
replaced
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> |
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
18 |
18 |
19 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
19 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
20 val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
20 val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
21 Proof.context -> thm list |
21 thm list -> Proof.context -> thm list |
22 end |
22 end |
23 |
23 |
24 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
24 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
25 struct |
25 struct |
26 |
26 |
202 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
202 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
203 in |
203 in |
204 induct_prove qtys props qinduct (K ss_tac) ctxt |
204 induct_prove qtys props qinduct (K ss_tac) ctxt |
205 end |
205 end |
206 |
206 |
207 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt = |
207 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = |
208 let |
208 let |
209 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
209 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
210 val p = Free (p, @{typ perm}) |
210 val p = Free (p, @{typ perm}) |
211 |
211 |
212 fun mk_goal qperm_bn alpha_bn = |
212 fun mk_goal qperm_bn alpha_bn = |
216 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
216 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
217 end |
217 end |
218 |
218 |
219 val props = map2 mk_goal qperm_bns alpha_bns |
219 val props = map2 mk_goal qperm_bns alpha_bns |
220 val ss_tac = (K (print_tac "test")) THEN' |
220 val ss_tac = (K (print_tac "test")) THEN' |
221 asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs)) |
221 asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls)) |
222 in |
222 in |
223 @{thms TrueI} |
223 induct_prove qtys props qinduct (K ss_tac) ctxt' |
224 (*induct_prove qtys props qinduct (K ss_tac) ctxt' |
|
225 |> ProofContext.export ctxt' ctxt |
224 |> ProofContext.export ctxt' ctxt |
226 |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*) |
225 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
227 end |
226 end |
228 |
227 |
229 |
228 |
230 end (* structure *) |
229 end (* structure *) |