145 abbreviation "Var \<equiv> VAR_raw"

   145 abbreviation "Var \<equiv> Var_raw"

   146 abbreviation "App \<equiv> APP_raw"

   146 abbreviation "App \<equiv> App_raw"

   154 (* not_yet_done

   154 (* not_yet_done *)

   155 name = namea \<Longrightarrow> alpha_trm'_raw (Var_raw name) (Var_raw namea)

   155 inductive 

   156 alpha_trm'_raw trm'_raw2 trm'_raw2a \<and> alpha_trm'_raw trm'_raw1 trm'_raw1a \<Longrightarrow>

   156   alpha_trm' :: "trm'_raw \<Rightarrow> trm'_raw \<Rightarrow> bool" and

   157 alpha_trm'_raw (App_raw trm'_raw1 trm'_raw2) (App_raw trm'_raw1a trm'_raw2a)

   157   alpha_pat'  :: "pat'_raw \<Rightarrow> pat'_raw \<Rightarrow> bool" and

   158 \<exists>pi. ({atom name}, trm'_raw) \<approx>gen alpha_trm'_raw fv_trm'_raw pi ({atom namea}, trm'_rawa) \<Longrightarrow>

   158   compat_pat' :: "pat'_raw \<Rightarrow> perm \<Rightarrow> pat'_raw \<Rightarrow> bool"

   159 alpha_trm'_raw (Lam_raw name trm'_raw) (Lam_raw namea trm'_rawa)

   159 where

   160 \<exists>pi. (f_raw pat'_raw,

   160   "name = name' \<Longrightarrow> alpha_trm' (Var name) (Var name')"

   161       trm'_raw2) \<approx>gen alpha_trm'_raw fv_trm'_raw pi (f_raw pat'_rawa, trm'_raw2a) \<and>

   161 | "alpha_trm' t2 t2' \<and> alpha_trm' t1 t1' \<Longrightarrow> alpha_trm' (App t1 t2) (App t1' t2')"

   162      alpha_trm'_raw trm'_raw1 trm'_raw1a \<and>

   162 | "\<exists>pi. ({atom x}, t) \<approx>gen alpha_trm' fv_trm'_raw pi ({atom x'}, t') \<Longrightarrow> alpha_trm' (Lam x t) (Lam x' t')"

   163      (f_raw pat'_raw,

   163 | "\<exists>pi. (f p, t) \<approx>gen alpha_trm' fv_trm'_raw pi (f p', t') \<and> alpha_trm' s s' \<and>

   164       pat'_raw) \<approx>gen alpha_pat'_raw fv_pat'_raw pi (f_raw pat'_rawa, pat'_rawa) \<Longrightarrow>

   164         compat_pat' p pi p' \<Longrightarrow> alpha_trm' (Lett p s t) (Lett p' s' t')"

   165 alpha_trm'_raw (Let_raw pat'_raw trm'_raw1 trm'_raw2) (Let_raw pat'_rawa trm'_raw1a trm'_raw2a)

   165 | "alpha_pat' PN PN"

   166 True \<Longrightarrow> alpha_pat'_raw PN_raw PN_raw

   166 | "name = name' \<Longrightarrow> alpha_pat' (PS name) (PS name')"

   167 name = namea \<Longrightarrow> alpha_pat'_raw (PS_raw name) (PS_raw namea)

   167 | "name2 = name2' \<and> name1 = name1' \<Longrightarrow> alpha_pat' (PD name1 name2) (PD name1' name2')"

   168 name2 = name2a \<and> name1 = name1a \<Longrightarrow> alpha_pat'_raw (PD_raw name1 name2) (PD_raw name1a name2a)

   168 | "compat_pat' PN pi PN"

   169 *)

   169 | "pi \<bullet> x = x' \<Longrightarrow> compat_pat' (PS x) pi (PS x')"

   170 

   170 | "pi \<bullet> p1 = p1' \<and> pi \<bullet> p2 = p2' \<Longrightarrow> compat_pat' (PD p1 p2) pi (PD p1' p2')"

   171 (* compat should be

   171 

   172 compat (PN) pi (PN) == True

   172 lemma

   173 compat (PS x) pi (PS x') == pi o x = x'

   173   assumes a: "distinct [x, y, z, u]"

   174 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'

   174   shows "alpha_trm' (Lett (PD x u) t (App (Var x) (Var y)))

   175 *)

   175                     (Lett (PD z u) t (App (Var z) (Var y)))"

   176 

   176 using a

   177 

   177 apply -

   178 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]

   178 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)

   179 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]

   179 apply(auto simp add: alpha_gen)

   180 thm f_raw.simps

   180 apply(rule_tac x="(x \<leftrightarrow> z)" in exI)

   181 (*thm trm'_pat'_induct

   181 apply(auto simp add: fresh_star_def)

   182 thm trm'_pat'_perm

   182 defer

   183 thm trm'_pat'_fv

   183 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)

   184 thm trm'_pat'_bn

   184 apply(simp add: alpha_trm'_alpha_pat'_compat_pat'.intros)

   185 thm trm'_pat'_inject*)

   185 defer

   186 apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)

   187 apply(simp)

   188 (* they can be proved *)

   189 oops

   190 

   191 lemma

   192   assumes a: "distinct [x, y, z, u]"

   193   shows "\<not> alpha_trm' (Lett (PD x u) t (App (Var x) (Var y)))

   194                       (Lett (PD z z) t (App (Var z) (Var y)))"

   195 using a

   196 apply(clarify)

   197 apply(erule alpha_trm'.cases)

   198 apply(simp_all)

   199 apply(auto simp add: alpha_gen)

   200 apply(erule alpha_trm'.cases)

   201 apply(simp_all)

   202 apply(clarify)

   203 apply(erule compat_pat'.cases)

   204 apply(simp_all)

   205 apply(clarify)

   206 apply(erule alpha_trm'.cases)

   207 apply(simp_all)

   208 done