--- a/Nominal/Ex/Ex4.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-theory Ex4
-imports "../NewParser"
-begin
-
-declare [[STEPS = 5]]
-
-atom_decl name
-
-nominal_datatype trm =
-  Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm"        bind_set x in t
-| Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
-| Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t
-| Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t
-and pat =
-  PN
-| PS "name"
-| PD "pat" "pat"
-binder
-  f::"pat \<Rightarrow> atom set"
-where
-  "f PN = {}"
-| "f (PS x) = {atom x}"
-| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-
-thm permute_trm_raw_permute_pat_raw.simps
-thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps
-
-thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
-
-(*
-inductive 
- alpha_trm_raw and alpha_pat_raw and alpha_f_raw
-where
-(* alpha_trm_raw *)
-  "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. (f_raw pat_raw, trm_raw2) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a);
-   alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\<rbrakk>
-  \<Longrightarrow> alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)"
-| "\<lbrakk>\<exists>p. (f_raw pat_raw1 \<union> f_raw pat_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \<union> f_raw pat_raw2a, trm_rawa);
-   alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
-   \<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)"
-| "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa);
-   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>
-  \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
-*)
-
-lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros
-
-lemma
-  shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x))
-                       (Foo2_raw y (PS_raw y) (Var_raw y))"
-apply(rule all)
-apply(rule_tac x="(atom x \<rightleftharpoons> atom y)" in exI)
-apply(simp add: alphas)
-apply(simp add: supp_at_base fresh_star_def)
-apply(rule conjI)
-apply(rule all)
-apply(simp)
-apply(perm_simp)
-apply(simp)
-apply(rule all)
-done
-
-
-
-end
-
-
-