--- a/Nominal-General/Nominal2_Supp.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy Tue May 04 16:18:07 2010 +0200
@@ -539,4 +539,5 @@
using fin
by (simp add: supp_of_fin_sets)
+
end
--- a/Nominal/Equivp.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Equivp.thy Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
theory Equivp
-imports "NewFv" "Tacs" "Rsp" "NewFv"
+imports "NewFv" "Tacs" "Rsp"
begin
ML {*
--- a/Nominal/Ex/Classical.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Classical.thy Tue May 04 16:18:07 2010 +0200
@@ -12,6 +12,10 @@
atom_decl name
atom_decl coname
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+ML {* val _ = cheat_fv_rsp := true *}
+
nominal_datatype trm =
Ax "name" "coname"
| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
--- a/Nominal/Ex/Ex2.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Ex2.thy Tue May 04 16:18:07 2010 +0200
@@ -1,35 +1,31 @@
theory Ex2
-imports "../Parser"
+imports "../NewParser"
begin
text {* example 2 *}
atom_decl name
-ML {* val _ = recursive := false *}
-nominal_datatype trm' =
+nominal_datatype trm =
Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'" bind x in t
-| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t
-and pat' =
+| App "trm" "trm"
+| Lam x::"name" t::"trm" bind_set x in t
+| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
+and pat =
PN
| PS "name"
| PD "name" "name"
binder
- f::"pat' \<Rightarrow> atom set"
+ f::"pat \<Rightarrow> atom set"
where
"f PN = {}"
| "f (PD x y) = {atom x, atom y}"
| "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
+thm trm_pat.bn
+thm trm_pat.perm
+thm trm_pat.induct
+thm trm_pat.distinct
+thm trm_pat.fv[simplified trm_pat.supp(1-2)]
end
--- a/Nominal/Ex/Ex3.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Ex3.thy Tue May 04 16:18:07 2010 +0200
@@ -1,35 +1,34 @@
theory Ex3
-imports "../Parser"
+imports "../NewParser"
begin
(* Example 3, identical to example 1 from Terms.thy *)
atom_decl name
-ML {* val _ = recursive := false *}
-nominal_datatype trm0 =
- Var0 "name"
-| App0 "trm0" "trm0"
-| Lam0 x::"name" t::"trm0" bind x in t
-| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t
-and pat0 =
- PN0
-| PS0 "name"
-| PD0 "pat0" "pat0"
+nominal_datatype trm =
+ Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm" bind_set x in t
+| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
+and pat =
+ PN
+| PS "name"
+| PD "pat" "pat"
binder
- f0::"pat0 \<Rightarrow> atom set"
+ f::"pat \<Rightarrow> atom set"
where
- "f0 PN0 = {}"
-| "f0 (PS0 x) = {atom x}"
-| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+ "f PN = {}"
+| "f (PS x) = {atom x}"
+| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-thm trm0_pat0.fv
-thm trm0_pat0.eq_iff
-thm trm0_pat0.bn
-thm trm0_pat0.perm
-thm trm0_pat0.induct
-thm trm0_pat0.distinct
-thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
+thm trm_pat.fv
+thm trm_pat.eq_iff
+thm trm_pat.bn
+thm trm_pat.perm
+thm trm_pat.induct
+thm trm_pat.distinct
+thm trm_pat.fv[simplified trm_pat.supp(1-2)]
end
--- a/Nominal/Ex/ExCoreHaskell.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy Tue May 04 16:18:07 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/ExLeroy.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLeroy.thy Tue May 04 16:18:07 2010 +0200
@@ -1,21 +1,20 @@
theory ExLeroy
-imports "../Parser"
+imports "../NewParser"
begin
(* example form Leroy 96 about modules; OTT *)
atom_decl name
-ML {* val _ = recursive := false *}
nominal_datatype mexp =
Acc "path"
| Stru "body"
-| Funct x::"name" "sexp" m::"mexp" bind x in m
+| Funct x::"name" "sexp" m::"mexp" bind_set x in m
| FApp "mexp" "path"
| Ascr "mexp" "sexp"
and body =
Empty
-| Seq c::defn d::"body" bind "cbinders c" in d
+| Seq c::defn d::"body" bind_set "cbinders c" in d
and defn =
Type "name" "tyty"
| Dty "name"
@@ -26,7 +25,7 @@
| SFunc "name" "sexp" "sexp"
and sbody =
SEmpty
-| SSeq C::spec D::sbody bind "Cbinders C" in D
+| SSeq C::spec D::sbody bind_set "Cbinders C" in D
and spec =
Type1 "name"
| Type2 "name" "tyty"
@@ -42,7 +41,7 @@
and trmtrm =
Tref1 "name"
| Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm" bind v in M
+| Lam' v::"name" "tyty" M::"trmtrm" bind_set v in M
| App' "trmtrm" "trmtrm"
| Let' "body" "trmtrm"
binder
@@ -65,8 +64,8 @@
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
end
--- a/Nominal/Ex/ExLet.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLet.thy Tue May 04 16:18:07 2010 +0200
@@ -1,17 +1,15 @@
theory ExLet
-imports "../Parser" "../../Attic/Prove"
+imports "../NewParser" "../../Attic/Prove"
begin
text {* example 3 or example 5 from Terms.thy *}
atom_decl name
-ML {* val _ = recursive := false *}
-ML {* val _ = alpha_type := AlphaLst *}
nominal_datatype trm =
Vr "name"
| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind x in t
+| Lm x::"name" t::"trm" bind_set x in t
| Lt a::"lts" t::"trm" bind "bn a" in t
(*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*)
and lts =
@@ -52,11 +50,10 @@
apply simp
apply clarify
apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+ apply (rule TrueI)+
apply simp_all
- apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
- apply simp
- apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
- apply simp
+ apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+ apply simp_all
done
lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
@@ -64,8 +61,8 @@
lemma permute_bn_zero:
"permute_bn 0 a = a"
apply(induct a rule: trm_lts.inducts(2))
- apply(rule TrueI)
- apply(simp_all add:permute_bn eqvts)
+ apply(rule TrueI)+
+ apply(simp_all add:permute_bn)
done
lemma permute_bn_add:
@@ -74,37 +71,29 @@
lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
apply(induct lts rule: trm_lts.inducts(2))
- apply(rule TrueI)
+ apply(rule TrueI)+
apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
done
lemma perm_bn:
"p \<bullet> bn l = bn(permute_bn p l)"
apply(induct l rule: trm_lts.inducts(2))
- apply(rule TrueI)
+ apply(rule TrueI)+
apply(simp_all add:permute_bn eqvts)
done
lemma fv_perm_bn:
"fv_bn l = fv_bn (permute_bn p l)"
apply(induct l rule: trm_lts.inducts(2))
- apply(rule TrueI)
+ apply(rule TrueI)+
apply(simp_all add:permute_bn eqvts)
done
-lemma fv_fv_bn:
- "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
- apply(induct l rule: trm_lts.inducts(2))
- apply(rule TrueI)
- apply(simp_all add:permute_bn eqvts)
- by blast
-
lemma Lt_subst:
"supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
- apply (simp only: trm_lts.eq_iff)
+ apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
apply (rule_tac x="q" in exI)
apply (simp add: alphas)
- apply (simp add: permute_bn_alpha_bn)
apply (simp add: perm_bn[symmetric])
apply (simp add: eqvts[symmetric])
apply (simp add: supp_abs)
@@ -204,8 +193,7 @@
"(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
apply (simp add: trm_lts.eq_iff)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alphas)
- apply (simp add: fresh_star_def eqvts)
+ apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
done
lemma lets_ok3:
--- a/Nominal/Ex/ExLetRec.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
theory ExLetRec
-imports "../Parser"
+imports "../NewParser"
begin
@@ -7,13 +7,11 @@
atom_decl name
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
nominal_datatype trm =
Vr "name"
| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind x in t
-| Lt a::"lts" t::"trm" bind "bn a" in t
+| Lm x::"name" t::"trm" bind_set x in t
+| Lt a::"lts" t::"trm" bind "bn a" in a t
and lts =
Lnil
| Lcons "name" "trm" "lts"
@@ -38,13 +36,13 @@
lemma lets_bla:
"x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
- by (simp add: trm_lts.eq_iff alphas2 set_sub)
+ by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base)
lemma lets_ok:
"(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
apply (simp add: trm_lts.eq_iff)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alphas2 fresh_star_def eqvts)
+ apply (simp_all add: alphas2 fresh_star_def eqvts supp_at_base)
done
lemma lets_ok3:
@@ -72,7 +70,7 @@
lemma lets_ok4:
"(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
(Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
- apply (simp add: alphas trm_lts.eq_iff)
+ apply (simp add: alphas trm_lts.eq_iff supp_at_base)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp add: atom_eqvt fresh_star_def)
done
--- a/Nominal/Ex/ExPS7.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy Tue May 04 16:18:07 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 =
--- a/Nominal/Ex/Lambda.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
theory Lambda
-imports "../Parser"
+imports "../NewParser"
begin
atom_decl name
@@ -7,7 +7,7 @@
nominal_datatype lam =
Var "name"
| App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l
+| Lam x::"name" l::"lam" bind_set x in l
thm lam.fv
thm lam.supp
@@ -17,7 +17,7 @@
section {* Strong Induction Principles*}
-(*
+(*
Old way of establishing strong induction
principles by chosing a fresh name.
*)
--- a/Nominal/Ex/SingleLet.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy Tue May 04 16:18:07 2010 +0200
@@ -1,16 +1,14 @@
theory SingleLet
-imports "../Parser"
+imports "../NewParser"
begin
atom_decl name
-ML {* val _ = recursive := false *}
-
nominal_datatype trm =
Var "name"
| App "trm" "trm"
-| Lam x::"name" t::"trm" bind x in t
-| Let a::"assg" t::"trm" bind "bn a" in t
+| Lam x::"name" t::"trm" bind_set x in t
+| Let a::"assg" t::"trm" bind_set "bn a" in t
and assg =
As "name" "trm"
binder
@@ -18,19 +16,23 @@
where
"bn (As x t) = {atom x}"
-print_theorems
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
thm trm_assg.fv
thm trm_assg.supp
-thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+thm trm_assg.eq_iff
thm trm_assg.bn
thm trm_assg.perm
thm trm_assg.induct
thm trm_assg.inducts
thm trm_assg.distinct
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-thm trm_assg.fv[simplified trm_assg.supp]
+thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+
+(*
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+declare permute_trm_raw_permute_assg_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_trm_raw
+*)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Term8.thy Tue May 04 16:18:07 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:17:46 2010 +0200
+++ b/Nominal/Ex/Test.thy Tue May 04 16:18:07 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/Ex/TypeSchemes.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy Tue May 04 16:18:07 2010 +0200
@@ -1,18 +1,16 @@
theory TypeSchemes
-imports "../Parser"
+imports "../NewParser"
begin
section {*** Type Schemes ***}
atom_decl name
-ML {* val _ = alpha_type := AlphaRes *}
-
nominal_datatype ty =
Var "name"
| Fun "ty" "ty"
and tys =
- All xs::"name fset" ty::"ty" bind xs in ty
+ All xs::"name fset" ty::"ty" bind_res xs in ty
lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
@@ -125,21 +123,21 @@
apply(simp add: ty_tys.eq_iff)
apply(rule_tac x="0::perm" in exI)
apply(simp add: alphas)
- apply(simp add: fresh_star_def fresh_zero_perm)
+ apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
done
lemma
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
apply(simp add: ty_tys.eq_iff)
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alphas fresh_star_def eqvts)
+ apply(simp add: alphas fresh_star_def eqvts supp_at_base)
done
lemma
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
apply(simp add: ty_tys.eq_iff)
apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+ apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
done
lemma
@@ -148,7 +146,7 @@
using a
apply(simp add: ty_tys.eq_iff)
apply(clarify)
- apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+ apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
apply auto
done
--- a/Nominal/Fv.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Fv.thy Tue May 04 16:18:07 2010 +0200
@@ -650,4 +650,29 @@
end
*}
+
+ML {*
+fun define_fv_alpha_export dt binds bns ctxt =
+let
+ val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
+ define_fv dt binds bns ctxt;
+ val (alpha, ctxt'') =
+ define_alpha dt binds bns fv_ts_loc ctxt';
+ val alpha_ts_loc = #preds alpha
+ val alpha_induct_loc = #induct alpha
+ val alpha_intros_loc = #intrs alpha;
+ val alpha_cases_loc = #elims alpha
+ val morphism = ProofContext.export_morphism ctxt'' ctxt;
+ val fv_ts = map (Morphism.term morphism) fv_ts_loc;
+ val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
+ val fv_def = Morphism.fact morphism fv_def_loc;
+ val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
+ val alpha_induct = Morphism.thm morphism alpha_induct_loc;
+ val alpha_intros = Morphism.fact morphism alpha_intros_loc
+ val alpha_cases = Morphism.fact morphism alpha_cases_loc
+in
+ ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
+end;
+*}
+
end
--- a/Nominal/Lift.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Lift.thy Tue May 04 16:18:07 2010 +0200
@@ -1,8 +1,8 @@
theory Lift
-imports "../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv"
+imports "../Nominal-General/Nominal2_Atoms"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Abs" "Perm" "Equivp" "Rsp"
begin
@@ -66,32 +66,5 @@
end
*}
-
-
-
-ML {*
-fun define_fv_alpha_export dt binds bns ctxt =
-let
- val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
- define_fv dt binds bns ctxt;
- val (alpha, ctxt'') =
- define_alpha dt binds bns fv_ts_loc ctxt';
- val alpha_ts_loc = #preds alpha
- val alpha_induct_loc = #induct alpha
- val alpha_intros_loc = #intrs alpha;
- val alpha_cases_loc = #elims alpha
- val morphism = ProofContext.export_morphism ctxt'' ctxt;
- val fv_ts = map (Morphism.term morphism) fv_ts_loc;
- val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
- val fv_def = Morphism.fact morphism fv_def_loc;
- val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
- val alpha_induct = Morphism.thm morphism alpha_induct_loc;
- val alpha_intros = Morphism.fact morphism alpha_intros_loc
- val alpha_cases = Morphism.fact morphism alpha_cases_loc
-in
- ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
-end;
-*}
-
end
--- a/Nominal/NewFv.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/NewFv.thy Tue May 04 16:18:07 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:17:46 2010 +0200
+++ b/Nominal/NewParser.thy Tue May 04 16:18:07 2010 +0200
@@ -159,8 +159,9 @@
end
*}
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+ append of elements and returns those elements together with bn functions
+ applied *)
ML {*
fun strip_bn_fun t =
case t of
@@ -258,6 +259,31 @@
end
*}
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+ val thy = ProofContext.theory_of ctxt
+ val ty = domain_type (fastype_of rel)
+ val cty = ctyp_of thy ty
+ val ct = cterm_of thy rel
+in
+ Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_equivp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_supp_eq = Unsynchronized.ref false *}
+
+ML {*
+fun remove_loop t =
+ let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
+ handle TERM _ => @{thm eqTrueI} OF [t]
+*}
text {*
nominal_datatype2 does the following things in order:
@@ -324,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 => typ_of_dtyp descr sorts (DtRec i)) (map fst 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);
@@ -362,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);
@@ -379,22 +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
- fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+ 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 lthy6;
+ val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
val alpha_equivp =
- build_equivps alpha_ts reflps alpha_induct
- inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+ if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+ else build_equivps alpha_ts reflps alpha_induct
+ 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
@@ -403,8 +455,8 @@
val raw_consts =
flat (map (fn (i, (_, _, l)) =>
map (fn (cname, dts) =>
- Const (cname, map (typ_of_dtyp descr sorts) dts --->
- typ_of_dtyp descr sorts (DtRec i))) l) descr);
+ Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
val _ = warning "Proving respects";
val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -412,8 +464,9 @@
fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
resolve_tac bns_rsp_pre' 1)) bns lthy8;
val bns_rsp = flat (map snd bns_rsp_pre);
- (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
- fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+
+ fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+ else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
val (fv_rsp_pre, lthy10) = fold_map
(fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -421,11 +474,14 @@
val fv_rsp = flat (map snd fv_rsp_pre);
val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
(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 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]
- (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+ alpha_bn_rsp_tac) alpha_ts_bn lthy11
fun const_rsp_tac _ =
- let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
- in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+ let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+ in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
const_rsp_tac) raw_consts lthy11a
val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
@@ -445,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 =
@@ -463,7 +519,7 @@
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
- val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+ val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
@@ -487,11 +543,14 @@
val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
val (names, supp_eq_t) = supp_eq fv_alpha_all;
val _ = warning "Support Equations";
- val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+ fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
+ supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
+ val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
+ let val _ = warning ("Support eqs failed") in [] end;
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 *}
@@ -660,6 +719,7 @@
(main_parser >> nominal_datatype2_cmd)
*}
+(*
atom_decl name
nominal_datatype lam =
@@ -676,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
@@ -740,7 +804,7 @@
thm ty_tys.fv[simplified ty_tys.supp]
thm ty_tys.eq_iff
-
+*)
(* some further tests *)
--- a/Nominal/Parser.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Parser.thy Tue May 04 16:18:07 2010 +0200
@@ -1,8 +1,8 @@
theory Parser
-imports "../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
- "Perm" "Equivp" "Rsp" "Lift"
+imports "../Nominal-General/Nominal2_Atoms"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Perm" "Equivp" "Rsp" "Lift" "Fv"
begin
section{* Interface for nominal_datatype *}
@@ -372,9 +372,9 @@
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
val {descr, sorts, ...} = dtinfo;
- fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+ fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);
val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
- val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst 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 dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
val rel_dtinfos = List.take (dtinfos, (length dts));
@@ -423,8 +423,8 @@
val raw_consts =
flat (map (fn (i, (_, _, l)) =>
map (fn (cname, dts) =>
- Const (cname, map (typ_of_dtyp descr sorts) dts --->
- typ_of_dtyp descr sorts (DtRec i))) l) descr);
+ Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
val _ = tracing "Proving respects";
val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -483,7 +483,7 @@
val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = tracing "Lifting eq-iff";
- val _ = map tracing (map PolyML.makestring alpha_eq_iff);
+(* val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
--- a/Nominal/Perm.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Perm.thy Tue May 04 16:18:07 2010 +0200
@@ -32,29 +32,29 @@
permute_fn p arg
- - in case the argument is non-recursive it will build
+ - in case the argument is non-recursive it will return
p o arg
*)
-fun perm_arg permute_fns pi (arg_dty, arg) =
+fun perm_arg permute_fn_frees p (arg_dty, arg) =
if Datatype_Aux.is_rec_type arg_dty
- then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
- else mk_perm pi arg
+ then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
+ else mk_perm p arg
*}
ML {*
-(* equation for permutation function for one constructor;
- i is the index of the correspodning datatype *)
-fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
+(* generates the equation for the permutation function for one constructor;
+ i is the index of the corresponding datatype *)
+fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
let
- val pi = Free ("p", @{typ perm})
+ val p = Free ("p", @{typ perm})
val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
val args = map Free (arg_names ~~ arg_tys)
val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
- val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)
- val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))
+ val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
+ val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
in
(Attrib.empty_binding, eq)
@@ -87,13 +87,13 @@
ML {*
fun prove_permute_plus lthy induct perm_defs perm_fns =
let
- val pi1 = Free ("p", @{typ perm})
- val pi2 = Free ("q", @{typ perm})
+ val p = Free ("p", @{typ perm})
+ val q = Free ("q", @{typ perm})
val perm_types = map (body_type o fastype_of) perm_fns
val perm_indnames = Datatype_Prop.make_tnames perm_types
- fun single_goal ((perm, T), x) = HOLogic.mk_eq
- (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+ fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
+ (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
val goals =
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -113,37 +113,34 @@
(* defines the permutation functions for raw datatypes and
proves that they are instances of pt
- dt_nos refers to the number of "un-unfolded" datatypes
+ user_dt_nos refers to the number of "un-unfolded" datatypes
given by the user
*)
-fun define_raw_perms (dt_info : Datatype_Aux.info) 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 full_tnames = List.take (all_full_tnames, dt_nos);
+ val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
-
- val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-
- val permute_fns = perm_fn_names ~~ perm_types
+ val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
+ val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
fun perm_eq (i, (_, _, constrs)) =
- map (perm_eq_constr dt_descr sorts permute_fns i) constrs;
+ map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
val perm_eqs = maps perm_eq dt_descr;
val lthy =
- Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+ Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
- val ((perm_fns, perm_ldef), lthy') =
+ val ((perm_funs, perm_eq_thms), lthy') =
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_ldef perm_fns
- val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
- val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
- val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
+ 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
val perms_zero_bind = Binding.name (perms_name ^ "_zero")
val perms_plus_bind = Binding.name (perms_name ^ "_plus")
@@ -158,10 +155,14 @@
|> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
|> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
|> Class_Target.prove_instantiation_exit_result morphism tac
- (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
+ (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
end
*}
+
+
+
+
(* permutations for quotient types *)
ML {*
--- a/Nominal/Rsp.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Rsp.thy Tue May 04 16:18:07 2010 +0200
@@ -97,7 +97,7 @@
ML {*
fun alpha_eqvt_tac induct simps ctxt =
rel_indtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps
--- a/Pearl-jv/Paper.thy Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/Paper.thy Tue May 04 16:18:07 2010 +0200
@@ -2,7 +2,8 @@
theory Paper
imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Atoms"
- "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
"../Nominal-General/Atoms"
"LaTeXsugar"
begin
@@ -43,24 +44,22 @@
section {* Introduction *}
text {*
+ The purpose of Nominal Isabelle is to provide a proving infratructure
+ for conveninet reasoning about programming languages. At its core
+ Nominal Isabelle is based on nominal logic by Pitts at al
+ \cite{GabbayPitts02,Pitts03}.
+
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
prover providing a proving infrastructure for convenient reasoning about
- programming languages. It has been used to formalise an equivalence checking
- algorithm for LF \cite{UrbanCheneyBerghofer08},
- Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
- \cite{BengtsonParrow07} and a strong normalisation result for
- cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used
- by Pollack for formalisations in the locally-nameless approach to binding
- \cite{SatoPollack10}.
+ programming languages. At its core Nominal Isabelle is based on the nominal
+ logic work of Pitts et al \cite{GabbayPitts02,Pitts03}. The most basic
+ notion in this work is a sort-respecting permutation operation defined over
+ a countably infinite collection of sorted atoms. The atoms are used for
+ representing variables that might be bound. Multiple sorts are necessary for
+ being able to represent different kinds of variables. For example, in the
+ language Mini-ML there are bound term variables and bound type variables;
+ each kind needs to be represented by a different sort of atoms.
- At its core Nominal Isabelle is based on the nominal logic work of Pitts et
- al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
- sort-respecting permutation operation defined over a countably infinite
- collection of sorted atoms. The atoms are used for representing variables
- that might be bound. Multiple sorts are necessary for being
- able to represent different kinds of variables. For example, in the language
- Mini-ML there are bound term variables and bound type variables; each kind
- needs to be represented by a different sort of atoms.
Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
atoms and sorts are used in the original formulation of the nominal logic work.
@@ -858,9 +857,41 @@
Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
*}
+section {* Support of Finite Sets *}
+
+text {*
+ Sets is one instance of a type that is not generally finitely supported.
+ However, it can be easily derived that finite sets of atoms are finitely
+ supported, because their support can be characterised as:
+
+ \begin{lemma}\label{finatomsets}
+ If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
+ \end{lemma}
+
+ \begin{proof}
+ finite-supp-unique
+ \end{proof}
+
+ More difficult is it to establish that finite sets of finitely
+ supported objects are finitely supported.
+*}
+
+
section {* Induction Principles *}
+text {*
+ While the use of functions as permutation provides us with a unique
+ representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
+ @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has
+ one draw back: it does not come readily with an induction principle.
+ Such an induction principle is handy for deriving properties like
+
+ @{thm [display, indent=10] supp_perm_eq}
+ \noindent
+ However, it is not too difficult to derive an induction principle,
+ given the fact that we allow only permutations with a finite domain.
+*}
section {* Concrete Atom Types *}
@@ -1167,6 +1198,12 @@
HOL-based languages.
*}
+section {* Related Work *}
+
+text {*
+ Add here comparison with old work.
+*}
+
section {* Conclusion *}
--- a/Pearl-jv/ROOT.ML Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/ROOT.ML Tue May 04 16:18:07 2010 +0200
@@ -1,6 +1,7 @@
no_document use_thys ["../Nominal-General/Nominal2_Base",
"../Nominal-General/Nominal2_Atoms",
"../Nominal-General/Nominal2_Eqvt",
+ "../Nominal-General/Nominal2_Supp",
"../Nominal-General/Atoms",
"LaTeXsugar"];
--- a/Pearl-jv/document/root.tex Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/document/root.tex Tue May 04 16:18:07 2010 +0200
@@ -24,28 +24,21 @@
\begin{document}
-\title{Proof Pearl: A New Foundation for Nominal Isabelle}
+\title{Implementing the Nominal Logic Work in Isabelle/HOL}
\author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
\institute{Portland State University \and Technical University of Munich}
\maketitle
\begin{abstract}
Pitts et al introduced a beautiful theory about names and binding based on the
-notions of permutation and support. The engineering challenge is to smoothly
-adapt this theory to a theorem prover environment, in our case Isabelle/HOL.
-We present a formalisation of this work that differs from our earlier approach
-in two important respects: First, instead of representing permutations as
-lists of pairs of atoms, we now use a more abstract representation based on
-functions. Second, whereas the earlier work modeled different sorts of atoms
-using different types, we now introduce a unified atom type that includes all
-sorts of atoms. Interestingly, we allow swappings, that is permutations build from
-two atoms, to be ill-sorted. As a result of these design changes, we can iron
-out inconveniences for the user, considerably simplify proofs and also
-drastically reduce the amount of custom ML-code. Furthermore we can extend the
-capabilities of Nominal Isabelle to deal with variables that carry additional
-information. We end up with a pleasing and formalised theory of permutations
-and support, on which we can build an improved and more powerful version of
-Nominal Isabelle.
+notions of atoms, permutations and support. The engineering challenge
+is to smoothly adapt this theory to a theorem prover environment, in our case
+Isabelle/HOL. We present a formalisation of this work that is based on a
+unified atom type (that includes all sorts of atoms) and that represents
+permutations by bijective functions from atoms to atoms. Interestingly, we
+allow swappings, which are permutations build from two atoms, to be
+ill-sorted. Furthermore we can extend the nominal logic with names that carry
+additional information.
\end{abstract}
% generated text of all theories
--- a/Quotient-Paper/document/root.tex Tue May 04 16:17:46 2010 +0200
+++ b/Quotient-Paper/document/root.tex Tue May 04 16:18:07 2010 +0200
@@ -13,13 +13,15 @@
\begin{document}
-\title{Quotients Revisited}
+\title{Quotients Revisited for Isabelle/HOL}
\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
\institute{$^*$ Technical University of Munich, Germany}
\maketitle
\begin{abstract}
-TBD
+Higher-order logic (HOL) is based on a safe logic kernel, which
+can only be extended by introducing new definitions and new types.
+
\end{abstract}
% generated text of all theories
--- a/TODO Tue May 04 16:17:46 2010 +0200
+++ b/TODO Tue May 04 16:18:07 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: