# HG changeset patch # User Christian Urban # Date 1293495650 0 # Node ID ffb5a181844b5cfc5b8749a1ebee515238a0c3c8 # Parent 16ffbc8442ca63d753c24145fe132b4d8f4ef833 proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Ex/CoreHaskell.thy --- 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 \* - p = as \* (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 \ 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 \ 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 \ 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 \ vars \ vars" -is "permute_bv_vs_raw" -quotient_definition "permute_bv_cvs :: perm \ cvars \ cvars" -is "permute_bv_cvs_raw" -quotient_definition "permute_bv_tvs :: perm \ tvars \ tvars" -is "permute_bv_tvs_raw" -quotient_definition "permute_bv :: perm \ pat \ pat" -is "permute_bv_raw" - -lemma rsp_pre: - "alpha_tvars_raw d a \ alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" - "alpha_cvars_raw e b \ alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" - "alpha_vars_raw f c \ 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 \ bv_cvs b = bv_cvs (permute_bv_cvs p b)" - "p \ bv_tvs c = bv_tvs (permute_bv_tvs p c)" - "p \ 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 \ 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) \* q \ (ACons pt trm al) = ACons (permute_bv q pt) (q \ 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 \* pa \ alpha_bv_tvs (pa \ 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 \* pa \ alpha_bv_cvs (pa \ 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 \* pa \ alpha_bv_vs (pa \ 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 \* pa \ alpha_bv (pa \ 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: "\b. P1 b KStar" and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" @@ -372,295 +162,19 @@ and a44: "\b. P12 b CvsNil" and a45: "\tvar ckind cvars b. \\c. P2 c ckind; \c. P12 c cvars\ \ P12 b (CvsCons tvar ckind cvars)" - shows "P1 (a :: 'a :: pt) tkind \ - P2 (b :: 'b :: pt) ckind \ - P3 (c :: 'c :: {pt,fs}) ty \ - P4 (d :: 'd :: pt) ty_lst \ - P5 (e :: 'e :: {pt,fs}) co \ - P6 (f :: 'f :: pt) co_lst \ - P7 (g :: 'g :: {pt,fs}) trm \ - P8 (h :: 'h :: {pt,fs}) assoc_lst \ - P9 (i :: 'i :: pt) pt \ - P10 (j :: 'j :: pt) vars \ - P11 (k :: 'k :: pt) tvars \ - P12 (l :: 'l :: pt) cvars" -proof - - have a1: "(\p a. P1 a (p \ tkind))" and "(\p b. P2 b (p \ ckind))" and "(\p c. P3 c (p \ ty))" and "(\p d. P4 d (p \ ty_lst))" and "(\p e. P5 e (p \ co))" and " (\p f. P6 f (p \ co_lst))" and "(\p g. P7 g (p \ trm))" and "(\p h. P8 h (p \ assoc_lst))" and a1:"(\p q i. P9 i (permute_bv p (q \ pt)))" and a2:"(\p q j. P10 j (permute_bv_vs q (p \ vars)))" and a3:"(\p q k. P11 k ( permute_bv_tvs q (p \ tvars)))" and a4:"(\p q l. P12 l (permute_bv_cvs q (p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ c \ - supp (Abs (p \ {atom tvar}) (p \ ty)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="TAll (p \ tvar) (p \ tkind) (p \ ty)" - and s="TAll (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ ty) - {atom (pa \ p \ tvar)}" - and s="pa \ (p \ supp ty - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ e \ - supp (Abs (p \ {atom cvar}) (p \ co)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="CAll (p \ cvar) (p \ ckind) (p \ co)" - and s="CAll (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ co) - {atom (pa \ p \ cvar)}" - and s="pa \ (p \ supp co - {p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ g \ - supp (Abs (p \ {atom tvar}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="LAMT (p \ tvar) (p \ tkind) (p \ trm)" - and s="LAMT (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ tvar)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ g \ - supp (Abs (p \ {atom cvar}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="LAMC (p \ cvar) (p \ ckind) (p \ trm)" - and s="LAMC (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ cvar)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ - supp (Abs (p \ {atom var}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="Lam (p \ var) (p \ ty) (p \ trm)" - and s="Lam (pa \ p \ var) (p \ ty) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ var)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ - supp (Abs (p \ {atom var}) (p \ trm2)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="Let (p \ var) (p \ ty) (p \ trm1) (p \ trm2)" - and s="Let (pa \ p \ var) (p \ ty) (p \ trm1) (pa \ p \ 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 \ p \ trm2) - {atom (pa \ p \ var)}" - and s="pa \ (p \ supp trm2 - {p \ 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 "\pa. ((pa \ (set (bv (p \ pat)))) \* h \ - supp (Abs_lst (p \ (bv pat)) (p \ trm)) \* 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 \ tkind)" and "P2 b (0 \ ckind)" "P3 c (0 \ ty)" and "P4 d (0 \ ty_lst)" and "P5 e (0 \ co)" and "P6 f (0 \ co_lst)" and "P7 g (0 \ trm)" and "P8 h (0 \ assoc_lst)" by (blast+) - moreover have "P9 i (permute_bv 0 (0 \ pt))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ 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 diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Ex/Foo2.thy --- 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 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: "\c. P2 c As_Nil" and a6: "\name1 name2 trm assg c. \\d. P1 d trm; \d. P2 d assg\ \ 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)) diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Ex/Multi_Recs2.thy --- 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 "\name c. P1 c (Var name)" + and "\c. P1 c Unit" + and "\exp1 exp2 c. \\c. P1 c exp1; \c. P1 c exp2\ \ P1 c (Multi_Recs2.Pair exp1 exp2)" + and "\lrbs exp c. \b_lrbs lrbs \* c; \c. P5 c lrbs; \c. P1 c exp\ \ P1 c (LetRec lrbs exp)" + and "\name pat exp c. \b_pat pat \* c; \c. P6 c pat; \c. P1 c exp\ \ P2 c (K name pat exp)" + and "\fnclause c. (\c. P2 c fnclause) \ P3 c (S fnclause)" + and "\fnclause fnclauses c. \\c. P2 c fnclause; \c. P3 c fnclauses\ \ + P3 c (ORs fnclause fnclauses)" + and "\fnclauses c. (\c. P3 c fnclauses) \ P4 c (Clause fnclauses)" + and "\lrb c. (\c. P4 c lrb) \ P5 c (Single lrb)" + and "\lrb lrbs c. \\c. P4 c lrb; \c. P5 c lrbs\ \ P5 c (More lrb lrbs)" + and "\name c. P6 c (PVar name)" + and "\c. P6 c PUnit" + and "\pat1 pat2 c. \\c. P6 c pat1; \c. P6 c pat2\ \ 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 diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Nominal2.thy --- 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 *) diff -r 16ffbc8442ca -r ffb5a181844b Nominal/induction_schema.ML --- /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 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 diff -r 16ffbc8442ca -r ffb5a181844b Nominal/nominal_dt_quot.ML --- 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