diff -r faeac3ae43e5 -r 25d813c5042d Nominal/Ex/BetaCR.thy
--- a/Nominal/Ex/BetaCR.thy	Tue Dec 20 18:07:48 2011 +0900
+++ b/Nominal/Ex/BetaCR.thy	Wed Dec 21 13:06:09 2011 +0900
@@ -1,90 +1,16 @@
 theory BetaCR
-imports 
-  "../Nominal2"
+imports CR
 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
-
-nominal_inductive beta
-  avoids b3: x
-       | b4: x
-  by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)
-
-
-
-(* The combination should look like this: *)
-
-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:*)
+(* TODO1: 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
+  by (erule beta_star.induct)
+     (metis beta.eqvt bs2 bs1)+
 
 lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))"
   apply rule
@@ -109,11 +35,6 @@
   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"
@@ -121,8 +42,8 @@
 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 obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using CR_for_Beta_star by blast
+  then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a bs3 by blast
   then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast
 qed
 
@@ -146,7 +67,7 @@
 lemma [quot_respect]:
   shows "(op = ===> equ) Var Var"
   and   "(equ ===> equ ===> equ) App App"
-  and   "(op = ===> equ ===> equ) BetaCR.Lam BetaCR.Lam"
+  and   "(op = ===> equ ===> equ) CR.Lam CR.Lam"
   unfolding fun_rel_def equ_def
   apply auto
   apply (rule_tac x="App r ra" in exI)
@@ -164,23 +85,11 @@
   apply auto
   apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]")
   apply (rotate_tac 1)
-  apply (erule beta_star_trans)
+  apply (erule bs3)
   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
@@ -200,13 +109,13 @@
   apply auto
   apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]")
   apply (rotate_tac 1)
-  apply (erule beta_star_trans)
+  apply (erule bs3)
   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
+  using beta_subst1 beta_subst2 bs3 by metis
 
 lemma subst_rsp_pre:
   "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]"
@@ -234,7 +143,7 @@
 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 BetaCR.Lam
+  where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is CR.Lam
 
 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]
 lemmas qlam_induct = lam.induct[quot_lifted]