1 theory Beta

     2 imports 

     3   "../Nominal2"

     4 begin

     5 

     6 

     7 atom_decl name

     8 

     9 nominal_datatype lam =

    10   Var "name"

    11 | App "lam" "lam"

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

    13 

    14 section {* capture-avoiding substitution *}

    15 

    16 nominal_primrec

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

    18 where

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

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

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

    22   unfolding eqvt_def subst_graph_def

    23   apply (rule, perm_simp, rule)

    24   apply(rule TrueI)

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

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

    27   apply(blast)+

    28   apply(simp_all add: fresh_star_def fresh_Pair_elim)

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

    30   apply(simp_all add: Abs_fresh_iff)

    31   apply(simp add: fresh_star_def fresh_Pair)

    32   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    33   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

    34 done

    35 

    36 termination (eqvt)

    37   by lexicographic_order

    38 

    39 lemma forget:

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

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

    42      (auto simp add: lam.fresh fresh_at_base)

    43 

    44 lemma fresh_fact:

    45   fixes z::"name"

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

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

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

    49   using a b

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

    51      (auto simp add: lam.fresh fresh_at_base)

    52 

    53 lemma substitution_lemma:  

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

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

    56 using a 

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

    58    (auto simp add: fresh_fact forget)

    59 

    60 inductive

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

    62 where

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

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

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

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

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

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

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

    70 

    71 equivariance equ

    72 

    73 nominal_inductive equ

    74   avoids equ_beta: "x" 

    75        | equ_Lam: "x"

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

    77 

    78 lemma [quot_respect]:

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

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

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

    82 unfolding fun_rel_def

    83 by (auto intro: equ.intros)

    84 

    85 lemma equ_subst1:

    86   assumes "t \<approx> s"

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

    88 using assms

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

    90 apply(simp)

    91 apply(rule equ_trans)

    92 apply(rule equ_beta)

    93 apply(simp add: fresh_fact)

    94 apply(subst (2) substitution_lemma)

    95 apply(simp add: fresh_at_base)

    96 apply(simp)

    97 apply(rule equ_refl)

    98 apply(rule equ_refl)

    99 apply(auto intro: equ_sym)[1]

   100 apply(blast intro: equ_trans)

   101 apply(simp add: equ_Lam)

   102 apply(simp add: equ_App1)

   103 apply(simp add: equ_App2)

   104 done

   105 

   106 lemma equ_subst2:

   107   assumes "t \<approx> s"

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

   109 using assms

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

   111 apply(simp add: equ_refl)

   112 apply(simp)

   113 apply(smt equ_App1 equ_App2 equ_trans)

   114 apply(simp)

   115 apply(metis equ_Lam)

   116 done

   117 

   118 lemma [quot_respect]:

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

   120 unfolding fun_rel_def

   121 by (metis equ_subst1 equ_subst2 equ_trans)

   122 

   123 lemma [quot_respect]:

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

   125 unfolding fun_rel_def

   126 by (auto intro: eqvt)

   127 

   128 quotient_type qlam = lam / equ

   129 apply(rule equivpI)

   130 apply(rule reflpI)

   131 apply(simp add: equ_refl)

   132 apply(rule sympI)

   133 apply(simp add: equ_sym)

   134 apply(rule transpI)

   135 apply(auto intro: equ_trans)

   136 done

   137 

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

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

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

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

   142 

   143 lemmas qlam_strong_induct = lam.strong_induct[quot_lifted]

   144 lemmas qlam_induct = lam.induct[quot_lifted]

   145 

   146 instantiation qlam :: pt

   147 begin

   148 

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

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

   151 

   152 instance

   153 apply default

   154 apply(descending)

   155 apply(simp)

   156 apply(rule equ_refl)

   157 apply(descending)

   158 apply(simp)

   159 apply(rule equ_refl)

   160 done

   161 

   162 end

   163 

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

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

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

   167  by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left)

   168 

   169 lemma supports_abs_qlam:

   170   "(supp t) supports (abs_qlam t)"

   171 unfolding supports_def

   172 unfolding fresh_def[symmetric]

   173 apply(auto)

   174 apply(perm_simp)

   175 apply(simp add: swap_fresh_fresh)

   176 done

   177 

   178 lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)"

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

   180  apply (rule rep_abs_rsp[OF Quotient_qlam])

   181  apply (rule equ_refl)

   182  done

   183 

   184 section {* Supp *}

   185 

   186 definition

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

   188 

   189 lemma [quot_respect]:

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

   191 unfolding fun_rel_def

   192 unfolding Supp_def

   193 apply(rule allI)+

   194 apply(rule impI)

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

   196 apply(auto)

   197 apply (metis equ_trans)

   198 by (metis equivp_def qlam_equivp)

   199 

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

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

   202 

   203 

   204 lemma

   205   fixes t::"qlam"

   206   shows "supp t = supp_qlam t"

   207 apply(descending)

   208 oops

   209 

   210 

   211  

   212 

   213 lemma [quot_respect]:

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

   215 unfolding fun_rel_def

   216 unfolding Size_def

   217 apply(auto)

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

   219 apply(auto)

   220 apply (metis equ_trans)

   221 by (metis equivp_def qlam_equivp)

   222 

   223 

   224 section {* Size *}

   225 

   226 definition

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

   228 

   229 lemma [quot_respect]:

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

   231 unfolding fun_rel_def

   232 unfolding Size_def

   233 apply(auto)

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

   235 apply(auto)

   236 apply (metis equ_trans)

   237 by (metis equivp_def qlam_equivp)

   238 

   239 instantiation qlam :: size

   240 begin

   241 

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

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

   244 

   245 instance

   246 apply default

   247 done

   248 

   249 end

   250 

   251 thm lam.size

   252 

   253 lemma

   254   "size (QVar x) = 0"

   255 apply(descending)

   256 apply(simp add: Size_def)

   257 apply(rule Least_equality)

   258 apply(auto)

   259 apply(simp add: Collect_def)

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

   261 apply(auto intro: equ_refl)

   262 done

   263 

   264 lemma

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

   266 apply(descending)

   267 apply(simp add: Size_def)

   268 apply(auto)

   269 apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2)

   270 apply(simp add: Collect_def)

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

   272 apply(auto intro: equ_refl)[1]

   273 apply(simp add: Collect_def)

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

   275 apply(auto intro: equ_refl)[1]

   276 apply(simp add: Collect_def)

   277 apply(auto)[1]

   278 defer

   279 apply(simp add: Collect_def)

   280 apply(auto)[1]

   281 

   282 apply(auto)

   283 done

   284 

   285 term rep_qlam

   286 lemmas qlam_size_def = Size_def[quot_lifted]

   287 

   288 lemma [quot_preserve]:

   289   assumes "Quotient equ Abs Rep"

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

   291 using assms

   292 unfolding Quotient_def

   293 apply(simp add: map_fun_def)

   294 apply(simp add: comp_def fun_eq_iff)

   295 

   296 sorry

   297 

   298 lemma [simp]:

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

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

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

   302 apply(lifting subst.simps(1))

   303 apply(lifting subst.simps(2))

   304 apply(lifting subst.simps(3))

   305 done

   306 

   307 

   308 

   309 end

   310 

   311 

   312