# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273774014 -3600
# Node ID 5111dadd11625c59c9802032fc18a987be0254d6
# Parent  f38adea0591cb6f44944d360b800a8a9e8110426
added a more instructive example - has some problems with fv though

diff -r f38adea0591c -r 5111dadd1162 Nominal/Ex/Ex4.thy
--- a/Nominal/Ex/Ex4.thy	Thu May 13 18:19:48 2010 +0100
+++ b/Nominal/Ex/Ex4.thy	Thu May 13 19:06:54 2010 +0100
@@ -49,11 +49,13 @@
    alpha_f_raw pat_raw pat_rawa\<rbrakk>
    \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)"
 
+(* alpha_pat_raw *)
 | "alpha_pat_raw PN_raw PN_raw"
 | "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)"
 | "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk>
    \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
 
+(* alpha_f_raw *)
 | "alpha_f_raw PN_raw PN_raw"
 | "alpha_f_raw (PS_raw name) (PS_raw namea)"
 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
diff -r f38adea0591c -r 5111dadd1162 Nominal/Ex/SingleLetFoo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/SingleLetFoo.thy	Thu May 13 19:06:54 2010 +0100
@@ -0,0 +1,101 @@
+theory SingleLetFoo
+imports "../NewParser"
+begin
+
+
+declare [[STEPS = 4]]
+(* alpha does not work for this type *)
+
+atom_decl name
+
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind_set x in t
+| Let a::"assg" t::"trm"  bind_set "bn a" in t
+| Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
+| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
+and assg =
+  As "name" "trm"
+binder
+  bn::"assg \<Rightarrow> atom set"
+where
+  "bn (As x t) = {atom x}"
+
+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
+
+lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry
+
+lemma
+  assumes "distinct [x,y, z, u]"
+  shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
+                       (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
+using assms
+apply(rule_tac all)
+apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
+apply(simp only: alphas)
+apply(rule conjI)
+apply(simp)
+apply(simp add: supp_at_base fresh_star_def)
+apply(rule conjI)
+apply(simp add: supp_at_base fresh_star_def)
+apply(rule conjI)
+apply(simp)
+apply(rule all)
+apply(simp)
+unfolding flip_def
+apply(perm_simp add: test)
+unfolding flip_def[symmetric]
+apply(simp)
+apply(subst flip_at_base_simps(3))
+apply(auto)[2]
+apply(simp)
+apply(rule all)
+apply(rule all)
+apply(simp)
+done
+
+lemma
+  assumes "distinct [x,y,z,u]"
+  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)
+
+
+end
+
+
+