--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Beta.thy	Wed Nov 09 11:44:01 2011 +0000
@@ -0,0 +1,312 @@
+theory Beta
+imports 
+  "../Nominal2"
+begin
+
+
+atom_decl name
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
+
+section {* capture-avoiding substitution *}
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
+where
+  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
+| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+  unfolding eqvt_def subst_graph_def
+  apply (rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply(auto simp add: lam.distinct lam.eq_iff)
+  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+  apply(blast)+
+  apply(simp_all add: fresh_star_def fresh_Pair_elim)
+  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+done
+
+termination (eqvt)
+  by lexicographic_order
+
+lemma forget:
+  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
+  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+     (auto simp add: lam.fresh fresh_at_base)
+
+lemma fresh_fact:
+  fixes z::"name"
+  assumes a: "atom z \<sharp> s"
+      and b: "z = y \<or> atom z \<sharp> t"
+  shows "atom z \<sharp> t[y ::= s]"
+  using a b
+  by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+     (auto simp add: lam.fresh fresh_at_base)
+
+lemma substitution_lemma:  
+  assumes a: "x \<noteq> y" "atom x \<sharp> u"
+  shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"
+using a 
+by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
+   (auto simp add: fresh_fact forget)
+
+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]"
+| equ_refl:  "t \<approx> t"
+| equ_sym:   "t \<approx> s \<Longrightarrow> s \<approx> t"
+| equ_trans: "\<lbrakk>t1 \<approx> t2; t2 \<approx> t3\<rbrakk> \<Longrightarrow> t1 \<approx> t3"
+| equ_Lam:   "t \<approx> s \<Longrightarrow> Lam [x].t \<approx> Lam [x].s"
+| equ_App1:  "t \<approx> s \<Longrightarrow> App t u \<approx> App s u"
+| equ_App2:  "t \<approx> s \<Longrightarrow> App u t \<approx> App u s"
+
+equivariance equ
+
+nominal_inductive equ
+  avoids equ_beta: "x" 
+       | equ_Lam: "x"
+by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+lemma [quot_respect]:
+  shows "(op = ===> equ) Var Var"
+  and   "(equ ===> equ ===> equ) App App"
+  and   "(op = ===> equ ===> equ) Beta.Lam Beta.Lam"
+unfolding fun_rel_def
+by (auto intro: equ.intros)
+
+lemma equ_subst1:
+  assumes "t \<approx> s"
+  shows "t[x ::= u] \<approx> s[x ::= u]"
+using assms
+apply(nominal_induct avoiding: x u rule: equ.strong_induct)
+apply(simp)
+apply(rule equ_trans)
+apply(rule equ_beta)
+apply(simp add: fresh_fact)
+apply(subst (2) substitution_lemma)
+apply(simp add: fresh_at_base)
+apply(simp)
+apply(rule equ_refl)
+apply(rule equ_refl)
+apply(auto intro: equ_sym)[1]
+apply(blast intro: equ_trans)
+apply(simp add: equ_Lam)
+apply(simp add: equ_App1)
+apply(simp add: equ_App2)
+done
+
+lemma equ_subst2:
+  assumes "t \<approx> s"
+  shows "u[x ::= t] \<approx> u[x ::= s]"
+using assms
+apply(nominal_induct u avoiding: x t s rule: lam.strong_induct)
+apply(simp add: equ_refl)
+apply(simp)
+apply(smt equ_App1 equ_App2 equ_trans)
+apply(simp)
+apply(metis equ_Lam)
+done
+
+lemma [quot_respect]:
+  shows "(equ ===> op = ===> equ ===> equ) subst subst"
+unfolding fun_rel_def
+by (metis equ_subst1 equ_subst2 equ_trans)
+
+lemma [quot_respect]:
+  shows "(op = ===> equ ===> equ) permute permute"
+unfolding fun_rel_def
+by (auto intro: eqvt)
+
+quotient_type qlam = lam / equ
+apply(rule equivpI)
+apply(rule reflpI)
+apply(simp add: equ_refl)
+apply(rule sympI)
+apply(simp add: equ_sym)
+apply(rule transpI)
+apply(auto intro: equ_trans)
+done
+
+quotient_definition "QVar::name \<Rightarrow> qlam" is Var
+quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App
+quotient_definition QLam ("QLam [_]._") 
+  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam
+
+lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]
+lemmas qlam_induct = lam.induct[quot_lifted]
+
+instantiation qlam :: pt
+begin
+
+quotient_definition "permute_qlam::perm \<Rightarrow> qlam \<Rightarrow> qlam" 
+  is "permute::perm \<Rightarrow> lam \<Rightarrow> lam"
+
+instance
+apply default
+apply(descending)
+apply(simp)
+apply(rule equ_refl)
+apply(descending)
+apply(simp)
+apply(rule equ_refl)
+done
+
+end
+
+lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)"
+ apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])
+ apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified])
+ by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left)
+
+lemma supports_abs_qlam:
+  "(supp t) supports (abs_qlam t)"
+unfolding supports_def
+unfolding fresh_def[symmetric]
+apply(auto)
+apply(perm_simp)
+apply(simp add: swap_fresh_fresh)
+done
+
+lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)"
+ apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])
+ apply (rule rep_abs_rsp[OF Quotient_qlam])
+ apply (rule equ_refl)
+ done
+
+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
+  fixes t::"qlam"
+  shows "supp t = supp_qlam t"
+apply(descending)
+oops
+
+
+ 
+
+lemma [quot_respect]:
+  shows "(equ ===> op=) Size Size"
+unfolding fun_rel_def
+unfolding Size_def
+apply(auto)
+apply(rule_tac f="Least" in arg_cong)
+apply(auto)
+apply (metis equ_trans)
+by (metis equivp_def qlam_equivp)
+
+
+section {* Size *}
+
+definition
+  "Size t = Least {size s | s. s \<approx> t}" 
+
+lemma [quot_respect]:
+  shows "(equ ===> op=) Size Size"
+unfolding fun_rel_def
+unfolding Size_def
+apply(auto)
+apply(rule_tac f="Least" in arg_cong)
+apply(auto)
+apply (metis equ_trans)
+by (metis equivp_def qlam_equivp)
+
+instantiation qlam :: size
+begin
+
+quotient_definition "size_qlam::qlam \<Rightarrow> nat" 
+  is "Size::lam \<Rightarrow> nat"
+
+instance
+apply default
+done
+
+end
+
+thm lam.size
+
+lemma
+  "size (QVar x) = 0"
+apply(descending)
+apply(simp add: Size_def)
+apply(rule Least_equality)
+apply(auto)
+apply(simp add: Collect_def)
+apply(rule_tac x="Var x" in exI)
+apply(auto intro: equ_refl)
+done
+
+lemma
+  "size (QLam [x].t) = Suc (size t)"
+apply(descending)
+apply(simp add: Size_def)
+apply(auto)
+apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2)
+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(rule_tac x="t" in exI)
+apply(auto intro: equ_refl)[1]
+apply(simp add: Collect_def)
+apply(auto)[1]
+defer
+apply(simp add: Collect_def)
+apply(auto)[1]
+
+apply(auto)
+done
+
+term rep_qlam
+lemmas qlam_size_def = Size_def[quot_lifted]
+
+lemma [quot_preserve]:
+  assumes "Quotient equ Abs Rep"
+  shows "(id ---> Rep ---> id) fresh = fresh"
+using assms
+unfolding Quotient_def
+apply(simp add: map_fun_def)
+apply(simp add: comp_def fun_eq_iff)
+
+sorry
+
+lemma [simp]:
+  shows "(QVar x)[y :::= s] = (if x = y then s else (QVar x))"
+  and "(QApp t1 t2)[y :::= s] = QApp (t1[y :::= s]) (t2[y :::= s])"
+  and "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y :::= s] = QLam [x].(t[y :::= s])"
+apply(lifting subst.simps(1))
+apply(lifting subst.simps(2))
+apply(lifting subst.simps(3))
+done
+
+
+
+end
+
+
+