# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273855243 -3600
# Node ID 2fc55508a6d0846950cf350c5f5150f6f9c40f4d
# Parent  ac3d4e4f5cbeca2407cc733b19e9bb7ad3928439
polished example

diff -r ac3d4e4f5cbe -r 2fc55508a6d0 Nominal/Ex/SingleLetFoo.thy
--- a/Nominal/Ex/SingleLetFoo.thy	Fri May 14 15:21:05 2010 +0100
+++ b/Nominal/Ex/SingleLetFoo.thy	Fri May 14 17:40:43 2010 +0100
@@ -31,35 +31,8 @@
 thm permute_trm_raw_permute_assg_raw.simps
 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]
 
-(* there is something wrong with the free variables *)
-
-text {*
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-*}
 
-inductive 
-  alpha_trm_raw and alpha_assg_raw and alpha_bn_raw
-where
-  "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
-| "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
-  \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
-| "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
-   alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
-| "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa);
-    alpha_bn_raw assg_raw assg_rawa\<rbrakk>
-    \<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)"
-| "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
-        (bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa);
-   alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk>
-   \<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)"
-| "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
-        ({atom namea} \<union> bn_raw assg_rawa, trm_rawa);
-   alpha_bn_raw assg_raw assg_rawa\<rbrakk>
-   \<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)"
-
-| "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk>
-  \<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
-| "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
 
 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
 
@@ -99,6 +72,7 @@
   shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
 using assms
 apply(simp add: supp_at_base)
+done
 
 
 end