1 theory Lambda

     2 imports 

     3   "../Nominal2"

     4 begin

     5 

     6 

     7 atom_decl name

     8 

     9 nominal_datatype lam =

    10   Var "name"

    11 | App "lam" "lam"

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

    13 

    14 

    15 nominal_datatype sem =

    16   L "env" x::"name" l::"lam" binds x in l

    17 | N "neu"

    18 and neu = 

    19   V "name"

    20 | A "neu" "sem"

    21 and env =

    22   ENil

    23 | ECons "env" "name" "sem"

    24 

    25 nominal_primrec 

    26   evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and

    27   evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"

    28 where

    29   "evals ENil (Var x) = N (V x)"

    30 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 

    31 | "evals env (Lam [x]. t) = L env x t"

    32 | "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"

    33 | "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"

    34 | "evals_aux (N n) t2 env = N (A n (evals env t2))"

    35 defer

    36 defer

    37 --"completeness"

    38 apply(case_tac x)

    39 apply(simp)

    40 apply(case_tac a)

    41 apply(simp)

    42 apply(case_tac aa rule: sem_neu_env.exhaust(3))

    43 apply(simp)

    44 apply(case_tac b rule: lam.exhaust)

    45 apply(metis)+

    46 apply(case_tac b rule: lam.exhaust)

    47 apply(metis)+

    48 apply(simp)

    49 apply(case_tac b)

    50 apply(simp)

    51 apply(case_tac a rule: sem_neu_env.exhaust(1))

    52 apply(metis)+

    53 --"compatibility"

    54 apply(all_trivials)

    55 apply(simp)

    56 apply(simp)

    57 apply(simp)

    58 apply(simp)

    59 defer

    60 apply(simp)

    61 sorry

    62 

    63 (* can probably not proved by a trivial size argument *)

    64 termination sorry

    65 

    66