30 section {* Simple examples from Norrish 2004 *}

    31 

    32 nominal_primrec 

    33   is_app :: "lam \<Rightarrow> bool"

    34 where

    35   "is_app (Var x) = False"

    36 | "is_app (App t1 t2) = True"

    37 | "is_app (Lam [x]. t) = False"

    38 apply(simp add: eqvt_def is_app_graph_def)

    39 apply (rule, perm_simp, rule)

    40 apply(rule TrueI)

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

    42 apply(auto)[3]

    43 apply(all_trivials)

    44 done

    45 

    46 termination by lexicographic_order

    47 

    48 lemma [eqvt]:

    49   shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"

    50 apply(induct t rule: lam.induct)

    51 apply(simp_all add: permute_bool_def)

    52 done

    53 

    54 nominal_primrec 

    55   rator :: "lam \<Rightarrow> lam option"

    56 where

    57   "rator (Var x) = None"

    58 | "rator (App t1 t2) = Some t1"

    59 | "rator (Lam [x]. t) = None"

    60 apply(simp add: eqvt_def rator_graph_def)

    61 apply (rule, perm_simp, rule)

    62 apply(rule TrueI)

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

    64 apply(auto)[3]

    65 apply(simp_all)

    66 done

    67 

    68 termination by lexicographic_order

    69 

    70 lemma [eqvt]:

    71   shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"

    72 apply(induct t rule: lam.induct)

    73 apply(simp_all)

    74 done

    75 

    76 nominal_primrec 

    77   rand :: "lam \<Rightarrow> lam option"

    78 where

    79   "rand (Var x) = None"

    80 | "rand (App t1 t2) = Some t2"

    81 | "rand (Lam [x]. t) = None"

    82 apply(simp add: eqvt_def rand_graph_def)

    83 apply (rule, perm_simp, rule)

    84 apply(rule TrueI)

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

    86 apply(auto)[3]

    87 apply(simp_all)

    88 done

    89 

    90 termination by lexicographic_order

    91 

    92 lemma [eqvt]:

    93   shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"

    94 apply(induct t rule: lam.induct)

    95 apply(simp_all)

    96 done

    97 

    98 nominal_primrec 

    99   is_eta_nf :: "lam \<Rightarrow> bool"

   100 where

   101   "is_eta_nf (Var x) = True"

   102 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"

   103 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 

   104                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"

   105 apply(simp add: eqvt_def is_eta_nf_graph_def)

   106 apply (rule, perm_simp, rule)

   107 apply(rule TrueI)

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

   109 apply(auto)[3]

   110 apply(simp_all)

   111 apply(erule_tac c="()" in Abs_lst1_fcb2')

   112 apply(simp_all add: pure_fresh fresh_star_def)[3]

   113 apply(simp add: eqvt_at_def conj_eqvt)

   114 apply(perm_simp)

   115 apply(rule refl)

   116 apply(simp add: eqvt_at_def conj_eqvt)

   117 apply(perm_simp)

   118 apply(rule refl)

   119 done

   120 

   121 termination by lexicographic_order

   122 

   123 nominal_datatype path = Left | Right | In

   124 

   125 section {* Paths to a free variables *} 

   126 

   127 instance path :: pure

   128 apply(default)

   129 apply(induct_tac "x::path" rule: path.induct)

   130 apply(simp_all)

   131 done

   132 

   133 nominal_primrec 

   134   var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"

   135 where

   136   "var_pos y (Var x) = (if y = x then {[]} else {})"

   137 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"

   138 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"

   139 apply(simp add: eqvt_def var_pos_graph_def)

   140 apply (rule, perm_simp, rule)

   141 apply(rule TrueI)

   142 apply(case_tac x)

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

   144 apply(auto simp add: fresh_star_def)[3]

   145 apply(simp_all)

   146 apply(erule conjE)+

   147 apply(erule_tac Abs_lst1_fcb2)

   148 apply(simp add: pure_fresh)

   149 apply(simp add: fresh_star_def)

   150 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)

   151 apply(perm_simp)

   152 apply(rule refl)

   153 apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)

   154 apply(perm_simp)

   155 apply(rule refl)

   156 done

   157 

   158 termination by lexicographic_order

   159 

   160 lemma var_pos1:

   161   assumes "atom y \<notin> supp t"

   162   shows "var_pos y t = {}"

   163 using assms

   164 apply(induct t rule: var_pos.induct)

   165 apply(simp_all add: lam.supp supp_at_base fresh_at_base)

   166 done

   167 

   168 lemma var_pos2:

   169   shows "var_pos y (Lam [y].t) = {}"

   170 apply(rule var_pos1)

   171 apply(simp add: lam.supp)

   172 done

   173 

   174 

   175 text {* strange substitution operation *}

   176 

   177 nominal_primrec

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

   179 where

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

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

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

   183   apply(simp add: eqvt_def subst'_graph_def)

   184   apply (rule, perm_simp, rule)

   185   apply(rule TrueI)

   186   apply(case_tac x)

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

   188   apply(auto simp add: fresh_star_def)[3]

   189   apply(simp_all)

   190   apply(erule conjE)+

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

   192   apply(simp_all add: Abs_fresh_iff)

   193   apply(simp add: fresh_star_def fresh_Pair)

   194   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

   195   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

   196 done

   197 

   198 termination by lexicographic_order

   199 

   200