diff -r 5098771ff041 -r 695c1ed61879 Nominal/Ex/ExCoreHaskell.thy --- a/Nominal/Ex/ExCoreHaskell.thy Tue May 04 13:52:40 2010 +0200 +++ b/Nominal/Ex/ExCoreHaskell.thy Tue May 04 14:13:18 2010 +0200 @@ -1,23 +1,15 @@ theory ExCoreHaskell -imports "../Parser" +imports "../NewParser" begin (* core haskell *) -ML {* val _ = recursive := false *} -(* this should not be an equivariance rule *) -(* for the moment, we force it to be *) -setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} -thm eqvts -(*declare permute_pure[eqvt]*) - atom_decl var atom_decl cvar atom_decl tvar (* there are types, coercion types and regular types list-data-structure *) -ML {* val _ = alpha_type := AlphaLst *} nominal_datatype tkind = KStar | KFun "tkind" "tkind" @@ -28,7 +20,7 @@ | TC "string" | TApp "ty" "ty" | TFun "string" "ty_lst" -| TAll tv::"tvar" "tkind" T::"ty" bind tv in T +| TAll tv::"tvar" "tkind" T::"ty" bind_set tv in T | TEq "ckind" "ty" and ty_lst = TsNil @@ -38,7 +30,7 @@ | CConst "string" | CApp "co" "co" | CFun "string" "co_lst" -| CAll cv::"cvar" "ckind" C::"co" bind cv in C +| CAll cv::"cvar" "ckind" C::"co" bind_set cv in C | CEq "ckind" "co" | CRefl "ty" | CSym "co" @@ -56,13 +48,13 @@ and trm = Var "var" | K "string" -| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t -| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t +| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t +| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t | AppT "trm" "ty" | AppC "trm" "co" -| Lam v::"var" "ty" t::"trm" bind v in t +| Lam v::"var" "ty" t::"trm" bind_set v in t | App "trm" "trm" -| Let x::"var" "ty" "trm" t::"trm" bind x in t +| Let x::"var" "ty" "trm" t::"trm" bind_set x in t | Case "trm" "assoc_lst" | Cast "trm" "ty" --"ty is supposed to be a coercion type only" and assoc_lst = @@ -93,86 +85,6 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" -(* -function -rfv_tkind_raw and rfv_ckind_raw and rfv_ty_raw and rfv_ty_lst_raw and rfv_co_raw and rfv_co_lst_raw and rfv_trm_raw and rfv_assoc_lst_raw and rfv_bv_raw and rfv_bv_vs_raw and rfv_bv_tvs_raw and rfv_bv_cvs_raw and rfv_pat_raw and rfv_vars_raw and rfv_tvars_raw and rfv_cvars_raw -where - "rfv_tkind_raw KStar_raw = {}" -| "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \ rfv_tkind_raw tkind_raw2" -| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \ rfv_ty_raw ty_raw2" -| "rfv_ty_raw (TVar_raw tvar) = {atom tvar}" -| "rfv_ty_raw (TC_raw list) = {}" -| "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \ rfv_ty_raw ty_raw2" -| "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw" -| "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) = - rfv_tkind_raw tkind_raw \ (rfv_ty_raw ty_raw - {atom tvar})" -| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \ rfv_ty_raw ty_raw" -| "rfv_ty_lst_raw TsNil_raw = {}" -| "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \ rfv_ty_lst_raw ty_lst_raw" -| "rfv_co_raw (CVar_raw cvar) = {atom cvar}" -| "rfv_co_raw (CConst_raw list) = {}" -| "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \ rfv_co_raw co_raw2" -| "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw" -| "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) = - rfv_ckind_raw ckind_raw \ (rfv_co_raw co_raw - {atom cvar})" -| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \ rfv_co_raw co_raw" -| "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw" -| "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw" -| "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \ rfv_co_raw co_raw2" -| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \ rfv_ty_raw ty_raw" -| "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw" -| "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw" -| "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \ rfv_co_raw co_raw2" -| "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw" -| "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw" -| "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \ rfv_co_raw co_raw2" -| "rfv_co_lst_raw CsNil_raw = {}" -| "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \ rfv_co_lst_raw co_lst_raw" -| "rfv_trm_raw (Var_raw var) = {atom var}" -| "rfv_trm_raw (K_raw list) = {}" -| "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) = - rfv_tkind_raw tkind_raw \ (rfv_trm_raw trm_raw - {atom tvar})" -| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) = - rfv_ckind_raw ckind_raw \ (rfv_trm_raw trm_raw - {atom cvar})" -| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \ rfv_ty_raw ty_raw" -| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \ rfv_co_raw co_raw" -| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \ (rfv_trm_raw trm_raw - {atom var})" -| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \ rfv_trm_raw trm_raw2" -| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) = - rfv_ty_raw ty_raw \ (rfv_trm_raw trm_raw1 \ (rfv_trm_raw trm_raw2 - {atom var}))" -| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \ rfv_assoc_lst_raw assoc_lst_raw" -| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \ rfv_ty_raw ty_raw" -| "rfv_assoc_lst_raw ANil_raw = {}" -| "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) = - rfv_bv_raw pat_raw \ (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \ rfv_assoc_lst_raw assoc_lst_raw)" -| "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = - rfv_bv_tvs_raw tvars_raw \ (rfv_bv_cvs_raw cvars_raw \ rfv_bv_vs_raw vars_raw)" -| "rfv_bv_vs_raw VsNil_raw = {}" -| "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \ rfv_bv_vs_raw vars_raw" -| "rfv_bv_tvs_raw TvsNil_raw = {}" -| "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) = - rfv_tkind_raw tkind_raw \ rfv_bv_tvs_raw tvars_raw" -| "rfv_bv_cvs_raw CvsNil_raw = {}" -| "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) = - rfv_ckind_raw ckind_raw \ rfv_bv_cvs_raw cvars_raw" -| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) = - rfv_tvars_raw tvars_raw \ (rfv_cvars_raw cvars_raw \ rfv_vars_raw vars_raw)" -| "rfv_vars_raw VsNil_raw = {}" -| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) = - {atom var} \ (rfv_ty_raw ty_raw \ rfv_vars_raw vars_raw)" -| "rfv_tvars_raw TvsNil_raw = {}" -| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) = - {atom tvar} \ (rfv_tkind_raw tkind_raw \ rfv_tvars_raw tvars_raw)" -| "rfv_cvars_raw CvsNil_raw = {}" -| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) = - {atom cvar} \ (rfv_ckind_raw ckind_raw \ rfv_cvars_raw cvars_raw)" -apply pat_completeness -apply auto -done -termination -by lexicographic_order -*) - lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm @@ -213,9 +125,7 @@ "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 - apply (rule_tac [!] alpha_intros) - apply simp_all + 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]: @@ -252,27 +162,23 @@ "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(rule TrueI) apply(simp_all add:permute_bv eqvts) apply(induct c rule: inducts(11)) - apply(rule TrueI) apply(simp_all add:permute_bv eqvts) apply(induct d rule: inducts(10)) - apply(rule TrueI) 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(rule TrueI) 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_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)) @@ -292,13 +198,13 @@ lemma ACons_subst: "supp (Abs_lst (bv pat) trm) \* q \ (ACons pat trm al) = ACons (permute_bv q pat) (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: eqvts[symmetric]) apply (simp add: supp_abs) apply (simp add: fv_supp) - apply (simp add: alpha_perm_bn) apply (rule supp_perm_eq[symmetric]) apply (subst supp_finite_atom_set) apply (rule finite_Diff) @@ -311,34 +217,27 @@ "permute_bv_tvs 0 c = c" "permute_bv_vs 0 d = d" apply(induct b rule: inducts(12)) - apply(rule TrueI) apply(simp_all add:permute_bv eqvts) apply(induct c rule: inducts(11)) - apply(rule TrueI) apply(simp_all add:permute_bv eqvts) apply(induct d rule: inducts(10)) - apply(rule TrueI) apply(simp_all add:permute_bv eqvts) done lemma permute_bv_zero2: "permute_bv 0 a = a" apply(induct a rule: inducts(9)) - apply(rule TrueI) 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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) -apply (simp_all add: eq_iff fresh_star_union) -apply (subst supp_perm_eq) -apply (simp_all add: fv_supp) -done + 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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) +apply (rule TrueI)+ apply (simp_all add: eq_iff fresh_star_union) apply (subst supp_perm_eq) apply (simp_all add: fv_supp) @@ -346,70 +245,65 @@ lemma fv_alpha3: "fv_bv_vs x \* pa \ alpha_bv_vs (pa \ x) x" apply (induct x rule: inducts(10)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) -apply (simp_all add: eq_iff fresh_star_union) +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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) +apply (rule TrueI)+ apply (simp_all add: eq_iff fresh_star_union) apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) -apply (simp add: eqvts) +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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma fin2: "finite (fv_bv_cvs x)" apply (induct x rule: inducts(12)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma fin3: "finite (fv_bv_vs x)" apply (induct x rule: inducts(10)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma fin_fv_bv: "finite (fv_bv x)" apply (induct x rule: inducts(9)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) +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 (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma finb2: "finite (set (bv_cvs x))" apply (induct x rule: inducts(12)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma finb3: "finite (set (bv_vs x))" apply (induct x rule: inducts(10)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) apply (simp_all add: fv_supp finite_supp) done lemma fin_bv: "finite (set (bv x))" apply (induct x rule: inducts(9)) -apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) -apply (simp add: finb1 finb2 finb3) +apply (simp_all add: finb1 finb2 finb3) done -thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct - lemma strong_induction_principle: assumes a01: "\b. P1 b KStar" and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" @@ -494,7 +388,7 @@ 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 only: eq_iff) + 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)}" @@ -534,7 +428,7 @@ 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 only: eq_iff) + 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)}" @@ -575,7 +469,7 @@ 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 only: eq_iff) + 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)}" @@ -615,7 +509,7 @@ 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 only: eq_iff) + 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)}" @@ -656,7 +550,7 @@ 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 only: eq_iff) + 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)}" @@ -697,7 +591,7 @@ 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 only: eq_iff) + 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)}" @@ -760,6 +654,12 @@ 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 @@ -769,7 +669,7 @@ equivariance alpha_tkind_raw thm eqvts -thm eqvts_raw +thm eqvts_raw*) end