--- 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 \<union> rfv_tkind_raw tkind_raw2"
-| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> 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 \<union> 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 \<union> (rfv_ty_raw ty_raw - {atom tvar})"
-| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> 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 \<union> 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 \<union> 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 \<union> (rfv_co_raw co_raw - {atom cvar})"
-| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> 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 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> 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 \<union> 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 \<union> 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 \<union> 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 \<union> (rfv_trm_raw trm_raw - {atom tvar})"
-| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) =
- rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})"
-| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw"
-| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})"
-| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2"
-| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) =
- rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))"
-| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw"
-| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> 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 \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> 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 \<union> (rfv_bv_cvs_raw cvars_raw \<union> 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 \<union> 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 \<union> 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 \<union> rfv_bv_cvs_raw cvars_raw"
-| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =
- rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_vars_raw VsNil_raw = {}"
-| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) =
- {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_tvars_raw TvsNil_raw = {}"
-| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) =
- {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)"
-| "rfv_cvars_raw CvsNil_raw = {}"
-| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) =
- {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> 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 \<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
- 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 \<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(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 \<bullet> 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) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (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: 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 \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> 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 \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> 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 \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> 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 \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> 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: "\<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)"
@@ -494,7 +388,7 @@
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 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 \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -534,7 +428,7 @@
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 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 \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -575,7 +469,7 @@
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 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 \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -615,7 +509,7 @@
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 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 \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -656,7 +550,7 @@
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 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 \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
@@ -697,7 +591,7 @@
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 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 \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> 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
--- 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 =
--- /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
+
+
--- 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
--- 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)
--- 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 \<union> 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
--- 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
--- 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
--- 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: