1 theory Beta

     2 imports 

     3   "../Nominal2"

     4 begin

     5 

     6 

     7 atom_decl name

     8 

     9 

    10 nominal_datatype lam =

    11   Var "name"

    12 | App "lam" "lam"

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

    14 

    15 section {* capture-avoiding substitution *}

    16 

    17 nominal_primrec

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

    19 where

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

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

    22 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

    23   unfolding eqvt_def subst_graph_def

    24   apply (rule, perm_simp, rule)

    25   apply(rule TrueI)

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

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

    28   apply(blast)+

    29   apply(simp_all add: fresh_star_def fresh_Pair_elim)

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

    31   apply(simp_all add: Abs_fresh_iff)

    32   apply(simp add: fresh_star_def fresh_Pair)

    33   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    34   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    35 done

    36 

    37 termination (eqvt)

    38   by lexicographic_order

    39 

    40 lemma forget:

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

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

    43      (auto simp add: lam.fresh fresh_at_base)

    44 

    45 lemma fresh_fact:

    46   fixes z::"name"

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

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

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

    50   using a b

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

    52      (auto simp add: lam.fresh fresh_at_base)

    53 

    54 lemma substitution_lemma:  

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

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

    57 using a 

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

    59    (auto simp add: fresh_fact forget)

    60 

    61 inductive

    62   beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _")

    63 where

    64   beta_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<rightarrow> t[x ::= s]"

    65 | beta_Lam:   "t \<rightarrow> s \<Longrightarrow> Lam [x].t \<rightarrow> Lam [x].s"

    66 | beta_App1:  "t \<rightarrow> s \<Longrightarrow> App t u \<rightarrow> App s u"

    67 | beta_App2:  "t \<rightarrow> s \<Longrightarrow> App u t \<rightarrow> App u s"

    68 

    69 equivariance beta

    70 

    71 nominal_inductive beta

    72   avoids beta_beta: "x" 

    73        | beta_Lam: "x"

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

    75 

    76 inductive

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

    78 where

    79   equ_beta:  "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<approx> t[x ::= s]"

    80 | equ_refl:  "t \<approx> t"

    81 | equ_sym:   "t \<approx> s \<Longrightarrow> s \<approx> t"

    82 | equ_trans: "\<lbrakk>t1 \<approx> t2; t2 \<approx> t3\<rbrakk> \<Longrightarrow> t1 \<approx> t3"

    83 | equ_Lam:   "t \<approx> s \<Longrightarrow> Lam [x].t \<approx> Lam [x].s"

    84 | equ_App1:  "t \<approx> s \<Longrightarrow> App t u \<approx> App s u"

    85 | equ_App2:  "t \<approx> s \<Longrightarrow> App u t \<approx> App u s"

    86 

    87 equivariance equ

    88 

    89 nominal_inductive equ

    90   avoids equ_beta: "x" 

    91        | equ_Lam: "x"

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

    93 

    94 inductive

    95   equ2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx>2 _")

    96 where

    97   equ2_beta1:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) t2 \<approx>2 s1[x ::= s2]"

    98 | equ2_beta2:  "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2  s2\<rbrakk> \<Longrightarrow> s1[x ::= s2] \<approx>2 App (Lam [x].t1) t2"

    99 | equ2_Var:   "Var x \<approx>2 Var x"

   100 | equ2_Lam:   "t \<approx>2 s \<Longrightarrow> Lam [x].t \<approx>2 Lam [x].s"

   101 | equ2_App:   "\<lbrakk>t1 \<approx>2 s1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> App t1 t2 \<approx>2 App s1 s2"

   102 

   103 equivariance equ2

   104 

   105 nominal_inductive equ2

   106   avoids equ2_beta1: "x"

   107        | equ2_beta2: "x" 

   108        | equ2_Lam: "x"

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

   110 

   111 lemma equ2_refl:

   112   fixes t::"lam"

   113   shows "t \<approx>2 t"

   114 apply(induct t rule: lam.induct)

   115 apply(auto intro: equ2.intros)

   116 done

   117 

   118 lemma equ2_symm:

   119   fixes t s::"lam"

   120   assumes "t \<approx>2 s"

   121   shows "s \<approx>2 t"

   122 using assms

   123 apply(induct)

   124 apply(auto intro: equ2.intros)

   125 done

   126 

   127 lemma equ2_trans:

   128   fixes t1 t2 t3::"lam"

   129   assumes "t1 \<approx>2 t2" "t2 \<approx>2 t3"

   130   shows "t1 \<approx>2 t3"

   131 using assms

   132 apply(nominal_induct t1 t2 avoiding: t3 rule: equ2.strong_induct)

   133 defer

   134 defer

   135 apply(erule equ2.cases)

   136 apply(auto)

   137 apply(rule equ2_beta2)

   138 apply(simp)

   139 apply(simp)

   140 apply(simp)

   141 apply(rule equ2_refl)

   142 defer

   143 apply(rotate_tac 4)

   144 apply(erule equ2.cases)

   145 apply(auto)

   146 oops

   147 

   148 lemma "a \<noteq> x \<Longrightarrow> x \<noteq> y \<Longrightarrow> y \<noteq> a \<Longrightarrow> y \<noteq> b \<Longrightarrow> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx> App (Var b) (Var a))"

   149   apply (rule equ_trans)

   150   apply (rule equ_App1)

   151   apply (rule equ_beta)

   152   apply (simp add: lam.fresh fresh_at_base)

   153   apply (subst subst.simps)

   154   apply (simp add: lam.fresh fresh_at_base)+

   155   apply (rule equ_trans)

   156   apply (rule equ_beta)

   157   apply (simp add: lam.fresh fresh_at_base)

   158   apply (simp add: equ_refl)

   159   done

   160 

   161 lemma "\<not> (Var b \<approx>2 Var a) \<Longrightarrow> \<not> (App (App (Lam[x]. Lam[y]. (App (Var y) (Var x))) (Var a)) (Var b) \<approx>2 App (Var b) (Var a))"

   162   apply rule

   163   apply (erule equ2.cases)

   164   apply auto

   165   done

   166 

   167 lemma [quot_respect]:

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

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

   170   and   "(op = ===> equ ===> equ) Beta.Lam Beta.Lam"

   171 unfolding fun_rel_def

   172 by (auto intro: equ.intros)

   173 

   174 lemma equ_subst1:

   175   assumes "t \<approx> s"

   176   shows "t[x ::= u] \<approx> s[x ::= u]"

   177 using assms

   178 apply(nominal_induct avoiding: x u rule: equ.strong_induct)

   179 apply(simp)

   180 apply(rule equ_trans)

   181 apply(rule equ_beta)

   182 apply(simp add: fresh_fact)

   183 apply(subst (2) substitution_lemma)

   184 apply(simp add: fresh_at_base)

   185 apply(simp)

   186 apply(rule equ_refl)

   187 apply(rule equ_refl)

   188 apply(auto intro: equ_sym)[1]

   189 apply(blast intro: equ_trans)

   190 apply(simp add: equ_Lam)

   191 apply(simp add: equ_App1)

   192 apply(simp add: equ_App2)

   193 done

   194 

   195 lemma equ_subst2:

   196   assumes "t \<approx> s"

   197   shows "u[x ::= t] \<approx> u[x ::= s]"

   198 using assms

   199 apply(nominal_induct u avoiding: x t s rule: lam.strong_induct)

   200 apply(simp add: equ_refl)

   201 apply(simp)

   202 apply(smt equ_App1 equ_App2 equ_trans)

   203 apply(simp)

   204 apply(metis equ_Lam)

   205 done

   206 

   207 lemma [quot_respect]:

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

   209 unfolding fun_rel_def

   210 by (metis equ_subst1 equ_subst2 equ_trans)

   211 

   212 lemma [quot_respect]:

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

   214 unfolding fun_rel_def

   215 by (auto intro: eqvts)

   216 

   217 quotient_type qlam = lam / equ

   218 apply(rule equivpI)

   219 apply(rule reflpI)

   220 apply(simp add: equ_refl)

   221 apply(rule sympI)

   222 apply(simp add: equ_sym)

   223 apply(rule transpI)

   224 apply(auto intro: equ_trans)

   225 done

   226 

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

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

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

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

   231 

   232 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]

   233 lemmas qlam_induct = lam.induct[quot_lifted]

   234 

   235 instantiation qlam :: pt

   236 begin

   237 

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

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

   240 

   241 instance

   242 apply default

   243 apply(descending)

   244 apply(simp)

   245 apply(rule equ_refl)

   246 apply(descending)

   247 apply(simp)

   248 apply(rule equ_refl)

   249 done

   250 

   251 end

   252 

   253 lemma qlam_perm[simp]:

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

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

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

   257 apply(descending)

   258 apply(simp add: equ_refl)

   259 apply(descending)

   260 apply(simp add: equ_refl)

   261 apply(descending)

   262 apply(simp add: equ_refl)

   263 done

   264 

   265 lemma qlam_supports:

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

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

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

   269 unfolding supports_def fresh_def[symmetric]

   270 by (auto simp add: swap_fresh_fresh)

   271 

   272 lemma qlam_fs:

   273   fixes t::"qlam"

   274   shows "finite (supp t)"

   275 apply(induct t rule: qlam_induct)

   276 apply(rule supports_finite)

   277 apply(rule qlam_supports)

   278 apply(simp)

   279 apply(rule supports_finite)

   280 apply(rule qlam_supports)

   281 apply(simp add: supp_Pair)

   282 apply(rule supports_finite)

   283 apply(rule qlam_supports)

   284 apply(simp add: supp_Pair finite_supp)

   285 done

   286 

   287 instantiation qlam :: fs

   288 begin

   289 

   290 instance

   291 apply(default)

   292 apply(rule qlam_fs)

   293 done

   294 

   295 end

   296 

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

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

   299 

   300 lemma

   301   "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))"

   302 apply(descending)

   303 apply(simp)

   304 apply(auto intro: equ_refl)

   305 done

   306 

   307 lemma

   308   "(QApp t1 t2)[y ::q= s] = QApp (t1[y ::q= s]) (t2[y ::q= s])"

   309 apply(descending)

   310 apply(simp)

   311 apply(rule equ_refl)

   312 done

   313 

   314 definition

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

   316 

   317 lemma [quot_respect]:

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

   319 unfolding fun_rel_def

   320 unfolding Supp_def

   321 apply(rule allI)+

   322 apply(rule impI)

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

   324 apply(auto)

   325 apply (metis equ_trans)

   326 by (metis equivp_def qlam_equivp)

   327 

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

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

   330 

   331 lemma Supp_supp:

   332   "Supp t \<subseteq> supp t"

   333 unfolding Supp_def

   334 apply(auto)

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

   336 apply(auto simp add: equ_refl)

   337 done

   338 

   339 lemma Supp_Lam:

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

   341 proof -

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

   343   then show ?thesis using Supp_supp

   344     by blast

   345 qed

   346 

   347 lemmas s = Supp_Lam[quot_lifted]

   348 

   349 definition

   350   ssupp :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ ssupp _")

   351 where

   352   "A ssupp x \<equiv> \<forall>p. (\<forall>a \<in> A. (p \<bullet> a) = a) \<longleftrightarrow> (p \<bullet> x) = x"

   353 

   354 lemma ssupp_supports:

   355   "A ssupp x \<Longrightarrow> A supports x"

   356 unfolding ssupp_def supports_def

   357 apply(rule allI)+

   358 apply(drule_tac x="(a \<rightleftharpoons> b)" in spec)

   359 apply(auto)

   360 by (metis swap_atom_simps(3))

   361 

   362 lemma ssupp_supp:

   363   assumes a: "finite A"

   364   and     b: "A ssupp x"

   365   shows "supp x = A"

   366 proof -

   367   { assume 0: "A - supp x \<noteq> {}"

   368     then obtain a where 1: "a \<in> A - supp x" by auto

   369     obtain a' where *: "a' \<in>  UNIV - A" and **: "sort_of a' = sort_of a"

   370       by (rule obtain_atom[OF a]) (auto)  

   371     have "(a \<rightleftharpoons> a') \<bullet> a = a'" using 1 ** * by (auto)

   372     then have w0: "(a \<rightleftharpoons> a') \<bullet> x \<noteq> x"

   373       using b unfolding ssupp_def 

   374       apply -

   375       apply(drule_tac x="(a \<rightleftharpoons> a')" in spec)

   376       apply(auto)

   377       using 1 *

   378       apply(auto)

   379       done

   380     have w1: "a \<sharp> x" unfolding fresh_def using 1 by auto 

   381     have w2: "a' \<sharp> x" using *

   382       apply(rule_tac supports_fresh)

   383       apply(rule ssupp_supports)

   384       apply(rule b)

   385       apply(rule a)

   386       apply(auto)

   387       done

   388     have "False" using w0 w1 w2 by (simp add: swap_fresh_fresh)

   389     then have "supp x = A" by simp }

   390   moreover

   391   { assume "A - supp x = {}"

   392     moreover

   393     have "supp x \<subseteq> A"

   394       apply(rule supp_is_subset)

   395       apply(rule ssupp_supports)

   396       apply(rule b)

   397       apply(rule a)

   398       done

   399     ultimately have "supp x = A"

   400       by blast

   401   }

   402   ultimately show "supp x = A" by blast

   403 qed

   404 

   405 lemma

   406   "(supp x) ssupp x"

   407 unfolding ssupp_def

   408 apply(auto)

   409 apply(rule supp_perm_eq)

   410 apply(simp add: fresh_star_def)

   411 apply(auto)

   412 apply(simp add: fresh_perm)

   413 apply(simp add: fresh_perm[symmetric])

   414 (*Tzevelekos 2008, section 2.1.2 property 2.5*)

   415 oops

   416 

   417 (* The above is not true. Take p=(a\<leftrightarrow>b) and x={a,b}, then the goal is provably false *)

   418 lemma

   419   "b \<noteq> a \<Longrightarrow> \<not>(supp {a :: name,b}) ssupp {a,b}"

   420 unfolding ssupp_def

   421 apply (auto)

   422 apply (intro exI[of _ "(a\<leftrightarrow>b) :: perm"])

   423 apply (subgoal_tac "(a \<leftrightarrow> b) \<bullet> {a, b} = {a, b}")

   424 apply simp

   425 apply (subgoal_tac "supp {a, b} = {atom a, atom b}")

   426 apply (simp add: flip_def)

   427 apply (simp add: supp_of_finite_insert supp_at_base supp_set_empty)

   428 apply blast

   429 by (smt empty_eqvt flip_at_simps(1) flip_at_simps(2) insert_commute insert_eqvt)

   430 

   431 function

   432   qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam"  ("_ [_ ::qq= _]" [90, 90, 90] 90)

   433 where

   434   "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))"

   435 | "(QApp t1 t2)[y ::qq= s] = QApp (t1[y ::qq= s]) (t2[y ::qq= s])"

   436 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y ::qq= s] = QLam [x].(t[y ::qq= s])"

   437 apply(simp_all add:)

   438 oops

   439 

   440 

   441 lemma

   442   assumes a: "Lam [x].t \<approx> s"

   443   shows "\<exists>x' t'. s = Lam [x']. t' \<and> t \<approx> t'"

   444 using a

   445 apply(induct s rule:lam.induct)

   446 apply(erule equ.cases)

   447 apply(auto)

   448 apply(erule equ.cases)

   449 apply(auto)

   450 

   451 

   452 

   453 lemma

   454   "atom x \<sharp> y \<Longrightarrow> atom x \<notin> supp_qlam s \<Longrightarrow> (QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])"

   455 apply(descending)

   456 oops

   457 

   458 

   459 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)"

   460  apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])

   461  apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified])

   462  by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left)

   463 

   464 lemma supports_abs_qlam:

   465   "(supp t) supports (abs_qlam t)"

   466 unfolding supports_def

   467 unfolding fresh_def[symmetric]

   468 apply(auto)

   469 apply(perm_simp)

   470 apply(simp add: swap_fresh_fresh)

   471 done

   472 

   473 lemma rep_qlam_inverse:

   474   "abs_qlam (rep_qlam t) = t"

   475 by (metis Quotient_abs_rep Quotient_qlam)

   476 

   477 lemma supports_rep_qlam:

   478   "supp (rep_qlam t) supports t"

   479 apply(subst (2) rep_qlam_inverse[symmetric])

   480 apply(rule supports_abs_qlam)

   481 done

   482 

   483  lemma supports_qvar:

   484   "{atom x} supports (QVar x)"

   485 apply(subgoal_tac "supp (Var x) supports (abs_qlam (Var x))")

   486 apply(simp add: lam.supp supp_at_base)

   487 defer

   488 apply(rule supports_abs_qlam)

   489 apply(simp add: QVar_def)

   490 done

   491 

   492 section {* Supp *}

   493 

   494 lemma s:

   495   assumes "s \<approx> t"

   496   shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)"

   497 using assms

   498 by (metis Quotient_qlam Quotient_rel_abs)

   499 

   500 lemma ss:

   501   "Supp t supports (abs_qlam t)"

   502 apply(simp only: supports_def)

   503 apply(rule allI)+

   504 apply(rule impI)

   505 apply(rule swap_fresh_fresh)

   506 apply(drule conjunct1)

   507 apply(auto)[1]

   508 apply(simp add: Supp_def)

   509 apply(auto)[1]

   510 apply(simp add: s[symmetric])

   511 apply(rule supports_fresh)

   512 apply(rule supports_abs_qlam)

   513 apply(simp add: finite_supp)

   514 apply(simp)

   515 apply(drule conjunct2)

   516 apply(auto)[1]

   517 apply(simp add: Supp_def)

   518 apply(auto)[1]

   519 apply(simp add: s[symmetric])

   520 apply(rule supports_fresh)

   521 apply(rule supports_abs_qlam)

   522 apply(simp add: finite_supp)

   523 apply(simp)

   524 done

   525 

   526 lemma

   527   fixes t::"qlam"

   528   shows "(supp x) supports (QVar x)"

   529 apply(rule_tac x="QVar x" in Abs_qlam_cases)

   530 apply(auto)

   531 thm QVar_def

   532 oops

   533 

   534 

   535  

   536 section {* Size *}

   537 

   538 definition

   539   "Size t = Least {size s | s. s \<approx> t}" 

   540 

   541 lemma [quot_respect]:

   542   shows "(equ ===> op=) Size Size"

   543 unfolding fun_rel_def

   544 unfolding Size_def

   545 apply(auto)

   546 apply(rule_tac f="Least" in arg_cong)

   547 apply(auto)

   548 apply (metis equ_trans)

   549 by (metis equivp_def qlam_equivp)

   550 

   551 instantiation qlam :: size

   552 begin

   553 

   554 quotient_definition "size_qlam::qlam \<Rightarrow> nat" 

   555   is "Size::lam \<Rightarrow> nat"

   556 

   557 instance

   558 apply default

   559 done

   560 

   561 end

   562 

   563 thm lam.size

   564 

   565 lemma

   566   "size (QVar x) = 0"

   567 apply(descending)

   568 apply(simp add: Size_def)

   569 apply(rule Least_equality)

   570 apply(auto)

   571 apply(simp add: Collect_def)

   572 apply(rule_tac x="Var x" in exI)

   573 apply(auto intro: equ_refl)

   574 done

   575 

   576 lemma

   577   "size (QLam [x].t) = Suc (size t)"

   578 apply(descending)

   579 apply(simp add: Size_def)

   580 thm Least_Suc

   581 apply(rule trans)

   582 apply(rule_tac n="Suc (size t)" in Least_Suc)

   583 apply(simp add: Collect_def)

   584 apply(rule_tac x="Lam [x].t" in exI)

   585 apply(auto intro: equ_refl)[1]

   586 apply(simp add: Collect_def)

   587 apply(auto)

   588 defer

   589 apply(simp add: Collect_def)

   590 apply(rule_tac x="t" in exI)

   591 apply(auto intro: equ_refl)[1]

   592 apply(simp add: Collect_def)

   593 defer

   594 apply(simp add: Collect_def)

   595 apply(auto)[1]

   596 

   597 apply(auto)

   598 done

   599 

   600 term rep_qlam

   601 lemmas qlam_size_def = Size_def[quot_lifted]

   602 

   603 lemma [quot_preserve]:

   604   assumes "Quotient equ Abs Rep"

   605   shows "(id ---> Rep ---> id) fresh = fresh"

   606 using assms

   607 unfolding Quotient_def

   608 apply(simp add: map_fun_def)

   609 apply(simp add: comp_def fun_eq_iff)

   610 

   611 sorry

   612 

   613 lemma [simp]:

   614   shows "(QVar x)[y :::= s] = (if x = y then s else (QVar x))"

   615   and "(QApp t1 t2)[y :::= s] = QApp (t1[y :::= s]) (t2[y :::= s])"

   616   and "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y :::= s] = QLam [x].(t[y :::= s])"

   617 apply(lifting subst.simps(1))

   618 apply(lifting subst.simps(2))

   619 apply(lifting subst.simps(3))

   620 done

   621 

   622 

   623 

   624 end

   625 

   626 

   627