--- a/Quot/Nominal/LamEx.thy Thu Jan 28 23:47:02 2010 +0100
+++ b/Quot/Nominal/LamEx.thy Fri Jan 29 00:22:00 2010 +0100
@@ -1,5 +1,5 @@
theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
begin
@@ -153,9 +153,17 @@
where
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)
\<Longrightarrow> rLam a t \<approx> rLam b s"
+lemma a3_inverse:
+ assumes "rLam a t \<approx> rLam b s"
+ shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)"
+using assms
+apply(erule_tac alpha.cases)
+apply(auto)
+done
+
text {* should be automatic with new version of eqvt-machinery *}
lemma alpha_eqvt:
shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
@@ -174,9 +182,6 @@
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
-apply(rule conjI)
-apply(subst permute_eqvt[symmetric])
-apply(simp)
apply(subst permute_eqvt[symmetric])
apply(simp)
done
@@ -201,13 +206,10 @@
apply(rule_tac x="- pi" in exI)
apply(simp)
apply(simp add: fresh_star_def fresh_minus_perm)
-apply(rule conjI)
apply(erule conjE)+
apply(rotate_tac 3)
apply(drule_tac pi="- pi" in alpha_eqvt)
apply(simp)
-apply(clarify)
-apply(simp)
done
lemma alpha_trans:
@@ -231,10 +233,10 @@
apply(simp add: fresh_star_plus)
apply(drule_tac x="- pia \<bullet> sa" in spec)
apply(drule mp)
-apply(rotate_tac 8)
+apply(rotate_tac 7)
apply(drule_tac pi="- pia" in alpha_eqvt)
apply(simp)
-apply(rotate_tac 11)
+apply(rotate_tac 9)
apply(drule_tac pi="pia" in alpha_eqvt)
apply(simp)
done
@@ -330,12 +332,7 @@
apply(simp)
apply(drule sym)
apply(simp)
-apply(case_tac "a = pi \<bullet> a")
-apply(simp)
-defer
-apply(simp)
-apply(simp add: fresh_star_def)
-sorry
+oops
quotient_type lam = rlam / alpha
by (rule alpha_equivp)
@@ -440,16 +437,23 @@
by (lifting a2)
lemma a3:
- "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk>
+ "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk>
\<Longrightarrow> Lam a t = Lam b s"
apply (lifting a3)
done
+lemma a3_inv:
+ assumes "Lam a t = Lam b s"
+ shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)"
+using assms
+apply(lifting a3_inverse)
+done
+
lemma alpha_cases:
"\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
\<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
- \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk>
+ \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk>
\<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (lifting alpha.cases)
@@ -460,7 +464,7 @@
\<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
\<And>t a s b.
\<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>
- (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk>
+ (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk>
\<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
by (lifting alpha.induct)
@@ -486,6 +490,16 @@
apply(simp_all)
done
+lemma Lam_pseudo_inject:
+ shows "(Lam a t = Lam b s) =
+ (\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s))"
+apply(rule iffI)
+apply(rule a3_inv)
+apply(assumption)
+apply(rule a3)
+apply(assumption)
+done
+
lemma rlam_distinct:
shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
@@ -560,42 +574,18 @@
apply(simp add: lam_fsupp1)
done
-lemma lam_fresh1:
- assumes f: "finite (supp t)"
- and a1: "b \<sharp> t"
- and a2: "atom a \<noteq> b"
- shows "b \<sharp> Lam a t"
- proof -
- have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry
- then obtain c where fr1: "c \<noteq> b"
- and fr2: "c \<noteq> atom a"
- and fr3: "c \<sharp> t"
- and fr4: "c \<sharp> Lam a t"
- and fr5: "sort_of b = sort_of c"
- apply(auto simp add: fresh_Pair fresh_atom)
- sorry
- have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2
- by simp
- from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))"
- by (simp only: fresh_permute_iff)
- then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e
- by simp
- then show ?thesis using a1 fr3
- by (simp only: swap_fresh_fresh)
-qed
-
-lemma lam_fresh2:
- assumes f: "finite (supp t)"
- shows "(atom a) \<sharp> Lam a t"
+lemma lam_supp2:
+ shows "supp (Lam x t) = supp (Abs {atom x} t)"
+apply(simp add: supp_def permute_set_eq atom_eqvt)
+apply(simp add: Lam_pseudo_inject)
+apply(simp add: abs_eq)
sorry
-
lemma lam_supp:
shows "supp (Lam x t) = ((supp t) - {atom x})"
-apply(default)
-apply(simp_all add: supp_conv_fresh)
-apply(auto)
-sorry
+apply(simp add: lam_supp2)
+apply(simp add: supp_Abs)
+done
lemma fresh_lam:
"(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"