--- 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]