--- 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