de Bruijn Index

Lambda.thy

theory Lambda
imports Main
begin

section {* Lambda Calculus *}
subsection {* Definitions *}

type_synonym var = nat
datatype lambda_p = Var var | Abs' var lambda_p | App' lambda_p lambda_p

definition "lambda1 ≡ (Abs' 0 (Abs' 1 (Var 1)))"

(*
datatype lambda = Free var | Bounded var | Abs lambda | App lambda lambda
*)

datatype lambda = Var var | Abs lambda | App lambda lambda

notation
  Abs ("λ _" [40] 50) and
  App (infixl "$" 70)

primrec shift' :: "nat ⇒ nat ⇒ lambda ⇒ lambda" where
  "shift' d c (Var v) = (if v < c then Var v else Var (v + d))"
  | "shift' d c (λ M) = (λ (shift' d (c+1) M))"
  | "shift' d c (M $ M') = (shift' d c M $ shift' d c M')"

definition shift where
  "shift d M ≡ shift' d 0 M"

primrec unshift' :: "nat ⇒ nat ⇒ lambda ⇒ lambda" where
  "unshift' d c (Var v) = (if v < c then Var v else Var (v - d))"
  | "unshift' d c (λ M) = (λ (unshift' d (c+1) M))"
  | "unshift' d c (M $ M') = (unshift' d c M $ unshift' d c M')"

definition unshift where
  "unshift d M ≡ unshift' d 0 M"

lemma shift_0_inv: "shift 0 M = M"
proof-
  have shift'_inv: "⋀n. shift' 0 n M = M"
    by (induct M, auto)
  show ?thesis
    by (simp add: shift_def shift'_inv)
qed

lemma unshift_0_inv: "unshift 0 M = M"
proof-
  have unshift'_inv: "⋀n. unshift' 0 n M = M"
    by (induct M, auto)
  show ?thesis
    by (simp add: unshift_def unshift'_inv)
qed

lemma shift'_unshift'_inv: "⋀c. unshift' n c (shift' n c M) = M"
by (induct M, auto)

lemma shift_unshift_inv: "unshift n (shift n M) = M"
by (simp add: shift_def unshift_def shift'_unshift'_inv)

lemma shift'_unshift'1_inv: "⋀c. unshift' n (c+1) (shift' n c M) = M"
by (induct M, auto)

lemma shift_unshift'1_inv: "unshift' n 1 (shift n M) = M"
apply (unfold shift_def)
using shift'_unshift'1_inv [of n 0 M] by simp

primrec subst :: "lambda ⇒ nat ⇒ lambda ⇒ lambda" ("_[_ ∷= _]" [90] 120) where
  "(Var i)[j ∷= t] = (if i = j then t else Var i)"
  | "(λ M)[j ∷= t] = (λ (M[j+1 ∷= shift 1 t]))"
  | "(M $ M')[j ∷= t] = (M[j ∷= t] $ M'[j ∷= t])"

inductive β_trans ("_ →⇩β _") where
  β_subst: "((λ M) $ N) →⇩β (unshift 1 (M[0 ∷= shift 1 N]))"
  | β_var: "(Var v) →⇩β (Var v)"
  | β_abs: "M →⇩β N ⟹ (λ M) →⇩β (λ N)"
  | β_appf: "M →⇩β N ⟹ (M $ P) →⇩β (N $ P)"
  | β_appl: "M →⇩β N ⟹ (P $ M) →⇩β (P $ N)"

lemma β_trans_inv: "M →⇩β M"
by (induct M, rule, rule, simp, rule, simp)

inductive β_seq ("_ ⟶⇩β _") where
  β_seq_0: "M ⟶⇩β M"
  | β_seq_step: "⟦ M' →⇩β M; M ⟶⇩β N ⟧ ⟹ M' ⟶⇩β N"

lemma β_seq_concat: "⟦ M ⟶⇩β M'; M' ⟶⇩β M'' ⟧ ⟹ M ⟶⇩β M''"
using β_seq.induct [of M M' "λx. λy. (y ⟶⇩β M'') ⟶ (x ⟶⇩β M'')"] apply rule
by (auto, rule, simp, simp)

lemma β_seq_appf: "M ⟶⇩β N ⟹ (M $ P) ⟶⇩β (N $ P)"
by (erule β_seq.induct, rule β_seq_0, rule, rule β_appf, simp, simp)

(* I ≡ λx.x *)
definition "I ≡ (λ (Var 0))"

lemma "(I $ M) ⟶⇩β M"
by (unfold I_def, rule, rule β_subst, simp add: shift_unshift_inv, rule β_seq_0)

(* K ≡ λxy.x *)
definition "K ≡ (λ λ (Var 1))"

lemma "(K $ M $ N) ⟶⇩β M"
apply (unfold K_def, rule, rule β_appf, rule β_subst, simp)
sorry
(* unshift 1 (λ shift 1 (shift 1 M)) $ N ⟶⇩β M *)

(* S ≡ λxyz. xz(yz) *)
definition "S ≡ (λ λ λ (Var 2 $ Var 0 $ (Var 1 $ Var 0)))"

lemma "(S $ K $ K) ⟶⇩β I"
proof-
  have 1: "(S $ K $ K) = (λ λ λ (Var 2 $ Var 0 $ (Var 1 $ Var 0))) $ K $ K"
    by (simp add: S_def)
  have 2: "… →⇩β ((λ λ (K $ Var 0 $ (Var 1 $ Var 0))) $ K)" (is "_ →⇩β (?R $ K)")
    proof (rule)
      have "unshift 1 ((λ λ Var 2 $ Var 0 $ (Var 1 $ Var 0))[0 ∷= shift 1 K]) = ?R"
        by (simp add: unshift_def shift_def K_def)
      thus "((λ λ λ Var 2 $ Var 0 $ (Var 1 $ Var 0)) $ K) →⇩β (λ λ K $ Var 0 $ (Var 1 $ Var 0))"
        by (metis β_subst)
    qed
  have 3: "… ⟶⇩β ((λ λ (Var 0)) $ K)"
    apply (rule β_seq_appf, rule β_seq_abs, rule β_seq_abs)
    apply (unfold K_def, rule, rule β_appf, rule β_subst, simp add: unshift_def shift_def)
    apply (rule, rule β_subst, simp add: unshift_def shift_def)
    apply (rule β_seq_0)
    done
  have 4: "… ⟶⇩β I"
    by (unfold I_def, rule, rule β_subst, simp add: unshift_def shift_def, rule β_seq_0)

  show ?thesis
    apply (simp add: 1, rule)
    using 2 apply simp
    apply (rule β_seq_concat)
    using 3 apply simp
    using 4 apply simp
    done
qed