1 theory BetaCR

     2 imports 

     3   "../Nominal2"

     4 begin

     5 

     6 atom_decl name

     7 

     8 nominal_datatype lam =

     9   Var "name"

    10 | App "lam" "lam"

    11 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

    12 

    13 nominal_primrec

    14   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)

    15 where

    16   "(Var x)[y ::= s] = (if x = y then s else (Var x))"

    17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

    18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

    19   unfolding eqvt_def subst_graph_def

    20   apply (rule, perm_simp, rule)

    21   apply(rule TrueI)

    22   apply(auto simp add: lam.distinct lam.eq_iff)

    23   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

    24   apply(blast)+

    25   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    26   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    27   apply(simp_all add: Abs_fresh_iff)

    28   apply(simp add: fresh_star_def fresh_Pair)

    29   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    30   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    31 done

    32 

    33 termination (eqvt)

    34   by lexicographic_order

    35 

    36 lemma fresh_fact:

    37   fixes z::"name"

    38   assumes a: "atom z \<sharp> s"

    39       and b: "z = y \<or> atom z \<sharp> t"

    40   shows "atom z \<sharp> t[y ::= s]"

    41   using a b

    42   by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

    43       (auto simp add: lam.fresh fresh_at_base)

    44 

    45 inductive 

    46   beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)

    47 where

    48   b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"

    49 | b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"

    50 | b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"

    51 | b4[intro]: "atom x \<sharp> s \<Longrightarrow> App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"

    52 

    53 equivariance beta

    54 

    55 (* HERE 1 *)

    56 nominal_inductive beta

    57   avoids b3: x

    58   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

    59 

    60 (* This also works, but we cannot have them together: *)

    61 (*nominal_inductive beta

    62   avoids b4: x

    63   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)*)

    64 

    65 (* But I need a combination, possibly with an 'and' syntax:

    66 nominal_inductive beta

    67   avoids b3: x and b4: x

    68   by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact)

    69 *)

    70 

    71 (* The combination should look like this: *)

    72 lemma beta_strong_induct:

    73   assumes "x1 \<longrightarrow>b x2"

    74   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)"

    75   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)"

    76   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)"

    77   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])"

    78   shows "P (c\<Colon>'a\<Colon>fs) x1 x2"

    79   sorry

    80 

    81 inductive

    82   beta_star :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b* _" [80,80] 80)

    83 where

    84   bs1[intro, simp]: "M \<longrightarrow>b* M"

    85 | bs2[intro]: "\<lbrakk>M1\<longrightarrow>b* M2; M2 \<longrightarrow>b M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>b* M3"

    86 

    87 lemma beta_star_trans:

    88   assumes "A \<longrightarrow>b* B"

    89   and     "B \<longrightarrow>b* C"

    90   shows   "A \<longrightarrow>b* C"

    91   using assms(2) assms(1)

    92   by induct auto

    93 

    94 (* HERE 2: Does not work:*)

    95 

    96 (* equivariance beta_star *)

    97 

    98 (* proved manually below. *)

    99 

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

   101   apply (erule beta_star.induct)

   102   apply auto

   103   using eqvt(1) bs2

   104   by blast

   105 

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

   107   apply rule

   108   apply (drule permute_boolE)

   109   apply (erule eqvt_helper)

   110   apply (intro permute_boolI)

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

   112   by simp

   113 

   114 definition

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

   116 where

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

   118 

   119 lemma equ_refl:

   120   shows "t \<approx> t"

   121   unfolding equ_def by auto

   122 

   123 lemma equ_sym:

   124   assumes "t \<approx> s"

   125   shows "s \<approx> t"

   126   using assms unfolding equ_def

   127   by auto

   128 

   129 (* can be ported from nominal1 *)

   130 lemma cr:

   131   assumes "t \<longrightarrow>b* t1" and "t \<longrightarrow>b* t2" shows "\<exists>t3. t1 \<longrightarrow>b* t3 \<and> t2 \<longrightarrow>b* t3"

   132   sorry

   133 

   134 lemma equ_trans:

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

   136   shows "A \<approx> C"

   137   using assms unfolding equ_def

   138 proof (elim exE conjE)

   139   fix D E

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

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

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

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

   144 qed

   145 

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

   147   apply (erule beta_star.induct)

   148   apply auto

   149   apply (erule beta_star.induct)

   150   apply auto

   151   done

   152 

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

   154   by (erule beta_star.induct) auto

   155 

   156 lemma [quot_respect]:

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

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

   159   and   "(op = ===> equ ===> equ) BetaCR.Lam BetaCR.Lam"

   160   unfolding fun_rel_def equ_def

   161   apply auto

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

   163   apply (auto simp add: App_beta)

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

   165   apply (auto simp add: Lam_beta)

   166   done

   167 

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

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

   170      (auto simp add: App_beta Lam_beta)

   171 

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

   173   apply (erule beta_star.induct)

   174   apply auto

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

   176   apply (rotate_tac 1)

   177   apply (erule beta_star_trans)

   178   apply assumption

   179   apply (simp add: beta_subst1_pre)

   180   done

   181 

   182 lemma forget:

   183   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

   184   by (nominal_induct t avoiding: x s rule: lam.strong_induct)

   185      (auto simp add: lam.fresh fresh_at_base)

   186 

   187 lemma substitution_lemma:

   188   assumes a: "x \<noteq> y" "atom x \<sharp> u"

   189   shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]"

   190   using a

   191   by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)

   192      (auto simp add: fresh_fact forget)

   193 

   194 lemma beta_subst2_pre:

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

   196   using assms

   197 (* HERE 3: nominal_induct doesn't work - leaves the assumption *)

   198 (*  apply (nominal_induct avoiding: x C rule: beta_strong_induct)*)

   199   apply -

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

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

   202   apply (subst substitution_lemma)

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

   204   apply (auto simp add: fresh_star_def fresh_Pair)

   205   apply (rule beta_star.intros)

   206   defer

   207   apply (subst beta.intros)

   208   apply (auto simp add: fresh_fact)

   209   done

   210 

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

   212   apply (erule beta_star.induct)

   213   apply auto

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

   215   apply (rotate_tac 1)

   216   apply (erule beta_star_trans)

   217   apply assumption

   218   apply (simp add: beta_subst2_pre)

   219   done

   220 

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

   222   using beta_subst1 beta_subst2 beta_star_trans by metis

   223 

   224 lemma [quot_respect]:

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

   226 unfolding fun_rel_def equ_def

   227 apply auto

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

   229 apply (simp add: beta_subst)

   230 done

   231 

   232 lemma [quot_respect]:

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

   234   unfolding fun_rel_def equ_def

   235   apply (auto intro: eqvts)

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

   237   using eqvts(1) permute_boolI by metis

   238 

   239 quotient_type qlam = lam / equ

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

   241      (erule equ_trans, assumption)

   242 

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

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

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

   246   where "QLam::name \<Rightarrow> qlam \<Rightarrow> qlam" is Beta.Lam

   247 

   248 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]

   249 lemmas qlam_induct = lam.induct[quot_lifted]

   250 

   251 instantiation qlam :: pt

   252 begin

   253 

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

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

   256 

   257 instance

   258 apply default

   259 apply(descending)

   260 apply(simp)

   261 apply(rule equ_refl)

   262 apply(descending)

   263 apply(simp)

   264 apply(rule equ_refl)

   265 done

   266 

   267 end

   268 

   269 lemma qlam_perm[simp, eqvt]:

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

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

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

   273   by(descending, simp add: equ_refl)+

   274 

   275 lemma qlam_supports:

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

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

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

   279 unfolding supports_def fresh_def[symmetric]

   280 by (auto simp add: swap_fresh_fresh)

   281 

   282 lemma qlam_fs:

   283   fixes t::"qlam"

   284   shows "finite (supp t)"

   285 apply(induct t rule: qlam_induct)

   286 apply(rule supports_finite)

   287 apply(rule qlam_supports)

   288 apply(simp)

   289 apply(rule supports_finite)

   290 apply(rule qlam_supports)

   291 apply(simp add: supp_Pair)

   292 apply(rule supports_finite)

   293 apply(rule qlam_supports)

   294 apply(simp add: supp_Pair finite_supp)

   295 done

   296 

   297 instantiation qlam :: fs

   298 begin

   299 

   300 instance

   301 apply(default)

   302 apply(rule qlam_fs)

   303 done

   304 

   305 end

   306 

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

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

   309 

   310 lemmas qsubst = subst.simps(1-2)[quot_lifted]

   311 

   312 definition

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

   314 

   315 lemma [quot_respect]:

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

   317   unfolding fun_rel_def Supp_def

   318   apply(intro allI impI)

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

   320   apply(auto)

   321   apply (metis equ_trans)

   322   by (metis equivp_def qlam_equivp)

   323 

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

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

   326 

   327 lemma Supp_supp:

   328   "Supp t \<subseteq> supp t"

   329 unfolding Supp_def

   330 apply(auto)

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

   332 apply(auto simp add: equ_refl)

   333 done

   334 

   335 lemma Supp_Lam:

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

   337 proof -

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

   339   then show ?thesis using Supp_supp

   340     by blast

   341 qed

   342 

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

   344   unfolding equ_def

   345   by perm_simp rule

   346 

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

   348   unfolding Supp_def

   349   by perm_simp rule

   350 

   351 lemmas s = Supp_Lam[quot_lifted]

   352 

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

   354   apply (induct rule: beta_star.induct)

   355   apply simp

   356   apply (subgoal_tac "M2 = Var name")

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

   358   apply (thin_tac "M1 = Var name")

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

   360   defer

   361   apply simp

   362   apply (erule_tac beta.cases)

   363   apply simp_all

   364   done

   365 

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

   367   by (auto simp add: var_beta_pre)

   368 

   369 lemma qlam_eq_iff:

   370   "(QVar n = QVar m) = (n = m)"

   371   apply descending unfolding equ_def var_beta by auto

   372 

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

   374   unfolding supp_def

   375   apply simp

   376   unfolding qlam_eq_iff

   377   apply (fold supp_def)

   378   apply (simp add: supp_at_base)

   379   done

   380 

   381 end

   382 

   383 

   384