proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
--- a/Nominal/Ex/CoreHaskell.thy Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Ex/CoreHaskell.thy Tue Dec 28 00:20:50 2010 +0000
@@ -102,218 +102,8 @@
thm core_haskell.size_eqvt
thm core_haskell.supp
-(*
-lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
- unfolding fresh_star_def Ball_def
- by auto (simp_all add: fresh_minus_perm)
-
-primrec permute_bv_vs_raw
-where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
-| "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
-primrec permute_bv_cvs_raw
-where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
-| "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
-primrec permute_bv_tvs_raw
-where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
-| "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
-primrec permute_bv_raw
-where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
- Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
-
-quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
-is "permute_bv_vs_raw"
-quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
-is "permute_bv_cvs_raw"
-quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
-is "permute_bv_tvs_raw"
-quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
-is "permute_bv_raw"
-
-lemma rsp_pre:
- "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
- "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
- "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
- apply (erule_tac [!] alpha_inducts)
- apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
- done
-
-lemma [quot_respect]:
- "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
- "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
- "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
- "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
- apply (simp_all add: rsp_pre)
- apply clarify
- apply (erule_tac alpha_inducts)
- apply (simp_all)
- apply (rule alpha_intros)
- apply (simp_all add: rsp_pre)
- done
-
-thm permute_bv_raw.simps[no_vars]
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma permute_bv_pre:
- "permute_bv p (Kpat c l1 l2 l3) =
- Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
- by (lifting permute_bv_raw.simps)
-
-lemmas permute_bv[simp] =
- permute_bv_pre
- permute_bv_vs_raw.simps[quot_lifted]
- permute_bv_cvs_raw.simps[quot_lifted]
- permute_bv_tvs_raw.simps[quot_lifted]
-
-lemma perm_bv1:
- "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
- "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
- "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
- apply(induct b rule: inducts(12))
- apply(simp_all add:permute_bv eqvts)
- apply(induct c rule: inducts(11))
- apply(simp_all add:permute_bv eqvts)
- apply(induct d rule: inducts(10))
- apply(simp_all add:permute_bv eqvts)
- done
-
-lemma perm_bv2:
- "p \<bullet> bv l = bv (permute_bv p l)"
- apply(induct l rule: inducts(9))
- apply(simp_all add:permute_bv)
- apply(simp add: perm_bv1[symmetric])
- apply(simp add: eqvts)
- done
-
-lemma alpha_perm_bn1:
- "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
- "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
- "alpha_bv_vs vars (permute_bv_vs q vars)"
- apply(induct tvars rule: inducts(11))
- apply(simp_all add:permute_bv eqvts eq_iff)
- apply(induct cvars rule: inducts(12))
- apply(simp_all add:permute_bv eqvts eq_iff)
- apply(induct vars rule: inducts(10))
- apply(simp_all add:permute_bv eqvts eq_iff)
- done
-
-lemma alpha_perm_bn:
- "alpha_bv pt (permute_bv q pt)"
- apply(induct pt rule: inducts(9))
- apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
- done
-
-lemma ACons_subst:
- "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
- apply (simp only: eq_iff)
- apply (simp add: alpha_perm_bn)
- apply (rule_tac x="q" in exI)
- apply (simp add: alphas)
- apply (simp add: perm_bv2[symmetric])
- apply (simp add: supp_abs)
- apply (simp add: fv_supp)
- apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
- apply (rule supp_perm_eq[symmetric])
- apply (subst supp_finite_atom_set)
- apply (rule finite_Diff)
- apply (simp add: finite_supp)
- apply (assumption)
- done
-
-lemma permute_bv_zero1:
- "permute_bv_cvs 0 b = b"
- "permute_bv_tvs 0 c = c"
- "permute_bv_vs 0 d = d"
- apply(induct b rule: inducts(12))
- apply(simp_all add:permute_bv eqvts)
- apply(induct c rule: inducts(11))
- apply(simp_all add:permute_bv eqvts)
- apply(induct d rule: inducts(10))
- apply(simp_all add:permute_bv eqvts)
- done
-
-lemma permute_bv_zero2:
- "permute_bv 0 a = a"
- apply(induct a rule: inducts(9))
- apply(simp_all add:permute_bv eqvts permute_bv_zero1)
- done
-
-lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
- apply (induct x rule: inducts(11))
- apply (simp_all add: eq_iff fresh_star_union)
- done
-
-lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
-apply (induct x rule: inducts(12))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
-apply (induct x rule: inducts(10))
-apply (rule TrueI)+
-apply (simp_all add: fresh_star_union eq_iff)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-apply (simp_all add: eq_iff fresh_star_union)
-apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
-
-lemma fin1: "finite (fv_bv_tvs x)"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin2: "finite (fv_bv_cvs x)"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin3: "finite (fv_bv_vs x)"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_fv_bv: "finite (fv_bv x)"
-apply (induct x rule: inducts(9))
-apply (rule TrueI)+
-defer
-apply (rule TrueI)+
-apply (simp add: fin1 fin2 fin3)
-apply (rule finite_supp)
-done
-
-lemma finb1: "finite (set (bv_tvs x))"
-apply (induct x rule: inducts(11))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb2: "finite (set (bv_cvs x))"
-apply (induct x rule: inducts(12))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma finb3: "finite (set (bv_vs x))"
-apply (induct x rule: inducts(10))
-apply (simp_all add: fv_supp finite_supp)
-done
-
-lemma fin_bv: "finite (set (bv x))"
-apply (induct x rule: inducts(9))
-apply (simp_all add: finb1 finb2 finb3)
-done
-
lemma strong_induction_principle:
+ fixes c::"'a::fs"
assumes a01: "\<And>b. P1 b KStar"
and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
@@ -372,295 +162,19 @@
and a44: "\<And>b. P12 b CvsNil"
and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
\<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
- shows "P1 (a :: 'a :: pt) tkind \<and>
- P2 (b :: 'b :: pt) ckind \<and>
- P3 (c :: 'c :: {pt,fs}) ty \<and>
- P4 (d :: 'd :: pt) ty_lst \<and>
- P5 (e :: 'e :: {pt,fs}) co \<and>
- P6 (f :: 'f :: pt) co_lst \<and>
- P7 (g :: 'g :: {pt,fs}) trm \<and>
- P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
- P9 (i :: 'i :: pt) pt \<and>
- P10 (j :: 'j :: pt) vars \<and>
- P11 (k :: 'k :: pt) tvars \<and>
- P12 (l :: 'l :: pt) cvars"
-proof -
- have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
- apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
- apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
- apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
-
---"GOAL1"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
- supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
- and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
- and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a08)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
---"GOAL2"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
- supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
- and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
- and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a15)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
- and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a29)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
---"GOAL4 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
- and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a30)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL5 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
- and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
- and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a32)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
-
---"GOAL6 a copy-and-paste"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
- supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm)
- apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
- and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
- apply (simp add: eq_iff)
- apply (rule_tac x="-pa" in exI)
- apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
- and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
- apply (simp add: eqvts)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
- apply assumption
- apply (simp add: fresh_star_minus_perm)
- apply (rule a34)
- apply simp
- apply simp
- apply(rotate_tac 2)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2_atom)
- apply (simp add: finite_supp)
- apply (simp add: finite_supp)
- apply (simp add: fresh_def)
- apply (simp only: supp_abs eqvts)
- apply blast
-
---"MAIN ACons Goal"
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
- supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
- apply clarify
- apply (simp only: perm eqvts)
- apply (subst ACons_subst)
- apply assumption
- apply (rule a38)
- apply simp
- apply(rotate_tac 1)
- apply(erule_tac x="(pa + p)" in allE)
- apply simp
- apply simp
- apply (simp add: perm_bv2[symmetric])
- apply (simp add: eqvts eqvts_raw)
- apply (rule at_set_avoiding2)
- apply (simp add: fin_bv)
- apply (simp add: finite_supp)
- apply (simp add: supp_abs)
- apply (simp add: finite_supp)
- apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
- done
- then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
- moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
- ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
-qed
-*)
-
-section {* test about equivariance for alpha *}
-
-(* this should not be an equivariance rule *)
-(* for the moment, we force it to be *)
-
-(*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
-
-thm eqvts
-thm eqvts_raw
-
+ shows "P1 c tkind"
+ "P2 c ckind"
+ "P3 c ty"
+ "P4 c ty_lst"
+ "P5 c co"
+ "P6 c co_lst"
+ "P7 c trm"
+ "P8 c assoc_lst"
+ "P9 c pt"
+ "P10 c vars"
+ "P11 c tvars"
+ "P12 c cvars"
+oops
end
--- a/Nominal/Ex/Foo2.thy Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Ex/Foo2.thy Tue Dec 28 00:20:50 2010 +0000
@@ -26,7 +26,6 @@
-
thm foo.bn_defs
thm foo.permute_bn
thm foo.perm_bn_alpha
@@ -49,6 +48,409 @@
thm foo.supp
thm foo.fresh
+ML {*
+
+open Function_Lib
+
+type rec_call_info = int * (string * typ) list * term list * term list
+
+datatype scheme_case = SchemeCase of
+ {bidx : int,
+ qs: (string * typ) list,
+ oqnames: string list,
+ gs: term list,
+ lhs: term list,
+ rs: rec_call_info list}
+
+datatype scheme_branch = SchemeBranch of
+ {P : term,
+ xs: (string * typ) list,
+ ws: (string * typ) list,
+ Cs: term list}
+
+datatype ind_scheme = IndScheme of
+ {T: typ, (* sum of products *)
+ branches: scheme_branch list,
+ cases: scheme_case list}
+
+val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
+val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
+
+fun meta thm = thm RS eq_reflection
+
+val sum_prod_conv = Raw_Simplifier.rewrite true
+ (map meta (@{thm split_conv} :: @{thms sum.cases}))
+
+fun term_conv thy cv t =
+ cv (cterm_of thy t)
+ |> prop_of |> Logic.dest_equals |> snd
+
+fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
+
+fun dest_hhf ctxt t =
+ let
+ val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
+ in
+ (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+ end
+
+fun mk_scheme' ctxt cases concl =
+ let
+ fun mk_branch concl =
+ let
+ val _ = tracing ("concl:\n" ^ Syntax.string_of_term ctxt concl)
+ val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+ val (P, xs) = strip_comb Pxs
+ val _ = tracing ("xs: " ^ commas (map @{make_string} xs))
+ val _ = map dest_Free xs
+ val _ = tracing ("done")
+ in
+ SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
+ end
+
+ val (branches, cases') = (* correction *)
+ case Logic.dest_conjunctions concl of
+ [conc] =>
+ let
+ val _ $ Pxs = Logic.strip_assums_concl conc
+ val (P, _) = strip_comb Pxs
+ val (cases', conds) =
+ take_prefix (Term.exists_subterm (curry op aconv P)) cases
+ val concl' = fold_rev (curry Logic.mk_implies) conds conc
+ in
+ ([mk_branch concl'], cases')
+ end
+ | concls => (map mk_branch concls, cases)
+
+ fun mk_case premise =
+ let
+ val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
+ val (P, lhs) = strip_comb Plhs
+
+ fun bidx Q =
+ find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
+
+ fun mk_rcinfo pr =
+ let
+ val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+ val (P', rcs) = strip_comb Phyp
+ in
+ (bidx P', Gvs, Gas, rcs)
+ end
+
+ fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
+
+ val (gs, rcprs) =
+ take_prefix (not o Term.exists_subterm is_pred) prems
+ in
+ SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
+ gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
+ end
+
+ fun PT_of (SchemeBranch { xs, ...}) =
+ foldr1 HOLogic.mk_prodT (map snd xs)
+
+ val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+ in
+ IndScheme {T=ST, cases=map mk_case cases', branches=branches }
+ end
+
+fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
+ let
+ val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
+ val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
+
+ val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
+ val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+ val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
+
+ fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
+ HOLogic.mk_Trueprop Pbool
+ |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
+ (xs' ~~ lhs)
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+ in
+ HOLogic.mk_Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
+ |> fold_rev (curry Logic.mk_implies) Cs'
+ |> fold_rev (Logic.all o Free) ws
+ |> fold_rev mk_forall_rename (map fst xs ~~ xs')
+ |> mk_forall_rename ("P", Pbool)
+ end
+
+fun mk_wf R (IndScheme {T, ...}) =
+ HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
+
+fun mk_ineqs R (IndScheme {T, cases, branches}) =
+ let
+ fun inject i ts =
+ SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+
+ val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
+
+ fun mk_pres bdx args =
+ let
+ val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
+ fun replace (x, v) t = betapply (lambda (Free x) t, v)
+ val Cs' = map (fold replace (xs ~~ args)) Cs
+ val cse =
+ HOLogic.mk_Trueprop thesis
+ |> fold_rev (curry Logic.mk_implies) Cs'
+ |> fold_rev (Logic.all o Free) ws
+ in
+ Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
+ end
+
+ fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) =
+ let
+ fun g (bidx', Gvs, Gas, rcarg) =
+ let val export =
+ fold_rev (curry Logic.mk_implies) Gas
+ #> fold_rev (curry Logic.mk_implies) gs
+ #> fold_rev (Logic.all o Free) Gvs
+ #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+ in
+ (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
+ |> HOLogic.mk_Trueprop
+ |> export,
+ mk_pres bidx' rcarg
+ |> export
+ |> Logic.all thesis)
+ end
+ in
+ map g rs
+ end
+ in
+ map f cases
+ end
+
+
+fun mk_ind_goal thy branches =
+ let
+ fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
+ HOLogic.mk_Trueprop (list_comb (P, map Free xs))
+ |> fold_rev (curry Logic.mk_implies) Cs
+ |> fold_rev (Logic.all o Free) ws
+ |> term_conv thy ind_atomize
+ |> Object_Logic.drop_judgment thy
+ |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+ in
+ SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+ end
+
+fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
+ (IndScheme {T, cases=scases, branches}) =
+ let
+ val n = length branches
+ val scases_idx = map_index I scases
+
+ fun inject i ts =
+ SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+ val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
+
+ val thy = ProofContext.theory_of ctxt
+ val cert = cterm_of thy
+
+ val P_comp = mk_ind_goal thy branches
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ val ihyp = Term.all T $ Abs ("z", T,
+ Logic.mk_implies
+ (HOLogic.mk_Trueprop (
+ Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
+ $ (HOLogic.pair_const T T $ Bound 0 $ x)
+ $ R),
+ HOLogic.mk_Trueprop (P_comp $ Bound 0)))
+ |> cert
+
+ val aihyp = Thm.assume ihyp
+
+ (* Rule for case splitting along the sum types *)
+ val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
+ val pats = map_index (uncurry inject) xss
+ val sum_split_rule =
+ Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+
+ fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
+ let
+ val fxs = map Free xs
+ val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+
+ val C_hyps = map (cert #> Thm.assume) Cs
+
+ val (relevant_cases, ineqss') =
+ (scases_idx ~~ ineqss)
+ |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx)
+ |> split_list
+
+ fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
+ let
+ val case_hyps =
+ map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+
+ val cqs = map (cert o Free) qs
+ val ags = map (Thm.assume o cert) gs
+
+ val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
+ val sih = full_simplify replace_x_ss aihyp
+
+ fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
+ let
+ val cGas = map (Thm.assume o cert) Gas
+ val cGvs = map (cert o Free) Gvs
+ val import = fold Thm.forall_elim (cqs @ cGvs)
+ #> fold Thm.elim_implies (ags @ cGas)
+ val ipres = pres
+ |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
+ |> import
+ in
+ sih
+ |> Thm.forall_elim (cert (inject idx rcargs))
+ |> Thm.elim_implies (import ineq) (* Psum rcargs *)
+ |> Conv.fconv_rule sum_prod_conv
+ |> Conv.fconv_rule ind_rulify
+ |> (fn th => th COMP ipres) (* P rs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) cGas
+ |> fold_rev Thm.forall_intr cGvs
+ end
+
+ val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *)
+
+ val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
+ |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev (Logic.all o Free) qs
+ |> cert
+
+ val Plhs_to_Pxs_conv =
+ foldl1 (uncurry Conv.combination_conv)
+ (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
+
+ val res = Thm.assume step
+ |> fold Thm.forall_elim cqs
+ |> fold Thm.elim_implies ags
+ |> fold Thm.elim_implies P_recs (* P lhs *)
+ |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
+ |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
+ in
+ (res, (cidx, step))
+ end
+
+ val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
+
+ val bstep = complete_thm
+ |> Thm.forall_elim (cert (list_comb (P, fxs)))
+ |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
+ |> fold Thm.elim_implies C_hyps
+ |> fold Thm.elim_implies cases (* P xs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
+ |> fold_rev (Thm.forall_intr o cert o Free) ws
+
+ val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+ |> Goal.init
+ |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+ THEN CONVERSION ind_rulify 1)
+ |> Seq.hd
+ |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
+ |> Goal.finish ctxt
+ |> Thm.implies_intr (cprop_of branch_hyp)
+ |> fold_rev (Thm.forall_intr o cert) fxs
+ in
+ (Pxs, steps)
+ end
+
+ val (branches, steps) =
+ map_index prove_branch (branches ~~ (complete_thms ~~ pats))
+ |> split_list |> apsnd flat
+
+ val istep = sum_split_rule
+ |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+ |> Thm.implies_intr ihyp
+ |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+
+ val induct_rule =
+ @{thm "wf_induct_rule"}
+ |> (curry op COMP) wf_thm
+ |> (curry op COMP) istep
+
+ val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
+ in
+ (steps_sorted, induct_rule)
+ end
+
+
+fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
+ (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
+ let
+ val (ctxt', _, cases, concl) = dest_hhf ctxt t
+ val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
+ val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
+ val R = Free (Rn, mk_relT ST)
+ val x = Free (xn, ST)
+ val cert = cterm_of (ProofContext.theory_of ctxt)
+
+ val ineqss = mk_ineqs R scheme
+ |> map (map (pairself (Thm.assume o cert)))
+ val complete =
+ map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
+ val wf_thm = mk_wf R scheme |> cert |> Thm.assume
+
+ val (descent, pres) = split_list (flat ineqss)
+ val newgoals = complete @ pres @ wf_thm :: descent
+
+ val (steps, indthm) =
+ mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
+
+ fun project (i, SchemeBranch {xs, ...}) =
+ let
+ val inst = (foldr1 HOLogic.mk_prod (map Free xs))
+ |> SumTree.mk_inj ST (length branches) (i + 1)
+ |> cert
+ in
+ indthm
+ |> Drule.instantiate' [] [SOME inst]
+ |> simplify SumTree.sumcase_split_ss
+ |> Conv.fconv_rule ind_rulify
+ end
+
+ val res = Conjunction.intr_balanced (map_index project branches)
+ |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
+ |> Drule.generalize ([], [Rn])
+
+ val nbranches = length branches
+ val npres = length pres
+ in
+ Thm.compose_no_flatten false (res, length newgoals) i
+ THEN term_tac (i + nbranches + npres)
+ THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
+ THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
+ end))
+
+
+fun induction_schema_tac ctxt =
+ mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+
+*}
+
+ML {*
+val trm1 = @{prop "P1 &&& P2 &&& P3"}
+val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"}
+*}
+
+ML {*
+ Logic.dest_conjunctions trm2
+*}
+
+lemma
+ shows "P1" "P2" "P4"
+oops
+
+lemma
+ shows "P1" "P2" "P3" "P4"
+oops
+
lemma strong_induct:
fixes c :: "'a :: fs"
and assg :: assg and trm :: trm
@@ -63,8 +465,7 @@
and a5: "\<And>c. P2 c As_Nil"
and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
shows "P1 c trm" "P2 c assg"
- using assms
- apply(induction_schema)
+ apply(raw_tactic {* induction_schema_tac @{context} @{thms assms} *})
apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1))
apply(simp_all)[5]
apply(rule_tac ya="assg" in foo.strong_exhaust(2))
--- a/Nominal/Ex/Multi_Recs2.thy Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy Tue Dec 28 00:20:50 2010 +0000
@@ -84,6 +84,44 @@
thm fun_recs.supp
+
+
+lemma
+ fixes c::"'a::fs"
+ assumes "\<And>name c. P1 c (Var name)"
+ and "\<And>c. P1 c Unit"
+ and "\<And>exp1 exp2 c. \<lbrakk>\<And>c. P1 c exp1; \<And>c. P1 c exp2\<rbrakk> \<Longrightarrow> P1 c (Multi_Recs2.Pair exp1 exp2)"
+ and "\<And>lrbs exp c. \<lbrakk>b_lrbs lrbs \<sharp>* c; \<And>c. P5 c lrbs; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P1 c (LetRec lrbs exp)"
+ and "\<And>name pat exp c. \<lbrakk>b_pat pat \<sharp>* c; \<And>c. P6 c pat; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P2 c (K name pat exp)"
+ and "\<And>fnclause c. (\<And>c. P2 c fnclause) \<Longrightarrow> P3 c (S fnclause)"
+ and "\<And>fnclause fnclauses c. \<lbrakk>\<And>c. P2 c fnclause; \<And>c. P3 c fnclauses\<rbrakk> \<Longrightarrow>
+ P3 c (ORs fnclause fnclauses)"
+ and "\<And>fnclauses c. (\<And>c. P3 c fnclauses) \<Longrightarrow> P4 c (Clause fnclauses)"
+ and "\<And>lrb c. (\<And>c. P4 c lrb) \<Longrightarrow> P5 c (Single lrb)"
+ and "\<And>lrb lrbs c. \<lbrakk>\<And>c. P4 c lrb; \<And>c. P5 c lrbs\<rbrakk> \<Longrightarrow> P5 c (More lrb lrbs)"
+ and "\<And>name c. P6 c (PVar name)"
+ and "\<And>c. P6 c PUnit"
+ and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"
+ shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"
+ apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
+oops
+
+ML {*
+ val trm1 = @{prop "P1 &&& P2 &&& P3"}
+ val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"}
+*}
+
+ML {*
+ Logic.dest_conjunction_list trm1;
+ Logic.dest_conjunction_list trm2
+*}
+
+ML {*
+ Logic.dest_conjunctions trm1;
+ Logic.dest_conjunctions trm2
+*}
+
+
end
--- a/Nominal/Nominal2.thy Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Nominal2.thy Tue Dec 28 00:20:50 2010 +0000
@@ -4,8 +4,10 @@
uses ("nominal_dt_rawfuns.ML")
("nominal_dt_alpha.ML")
("nominal_dt_quot.ML")
+ ("induction_schema.ML")
begin
+use "induction_schema.ML"
use "nominal_dt_rawfuns.ML"
ML {* open Nominal_Dt_RawFuns *}
@@ -533,7 +535,7 @@
val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
- val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses
+ val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses
(* noting the theorems *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/induction_schema.ML Tue Dec 28 00:20:50 2010 +0000
@@ -0,0 +1,401 @@
+(* Title: HOL/Tools/Function/induction_schema.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A method to prove induction schemas.
+*)
+
+signature INDUCTION_SCHEMA =
+sig
+ val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
+ -> Proof.context -> thm list -> tactic
+ val induction_schema_tac : Proof.context -> thm list -> tactic
+ val setup : theory -> theory
+end
+
+
+structure Induction_Schema : INDUCTION_SCHEMA =
+struct
+
+open Function_Lib
+
+type rec_call_info = int * (string * typ) list * term list * term list
+
+datatype scheme_case = SchemeCase of
+ {bidx : int,
+ qs: (string * typ) list,
+ oqnames: string list,
+ gs: term list,
+ lhs: term list,
+ rs: rec_call_info list}
+
+datatype scheme_branch = SchemeBranch of
+ {P : term,
+ xs: (string * typ) list,
+ ws: (string * typ) list,
+ Cs: term list}
+
+datatype ind_scheme = IndScheme of
+ {T: typ, (* sum of products *)
+ branches: scheme_branch list,
+ cases: scheme_case list}
+
+val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
+val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
+
+fun meta thm = thm RS eq_reflection
+
+val sum_prod_conv = Raw_Simplifier.rewrite true
+ (map meta (@{thm split_conv} :: @{thms sum.cases}))
+
+fun term_conv thy cv t =
+ cv (cterm_of thy t)
+ |> prop_of |> Logic.dest_equals |> snd
+
+fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
+
+fun dest_hhf ctxt t =
+ let
+ val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
+ in
+ (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+ end
+
+fun mk_scheme' ctxt cases concl =
+ let
+ fun mk_branch concl =
+ let
+ val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+ val (P, xs) = strip_comb Pxs
+ in
+ SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
+ end
+
+ val (branches, cases') = (* correction *)
+ case Logic.dest_conjunctions concl of
+ [conc] =>
+ let
+ val _ $ Pxs = Logic.strip_assums_concl conc
+ val (P, _) = strip_comb Pxs
+ val (cases', conds) =
+ take_prefix (Term.exists_subterm (curry op aconv P)) cases
+ val concl' = fold_rev (curry Logic.mk_implies) conds conc
+ in
+ ([mk_branch concl'], cases')
+ end
+ | concls => (map mk_branch concls, cases)
+
+ fun mk_case premise =
+ let
+ val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
+ val (P, lhs) = strip_comb Plhs
+
+ fun bidx Q =
+ find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
+
+ fun mk_rcinfo pr =
+ let
+ val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+ val (P', rcs) = strip_comb Phyp
+ in
+ (bidx P', Gvs, Gas, rcs)
+ end
+
+ fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
+
+ val (gs, rcprs) =
+ take_prefix (not o Term.exists_subterm is_pred) prems
+ in
+ SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
+ gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
+ end
+
+ fun PT_of (SchemeBranch { xs, ...}) =
+ foldr1 HOLogic.mk_prodT (map snd xs)
+
+ val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+ in
+ IndScheme {T=ST, cases=map mk_case cases', branches=branches }
+ end
+
+fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
+ let
+ val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
+ val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
+
+ val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
+ val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+ val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
+
+ fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
+ HOLogic.mk_Trueprop Pbool
+ |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
+ (xs' ~~ lhs)
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+ in
+ HOLogic.mk_Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
+ |> fold_rev (curry Logic.mk_implies) Cs'
+ |> fold_rev (Logic.all o Free) ws
+ |> fold_rev mk_forall_rename (map fst xs ~~ xs')
+ |> mk_forall_rename ("P", Pbool)
+ end
+
+fun mk_wf R (IndScheme {T, ...}) =
+ HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
+
+fun mk_ineqs R (IndScheme {T, cases, branches}) =
+ let
+ fun inject i ts =
+ SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+
+ val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
+
+ fun mk_pres bdx args =
+ let
+ val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
+ fun replace (x, v) t = betapply (lambda (Free x) t, v)
+ val Cs' = map (fold replace (xs ~~ args)) Cs
+ val cse =
+ HOLogic.mk_Trueprop thesis
+ |> fold_rev (curry Logic.mk_implies) Cs'
+ |> fold_rev (Logic.all o Free) ws
+ in
+ Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
+ end
+
+ fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) =
+ let
+ fun g (bidx', Gvs, Gas, rcarg) =
+ let val export =
+ fold_rev (curry Logic.mk_implies) Gas
+ #> fold_rev (curry Logic.mk_implies) gs
+ #> fold_rev (Logic.all o Free) Gvs
+ #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+ in
+ (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
+ |> HOLogic.mk_Trueprop
+ |> export,
+ mk_pres bidx' rcarg
+ |> export
+ |> Logic.all thesis)
+ end
+ in
+ map g rs
+ end
+ in
+ map f cases
+ end
+
+
+fun mk_ind_goal thy branches =
+ let
+ fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
+ HOLogic.mk_Trueprop (list_comb (P, map Free xs))
+ |> fold_rev (curry Logic.mk_implies) Cs
+ |> fold_rev (Logic.all o Free) ws
+ |> term_conv thy ind_atomize
+ |> Object_Logic.drop_judgment thy
+ |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+ in
+ SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+ end
+
+fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
+ (IndScheme {T, cases=scases, branches}) =
+ let
+ val n = length branches
+ val scases_idx = map_index I scases
+
+ fun inject i ts =
+ SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+ val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
+
+ val thy = ProofContext.theory_of ctxt
+ val cert = cterm_of thy
+
+ val P_comp = mk_ind_goal thy branches
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ val ihyp = Term.all T $ Abs ("z", T,
+ Logic.mk_implies
+ (HOLogic.mk_Trueprop (
+ Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
+ $ (HOLogic.pair_const T T $ Bound 0 $ x)
+ $ R),
+ HOLogic.mk_Trueprop (P_comp $ Bound 0)))
+ |> cert
+
+ val aihyp = Thm.assume ihyp
+
+ (* Rule for case splitting along the sum types *)
+ val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
+ val pats = map_index (uncurry inject) xss
+ val sum_split_rule =
+ Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+
+ fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
+ let
+ val fxs = map Free xs
+ val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+
+ val C_hyps = map (cert #> Thm.assume) Cs
+
+ val (relevant_cases, ineqss') =
+ (scases_idx ~~ ineqss)
+ |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx)
+ |> split_list
+
+ fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
+ let
+ val case_hyps =
+ map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+
+ val cqs = map (cert o Free) qs
+ val ags = map (Thm.assume o cert) gs
+
+ val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
+ val sih = full_simplify replace_x_ss aihyp
+
+ fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
+ let
+ val cGas = map (Thm.assume o cert) Gas
+ val cGvs = map (cert o Free) Gvs
+ val import = fold Thm.forall_elim (cqs @ cGvs)
+ #> fold Thm.elim_implies (ags @ cGas)
+ val ipres = pres
+ |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
+ |> import
+ in
+ sih
+ |> Thm.forall_elim (cert (inject idx rcargs))
+ |> Thm.elim_implies (import ineq) (* Psum rcargs *)
+ |> Conv.fconv_rule sum_prod_conv
+ |> Conv.fconv_rule ind_rulify
+ |> (fn th => th COMP ipres) (* P rs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) cGas
+ |> fold_rev Thm.forall_intr cGvs
+ end
+
+ val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *)
+
+ val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
+ |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev (Logic.all o Free) qs
+ |> cert
+
+ val Plhs_to_Pxs_conv =
+ foldl1 (uncurry Conv.combination_conv)
+ (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
+
+ val res = Thm.assume step
+ |> fold Thm.forall_elim cqs
+ |> fold Thm.elim_implies ags
+ |> fold Thm.elim_implies P_recs (* P lhs *)
+ |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
+ |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
+ in
+ (res, (cidx, step))
+ end
+
+ val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
+
+ val bstep = complete_thm
+ |> Thm.forall_elim (cert (list_comb (P, fxs)))
+ |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
+ |> fold Thm.elim_implies C_hyps
+ |> fold Thm.elim_implies cases (* P xs *)
+ |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
+ |> fold_rev (Thm.forall_intr o cert o Free) ws
+
+ val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+ |> Goal.init
+ |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+ THEN CONVERSION ind_rulify 1)
+ |> Seq.hd
+ |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
+ |> Goal.finish ctxt
+ |> Thm.implies_intr (cprop_of branch_hyp)
+ |> fold_rev (Thm.forall_intr o cert) fxs
+ in
+ (Pxs, steps)
+ end
+
+ val (branches, steps) =
+ map_index prove_branch (branches ~~ (complete_thms ~~ pats))
+ |> split_list |> apsnd flat
+
+ val istep = sum_split_rule
+ |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+ |> Thm.implies_intr ihyp
+ |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+
+ val induct_rule =
+ @{thm "wf_induct_rule"}
+ |> (curry op COMP) wf_thm
+ |> (curry op COMP) istep
+
+ val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
+ in
+ (steps_sorted, induct_rule)
+ end
+
+
+fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
+ (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
+ let
+ val (ctxt', _, cases, concl) = dest_hhf ctxt t
+ val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
+ val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
+ val R = Free (Rn, mk_relT ST)
+ val x = Free (xn, ST)
+ val cert = cterm_of (ProofContext.theory_of ctxt)
+
+ val ineqss = mk_ineqs R scheme
+ |> map (map (pairself (Thm.assume o cert)))
+ val complete =
+ map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
+ val wf_thm = mk_wf R scheme |> cert |> Thm.assume
+
+ val (descent, pres) = split_list (flat ineqss)
+ val newgoals = complete @ pres @ wf_thm :: descent
+
+ val (steps, indthm) =
+ mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
+
+ fun project (i, SchemeBranch {xs, ...}) =
+ let
+ val inst = (foldr1 HOLogic.mk_prod (map Free xs))
+ |> SumTree.mk_inj ST (length branches) (i + 1)
+ |> cert
+ in
+ indthm
+ |> Drule.instantiate' [] [SOME inst]
+ |> simplify SumTree.sumcase_split_ss
+ |> Conv.fconv_rule ind_rulify
+ end
+
+ val res = Conjunction.intr_balanced (map_index project branches)
+ |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
+ |> Drule.generalize ([], [Rn])
+
+ val nbranches = length branches
+ val npres = length pres
+ in
+ Thm.compose_no_flatten false (res, length newgoals) i
+ THEN term_tac (i + nbranches + npres)
+ THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
+ THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
+ end))
+
+
+fun induction_schema_tac ctxt =
+ mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+
+val setup =
+ Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
+ "proves an induction principle"
+
+end
--- a/Nominal/nominal_dt_quot.ML Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML Tue Dec 28 00:20:50 2010 +0000
@@ -48,6 +48,8 @@
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
struct
+fun lookup xs x = the (AList.lookup (op=) xs x)
+
(* defines the quotient types *)
fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
@@ -379,8 +381,8 @@
end
-(** proves strong exhauts theorems **)
+(*** proves strong exhauts theorems ***)
(* fixme: move into nominal_library *)
fun abs_const bmode ty =
@@ -629,7 +631,7 @@
|> HOLogic.mk_Trueprop
|> mk_all (c_name, c_ty)
-fun prep_prem lthy c (c_name, c_ty) bclauses (params, prems, concl) =
+fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) =
let
val tys = map snd params
val binders = get_all_binders bclauses
@@ -686,15 +688,33 @@
val prems' = prems
|> map strip_full_horn
- |> map2 (prep_prem lthy'' c (c_name, c_ty)) (flat bclausesss)
- |> map (Syntax.check_term lthy'')
+ |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
- val _ = tracing ("induct:\n" ^ Syntax.string_of_term lthy'' (prop_of induct'))
- val _ = tracing ("concls:\n" ^ commas (map (Syntax.string_of_term lthy'') concls))
- val _ = tracing ("prems':\n" ^ cat_lines (map (Syntax.string_of_term lthy'') prems'))
-
+ fun pat_tac ctxt thm =
+ Subgoal.FOCUS (fn {params, context, ...} =>
+ let
+ val thy = ProofContext.theory_of context
+ val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
+ val vs = Term.add_vars (prop_of thm) []
+ val vs_tys = map (Type.legacy_freeze_type o snd) vs
+ val vs_ctrms = map (cterm_of thy o Var) vs
+ val assigns = map (lookup ty_parms) vs_tys
+
+ val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
+ in
+ rtac thm' 1
+ end) ctxt
+ THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss
+
val thm = Goal.prove_multi lthy'' [] prems' concls
- (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy''))
+ (fn {prems, context} =>
+ print_tac "start"
+ THEN Induction_Schema.induction_schema_tac context prems
+ THEN print_tac "after induct schema"
+ THEN RANGE (map (pat_tac context) exhausts) 1
+ THEN print_tac "after pat"
+ THEN Skip_Proof.cheat_tac (ProofContext.theory_of context)
+ )
in
@{thm TrueI}
end