--- a/Nominal/Ex/ExNotRsp.thy Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExNotRsp.thy Sun May 09 12:26:10 2010 +0100
@@ -1,46 +1,52 @@
theory ExNotRsp
-imports "../Parser"
+imports "../NewParser"
begin
atom_decl name
-(* example 6 from Terms.thy *)
-
-nominal_datatype trm6 =
- Vr6 "name"
-| Lm6 x::"name" t::"trm6" bind x in t
-| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
+(* this example binds bound names and
+ so is not respectful *)
+(*
+nominal_datatype trm =
+ Vr "name"
+| Lm x::"name" t::"trm" bind x in t
+| Lt left::"trm" right::"trm" bind "bv left" in right
binder
- bv6
+ bv
where
- "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-
-(* example 7 from Terms.thy *)
-nominal_datatype trm7 =
- Vr7 "name"
-| Lm7 l::"name" r::"trm7" bind l in r
-| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
-binder
- bv7
-where
- "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+ "bv (Vr n) = {}"
+| "bv (Lm n t) = {atom n} \<union> bv t"
+| "bv (Lt l r) = bv l \<union> bv r"
*)
-(* example 9 from Terms.thy *)
-nominal_datatype lam9 =
- Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
- Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+(* this example uses "-" in the binding function;
+ at the moment this is unsupported *)
+(*
+nominal_datatype trm' =
+ Vr' "name"
+| Lm' l::"name" r::"trm'" bind l in r
+| Lt' l::"trm'" r::"trm'" bind "bv' l" in r
binder
- bv9
+ bv'
where
- "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
+ "bv' (Vr' n) = {atom n}"
+| "bv' (Lm' n t) = bv' t - {atom n}"
+| "bv' (Lt' l r) = bv' l \<union> bv' r"
+*)
+
+(* this example again binds bound names *)
+(*
+nominal_datatype trm'' =
+ Va'' "name"
+| Lm'' n::"name" l::"trm''" bind n in l
+and bla'' =
+ Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+binder
+ bv''
+where
+ "bv'' (Vm'' x) = {}"
+| "bv'' (Lm'' x b) = {atom x}"
+*)
end