--- a/Nominal/Ex/NoneExamples.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/NoneExamples.thy Wed Dec 22 21:13:44 2010 +0000
@@ -3,7 +3,7 @@
begin
text {*
- This example is not covered by our binding
+ These examples are not covered by our binding
specification.
*}
@@ -25,7 +25,7 @@
*)
text {*
- this example binds bound names and therefore the
+ This example binds bound names and therefore the
fv-function is not respectful - the proof just fails.
*}
@@ -43,7 +43,7 @@
*)
text {*
- this example uses "-" in the binding function;
+ This example uses "-" in the binding function;
at the moment this is unsupported
*}
@@ -61,7 +61,7 @@
*)
text {*
- again this example binds bound names - so not respectful
+ Again this example binds bound names - so is not respectful
*}
(*
@@ -73,10 +73,33 @@
binder
bv :: "trm \<Rightarrow> atom set"
where
- "bv (Vam x) = {}"
+ "bv (Var x) = {}"
| "bv (Lam x b) = {atom x}"
*)
+text {*
+ This example has mal-formed deep recursive binders.
+
+ - Bla1: recursive deep binder used twice
+ - Bla2: deep binder used recursively and non-recursively
+ - Bla3: x used in recursive deep binder and somewhere else
+*}
+
+(*
+nominal_datatype trm =
+ Var "name"
+and bla =
+ App "trm" "trm"
+| Bla1 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1 f, bind "bv f" in s2 f
+| Bla2 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1, bind "bv f" in s2 f
+| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2
+binder
+ bv :: "trm \<Rightarrow> atom list"
+where
+ "bv (Var a) = [atom a]"
+*)
+
+
end
--- a/Nominal/Ex/Shallow.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/Shallow.thy Wed Dec 22 21:13:44 2010 +0000
@@ -15,6 +15,8 @@
| App1 "trm1" "trm1"
| Lam1 xs::"name list" t::"trm1" bind xs in t
+thm trm1.strong_exhaust
+
text {* binding a finite set of names *}
@@ -23,6 +25,7 @@
| App2 "trm2" "trm2"
| Lam2 xs::"name fset" t::"trm2" bind (set) xs in t
+thm trm2.strong_exhaust
text {* restricting a finite set of names *}
@@ -31,6 +34,7 @@
| App3 "trm3" "trm3"
| Lam3 xs::"name fset" t::"trm3" bind (res) xs in t
+thm trm3.strong_exhaust
end
--- a/Nominal/Ex/SingleLet.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy Wed Dec 22 21:13:44 2010 +0000
@@ -22,7 +22,8 @@
thm single_let.distinct
thm single_let.induct
thm single_let.inducts
-thm single_let.exhaust[no_vars]
+thm single_let.exhaust
+thm single_let.strong_exhaust
thm single_let.fv_defs
thm single_let.bn_defs
thm single_let.perm_simps
@@ -34,107 +35,6 @@
thm single_let.supp
thm single_let.fresh
-lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
-
-lemma uu:
- shows "alpha_bn as (permute_bn p as)"
-apply(induct as rule: single_let.inducts(2))
-apply(auto)[7]
-apply(simp add: permute_bn)
-apply(simp add: single_let.eq_iff)
-done
-
-lemma tt:
- shows "(p \<bullet> bn as) = bn (permute_bn p as)"
-apply(induct as rule: single_let.inducts(2))
-apply(auto)[7]
-apply(simp add: permute_bn single_let.bn_defs)
-apply(simp add: atom_eqvt)
-done
-
-lemma Abs_fresh_star':
- fixes x::"'a::fs"
- shows "set bs = as \<Longrightarrow> as \<sharp>* Abs_lst bs x"
- unfolding fresh_star_def
- by(simp_all add: Abs_fresh_iff)
-
-lemma strong_exhaust:
- fixes c::"'a::fs"
- assumes "\<And>name. y = Var name \<Longrightarrow> P"
- and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
- and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>assg trm. \<lbrakk>set (bn assg) \<sharp>* c; y = Let assg trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>name1 name2 trm1 trm2 trm3. \<lbrakk>{atom name1} \<sharp>* c; y = Foo name1 name2 trm1 trm2 trm3\<rbrakk> \<Longrightarrow> P"
- and "\<And>name1 name2 trm. \<lbrakk>{atom name1, atom name2} \<sharp>* c; y = Bar name1 name2 trm\<rbrakk> \<Longrightarrow> P"
- and "\<And>name trm1 trm2. \<lbrakk>{atom name} \<sharp>* c; y = Baz name trm1 trm2\<rbrakk> \<Longrightarrow> P"
- shows "P"
- apply(rule_tac y="y" in single_let.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 ([[atom name]]lst.trm) \<sharp>* q")
- apply(erule exE)
- apply(erule conjE)
- apply(perm_simp)
- apply(rule assms(3))
- apply(assumption)
- apply(drule supp_perm_eq[symmetric])
- apply(simp add: single_let.eq_iff)
- apply(perm_simp)
- apply(rule refl)
- 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')
- apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg))) \<sharp>* (c::'a::fs) \<and> supp ([bn assg]lst.trm) \<sharp>* q")
- apply(erule exE)
- apply(erule conjE)
- apply(perm_simp add: tt)
- apply(rule_tac assms(4))
- apply(assumption)
- apply(drule supp_perm_eq[symmetric])
- apply(simp add: single_let.eq_iff)
- 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)
- apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* (c::'a::fs) \<and>
- supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \<sharp>* q")
- apply(erule exE)
- apply(erule conjE)
- apply(perm_simp add: tt)
- apply(rule_tac assms(5))
- apply(assumption)
- apply(drule supp_perm_eq[symmetric])
- apply(simp add: single_let.eq_iff)
- apply(perm_simp)
- apply(rule refl)
- 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)
- apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* (c::'a::fs) \<and>
- supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \<sharp>* q")
- apply(erule exE)
- apply(erule conjE)
- apply(perm_simp add: tt)
- apply(rule_tac assms(6))
- apply(assumption)
- apply(drule supp_perm_eq[symmetric])
- apply(simp add: single_let.eq_iff)
- apply(perm_simp)
- apply(rule refl)
- apply(rule at_set_avoiding2)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- apply(simp add: finite_supp)
- oops
-
end
--- a/Nominal/Ex/SystemFOmega.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/SystemFOmega.thy Wed Dec 22 21:13:44 2010 +0000
@@ -13,7 +13,8 @@
atom_decl label
nominal_datatype kind =
- \<Omega> | KFun kind kind
+ \<Omega>
+| KFun kind kind
nominal_datatype ty =
TVar tvar
@@ -41,7 +42,6 @@
RNil
| RCons label trm rec
-
thm ty_trec.distinct
thm ty_trec.induct
thm ty_trec.inducts
--- a/Nominal/Ex/TypeSchemes.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy Wed Dec 22 21:13:44 2010 +0000
@@ -6,7 +6,6 @@
atom_decl name
-
(* defined as a single nominal datatype *)
nominal_datatype ty =
--- a/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 21:13:44 2010 +0000
@@ -7,7 +7,7 @@
(* the sort constraints need to be attached to the *)
(* first occurence of the type variables on the *)
-(* left-hand side *)
+(* right-hand side *)
atom_decl name
@@ -22,7 +22,7 @@
| 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
+| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l (* Bar binds a polymorphic atom *)
term Foo
term Bar