# HG changeset patch # User Cezary Kaliszyk # Date 1272983610 -7200 # Node ID f2f427bc4fd171e58ed0d3e3a63a6c02d8fd06c8 # Parent 8bd75f2fd7b0f6856f55d4286f1d117e2684a777# Parent 13da6048711210ee547229fcfe5832af2f9c00c1 merge diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Ex/ExCoreHaskell.thy --- a/Nominal/Ex/ExCoreHaskell.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/Ex/ExCoreHaskell.thy Tue May 04 16:33:30 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 diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Ex/ExPS7.thy --- a/Nominal/Ex/ExPS7.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/Ex/ExPS7.thy Tue May 04 16:33:30 2010 +0200 @@ -1,17 +1,16 @@ theory ExPS7 -imports "../Parser" +imports "../NewParser" begin (* example 7 from Peter Sewell's bestiary *) atom_decl name -ML {* val _ = recursive := true *} nominal_datatype exp7 = EVar name | EUnit | EPair exp7 exp7 -| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e +| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e and lrb = Assign name exp7 and lrbs = diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Ex/Term8.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Ex/Term8.thy Tue May 04 16:33:30 2010 +0200 @@ -0,0 +1,23 @@ +theory Term8 +imports "../NewParser" +begin + +(* example 8 from Terms.thy *) + +atom_decl name + +nominal_datatype foo = + Foo0 "name" +| Foo1 b::"bar" f::"foo" bind_set "bv b" in f +and bar = + Bar0 "name" +| Bar1 "name" s::"name" b::"bar" bind_set s in b +binder + bv +where + "bv (Bar0 x) = {}" +| "bv (Bar1 v x b) = {atom v}" + +end + + diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Ex/Test.thy --- a/Nominal/Ex/Test.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/Ex/Test.thy Tue May 04 16:33:30 2010 +0200 @@ -20,23 +20,6 @@ thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] *) -(* example 8 from Terms.thy *) - -(* Binding in a term under a bn, needs to fail *) -(* -nominal_datatype foo8 = - Foo0 "name" -| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" -and bar8 = - Bar0 "name" -| Bar1 "name" s::"name" b::"bar8" bind s in b -binder - bv8 -where - "bv8 (Bar0 x) = {}" -| "bv8 (Bar1 v x b) = {atom v}" -*) - end diff -r 13da60487112 -r f2f427bc4fd1 Nominal/NewFv.thy --- a/Nominal/NewFv.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/NewFv.thy Tue May 04 16:33:30 2010 +0200 @@ -4,6 +4,8 @@ begin ML {* +(* binding modes *) + datatype bmodes = BEmy of int | BLst of ((term option * int) list) * (int list) @@ -243,18 +245,19 @@ *} ML {* -fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy = +fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy = let val thy = ProofContext.theory_of lthy; - val {descr as dt_descr, sorts, ...} = dt_info; val fv_names = prefix_dt_names dt_descr sorts "fv_" - val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; + val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr; val fv_frees = map Free (fv_names ~~ fv_types); + (* free variables for the bn-functions *) val (bn_fvbn, fv_bn_names, fv_bn_eqs) = fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; + val fv_bns = map snd bn_fvbn; val fv_nums = 0 upto (length fv_frees - 1) diff -r 13da60487112 -r f2f427bc4fd1 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/NewParser.thy Tue May 04 16:33:30 2010 +0200 @@ -350,31 +350,45 @@ 29) prove supp = fv *} +ML {* +(* for testing porposes - to exit the procedure early *) +exception TEST of Proof.context + +val STEPS = 10 +*} ML {* fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = let (* definition of the raw datatype and raw bn-functions *) val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = - raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + else raise TEST lthy val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) + val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; - val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; - val inject = flat (map #inject dtinfos); - val distincts = flat (map #distinct dtinfos); - val rel_dtinfos = List.take (dtinfos, (length dts)); - val rel_distinct = map #distinct rel_dtinfos; - val induct = #induct dtinfo; - val exhausts = map #exhaust dtinfos; + + (* what is the difference between raw_dt_names and all_full_tnames ? *) + (* what is the purpose of dtinfo and dtinfos ? *) + val _ = tracing ("raw_dt_names " ^ commas raw_dt_names) + val _ = tracing ("all_full_tnames " ^ commas all_full_tnames) + + val inject_thms = flat (map #inject dtinfos); + val distinct_thms = flat (map #distinct dtinfos); + val rel_dtinfos = List.take (dtinfos, (length dts)); + val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) + val induct_thm = #induct dtinfo; + val exhaust_thms = map #exhaust dtinfos; (* definitions of raw permutations *) val ((raw_perm_def, raw_perm_simps, perms), lthy2) = - Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; + if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 + else raise TEST lthy1 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); @@ -388,11 +402,18 @@ val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; (* definition of raw fv_functions *) - val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; + val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) + val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls) + val ((fv, fvbn), fv_def, lthy3a) = + if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 + else raise TEST lthy3 + (* definition of raw alphas *) val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = - define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; + if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a + else raise TEST lthy3a + val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); @@ -405,27 +426,27 @@ ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) (* definition of raw_alpha_eq_iff lemmas *) - val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 + val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); (* proving equivariance lemmas *) val _ = warning "Proving equivariance"; - val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 - val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 + val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 + val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; - (* provind alpha equivalence *) + (* proving alpha equivalence *) val _ = warning "Proving equivalence"; val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6; + val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6; val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy6) alpha_ts else build_equivps alpha_ts reflps alpha_induct - inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6; + inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names @@ -455,7 +476,7 @@ (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else - let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; + let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] alpha_bn_rsp_tac) alpha_ts_bn lthy11 fun const_rsp_tac _ = @@ -480,7 +501,7 @@ fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; - val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); + val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); fun note_simp_suffix s th ctxt = @@ -529,7 +550,7 @@ val lthy23 = note_suffix "supp" q_supp lthy22; in (0, lthy23) -end +end handle TEST ctxt => (0, ctxt) *} section {* Preparing and parsing of the specification *} @@ -698,7 +719,7 @@ (main_parser >> nominal_datatype2_cmd) *} - +(* atom_decl name nominal_datatype lam = @@ -715,6 +736,10 @@ "bn (P1 x) = {atom x}" | "bn (P2 p1 p2) = bn p1 \ bn p2" +find_theorems Var_raw + + + thm lam_pt.bn thm lam_pt.fv[simplified lam_pt.supp(1-2)] thm lam_pt.eq_iff diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Perm.thy --- a/Nominal/Perm.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/Perm.thy Tue May 04 16:33:30 2010 +0200 @@ -116,9 +116,8 @@ user_dt_nos refers to the number of "un-unfolded" datatypes given by the user *) -fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos thy = +fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = let - val {descr as dt_descr, induct, sorts, ...} = dt_info; val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; val user_full_tnames = List.take (all_full_tnames, user_dt_nos); @@ -138,8 +137,8 @@ Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; - val perm_zero_thms = prove_permute_zero lthy' induct perm_eq_thms perm_funs - val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs + val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs + val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) val perms_name = space_implode "_" perm_fn_names diff -r 13da60487112 -r f2f427bc4fd1 Nominal/Tacs.thy --- a/Nominal/Tacs.thy Tue May 04 16:30:31 2010 +0200 +++ b/Nominal/Tacs.thy Tue May 04 16:33:30 2010 +0200 @@ -158,9 +158,9 @@ *} ML {* -fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free" +fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free" | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic" - | dtyp_no_of_typ dts (Type (tname, Ts)) = + | dtyp_no_of_typ dts (Type (tname, _)) = case try (find_index (curry op = tname o fst)) dts of NONE => error "dtyp_no_of_typ: Illegal recursion" | SOME i => i diff -r 13da60487112 -r f2f427bc4fd1 TODO --- a/TODO Tue May 04 16:30:31 2010 +0200 +++ b/TODO Tue May 04 16:33:30 2010 +0200 @@ -14,6 +14,7 @@ - types of bindings match types of binding functions - fsets are not bound in lst bindings - bound arguments are not datatypes +- binder is referred to by name and not by type Smaller things: