22 nominal_primrec

    23   depth :: "lam \<Rightarrow> nat"

    24 where

    25   "depth (Var x) = 1"

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

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

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

    29 apply(simp_all)[3]

    30 apply(simp_all only: lam.distinct)

    31 apply(simp add: lam.eq_iff)

    32 apply(simp add: lam.eq_iff)

    33 apply(subst (asm) Abs_eq_iff)

    34 apply(erule exE)

    35 apply(simp add: alphas)

    36 apply(clarify)

    37 apply(rule trans)

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

    39 apply(simp add: pure_supp)

    40 apply(simp add: fresh_star_def)

    41 apply(simp add: eqvt_at_def)

    42 done

    43 

    44 termination

    45   apply(relation "measure size")

    46   apply(simp_all add: lam.size)

    47   done

    48   

    49 lemma removeAll_eqvt[eqvt]:

    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 (* a small lemma *)

    99 lemma

   100   "supp t = set (frees_lst t)"

   101 apply(induct t rule: lam.induct)

   102 apply(simp_all add: lam.supp supp_at_base)

   103 done

   104 

   105 nominal_primrec

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

   107 where

   108   "(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])"

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

   111 apply(case_tac x)

   112 apply(simp)

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

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

   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)+

   124 oops

   125