--- a/Nominal/Ex/Beta.thy	Wed Dec 14 01:32:42 2011 +0000
+++ b/Nominal/Ex/Beta.thy	Thu Dec 15 16:20:11 2011 +0000
@@ -6,6 +6,7 @@
 
 atom_decl name
 
+
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
@@ -58,6 +59,21 @@
    (auto simp add: fresh_fact forget)
 
 inductive
+  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _")
+where
+  beta_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<rightarrow> t[x ::= s]"
+| beta_Lam:   "t \<rightarrow> s \<Longrightarrow> Lam [x].t \<rightarrow> Lam [x].s"
+| beta_App1:  "t \<rightarrow> s \<Longrightarrow> App t u \<rightarrow> App s u"
+| beta_App2:  "t \<rightarrow> s \<Longrightarrow> App u t \<rightarrow> App u s"
+
+equivariance beta
+
+nominal_inductive beta
+  avoids beta_beta: "x" 
+       | beta_Lam: "x"
+by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+inductive
   equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _")
 where
   equ_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<approx> t[x ::= s]"
@@ -75,6 +91,64 @@
        | equ_Lam: "x"
 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
 
+inductive
+  equ2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx>2 _")
+where
+  equ2_beta1:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) t2 \<approx>2 s1[x ::= s2]"
+| equ2_beta2:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> s1[x ::= s2] \<approx>2 App (Lam [x].t1) t2"
+| equ2_Var:   "Var x \<approx>2 Var x"
+| equ2_Lam:   "t \<approx>2 s \<Longrightarrow> Lam [x].t \<approx>2 Lam [x].s"
+| equ2_App:   "\<lbrakk>t1 \<approx>2 s1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> App t1 t2 \<approx>2 App s1 s2"
+
+equivariance equ2
+
+nominal_inductive equ2
+  avoids equ2_beta1: "x"
+       | equ2_beta2: "x" 
+       | equ2_Lam: "x"
+by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+lemma equ2_refl:
+  fixes t::"lam"
+  shows "t \<approx>2 t"
+apply(induct t rule: lam.induct)
+apply(auto intro: equ2.intros)
+done
+
+lemma equ2_symm:
+  fixes t s::"lam"
+  assumes "t \<approx>2 s"
+  shows "s \<approx>2 t"
+using assms
+apply(induct)
+apply(auto intro: equ2.intros)
+done
+
+lemma equ2_trans:
+  fixes t1 t2 t3::"lam"
+  assumes "t1 \<approx>2 t2" "t2 \<approx>2 t3"
+  shows "t1 \<approx>2 t3"
+using assms
+apply(nominal_induct t1 t2 avoiding: t3 rule: equ2.strong_induct)
+defer
+defer
+apply(erule equ2.cases)
+apply(auto)
+apply(rule equ2_beta2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(rule equ2_refl)
+defer
+apply(rotate_tac 4)
+apply(erule equ2.cases)
+apply(auto)
+oops
+
+
+
+
+
 lemma [quot_respect]:
   shows "(op = ===> equ) Var Var"
   and   "(equ ===> equ ===> equ) App App"
@@ -123,7 +197,7 @@
 lemma [quot_respect]:
   shows "(op = ===> equ ===> equ) permute permute"
 unfolding fun_rel_def
-by (auto intro: eqvt)
+by (auto intro: eqvts)
 
 quotient_type qlam = lam / equ
 apply(rule equivpI)
@@ -161,8 +235,52 @@
 
 end
 
+lemma qlam_perm[simp]:
+  shows "p \<bullet> (QVar x) = QVar (p \<bullet> x)"
+  and "p \<bullet> (QApp t s) = QApp (p \<bullet> t) (p \<bullet> s)"
+  and "p \<bullet> (QLam [x].t) = QLam [p \<bullet> x].(p \<bullet> t)"
+apply(descending)
+apply(simp add: equ_refl)
+apply(descending)
+apply(simp add: equ_refl)
+apply(descending)
+apply(simp add: equ_refl)
+done
+
+lemma qlam_supports:
+  shows "{atom x} supports (QVar x)"
+  and   "supp (t, s) supports (QApp t s)"
+  and   "supp (x, t) supports (QLam [x].t)"
+unfolding supports_def fresh_def[symmetric]
+by (auto simp add: swap_fresh_fresh)
+
+lemma qlam_fs:
+  fixes t::"qlam"
+  shows "finite (supp t)"
+apply(induct t rule: qlam_induct)
+apply(rule supports_finite)
+apply(rule qlam_supports)
+apply(simp)
+apply(rule supports_finite)
+apply(rule qlam_supports)
+apply(simp add: supp_Pair)
+apply(rule supports_finite)
+apply(rule qlam_supports)
+apply(simp add: supp_Pair finite_supp)
+done
+
+instantiation qlam :: fs
+begin
+
+instance
+apply(default)
+apply(rule qlam_fs)
+done
+
+end
+
 quotient_definition subst_qlam ("_[_ ::q= _]")
- where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  
+  where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  
 
 lemma
   "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))"
@@ -178,12 +296,136 @@
 apply(rule equ_refl)
 done
 
+definition
+  "Supp t = \<Inter>{supp s | s. s \<approx> t}"
+
+lemma [quot_respect]:
+  shows "(equ ===> op=) Supp Supp"
+unfolding fun_rel_def
+unfolding Supp_def
+apply(rule allI)+
+apply(rule impI)
+apply(rule_tac f="Inter" in arg_cong)
+apply(auto)
+apply (metis equ_trans)
+by (metis equivp_def qlam_equivp)
+
+quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 
+  is "Supp::lam \<Rightarrow> atom set"
+
+lemma Supp_supp:
+  "Supp t \<subseteq> supp t"
+unfolding Supp_def
+apply(auto)
+apply(drule_tac x="supp t" in spec)
+apply(auto simp add: equ_refl)
+done
+
+lemma Supp_Lam:
+  "atom a \<notin> Supp (Lam [a].t)"
+proof -
+  have "atom a \<notin> supp (Lam [a].t)" by (simp add: lam.supp)
+  then show ?thesis using Supp_supp
+    by blast
+qed
+
+lemmas s = Supp_Lam[quot_lifted]
+
+definition
+  ssupp :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ ssupp _")
+where
+  "A ssupp x \<equiv> \<forall>p. (\<forall>a \<in> A. (p \<bullet> a) = a) \<longleftrightarrow> (p \<bullet> x) = x"
+
+lemma ssupp_supports:
+  "A ssupp x \<Longrightarrow> A supports x"
+unfolding ssupp_def supports_def
+apply(rule allI)+
+apply(drule_tac x="(a \<rightleftharpoons> b)" in spec)
+apply(auto)
+by (metis swap_atom_simps(3))
+
+lemma ssupp_supp:
+  assumes a: "finite A"
+  and     b: "A ssupp x"
+  shows "supp x = A"
+proof -
+  { assume 0: "A - supp x \<noteq> {}"
+    then obtain a where 1: "a \<in> A - supp x" by auto
+    obtain a' where *: "a' \<in>  UNIV - A" and **: "sort_of a' = sort_of a"
+      by (rule obtain_atom[OF a]) (auto)  
+    have "(a \<rightleftharpoons> a') \<bullet> a = a'" using 1 ** * by (auto)
+    then have w0: "(a \<rightleftharpoons> a') \<bullet> x \<noteq> x"
+      using b unfolding ssupp_def 
+      apply -
+      apply(drule_tac x="(a \<rightleftharpoons> a')" in spec)
+      apply(auto)
+      using 1 *
+      apply(auto)
+      done
+    have w1: "a \<sharp> x" unfolding fresh_def using 1 by auto 
+    have w2: "a' \<sharp> x" using *
+      apply(rule_tac supports_fresh)
+      apply(rule ssupp_supports)
+      apply(rule b)
+      apply(rule a)
+      apply(auto)
+      done
+    have "False" using w0 w1 w2 by (simp add: swap_fresh_fresh)
+    then have "supp x = A" by simp }
+  moreover
+  { assume "A - supp x = {}"
+    moreover
+    have "supp x \<subseteq> A"
+      apply(rule supp_is_subset)
+      apply(rule ssupp_supports)
+      apply(rule b)
+      apply(rule a)
+      done
+    ultimately have "supp x = A"
+      by blast
+  }
+  ultimately show "supp x = A" by blast
+qed
+      
+
 lemma
-  "(QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])"
+  "(supp x) ssupp x"
+unfolding ssupp_def
+apply(auto)
+apply(rule supp_perm_eq)
+apply(simp add: fresh_star_def)
+apply(auto)
+apply(simp add: fresh_perm)
+apply(simp add: fresh_perm[symmetric])
+(*Tzevelekos 2008, section 2.1.2 property 2.5*)
+oops
+
+
+function
+  qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam"  ("_ [_ ::qq= _]" [90, 90, 90] 90)
+where
+  "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))"
+| "(QApp t1 t2)[y ::qq= s] = QApp (t1[y ::qq= s]) (t2[y ::qq= s])"
+| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y ::qq= s] = QLam [x].(t[y ::qq= s])"
+apply(simp_all add:)
+oops
+
+
+lemma
+  assumes a: "Lam [x].t \<approx> s"
+  shows "\<exists>x' t'. s = Lam [x']. t' \<and> t \<approx> t'"
+using a
+apply(induct s rule:lam.induct)
+apply(erule equ.cases)
+apply(auto)
+apply(erule equ.cases)
+apply(auto)
+
+
+
+lemma
+  "atom x \<sharp> y \<Longrightarrow> atom x \<notin> supp_qlam s \<Longrightarrow> (QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])"
 apply(descending)
-apply(subst subst.simps)
-prefer 3
-apply(rule equ_refl)
 oops
 
 
@@ -222,23 +464,6 @@
 
 section {* Supp *}
 
-definition
-  "Supp t = \<Inter>{supp s | s. s \<approx> t}"
-
-lemma [quot_respect]:
-  shows "(equ ===> op=) Supp Supp"
-unfolding fun_rel_def
-unfolding Supp_def
-apply(rule allI)+
-apply(rule impI)
-apply(rule_tac f="Inter" in arg_cong)
-apply(auto)
-apply (metis equ_trans)
-by (metis equivp_def qlam_equivp)
-
-quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 
-  is "Supp::lam \<Rightarrow> atom set"
-
 lemma s:
   assumes "s \<approx> t"
   shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)"
@@ -277,7 +502,6 @@
 apply(rule_tac x="QVar x" in Abs_qlam_cases)
 apply(auto)
 thm QVar_def
-apply(descending)
 oops
 
 
@@ -326,11 +550,16 @@
   "size (QLam [x].t) = Suc (size t)"
 apply(descending)
 apply(simp add: Size_def)
-apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2)
+thm Least_Suc
+apply(rule trans)
+apply(rule_tac n="Suc (size t)" in Least_Suc)
 apply(simp add: Collect_def)
 apply(rule_tac x="Lam [x].t" in exI)
 apply(auto intro: equ_refl)[1]
 apply(simp add: Collect_def)
+apply(auto)
+defer
+apply(simp add: Collect_def)
 apply(rule_tac x="t" in exI)
 apply(auto intro: equ_refl)[1]
 apply(simp add: Collect_def)