# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268120815 -3600
# Node ID 424962b8b699cc5c326ef7f24c8dbc377158527d
# Parent  c0cb30581f581296a860a58b40306f5740e4807b
added another compat example

diff -r c0cb30581f58 -r 424962b8b699 Nominal/Test_compat.thy
--- a/Nominal/Test_compat.thy	Mon Mar 08 20:18:27 2010 +0100
+++ b/Nominal/Test_compat.thy	Tue Mar 09 08:46:55 2010 +0100
@@ -142,8 +142,8 @@
 
 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
 
-abbreviation "Var \<equiv> VAR_raw"
-abbreviation "App \<equiv> APP_raw"
+abbreviation "Var \<equiv> Var_raw"
+abbreviation "App \<equiv> App_raw"
 abbreviation "Lam \<equiv> Lam_raw"
 abbreviation "Lett \<equiv> Let_raw"
 abbreviation "PN \<equiv> PN_raw"
@@ -151,38 +151,61 @@
 abbreviation "PD \<equiv> PD_raw"
 abbreviation "f \<equiv> f_raw"
 
-(* not_yet_done
-name = namea \<Longrightarrow> alpha_trm'_raw (Var_raw name) (Var_raw namea)
-alpha_trm'_raw trm'_raw2 trm'_raw2a \<and> alpha_trm'_raw trm'_raw1 trm'_raw1a \<Longrightarrow>
-alpha_trm'_raw (App_raw trm'_raw1 trm'_raw2) (App_raw trm'_raw1a trm'_raw2a)
-\<exists>pi. ({atom name}, trm'_raw) \<approx>gen alpha_trm'_raw fv_trm'_raw pi ({atom namea}, trm'_rawa) \<Longrightarrow>
-alpha_trm'_raw (Lam_raw name trm'_raw) (Lam_raw namea trm'_rawa)
-\<exists>pi. (f_raw pat'_raw,
-      trm'_raw2) \<approx>gen alpha_trm'_raw fv_trm'_raw pi (f_raw pat'_rawa, trm'_raw2a) \<and>
-     alpha_trm'_raw trm'_raw1 trm'_raw1a \<and>
-     (f_raw pat'_raw,
-      pat'_raw) \<approx>gen alpha_pat'_raw fv_pat'_raw pi (f_raw pat'_rawa, pat'_rawa) \<Longrightarrow>
-alpha_trm'_raw (Let_raw pat'_raw trm'_raw1 trm'_raw2) (Let_raw pat'_rawa trm'_raw1a trm'_raw2a)
-True \<Longrightarrow> alpha_pat'_raw PN_raw PN_raw
-name = namea \<Longrightarrow> alpha_pat'_raw (PS_raw name) (PS_raw namea)
-name2 = name2a \<and> name1 = name1a \<Longrightarrow> alpha_pat'_raw (PD_raw name1 name2) (PD_raw name1a name2a)
-*)
+(* not_yet_done *)
+inductive 
+  alpha_trm' :: "trm'_raw \<Rightarrow> trm'_raw \<Rightarrow> bool" and
+  alpha_pat'  :: "pat'_raw \<Rightarrow> pat'_raw \<Rightarrow> bool" and
+  compat_pat' :: "pat'_raw \<Rightarrow> perm \<Rightarrow> pat'_raw \<Rightarrow> bool"
+where
+  "name = name' \<Longrightarrow> alpha_trm' (Var name) (Var name')"
+| "alpha_trm' t2 t2' \<and> alpha_trm' t1 t1' \<Longrightarrow> alpha_trm' (App t1 t2) (App t1' t2')"
+| "\<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')"
+| "\<exists>pi. (f p, t) \<approx>gen alpha_trm' fv_trm'_raw pi (f p', t') \<and> alpha_trm' s s' \<and>
+        compat_pat' p pi p' \<Longrightarrow> alpha_trm' (Lett p s t) (Lett p' s' t')"
+| "alpha_pat' PN PN"
+| "name = name' \<Longrightarrow> alpha_pat' (PS name) (PS name')"
+| "name2 = name2' \<and> name1 = name1' \<Longrightarrow> alpha_pat' (PD name1 name2) (PD name1' name2')"
+| "compat_pat' PN pi PN"
+| "pi \<bullet> x = x' \<Longrightarrow> compat_pat' (PS x) pi (PS x')"
+| "pi \<bullet> p1 = p1' \<and> pi \<bullet> p2 = p2' \<Longrightarrow> compat_pat' (PD p1 p2) pi (PD p1' p2')"
 
-(* compat should be
-compat (PN) pi (PN) == True
-compat (PS x) pi (PS x') == pi o x = x'
-compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
-*)
-
+lemma
+  assumes a: "distinct [x, y, z, u]"
+  shows "alpha_trm' (Lett (PD x u) t (App (Var x) (Var y)))
+                    (Lett (PD z u) t (App (Var z) (Var y)))"
+using a
+apply -
+apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)
+apply(auto simp add: alpha_gen)
+apply(rule_tac x="(x \<leftrightarrow> z)" in exI)
+apply(auto simp add: fresh_star_def)
+defer
+apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)
+apply(simp add: alpha_trm'_alpha_pat'_compat_pat'.intros)
+defer
+apply(rule alpha_trm'_alpha_pat'_compat_pat'.intros)
+apply(simp)
+(* they can be proved *)
+oops
 
-thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
-thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
-thm f_raw.simps
-(*thm trm'_pat'_induct
-thm trm'_pat'_perm
-thm trm'_pat'_fv
-thm trm'_pat'_bn
-thm trm'_pat'_inject*)
+lemma
+  assumes a: "distinct [x, y, z, u]"
+  shows "\<not> alpha_trm' (Lett (PD x u) t (App (Var x) (Var y)))
+                      (Lett (PD z z) t (App (Var z) (Var y)))"
+using a
+apply(clarify)
+apply(erule alpha_trm'.cases)
+apply(simp_all)
+apply(auto simp add: alpha_gen)
+apply(erule alpha_trm'.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule compat_pat'.cases)
+apply(simp_all)
+apply(clarify)
+apply(erule alpha_trm'.cases)
+apply(simp_all)
+done
 
 nominal_datatype trm0 =
   Var0 "name"