# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295281221 -3600
# Node ID e3f8673085b15418d394ef030098f0658ecde093
# Parent  324a5d1289a34e18416ac09d328c844977e715d6
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)

diff -r 324a5d1289a3 -r e3f8673085b1 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Jan 17 15:12:03 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jan 17 17:20:21 2011 +0100
@@ -102,6 +102,101 @@
 apply(simp_all add: lam.supp supp_at_base)
 done
 
+nominal_datatype db = 
+  DBVar nat
+| DBApp db db
+| DBLam db
+
+abbreviation
+  mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
+where  
+  "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
+
+
+lemma mbind_eqvt:
+  fixes c::"'a::pt option"
+  shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
+apply(cases c)
+apply(simp_all)
+apply(perm_simp)
+apply(rule refl)
+done
+
+lemma mbind_eqvt_raw[eqvt_raw]:
+  shows "(p \<bullet> option_case) \<equiv> option_case"
+apply(rule eq_reflection)
+apply(rule ext)+
+apply(case_tac xb)
+apply(simp_all)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+done
+
+fun
+  index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 
+where
+  "index [] n x = None"
+| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
+
+lemma [eqvt]:
+  shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+apply(induct xs arbitrary: n)
+apply(simp_all add: permute_pure)
+done
+
+ML {*
+Nominal_Function_Core.trace := true
+*}
+
+(*
+inductive
+  trans_graph
+where
+  "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" 
+| "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); 
+    \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>
+    \<Longrightarrow> trans_graph (App t1 t2, xs) 
+       (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"
+| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>
+    trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"
+
+lemma
+  assumes a: "trans_graph x t"
+  shows "trans_graph (p \<bullet> x) (p \<bullet> t)"
+using a
+apply(induct)
+apply(perm_simp)
+apply(rule trans_graph.intros)
+apply(perm_simp)
+apply(rule trans_graph.intros)
+apply(simp)
+apply(simp)
+defer
+apply(perm_simp)
+apply(rule trans_graph.intros)
+apply(simp)
+apply(rotate_tac 3)
+apply(drule_tac x="FOO" in meta_spec)
+apply(drule meta_mp)
+prefer 2
+apply(simp)
+
+equivariance trans_graph
+*)
+
+(* equivariance fails at the moment
+nominal_primrec
+  trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
+where
+  "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
+| "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
+| "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+*)
+
 nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
 where
diff -r 324a5d1289a3 -r e3f8673085b1 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Jan 17 15:12:03 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Jan 17 17:20:21 2011 +0100
@@ -33,7 +33,7 @@
   swap_eqvt flip_eqvt
 
   (* datatypes *)
-  Pair_eqvt permute_list.simps 
+  Pair_eqvt permute_list.simps permute_option.simps
 
   (* sets *)
   mem_eqvt empty_eqvt insert_eqvt set_eqvt