105 nominal_datatype db = 

   106   DBVar nat

   107 | DBApp db db

   108 | DBLam db

   109 

   110 abbreviation

   111   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 

   112 where  

   113   "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"

   114 

   115 

   116 lemma mbind_eqvt:

   117   fixes c::"'a::pt option"

   118   shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"

   119 apply(cases c)

   120 apply(simp_all)

   121 apply(perm_simp)

   122 apply(rule refl)

   123 done

   124 

   125 lemma mbind_eqvt_raw[eqvt_raw]:

   126   shows "(p \<bullet> option_case) \<equiv> option_case"

   127 apply(rule eq_reflection)

   128 apply(rule ext)+

   129 apply(case_tac xb)

   130 apply(simp_all)

   131 apply(rule_tac p="-p" in permute_boolE)

   132 apply(perm_simp add: permute_minus_cancel)

   133 apply(simp)

   134 apply(rule_tac p="-p" in permute_boolE)

   135 apply(perm_simp add: permute_minus_cancel)

   136 apply(simp)

   137 done

   138 

   139 fun

   140   index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 

   141 where

   142   "index [] n x = None"

   143 | "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"

   144 

   145 lemma [eqvt]:

   146   shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"

   147 apply(induct xs arbitrary: n)

   148 apply(simp_all add: permute_pure)

   149 done

   150 

   151 ML {*

   152 Nominal_Function_Core.trace := true

   153 *}

   154 

   155 (*

   156 inductive

   157   trans_graph

   158 where

   159   "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" 

   160 | "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); 

   161     \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>

   162     \<Longrightarrow> trans_graph (App t1 t2, xs) 

   163        (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"

   164 | "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>

   165     trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"

   166 

   167 lemma

   168   assumes a: "trans_graph x t"

   169   shows "trans_graph (p \<bullet> x) (p \<bullet> t)"

   170 using a

   171 apply(induct)

   172 apply(perm_simp)

   173 apply(rule trans_graph.intros)

   174 apply(perm_simp)

   175 apply(rule trans_graph.intros)

   176 apply(simp)

   177 apply(simp)

   178 defer

   179 apply(perm_simp)

   180 apply(rule trans_graph.intros)

   181 apply(simp)

   182 apply(rotate_tac 3)

   183 apply(drule_tac x="FOO" in meta_spec)

   184 apply(drule meta_mp)

   185 prefer 2

   186 apply(simp)

   187 

   188 equivariance trans_graph

   189 *)

   190 

   191 (* equivariance fails at the moment

   192 nominal_primrec

   193   trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"

   194 where

   195   "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"

   196 | "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"

   197 | "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"

   198 *)

   199