# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1309320264 -32400
# Node ID 6d46f7ea16616ed43718a57937fc02c67039ce65
# Parent  a27215ab674e247a115c82a57905fff3811d712f
Prove bn injectivity and experiment more with Let

diff -r a27215ab674e -r 6d46f7ea1661 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Wed Jun 29 00:48:50 2011 +0100
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 13:04:24 2011 +0900
@@ -18,10 +18,8 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-print_theorems
-
 thm trm_assn.fv_defs
-thm trm_assn.eq_iff 
+thm trm_assn.eq_iff
 thm trm_assn.bn_defs
 thm trm_assn.bn_inducts
 thm trm_assn.perm_simps
@@ -33,17 +31,50 @@
 thm trm_assn.exhaust
 thm trm_assn.strong_exhaust
 
-lemma bn_inj:
-  assumes a: "alpha_bn_raw x y"
-  shows "bn_raw x = bn_raw y \<Longrightarrow> x = y"
-using a
-apply(induct)
-apply(auto)[6]
-apply(simp)
-apply(simp)
-oops
-  
+lemma alpha_bn_inducts_raw:
+  "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw;
+ \<And>trm_raw trm_rawa assn_raw assn_rawa name namea.
+    \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa;
+     P3 assn_raw assn_rawa\<rbrakk>
+    \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw)
+        (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b"
+  by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto
+
+lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted]
+
+
+
+lemma alpha_bn_refl: "alpha_bn x x"
+  by (induct x rule: trm_assn.inducts(2))
+     (rule TrueI, auto simp add: trm_assn.eq_iff)
+lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x"
+  sorry
+lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
+  sorry
 
+lemma bn_inj[rule_format]:
+  assumes a: "alpha_bn x y"
+  shows "bn x = bn y \<longrightarrow> x = y"
+  by (rule alpha_bn_inducts[OF a]) (simp_all add: trm_assn.bn_defs)
+
+(*lemma alpha_bn_permute:
+  assumes a: "alpha_bn x y"
+      and b: "q \<bullet> bn x = r \<bullet> bn y"
+    shows "alpha_bn (q \<bullet> x) (r \<bullet> y)"
+proof -
+  have "alpha_bn x (permute_bn r y)"
+    by (rule alpha_bn_trans[OF a]) (rule trm_assn.perm_bn_alpha)
+  then have "alpha_bn (permute_bn r y) x"
+    by (rule alpha_bn_sym)
+  then have "alpha_bn (permute_bn r y) (permute_bn q x)"
+    by (rule alpha_bn_trans) (rule trm_assn.perm_bn_alpha)
+  then have "alpha_bn (permute_bn q x) (permute_bn r y)"
+    by (rule alpha_bn_sym)
+  moreover have "bn (permute_bn q x) = bn (permute_bn r y)"
+    using b trm_assn.permute_bn by simp
+  ultimately have "permute_bn q x = permute_bn r y"
+    using bn_inj by simp
+*)
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))"
@@ -64,7 +95,6 @@
   apply (simp add: trm_assn.eq_iff)
   done
 
-
 lemma lets_not_ok1:
   "x \<noteq> y \<Longrightarrow>
    (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
@@ -87,32 +117,9 @@
   apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
   by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)
 
-lemma alpha_bn_refl: "alpha_bn x x"
-apply (induct x rule: trm_assn.inducts(2))
-apply (rule TrueI)
-apply (auto simp add: trm_assn.eq_iff)
-done
-
-lemma alpha_bn_inducts_raw:
-  "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw;
- \<And>trm_raw trm_rawa assn_raw assn_rawa name namea.
-    \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa;
-     P3 assn_raw assn_rawa\<rbrakk>
-    \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw)
-        (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b"
-  by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto
-
-lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted]
-
 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
   by (simp add: permute_pure)
 
-(* TODO: should be provided by nominal *)
-lemmas [eqvt] = trm_assn.fv_bn_eqvt
-
-thm Abs_lst_fcb
-
-(*
 lemma Abs_lst_fcb2:
   fixes as bs :: "'a :: fs"
     and x y :: "'b :: fs"
@@ -123,6 +130,10 @@
   and fresh2: "set (ba bs) \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
+(* What we would like in this proof, and lets this proof finish *)
+  and bainj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs"
+(* What the user can supply with the help of alpha_bn *)
+(*  and bainj: "ba as = ba bs \<Longrightarrow> as = bs"*)
   shows "f as x c = f bs y c"
 proof -
   have "supp (as, x, c) supports (f as x c)"
@@ -167,31 +178,30 @@
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
-  then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2
+  then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj 
     by simp
-  then have "r \<bullet> ((set (ba bs)) \<sharp>* f (ba bs) y c)"
+  then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)"
     apply(simp add: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
     done
-  then have fcb2: "(set (ba bs)) \<sharp>* f (ba bs) y c" by (simp add: permute_bool_def)
-  have "f (ba as) x c = q \<bullet> (f (ba as) x c)"
+  then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def)
+  have "f as x c = q \<bullet> (f as x c)"
     apply(rule perm_supp_eq[symmetric])
     using inc fcb1 fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (q \<bullet> (ba as)) (q \<bullet> x) c" 
+  also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
     apply(rule perm1)
     using inc fresh1 fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (r \<bullet> (ba bs)) (r \<bullet> y) c" using qq1 qq2 by simp
-  also have "\<dots> = r \<bullet> (f (ba bs) y c)"
+  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 bainj by simp
+  also have "\<dots> = r \<bullet> (f bs y c)"
     apply(rule perm2[symmetric])
     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
-  also have "... = f (ba bs) y c"
+  also have "... = f bs y c"
     apply(rule perm_supp_eq)
     using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)
   finally show ?thesis by simp
 qed
-*)
 
 nominal_primrec
     height_trm :: "trm \<Rightarrow> nat"
@@ -214,11 +224,11 @@
   apply (case_tac b rule: trm_assn.exhaust(2))
   apply (auto)[2]
   apply(simp_all)
-  thm  trm_assn.perm_bn_alpha trm_assn.permute_bn
   apply (erule_tac c="()" in Abs_lst_fcb2)
   apply (simp_all add: pure_fresh fresh_star_def)[3]
   apply (simp add: eqvt_at_def)
   apply (simp add: eqvt_at_def)
+  apply assumption
   apply(erule conjE)
   apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
   apply (simp add: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff])
@@ -241,14 +251,13 @@
   apply (erule_tac c="()" in Abs_lst_fcb2)
   apply (simp_all add: pure_fresh fresh_star_def)[3]
   apply (simp_all add: eqvt_at_def)[2]
-  apply (drule_tac c="()" in Abs_lst_fcb2)
+  apply assumption
+  apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2)
   apply (simp_all add: pure_fresh fresh_star_def)[3]
   apply (simp_all add: eqvt_at_def)[2]
-  apply(simp add: eqvt_def)
-  apply(perm_simp)
-  apply(simp)
-  apply(simp add: inj_on_def)
-  apply (rule arg_cong) back
+  apply (rule bn_inj)
+  prefer 2
+  apply (simp add: eqvts)
   oops
 
 nominal_primrec
@@ -280,7 +289,10 @@
   apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
   apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff])
   prefer 2
-  apply (erule_tac Abs_lst_fcb2)
+  apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2)
+  apply (simp_all add: fresh_star_Pair)
+  prefer 6
+  apply (erule alpha_bn_inducts)
  oops
 
 end