26 {* NominalInduct.nominal_induct_method *} |
26 {* NominalInduct.nominal_induct_method *} |
27 {* nominal induction *} |
27 {* nominal induction *} |
28 |
28 |
29 (****************************************************) |
29 (****************************************************) |
30 (* inductive definition involving nominal datatypes *) |
30 (* inductive definition involving nominal datatypes *) |
31 ML_file "nominal_inductive.ML" |
31 ML_file "nominal_inductive.ML" |
32 |
32 |
33 |
33 |
34 (***************************************) |
34 (***************************************) |
35 (* forked code of the function package *) |
35 (* forked code of the function package *) |
36 (* for defining nominal functions *) |
36 (* for defining nominal functions *) |
440 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
440 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
441 |> map Drule.eta_contraction_rule |
441 |> map Drule.eta_contraction_rule |
442 |
442 |
443 (* postprocessing of eq and fv theorems *) |
443 (* postprocessing of eq and fv theorems *) |
444 val qeq_iffs' = qeq_iffs |
444 val qeq_iffs' = qeq_iffs |
445 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
445 |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps qfv_supp_thms)) |
446 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
446 |> map (simplify (put_simpset HOL_basic_ss lthyC |
|
447 addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
447 |
448 |
448 (* filters the theorems that are of the form "qfv = supp" *) |
449 (* filters the theorems that are of the form "qfv = supp" *) |
449 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs |
450 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs |
450 | is_qfv_thm _ = false |
451 | is_qfv_thm _ = false |
451 |
452 |
452 val qsupp_constrs = qfv_defs |
453 val qsupp_constrs = qfv_defs |
453 |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
454 |> map (simplify (put_simpset HOL_basic_ss lthyC |
|
455 addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
454 |
456 |
455 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
457 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
456 val transform_thms = |
458 val transform_thms = |
457 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
459 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
458 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
460 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
459 @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, |
461 @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, |
460 @{thm fresh_def[symmetric]}] |
462 @{thm fresh_def[symmetric]}] |
461 |
463 |
462 val qfresh_constrs = qsupp_constrs |
464 val qfresh_constrs = qsupp_constrs |
463 |> map (fn thm => thm RS transform_thm) |
465 |> map (fn thm => thm RS transform_thm) |
464 |> map (simplify (HOL_basic_ss addsimps transform_thms)) |
466 |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps transform_thms)) |
465 |
467 |
466 (* proving that the qbn result is finite *) |
468 (* proving that the qbn result is finite *) |
467 val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
469 val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
468 |
470 |
469 (* proving that perm_bns preserve alpha *) |
471 (* proving that perm_bns preserve alpha *) |