# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324280360 -32400
# Node ID abf147627b4bfacbc9ff85fd3f83fa67670282f9
# Parent  df1055004f5294fec08848fc565634913f090a4c
Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.

diff -r df1055004f52 -r abf147627b4b Nominal/Ex/BetaCR.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/BetaCR.thy	Mon Dec 19 16:39:20 2011 +0900
@@ -0,0 +1,384 @@
+theory BetaCR
+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)
+
+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])"
+| "atom x \<sharp> (y, s) \<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 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)
+
+inductive 
+  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
+where
+  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
+| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
+| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
+| b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
+
+equivariance beta
+
+(* HERE 1 *)
+nominal_inductive beta
+  avoids b3: x
+  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+
+(* This also works, but we cannot have them together: *)
+(*nominal_inductive beta
+  avoids b4: x
+  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)*)
+
+(* But I need a combination, possibly with an 'and' syntax:
+nominal_inductive beta
+  avoids b3: x and b4: x
+  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
+*)
+
+(* The combination should look like this: *)
+lemma beta_strong_induct:
+  assumes "x1 \<longrightarrow>b x2"
+  and "\<And>t1 t2 s c. \<lbrakk> t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (App t1 s) (App t2 s)"
+  and "\<And>s1 s2 t c. \<lbrakk> s1 \<longrightarrow>b s2; \<And>c. P c s1 s2\<rbrakk> \<Longrightarrow> P c (App t s1) (App t s2)"
+  and "\<And>t1 t2 x c. \<lbrakk>{atom x} \<sharp>* c;  t1 \<longrightarrow>b t2; \<And>c. P c t1 t2\<rbrakk> \<Longrightarrow> P c (Lam [x]. t1) (Lam [x]. t2)"
+  and "\<And>x s t c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> s\<rbrakk> \<Longrightarrow> P c (App (Lam [x]. t) s) (t [x ::= s])"
+  shows "P (c\<Colon>'a\<Colon>fs) x1 x2"
+  sorry
+
+inductive
+  beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80)
+where
+  bs1[intro, simp]: "M \<longrightarrow>b* M"
+| bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"
+
+lemma beta_star_trans:
+  assumes "A \<longrightarrow>b* B"
+  and     "B \<longrightarrow>b* C"
+  shows   "A \<longrightarrow>b* C"
+  using assms(2) assms(1)
+  by induct auto
+
+(* HERE 2: Does not work:*)
+
+(* equivariance beta_star *)
+
+(* proved manually below. *)
+
+lemma eqvt_helper: "x1 \<longrightarrow>b* x2 \<Longrightarrow>  (p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2)"
+  apply (erule beta_star.induct)
+  apply auto
+  using eqvt(1) bs2
+  by blast
+
+lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))"
+  apply rule
+  apply (drule permute_boolE)
+  apply (erule eqvt_helper)
+  apply (intro permute_boolI)
+  apply (drule_tac p="-p" in eqvt_helper)
+  by simp
+
+definition
+  equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _")
+where
+  "t \<approx> s \<longleftrightarrow> (\<exists>r. t \<longrightarrow>b* r \<and> s \<longrightarrow>b* r)"
+
+lemma equ_refl:
+  shows "t \<approx> t"
+  unfolding equ_def by auto
+
+lemma equ_sym:
+  assumes "t \<approx> s"
+  shows "s \<approx> t"
+  using assms unfolding equ_def
+  by auto
+
+(* can be ported from nominal1 *)
+lemma cr:
+  assumes "t \<longrightarrow>b* t1" and "t \<longrightarrow>b* t2" shows "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3"
+  sorry
+
+lemma equ_trans:
+  assumes "A \<approx> B" "B \<approx> C"
+  shows "A \<approx> C"
+  using assms unfolding equ_def
+proof (elim exE conjE)
+  fix D E
+  assume a: "A \<longrightarrow>b* D" "B \<longrightarrow>b* D" "B \<longrightarrow>b* E" "C \<longrightarrow>b* E"
+  then obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using cr by blast
+  then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a beta_star_trans by blast
+  then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast
+qed
+
+lemma App_beta: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> App A C \<longrightarrow>b* App B D"
+  apply (erule beta_star.induct)
+  apply auto
+  apply (erule beta_star.induct)
+  apply auto
+  done
+
+lemma Lam_beta: "A \<longrightarrow>b* B \<Longrightarrow> Lam [x]. A \<longrightarrow>b* Lam [x]. B"
+  by (erule beta_star.induct) auto
+
+lemma [quot_respect]:
+  shows "(op = ===> equ) Var Var"
+  and   "(equ ===> equ ===> equ) App App"
+  and   "(op = ===> equ ===> equ) BetaCR.Lam BetaCR.Lam"
+  unfolding fun_rel_def equ_def
+  apply auto
+  apply (rule_tac x="App r ra" in exI)
+  apply (auto simp add: App_beta)
+  apply (rule_tac x="Lam [x]. r" in exI)
+  apply (auto simp add: Lam_beta)
+  done
+
+lemma beta_subst1_pre: "B \<longrightarrow>b C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"
+  by (nominal_induct A avoiding: x B C rule: lam.strong_induct)
+     (auto simp add: App_beta Lam_beta)
+
+lemma beta_subst1: "B \<longrightarrow>b* C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"
+  apply (erule beta_star.induct)
+  apply auto
+  apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]")
+  apply (rotate_tac 1)
+  apply (erule beta_star_trans)
+  apply assumption
+  apply (simp add: beta_subst1_pre)
+  done
+
+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 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)
+
+lemma beta_subst2_pre:
+  assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]"
+  using assms
+(* HERE 3: nominal_induct doesn't work - leaves the assumption *)
+(*  apply (nominal_induct avoiding: x C rule: beta_strong_induct)*)
+  apply -
+  apply (erule beta_strong_induct[of A B "\<lambda>c A B. A [(fst c) ::= (snd c)] \<longrightarrow>b* B [(fst c) ::= (snd c)]" "(x, C)", simplified])
+  apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3]
+  apply (subst substitution_lemma)
+  apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2]
+  apply (auto simp add: fresh_star_def fresh_Pair)
+  apply (rule beta_star.intros)
+  defer
+  apply (subst beta.intros)
+  apply (auto simp add: fresh_fact)
+  done
+
+lemma beta_subst2: "A \<longrightarrow>b* B \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= C]"
+  apply (erule beta_star.induct)
+  apply auto
+  apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]")
+  apply (rotate_tac 1)
+  apply (erule beta_star_trans)
+  apply assumption
+  apply (simp add: beta_subst2_pre)
+  done
+
+lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]"
+  using beta_subst1 beta_subst2 beta_star_trans by metis
+
+lemma [quot_respect]:
+  shows "(equ ===> op = ===> equ ===> equ) subst subst"
+unfolding fun_rel_def equ_def
+apply auto
+apply (rule_tac x="r [xa ::= ra]" in exI)
+apply (simp add: beta_subst)
+done
+
+lemma [quot_respect]:
+  shows "(op = ===> equ ===> equ) permute permute"
+  unfolding fun_rel_def equ_def
+  apply (auto intro: eqvts)
+  apply (rule_tac x="x \<bullet> r" in exI)
+  using eqvts(1) permute_boolI by metis
+
+quotient_type qlam = lam / equ
+  by (auto intro!: equivpI reflpI sympI transpI simp add: equ_refl equ_sym)
+     (erule equ_trans, assumption)
+
+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 qlam_perm[simp, eqvt]:
+  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)"
+  by(descending, simp add: equ_refl)+
+
+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  
+
+lemmas qsubst = subst.simps(1-2)[quot_lifted]
+
+definition
+  "Supp t = \<Inter>{supp s | s. s \<approx> t}"
+
+lemma [quot_respect]:
+  shows "(equ ===> op=) Supp Supp"
+  unfolding fun_rel_def Supp_def
+  apply(intro allI 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
+
+lemma [eqvt]: "(p \<bullet> (a \<approx> b)) = ((p \<bullet> a) \<approx> (p \<bullet> b))"
+  unfolding equ_def
+  by perm_simp rule
+
+lemma [eqvt]: "p \<bullet> (Supp x) = Supp (p \<bullet> x)"
+  unfolding Supp_def
+  by perm_simp rule
+
+lemmas s = Supp_Lam[quot_lifted]
+
+lemma var_beta_pre: "s \<longrightarrow>b* r \<Longrightarrow> s = Var name \<Longrightarrow> r = Var name"
+  apply (induct rule: beta_star.induct)
+  apply simp
+  apply (subgoal_tac "M2 = Var name")
+  apply (thin_tac "M1 \<longrightarrow>b* M2")
+  apply (thin_tac "M1 = Var name")
+  apply (thin_tac "M1 = Var name \<Longrightarrow> M2 = Var name")
+  defer
+  apply simp
+  apply (erule_tac beta.cases)
+  apply simp_all
+  done
+
+lemma var_beta: "Var name \<longrightarrow>b* r \<longleftrightarrow> r = Var name"
+  by (auto simp add: var_beta_pre)
+
+lemma qlam_eq_iff:
+  "(QVar n = QVar m) = (n = m)"
+  apply descending unfolding equ_def var_beta by auto
+
+lemma "supp (QVar n) = {atom n}"
+  unfolding supp_def
+  apply simp
+  unfolding qlam_eq_iff
+  apply (fold supp_def)
+  apply (simp add: supp_at_base)
+  done
+
+end
+
+
+