--- a/Nominal/Ex/Classical.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Classical.thy Wed Dec 22 09:13:25 2010 +0000
@@ -2,7 +2,7 @@
imports "../Nominal2"
begin
-(* example from my Urban's PhD *)
+(* example from Urban's PhD *)
atom_decl name
atom_decl coname
@@ -19,12 +19,16 @@
thm trm.distinct
thm trm.induct
thm trm.exhaust
+thm trm.strong_exhaust
+thm trm.strong_exhaust[simplified]
thm trm.fv_defs
thm trm.bn_defs
thm trm.perm_simps
thm trm.eq_iff
thm trm.fv_bn_eqvt
thm trm.size_eqvt
+thm trm.supp
+thm trm.supp[simplified]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CoreHaskell2.thy Wed Dec 22 09:13:25 2010 +0000
@@ -0,0 +1,79 @@
+theory CoreHaskell2
+imports "../Nominal2"
+begin
+
+(* Core Haskell by John Matthews *)
+
+atom_decl var
+atom_decl cvar
+atom_decl tvar
+
+
+nominal_datatype kinds:
+ Kind =
+ Klifted
+ | Kunlifted
+ | Kopen
+ | Karrow Kind Kind
+ | Keq Ty Ty
+and Ty =
+ Tvar tvar
+ | Tcon string
+ | Tapp Ty Ty
+ | Tforall pb::PBind ty::Ty bind "bind_pb pb" in ty
+and PBind =
+ Pbind tvar Kind
+binder
+ bind_pb
+where
+ "bind_pb (Pbind tv k) = [atom tv]"
+
+nominal_datatype expressions:
+ Bind =
+ Vb var Ty
+ | Tb tvar Kind
+and Exp =
+ Var var
+ | Dcon string
+ | App Exp Exp
+ | Appt Exp Ty
+ | Lam b::Bind e::Exp bind "bind_b b" in e
+binder
+ bind_b
+where
+ "bind_b (Vb v ty) = [atom v]"
+| "bind_b (Tb tv kind) = [atom tv]"
+
+thm kinds.distinct
+thm kinds.induct
+thm kinds.inducts
+thm kinds.exhaust
+thm kinds.strong_exhaust
+thm kinds.fv_defs
+thm kinds.bn_defs
+thm kinds.perm_simps
+thm kinds.eq_iff
+thm kinds.fv_bn_eqvt
+thm kinds.size_eqvt
+thm kinds.supports
+thm kinds.fsupp
+thm kinds.supp
+thm kinds.fresh
+
+thm expressions.distinct
+thm expressions.induct
+thm expressions.inducts
+thm expressions.exhaust
+thm expressions.fv_defs
+thm expressions.bn_defs
+thm expressions.perm_simps
+thm expressions.eq_iff
+thm expressions.fv_bn_eqvt
+thm expressions.size_eqvt
+thm expressions.supports
+thm expressions.fsupp
+thm expressions.supp
+thm expressions.fresh
+
+end
+
--- a/Nominal/Ex/Datatypes.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy Wed Dec 22 09:13:25 2010 +0000
@@ -17,6 +17,7 @@
thm Maybe.distinct
thm Maybe.induct
thm Maybe.exhaust
+thm Maybe.strong_exhaust
thm Maybe.fv_defs
thm Maybe.bn_defs
thm Maybe.perm_simps
@@ -27,6 +28,9 @@
(*
using a datatype inside a nominal_datatype
+
+ the datatype needs to be shown to be an instance
+ of the pure class (this is usually trivial)
*)
atom_decl name
@@ -55,6 +59,7 @@
thm baz.distinct
thm baz.induct
thm baz.exhaust
+thm baz.strong_exhaust
thm baz.fv_defs
thm baz.bn_defs
thm baz.perm_simps
--- a/Nominal/Ex/LF.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/LF.thy Wed Dec 22 09:13:25 2010 +0000
@@ -2,25 +2,40 @@
imports "../Nominal2"
begin
-declare [[STEPS = 100]]
-
atom_decl name
atom_decl ident
-nominal_datatype kind =
- Type
- | KPi "ty" n::"name" k::"kind" bind n in k
+nominal_datatype lf:
+ kind =
+ Type
+ | KPi "ty" n::"name" k::"kind" bind n in k
and ty =
- TConst "ident"
- | TApp "ty" "trm"
- | TPi "ty" n::"name" ty::"ty" bind n in ty
+ TConst "ident"
+ | TApp "ty" "trm"
+ | TPi "ty" n::"name" ty::"ty" bind n in ty
and trm =
- Const "ident"
- | Var "name"
- | App "trm" "trm"
- | Lam "ty" n::"name" t::"trm" bind n in t
+ Const "ident"
+ | Var "name"
+ | App "trm" "trm"
+ | Lam "ty" n::"name" t::"trm" bind n in t
-(*thm kind_ty_trm.supp*)
+thm lf.distinct
+thm lf.induct
+thm lf.inducts
+thm lf.exhaust
+thm lf.strong_exhaust
+thm lf.fv_defs
+thm lf.bn_defs
+thm lf.perm_simps
+thm lf.eq_iff
+thm lf.fv_bn_eqvt
+thm lf.size_eqvt
+thm lf.supports
+thm lf.fsupp
+thm lf.supp
+thm lf.fresh
+thm lf.fresh[simplified]
+
end
--- a/Nominal/Ex/Lambda.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Lambda.thy Wed Dec 22 09:13:25 2010 +0000
@@ -3,7 +3,6 @@
begin
atom_decl name
-declare [[STEPS = 100]]
nominal_datatype lam =
Var "name"
@@ -12,53 +11,27 @@
thm lam.distinct
thm lam.induct
-thm lam.exhaust
+thm lam.exhaust lam.strong_exhaust
thm lam.fv_defs
thm lam.bn_defs
thm lam.perm_simps
thm lam.eq_iff
-thm lam.eq_iff[folded alphas]
thm lam.fv_bn_eqvt
thm lam.size_eqvt
-section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *}
-
-lemma strong_exhaust:
- fixes c::"'a::fs"
- assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P"
- and "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P"
- and "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="y" in lam.exhaust)
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(rule assms(3))
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(rule at_set_avoiding2_atom)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: lam.fresh)
-done
+section {* Strong Induction Lemma via Induct_schema *}
lemma strong_induct:
fixes c::"'a::fs"
assumes a1: "\<And>name c. P c (Var name)"
and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
- and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+ and a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
shows "P c lam"
using assms
apply(induction_schema)
-apply(rule_tac y="lam" in strong_exhaust)
+apply(rule_tac y="lam" in lam.strong_exhaust)
apply(blast)
apply(blast)
apply(blast)
@@ -66,99 +39,6 @@
apply(simp_all add: lam.size)
done
-section {* Strong Induction Principles*}
-
-(*
- Old way of establishing strong induction
- principles by chosing a fresh name.
-*)
-(*
-lemma
- fixes c::"'a::fs"
- assumes a1: "\<And>name c. P c (Var name)"
- and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
- and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
- shows "P c lam"
-proof -
- have "\<And>p. P c (p \<bullet> lam)"
- apply(induct lam arbitrary: c rule: lam.induct)
- apply(perm_simp)
- apply(rule a1)
- apply(perm_simp)
- apply(rule a2)
- apply(assumption)
- apply(assumption)
- apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
- defer
- apply(simp add: fresh_def)
- apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
- apply(simp add: supp_Pair finite_supp)
- apply(blast)
- apply(erule exE)
- apply(rule_tac t="p \<bullet> Lam name lam" and
- s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
- apply(simp del: lam.perm)
- apply(subst lam.perm)
- apply(subst (2) lam.perm)
- apply(rule flip_fresh_fresh)
- apply(simp add: fresh_def)
- apply(simp only: supp_fn')
- apply(simp)
- apply(simp add: fresh_Pair)
- apply(simp)
- apply(rule a3)
- apply(simp add: fresh_Pair)
- apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
- apply(simp)
- done
- then have "P c (0 \<bullet> lam)" by blast
- then show "P c lam" by simp
-qed
-*)
-(*
- New way of establishing strong induction
- principles by using a appropriate permutation.
-*)
-(*
-lemma
- fixes c::"'a::fs"
- assumes a1: "\<And>name c. P c (Var name)"
- and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
- and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
- shows "P c lam"
-proof -
- have "\<And>p. P c (p \<bullet> lam)"
- apply(induct lam arbitrary: c rule: lam.induct)
- apply(perm_simp)
- apply(rule a1)
- apply(perm_simp)
- apply(rule a2)
- apply(assumption)
- apply(assumption)
- apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
- apply(erule exE)
- apply(rule_tac t="p \<bullet> Lam name lam" and
- s="q \<bullet> p \<bullet> Lam name lam" in subst)
- defer
- apply(simp)
- apply(rule a3)
- apply(simp add: eqvts fresh_star_def)
- apply(drule_tac x="q + p" in meta_spec)
- apply(simp)
- apply(rule at_set_avoiding2)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- apply(perm_simp)
- apply(simp add: fresh_star_def fresh_def supp_fn')
- apply(rule supp_perm_eq)
- apply(simp)
- done
- then have "P c (0 \<bullet> lam)" by blast
- then show "P c lam" by simp
-qed
-*)
-
section {* Typing *}
nominal_datatype ty =
--- a/Nominal/Ex/Let.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Let.thy Wed Dec 22 09:13:25 2010 +0000
@@ -18,7 +18,6 @@
"bn ANil = []"
| "bn (ACons x t as) = (atom x) # (bn as)"
-thm at_set_avoiding2
thm trm_assn.fv_defs
thm trm_assn.eq_iff
thm trm_assn.bn_defs
@@ -28,28 +27,8 @@
thm trm_assn.distinct
thm trm_assn.supp
thm trm_assn.fresh
-thm trm_assn.exhaust[where y="t", no_vars]
-
-lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
-
-lemma uu:
- shows "alpha_bn as (permute_bn p as)"
-apply(induct as rule: trm_assn.inducts(2))
-apply(auto)[4]
-apply(simp add: permute_bn)
-apply(simp add: trm_assn.eq_iff)
-apply(simp add: permute_bn)
-apply(simp add: trm_assn.eq_iff)
-done
-
-lemma tt:
- shows "(p \<bullet> bn as) = bn (permute_bn p as)"
-apply(induct as rule: trm_assn.inducts(2))
-apply(auto)[4]
-apply(simp add: permute_bn trm_assn.bn_defs)
-apply(simp add: permute_bn trm_assn.bn_defs)
-apply(simp add: atom_eqvt)
-done
+thm trm_assn.exhaust
+thm trm_assn.strong_exhaust
lemma strong_exhaust1:
fixes c::"'a::fs"
@@ -58,41 +37,18 @@
and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
shows "P"
-apply(rule_tac y="y" in trm_assn.exhaust(1))
+apply(rule_tac y="y" in trm_assn.strong_exhaust(1))
apply(rule assms(1))
apply(assumption)
apply(rule assms(2))
apply(assumption)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
apply(rule assms(3))
-apply(perm_simp)
+apply(assumption)
apply(assumption)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(simp add: set_eqvt)
-apply(subst (asm) tt)
-apply(rule_tac assms(4))
-apply(simp)
-apply(simp add: trm_assn.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt uu)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-done
+apply(rule assms(4))
+apply(assumption)
+apply(assumption)
+sorry
lemma strong_exhaust2:
--- a/Nominal/Ex/SystemFOmega.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/SystemFOmega.thy Wed Dec 22 09:13:25 2010 +0000
@@ -18,9 +18,9 @@
nominal_datatype ty =
TVar tvar
| TFun ty ty
-| TAll a::tvar kind t::ty bind a in t
-| TEx a::tvar kind t::ty bind a in t
-| TLam a::tvar kind t::ty bind a in t
+| TAll a::tvar kind t::ty bind a in t
+| TEx a::tvar kind t::ty bind a in t
+| TLam a::tvar kind t::ty bind a in t
| TApp ty ty
| TRec trec
and trec =
@@ -29,20 +29,50 @@
nominal_datatype trm =
Var var
-| Lam x::var ty t::trm bind x in t
+| Lam x::var ty t::trm bind x in t
| App trm trm
| Dot trm label
-| LAM a::tvar kind t::trm bind a in t
+| LAM a::tvar kind t::trm bind a in t
| APP trm ty
| Pack ty trm
-| Unpack a::tvar x::var trm t::trm bind a x in t
+| Unpack a::tvar x::var trm t::trm bind a x in t
| Rec rec
and rec =
RNil
| RCons label trm rec
+thm ty_trec.distinct
+thm ty_trec.induct
+thm ty_trec.inducts
+thm ty_trec.exhaust
+thm ty_trec.strong_exhaust
+thm ty_trec.fv_defs
+thm ty_trec.bn_defs
+thm ty_trec.perm_simps
+thm ty_trec.eq_iff
+thm ty_trec.fv_bn_eqvt
+thm ty_trec.size_eqvt
+thm ty_trec.supports
+thm ty_trec.fsupp
+thm ty_trec.supp
+thm ty_trec.fresh
+thm trm_rec.distinct
+thm trm_rec.induct
+thm trm_rec.inducts
+thm trm_rec.exhaust
+thm trm_rec.strong_exhaust
+thm trm_rec.fv_defs
+thm trm_rec.bn_defs
+thm trm_rec.perm_simps
+thm trm_rec.eq_iff
+thm trm_rec.fv_bn_eqvt
+thm trm_rec.size_eqvt
+thm trm_rec.supports
+thm trm_rec.fsupp
+thm trm_rec.supp
+thm trm_rec.fresh
end
--- a/Nominal/Ex/TypeSchemes.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy Wed Dec 22 09:13:25 2010 +0000
@@ -9,8 +9,6 @@
(* defined as a single nominal datatype *)
-thm finite_set
-
nominal_datatype ty =
Var "name"
| Fun "ty" "ty"
@@ -19,7 +17,8 @@
thm ty_tys.distinct
thm ty_tys.induct
-thm ty_tys.exhaust
+thm ty_tys.inducts
+thm ty_tys.exhaust ty_tys.strong_exhaust
thm ty_tys.fv_defs
thm ty_tys.bn_defs
thm ty_tys.perm_simps
@@ -41,7 +40,7 @@
thm tys2.distinct
thm tys2.induct
-thm tys2.exhaust
+thm tys2.exhaust tys2.strong_exhaust
thm tys2.fv_defs
thm tys2.bn_defs
thm tys2.perm_simps
@@ -52,39 +51,13 @@
thm tys2.supp
thm tys2.fresh
-
-lemma strong_exhaust:
- fixes c::"'a::fs"
- assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P"
- shows "P"
-apply(rule_tac y="y" in tys2.exhaust)
-apply(rename_tac names ty2)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q")
-apply(erule exE)
-apply(perm_simp)
-apply(erule conjE)
-apply(rule assms(1))
-apply(assumption)
-apply(clarify)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp)
-apply(simp add: fresh_star_def)
-apply(simp add: tys2.fresh)
-done
-
-
lemma strong_induct:
fixes c::"'a::fs"
assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)"
shows "P c tys"
using assms
apply(induction_schema)
-apply(rule_tac y="tys" in strong_exhaust)
+apply(rule_tac y="tys" in tys2.strong_exhaust)
apply(blast)
apply(relation "measure (\<lambda>(x,y). size y)")
apply(simp_all add: tys2.size)
--- a/Nominal/Ex/TypeVarsTest.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 09:13:25 2010 +0000
@@ -2,6 +2,13 @@
imports "../Nominal2"
begin
+(* a nominal datatype with type variables and sorts *)
+
+
+(* the sort constraints need to be attached to the *)
+(* first occurence of the type variables on the *)
+(* left-hand side *)
+
atom_decl name
class s1
@@ -10,14 +17,20 @@
instance nat :: s1 ..
instance int :: s2 ..
-nominal_datatype ('a, 'b) lam =
+nominal_datatype ('a, 'b, 'c) lam =
Var "name"
-| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
-| Lam x::"name" l::"('a, 'b) lam" bind x in l
+| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
+| Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l
+| Foo "'a" "'b"
+| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l
+
+term Foo
+term Bar
thm lam.distinct
thm lam.induct
-thm lam.exhaust
+thm lam.exhaust
+thm lam.strong_exhaust
thm lam.fv_defs
thm lam.bn_defs
thm lam.perm_simps
--- a/Nominal/Nominal2.thy Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Nominal2.thy Wed Dec 22 09:13:25 2010 +0000
@@ -307,6 +307,7 @@
RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas)
(prems' ~~ bclausesss) exhausts')]
end)
+ |> ProofContext.export lthy'' lthy
end
*}
@@ -847,6 +848,7 @@
||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct])
||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
+ ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
--- a/Nominal/ROOT.ML Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/ROOT.ML Wed Dec 22 09:13:25 2010 +0000
@@ -25,4 +25,5 @@
(*"Ex/Foo1",
"Ex/Foo2",*)
"Ex/CoreHaskell"
+ "Ex/CoreHaskell2"
];