1 theory BetaCR

     2 imports CR

     3 begin

     4 

     5 (* TODO1: Does not work:*)

     6 

     7 (* equivariance beta_star *)

     8 

     9 (* proved manually below. *)

    10 

    11 lemma eqvt_helper: "x1 \<longrightarrow>b* x2 \<Longrightarrow>  (p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2)"

    12   by (erule beta_star.induct)

    13      (metis beta.eqvt bs2 bs1)+

    14 

    15 lemma [eqvt]: "p \<bullet> (x1 \<longrightarrow>b* x2) = ((p \<bullet> x1) \<longrightarrow>b* (p \<bullet> x2))"

    16   apply rule

    17   apply (drule permute_boolE)

    18   apply (erule eqvt_helper)

    19   apply (intro permute_boolI)

    20   apply (drule_tac p="-p" in eqvt_helper)

    21   by simp

    22 

    23 definition

    24   equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _")

    25 where

    26   "t \<approx> s \<longleftrightarrow> (\<exists>r. t \<longrightarrow>b* r \<and> s \<longrightarrow>b* r)"

    27 

    28 lemma equ_refl:

    29   shows "t \<approx> t"

    30   unfolding equ_def by auto

    31 

    32 lemma equ_sym:

    33   assumes "t \<approx> s"

    34   shows "s \<approx> t"

    35   using assms unfolding equ_def

    36   by auto

    37 

    38 lemma equ_trans:

    39   assumes "A \<approx> B" "B \<approx> C"

    40   shows "A \<approx> C"

    41   using assms unfolding equ_def

    42 proof (elim exE conjE)

    43   fix D E

    44   assume a: "A \<longrightarrow>b* D" "B \<longrightarrow>b* D" "B \<longrightarrow>b* E" "C \<longrightarrow>b* E"

    45   then obtain F where "D \<longrightarrow>b* F" "E \<longrightarrow>b* F" using CR_for_Beta_star by blast

    46   then have "A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" using a bs3 by blast

    47   then show "\<exists>F. A \<longrightarrow>b* F \<and> C \<longrightarrow>b* F" by blast

    48 qed

    49 

    50 lemma App_beta: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> App A C \<longrightarrow>b* App B D"

    51   apply (erule beta_star.induct)

    52   apply auto

    53   apply (erule beta_star.induct)

    54   apply auto

    55   done

    56 

    57 lemma Lam_beta: "A \<longrightarrow>b* B \<Longrightarrow> Lam [x]. A \<longrightarrow>b* Lam [x]. B"

    58   by (erule beta_star.induct) auto

    59 

    60 lemma Lam_rsp: "A \<approx> B \<Longrightarrow> Lam [x]. A \<approx> Lam [x]. B"

    61   unfolding equ_def

    62   apply auto

    63   apply (rule_tac x="Lam [x]. r" in exI)

    64   apply (auto simp add: Lam_beta)

    65   done

    66 

    67 lemma [quot_respect]:

    68   shows "(op = ===> equ) Var Var"

    69   and   "(equ ===> equ ===> equ) App App"

    70   and   "(op = ===> equ ===> equ) CR.Lam CR.Lam"

    71   unfolding fun_rel_def equ_def

    72   apply auto

    73   apply (rule_tac x="App r ra" in exI)

    74   apply (auto simp add: App_beta)

    75   apply (rule_tac x="Lam [x]. r" in exI)

    76   apply (auto simp add: Lam_beta)

    77   done

    78 

    79 lemma beta_subst1_pre: "B \<longrightarrow>b C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"

    80   by (nominal_induct A avoiding: x B C rule: lam.strong_induct)

    81      (auto simp add: App_beta Lam_beta)

    82 

    83 lemma beta_subst1: "B \<longrightarrow>b* C \<Longrightarrow> A [x ::= B] \<longrightarrow>b* A [x ::= C]"

    84   apply (erule beta_star.induct)

    85   apply auto

    86   apply (subgoal_tac "A [x ::= M2] \<longrightarrow>b* A [x ::= M3]")

    87   apply (rotate_tac 1)

    88   apply (erule bs3)

    89   apply assumption

    90   apply (simp add: beta_subst1_pre)

    91   done

    92 

    93 lemma beta_subst2_pre:

    94   assumes "A \<longrightarrow>b B" shows "A [x ::= C] \<longrightarrow>b* B [x ::= C]"

    95   using assms

    96   apply (nominal_induct avoiding: x C rule: beta.strong_induct)

    97   apply (auto simp add: App_beta fresh_star_def fresh_Pair Lam_beta)[3]

    98   apply (subst substitution_lemma)

    99   apply (auto simp add: fresh_star_def fresh_Pair fresh_at_base)[2]

   100   apply (auto simp add: fresh_star_def fresh_Pair)

   101   apply (rule beta_star.intros)

   102   defer

   103   apply (subst beta.intros)

   104   apply (auto simp add: fresh_fact)

   105   done

   106 

   107 lemma beta_subst2: "A \<longrightarrow>b* B \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= C]"

   108   apply (erule beta_star.induct)

   109   apply auto

   110   apply (subgoal_tac "M2[x ::= C] \<longrightarrow>b* M3[x ::= C]")

   111   apply (rotate_tac 1)

   112   apply (erule bs3)

   113   apply assumption

   114   apply (simp add: beta_subst2_pre)

   115   done

   116 

   117 lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]"

   118   using beta_subst1 beta_subst2 bs3 by metis

   119 

   120 lemma subst_rsp_pre:

   121   "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]"

   122   unfolding equ_def

   123   apply auto

   124   apply (rule_tac x="r [xa ::= ra]" in exI)

   125   apply (simp add: beta_subst)

   126   done

   127 

   128 lemma [quot_respect]:

   129   shows "(equ ===> op = ===> equ ===> equ) subst subst"

   130 unfolding fun_rel_def by (auto simp add: subst_rsp_pre)

   131 

   132 lemma [quot_respect]:

   133   shows "(op = ===> equ ===> equ) permute permute"

   134   unfolding fun_rel_def equ_def

   135   apply (auto intro: eqvts)

   136   apply (rule_tac x="x \<bullet> r" in exI)

   137   using eqvts(1) permute_boolI by metis

   138 

   139 quotient_type qlam = lam / equ

   140   by (auto intro!: equivpI reflpI sympI transpI simp add: equ_refl equ_sym)

   141      (erule equ_trans, assumption)

   142 

   143 quotient_definition "QVar::name \<Rightarrow> qlam" is Var

   144 quotient_definition "QApp::qlam \<Rightarrow> qlam \<Rightarrow> qlam" is App

   145 quotient_definition QLam ("QLam [_]._")

   146   where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is CR.Lam

   147 

   148 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]

   149 lemmas qlam_induct = lam.induct[quot_lifted]

   150 

   151 instantiation qlam :: pt

   152 begin

   153 

   154 quotient_definition "permute_qlam::perm \<Rightarrow> qlam \<Rightarrow> qlam" 

   155   is "permute::perm \<Rightarrow> lam \<Rightarrow> lam"

   156 

   157 instance

   158 apply default

   159 apply(descending)

   160 apply(simp)

   161 apply(rule equ_refl)

   162 apply(descending)

   163 apply(simp)

   164 apply(rule equ_refl)

   165 done

   166 

   167 end

   168 

   169 lemma qlam_perm[simp, eqvt]:

   170   shows "p \<bullet> (QVar x) = QVar (p \<bullet> x)"

   171   and "p \<bullet> (QApp t s) = QApp (p \<bullet> t) (p \<bullet> s)"

   172   and "p \<bullet> (QLam [x].t) = QLam [p \<bullet> x].(p \<bullet> t)"

   173   by(descending, simp add: equ_refl)+

   174 

   175 lemma qlam_supports:

   176   shows "{atom x} supports (QVar x)"

   177   and   "supp (t, s) supports (QApp t s)"

   178   and   "supp (x, t) supports (QLam [x].t)"

   179 unfolding supports_def fresh_def[symmetric]

   180 by (auto simp add: swap_fresh_fresh)

   181 

   182 lemma qlam_fs:

   183   fixes t::"qlam"

   184   shows "finite (supp t)"

   185 apply(induct t rule: qlam_induct)

   186 apply(rule supports_finite)

   187 apply(rule qlam_supports)

   188 apply(simp)

   189 apply(rule supports_finite)

   190 apply(rule qlam_supports)

   191 apply(simp add: supp_Pair)

   192 apply(rule supports_finite)

   193 apply(rule qlam_supports)

   194 apply(simp add: supp_Pair finite_supp)

   195 done

   196 

   197 instantiation qlam :: fs

   198 begin

   199 

   200 instance

   201 apply(default)

   202 apply(rule qlam_fs)

   203 done

   204 

   205 end

   206 

   207 quotient_definition subst_qlam ("_[_ ::q= _]")

   208   where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  

   209 

   210 definition

   211   "Supp t = \<Inter>{supp s | s. s \<approx> t}"

   212 

   213 lemma Supp_rsp:

   214   "a \<approx> b \<Longrightarrow> Supp a = Supp b"

   215   unfolding Supp_def

   216   apply(rule_tac f="Inter" in arg_cong)

   217   apply(auto)

   218   apply (metis equ_trans)

   219   by (metis equivp_def qlam_equivp)

   220 

   221 lemma [quot_respect]:

   222   shows "(equ ===> op=) Supp Supp"

   223   unfolding fun_rel_def by (auto simp add: Supp_rsp)

   224 

   225 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 

   226   is "Supp::lam \<Rightarrow> atom set"

   227 

   228 lemma Supp_supp:

   229   "Supp t \<subseteq> supp t"

   230 unfolding Supp_def

   231 apply(auto)

   232 apply(drule_tac x="supp t" in spec)

   233 apply(auto simp add: equ_refl)

   234 done

   235 

   236 lemma supp_subst:

   237   shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"

   238   by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)

   239 

   240 lemma supp_beta: "x \<longrightarrow>b r \<Longrightarrow> supp r \<subseteq> supp x"

   241   apply (induct rule: beta.induct)

   242   apply (simp_all add: lam.supp)

   243   apply blast+

   244   using supp_subst by blast

   245 

   246 lemma supp_beta_star: "x \<longrightarrow>b* r \<Longrightarrow> supp r \<subseteq> supp x"

   247   apply (erule beta_star.induct)

   248   apply auto

   249   using supp_beta by blast

   250 

   251 lemma supp_equ: "x \<approx> y \<Longrightarrow> \<exists>z. z \<approx> x \<and> supp z \<subseteq> supp x \<inter> supp y"

   252   unfolding equ_def

   253   apply (simp (no_asm) only: equ_def[symmetric])

   254   apply (elim exE)

   255   apply (rule_tac x=r in exI)

   256   apply rule

   257   apply (metis bs1 equ_def)

   258   using supp_beta_star by blast

   259 

   260 lemma supp_psubset: "Supp x \<subset> supp x \<Longrightarrow> \<exists>t. t \<approx> x \<and> supp t \<subset> supp x"

   261 proof -

   262   assume "Supp x \<subset> supp x"

   263   then obtain a where "a \<in> supp x" "a \<notin> Supp x" by blast

   264   then obtain y where nin: "y \<approx> x" "a \<notin> supp y" unfolding Supp_def by blast

   265   then obtain t where eq: "t \<approx> x" "supp t \<subseteq> supp x \<inter> supp y"

   266     using supp_equ equ_sym by blast

   267   then have "supp t \<subset> supp x" using nin

   268     by (metis `(a\<Colon>atom) \<in> supp (x\<Colon>lam)` le_infE psubset_eq set_rev_mp)

   269   then show "\<exists>t. t \<approx> x \<and> supp t \<subset> supp x" using eq by blast

   270 qed

   271 

   272 lemma Supp_exists: "\<exists>t. supp t = Supp t \<and> t \<approx> x"

   273 proof -

   274   have "\<And>fs x. supp x = fs \<Longrightarrow> \<exists>t. supp t = Supp t \<and> t \<approx> x"

   275   proof -

   276     fix fs

   277     show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   278     proof (cases "finite fs")

   279       case True

   280       assume fs: "finite fs"

   281       then show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   282       proof (induct fs rule: finite_psubset_induct, clarify)

   283         fix A :: "atom set" fix x :: lam

   284         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"

   285         show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   286         proof (cases "supp x = Supp x")

   287           assume "supp x = Supp x"

   288           then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   289             by (rule_tac x="x" in exI) (simp add: equ_refl)

   290         next

   291           assume "supp x \<noteq> Supp x"

   292           then have "Supp x \<subset> supp x" using Supp_supp by blast

   293           then obtain y where a1: "supp y \<subset> supp x" "y \<approx> x"

   294             using supp_psubset by blast

   295           then obtain t where "supp t = Supp t \<and> t \<approx> y"

   296             using IH[of "supp y" y] by blast

   297           then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" using a1 equ_trans

   298             by blast

   299         qed

   300       qed

   301     next

   302       case False

   303       fix x :: lam

   304       assume "supp x = fs" "infinite fs"

   305       then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   306         by (auto simp add: finite_supp)

   307     qed simp

   308   qed

   309   then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by blast

   310 qed

   311 

   312 lemma subst3: "x \<noteq> y \<and> atom x \<notin> Supp s \<Longrightarrow> Lam [x]. t [y ::= s] \<approx> Lam [x]. (t [y ::= s])"

   313 proof -

   314   assume as: "x \<noteq> y \<and> atom x \<notin> Supp s"

   315   obtain s' where s: "supp s' = Supp s'" "s' \<approx> s" using Supp_exists[of s] by blast

   316   then have lhs: "Lam [x]. t [y ::= s] \<approx> Lam [x]. t [y ::= s']" using subst_rsp_pre equ_refl equ_sym by blast

   317   have supp: "Supp s' = Supp s" using Supp_rsp s(2) by blast

   318   have lhs_rhs: "Lam [x]. t [y ::= s'] = Lam [x]. (t [y ::= s'])"

   319     by (simp add: fresh_def supp_Pair s supp as supp_at_base)

   320   have "t [y ::= s'] \<approx> t [y ::= s]"

   321     using subst_rsp_pre[OF equ_refl s(2)] .

   322   with Lam_rsp have rhs: "Lam [x]. (t [y ::= s']) \<approx> Lam [x]. (t [y ::= s])" .

   323   show ?thesis 

   324     using lhs[unfolded lhs_rhs] rhs equ_trans by blast

   325 qed

   326 

   327 thm subst3[quot_lifted]

   328 

   329 lemma Supp_Lam:

   330   "atom a \<notin> Supp (Lam [a].t)"

   331 proof -

   332   have "atom a \<notin> supp (Lam [a].t)" by (simp add: lam.supp)

   333   then show ?thesis using Supp_supp

   334     by blast

   335 qed

   336 

   337 lemma [eqvt]: "(p \<bullet> (a \<approx> b)) = ((p \<bullet> a) \<approx> (p \<bullet> b))"

   338   unfolding equ_def

   339   by perm_simp rule

   340 

   341 lemma [eqvt]: "p \<bullet> (Supp x) = Supp (p \<bullet> x)"

   342   unfolding Supp_def

   343   by perm_simp rule

   344 

   345 lemmas s = Supp_Lam[quot_lifted]

   346 

   347 lemma var_beta_pre: "s \<longrightarrow>b* r \<Longrightarrow> s = Var name \<Longrightarrow> r = Var name"

   348   apply (induct rule: beta_star.induct)

   349   apply simp

   350   apply (subgoal_tac "M2 = Var name")

   351   apply (thin_tac "M1 \<longrightarrow>b* M2")

   352   apply (thin_tac "M1 = Var name")

   353   apply (thin_tac "M1 = Var name \<Longrightarrow> M2 = Var name")

   354   defer

   355   apply simp

   356   apply (erule_tac beta.cases)

   357   apply simp_all

   358   done

   359 

   360 lemma var_beta: "Var name \<longrightarrow>b* r \<longleftrightarrow> r = Var name"

   361   by (auto simp add: var_beta_pre)

   362 

   363 lemma qlam_eq_iff:

   364   "(QVar n = QVar m) = (n = m)"

   365   apply descending unfolding equ_def var_beta by auto

   366 

   367 lemma "supp (QVar n) = {atom n}"

   368   unfolding supp_def

   369   apply simp

   370   unfolding qlam_eq_iff

   371   apply (fold supp_def)

   372   apply (simp add: supp_at_base)

   373   done

   374 

   375 end

   376 

   377 

   378