theory BetaCRimports CRbegin(* 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)" 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 apply (drule permute_boolE) apply (erule eqvt_helper) apply (intro permute_boolI) apply (drule_tac p="-p" in eqvt_helper) by simpdefinition 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 autolemma equ_sym: assumes "t \<approx> s" shows "s \<approx> t" using assms unfolding equ_def by autolemma equ_trans: assumes "A \<approx> B" "B \<approx> C" shows "A \<approx> C" using assms unfolding equ_defproof (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_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 blastqedlemma 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 donelemma Lam_beta: "A \<longrightarrow>b* B \<Longrightarrow> Lam [x]. A \<longrightarrow>b* Lam [x]. B" by (erule beta_star.induct) autolemma Lam_rsp: "A \<approx> B \<Longrightarrow> Lam [x]. A \<approx> Lam [x]. B" unfolding equ_def apply auto apply (rule_tac x="Lam [x]. r" in exI) apply (auto simp add: Lam_beta) donelemma [quot_respect]: shows "(op = ===> equ) Var Var" and "(equ ===> equ ===> equ) App App" 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) apply (auto simp add: App_beta) apply (rule_tac x="Lam [x]. r" in exI) apply (auto simp add: Lam_beta) donelemma 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 bs3) apply assumption apply (simp add: beta_subst1_pre) donelemma beta_subst2_pre: assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]" using assms apply (nominal_induct avoiding: x C rule: beta.strong_induct) 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) donelemma 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 bs3) apply assumption apply (simp add: beta_subst2_pre) donelemma 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 bs3 by metislemma subst_rsp_pre: "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]" unfolding equ_def apply auto apply (rule_tac x="r [xa ::= ra]" in exI) apply (simp add: beta_subst) donelemma [quot_respect]: shows "(equ ===> op = ===> equ ===> equ) subst subst"unfolding fun_rel_def by (auto simp add: subst_rsp_pre)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 metisquotient_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 Varquotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is Appquotient_definition QLam ("QLam [_]._") where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is CR.Lamlemmas qlam_strong_induct = lam.strong_induct[quot_lifted]lemmas qlam_induct = lam.induct[quot_lifted]instantiation qlam :: ptbeginquotient_definition "permute_qlam::perm \<Rightarrow> qlam \<Rightarrow> qlam" is "permute::perm \<Rightarrow> lam \<Rightarrow> lam"instanceapply defaultapply(descending)apply(simp)apply(rule equ_refl)apply(descending)apply(simp)apply(rule equ_refl)doneendlemma 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)doneinstantiation qlam :: fsbegininstanceapply(default)apply(rule qlam_fs)doneendquotient_definition subst_qlam ("_[_ ::q= _]") where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst definition "Supp t = \<Inter>{supp s | s. s \<approx> t}"lemma Supp_rsp: "a \<approx> b \<Longrightarrow> Supp a = Supp b" unfolding Supp_def apply(rule_tac f="Inter" in arg_cong) apply(auto) apply (metis equ_trans) by (metis equivp_def qlam_equivp)lemma [quot_respect]: shows "(equ ===> op=) Supp Supp" unfolding fun_rel_def by (auto simp add: Supp_rsp)quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" is "Supp::lam \<Rightarrow> atom set"lemma Supp_supp: "Supp t \<subseteq> supp t"unfolding Supp_defapply(auto)apply(drule_tac x="supp t" in spec)apply(auto simp add: equ_refl)donelemma supp_subst: shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s" by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)lemma supp_beta: "x \<longrightarrow>b r \<Longrightarrow> supp r \<subseteq> supp x" apply (induct rule: beta.induct) apply (simp_all add: lam.supp) apply blast+ using supp_subst by blastlemma supp_beta_star: "x \<longrightarrow>b* r \<Longrightarrow> supp r \<subseteq> supp x" apply (erule beta_star.induct) apply auto using supp_beta by blastlemma supp_equ: "x \<approx> y \<Longrightarrow> \<exists>z. z \<approx> x \<and> supp z \<subseteq> supp x \<inter> supp y" unfolding equ_def apply (simp (no_asm) only: equ_def[symmetric]) apply (elim exE) apply (rule_tac x=r in exI) apply rule apply (metis bs1 equ_def) using supp_beta_star by blastlemma supp_psubset: "Supp x \<subset> supp x \<Longrightarrow> \<exists>t. t \<approx> x \<and> supp t \<subset> supp x"proof - assume "Supp x \<subset> supp x" then obtain a where "a \<in> supp x" "a \<notin> Supp x" by blast then obtain y where nin: "y \<approx> x" "a \<notin> supp y" unfolding Supp_def by blast then obtain t where eq: "t \<approx> x" "supp t \<subseteq> supp x \<inter> supp y" using supp_equ equ_sym by blast then have "supp t \<subset> supp x" using nin by (metis `(a\<Colon>atom) \<in> supp (x\<Colon>lam)` le_infE psubset_eq set_rev_mp) then show "\<exists>t. t \<approx> x \<and> supp t \<subset> supp x" using eq by blastqedlemma Supp_exists: "\<exists>t. supp t = Supp t \<and> t \<approx> x"proof - have "\<And>fs x. supp x = fs \<Longrightarrow> \<exists>t. supp t = Supp t \<and> t \<approx> x" proof - fix fs show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" proof (cases "finite fs") case True assume fs: "finite fs" then show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" proof (induct fs rule: finite_psubset_induct, clarify) fix A :: "atom set" fix x :: lam assume IH: "\<And>B xa. \<lbrakk>B \<subset> supp x; supp xa = B\<rbrakk> \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> xa" show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" proof (cases "supp x = Supp x") assume "supp x = Supp x" then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by (rule_tac x="x" in exI) (simp add: equ_refl) next assume "supp x \<noteq> Supp x" then have "Supp x \<subset> supp x" using Supp_supp by blast then obtain y where a1: "supp y \<subset> supp x" "y \<approx> x" using supp_psubset by blast then obtain t where "supp t = Supp t \<and> t \<approx> y" using IH[of "supp y" y] by blast then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" using a1 equ_trans by blast qed qed next case False fix x :: lam assume "supp x = fs" "infinite fs" then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by (auto simp add: finite_supp) qed simp qed then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by blastqedlemma subst3: "x \<noteq> y \<and> atom x \<notin> Supp s \<Longrightarrow> Lam [x]. t [y ::= s] \<approx> Lam [x]. (t [y ::= s])"proof - assume as: "x \<noteq> y \<and> atom x \<notin> Supp s" obtain s' where s: "supp s' = Supp s'" "s' \<approx> s" using Supp_exists[of s] by blast then have lhs: "Lam [x]. t [y ::= s] \<approx> Lam [x]. t [y ::= s']" using subst_rsp_pre equ_refl equ_sym by blast have supp: "Supp s' = Supp s" using Supp_rsp s(2) by blast have lhs_rhs: "Lam [x]. t [y ::= s'] = Lam [x]. (t [y ::= s'])" by (simp add: fresh_def supp_Pair s supp as supp_at_base) have "t [y ::= s'] \<approx> t [y ::= s]" using subst_rsp_pre[OF equ_refl s(2)] . with Lam_rsp have rhs: "Lam [x]. (t [y ::= s']) \<approx> Lam [x]. (t [y ::= s])" . show ?thesis using lhs[unfolded lhs_rhs] rhs equ_trans by blastqedthm subst3[quot_lifted]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 blastqedlemma [eqvt]: "(p \<bullet> (a \<approx> b)) = ((p \<bullet> a) \<approx> (p \<bullet> b))" unfolding equ_def by perm_simp rulelemma [eqvt]: "p \<bullet> (Supp x) = Supp (p \<bullet> x)" unfolding Supp_def by perm_simp rulelemmas 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 donelemma 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 autolemma "supp (QVar n) = {atom n}" unfolding supp_def apply simp unfolding qlam_eq_iff apply (fold supp_def) apply (simp add: supp_at_base) doneend