10 | Lam x::"name" l::"lam"  bind x in l

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

    11 

    11 

    12 thm lam.distinct

    12 text {* height function *}

    13 thm lam.induct

    14 thm lam.exhaust lam.strong_exhaust

    15 thm lam.fv_defs

    16 thm lam.bn_defs

    17 thm lam.perm_simps

    18 thm lam.eq_iff

    19 thm lam.fv_bn_eqvt

    20 thm lam.size_eqvt

    26 | "height (App t1 t2) = (max (height t1) (height t2)) + 1"

    18 | "height (App t1 t2) = max (height t1) (height t2) + 1"

    27 | "height (Lam x t) = (height t) + 1"

    19 | "height (Lam [x].t) = height t + 1"

    20 apply(rule_tac y="x" in lam.exhaust)

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

    22 apply(simp add: Abs_eq_iff alphas)

    23 apply(clarify)

    24 apply(subst (4) supp_perm_eq[where p="p", symmetric])

    25 apply(simp add: pure_supp fresh_star_def)

    26 apply(simp add: eqvt_at_def)

    27 done

    28 

    29 termination

    30   by (relation "measure size") (simp_all add: lam.size)

    31   

    32   

    33 text {* free name function - returns atom lists *}

    34 

    35 nominal_primrec 

    36   frees_lst :: "lam \<Rightarrow> atom list"

    37 where

    38   "frees_lst (Var x) = [atom x]"

    39 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"

    40 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"

    33 apply(subst (asm) Abs_eq_iff)

    46 apply(simp add: lam.eq_iff)

    47 apply(simp add: Abs_eq_iff)

    39 apply(simp add: pure_supp)

    54 apply(simp (no_asm) add: supp_removeAll)

    40 apply(simp add: fresh_star_def)

    55 apply(drule supp_eqvt_at)

    41 apply(simp add: eqvt_at_def)

    56 apply(simp add: finite_supp)

    57 apply(auto simp add: fresh_star_def)[1]

    58 unfolding eqvt_at_def

    59 apply(simp only: removeAll_eqvt atom_eqvt)

    48   

    66 

    49 lemma removeAll_eqvt[eqvt]:

    67 text {* a small test lemma *}

    50   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"

    51 by (induct xs) (auto)

    52 

    53 lemma supp_removeAll:

    54   fixes x::"atom"

    55   shows "supp (removeAll x xs) = (supp xs - {x})"

    56 apply(induct xs)

    57 apply(simp_all add: supp_Nil supp_Cons)

    58 apply(rule conjI)

    59 apply(rule impI)

    60 apply(simp add: supp_atom)

    61 apply(rule impI)

    62 apply(simp add: supp_atom)

    63 apply(blast)

    64 done

    65 

    66 nominal_primrec 

    67   frees_lst :: "lam \<Rightarrow> atom list"

    68 where

    69   "frees_lst (Var x) = [atom x]"

    70 | "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"

    71 | "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"

    72 apply(rule_tac y="x" in lam.exhaust)

    73 apply(simp_all)[3]

    74 apply(simp_all only: lam.distinct)

    75 apply(simp add: lam.eq_iff)

    76 apply(simp add: lam.eq_iff)

    77 apply(simp add: lam.eq_iff)

    78 apply(simp add: Abs_eq_iff)

    79 apply(erule exE)

    80 apply(simp add: alphas)

    81 apply(simp add: atom_eqvt)

    82 apply(clarify)

    83 apply(rule trans)

    84 apply(rule_tac p="p" in supp_perm_eq[symmetric])

    85 apply(simp (no_asm) add: supp_removeAll)

    86 apply(drule supp_eqvt_at)

    87 apply(simp add: finite_supp)

    88 apply(auto simp add: fresh_star_def)[1]

    89 unfolding eqvt_at_def

    90 apply(simp only: removeAll_eqvt atom_eqvt)

    91 done

    92 

    93 termination

    94   apply(relation "measure size")

    95   apply(simp_all add: lam.size)

    96   done

    97 

    98 text {* a small lemma *}

   100   "supp t = set (frees_lst t)"

    69   shows "supp t = set (frees_lst t)"

   101 apply(induct t rule: lam.induct)

    70 apply(induct t rule: frees_lst.induct)

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

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

   107 where

    78 where

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

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

   109 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"

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

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

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

   111 apply(case_tac x)

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

   112 apply(simp)

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

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

    84 apply(blast)+

   114 apply(simp add: lam.eq_iff lam.distinct)

    85 apply(simp add: fresh_star_def)

   115 apply(auto)[1]

   116 apply(simp add: lam.eq_iff lam.distinct)

   117 apply(auto)[1]

   118 apply(simp add: fresh_star_def lam.eq_iff lam.distinct)

   119 apply(simp_all add: lam.distinct)[5]

   120 apply(simp add: lam.eq_iff)

   121 apply(simp add: lam.eq_iff)

   122 apply(simp add: lam.eq_iff)

   123 apply(erule conjE)+

   131 apply(auto)

    88 apply(simp add: alphas atom_eqvt)

   132 apply(simp add: alphas)

   133 apply(simp add: atom_eqvt)

   154 unfolding eqvt_at_def

   109 apply(simp add: atom_eqvt eqvt_at_def)

   155 apply(simp add: atom_eqvt fresh_Pair)

   163   apply(relation "measure (\<lambda>(t,_,_). size t)")

   121   by (relation "measure (\<lambda>(t,_,_). size t)")

   164   apply(simp_all add: lam.size)

   122      (simp_all add: lam.size)

   165   done

   123 

   124 lemma subst_eqvt[eqvt]:

   125   shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"

   126 by (induct t x s rule: subst.induct) (simp_all)

   127 

   128 lemma forget:

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

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

   131 apply(auto simp add: lam.fresh fresh_at_base)

   132 done

   133 

   134 text {* same lemma but with subst.induction *}

   135 lemma forget2:

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

   137 apply(induct t x s rule: subst.induct)

   138 apply(auto simp add: lam.fresh fresh_at_base fresh_Pair)

   139 done

   140 

   141 lemma fresh_fact:

   142   fixes z::"name"

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

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

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

   146 using a b

   147 apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)

   148 apply (auto simp add: lam.fresh fresh_at_base)

   149 done

   150 

   151 lemma substitution_lemma:  

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

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

   154 using a 

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

   156    (auto simp add: fresh_fact forget)

   157 

   158 lemma subst_rename: 

   159   assumes a: "atom y \<sharp> t"

   160   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"

   161 using a 

   162 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)

   163 apply (auto simp add: lam.fresh fresh_at_base)

   164 done

   165 

   166 

   167 subsection {* single-step beta-reduction *}

   168 

   169 inductive 

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

   171 where

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

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

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

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

   176 

   177 equivariance beta

   178 

   179 nominal_inductive beta

   180   avoids b4: "x"

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

   182 

   183 text {* One-Reduction *}

   184 

   185 inductive 

   186   One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80)

   187 where

   188   o1[intro]: "Var x \<longrightarrow>1 Var x"

   189 | o2[intro]: "\<lbrakk>t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>1 App t2 s2"

   190 | o3[intro]: "t1 \<longrightarrow>1 t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>1 Lam [x].t2"

   191 | o4[intro]: "\<lbrakk>atom x \<sharp> (s1, s2); t1 \<longrightarrow>1 t2; s1 \<longrightarrow>1 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]"

   192 

   193 equivariance One

   194 

   195 nominal_inductive One 

   196   avoids o3: "x"

   197       |  o4: "x"

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

   199 

   200 lemma One_refl:

   201   shows "t \<longrightarrow>1 t"

   202 by (nominal_induct t rule: lam.strong_induct) (auto)

   203 

   204 lemma One_subst: 

   205   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"

   206   shows "t1[x ::= s1] \<longrightarrow>1 t2[x ::= s2]" 

   207 using a 

   208 apply(nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)

   209 apply(auto simp add: substitution_lemma fresh_at_base fresh_fact fresh_Pair)

   210 done

   211 

   212 lemma better_o4_intro:

   213   assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2"

   214   shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]"

   215 proof -

   216   obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" sorry

   217   have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs

   218     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)

   219   also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt)

   220   also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric])

   221   finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp

   222 qed

   223 

   224 

   225 

   226 

   227 

   228 section {* Locally Nameless Terms *}