Quelle  Lambda_Example.thy

theory Lambda_Example
imports "HOL-Library.Code_Prolog"
begin

subsection ‹Lambda›

datatype type =
    Atom nat
  | Fun type type    (infixr ‹==>› 200)

datatype dB =
    Var nat
  | App dB dB (infixl ‹🍋› 200)
  | Abs type dB

primrec
  nth_el :: "'a list ==> nat ==> 'a option" (‹_⟨_⟩› [90, 0] 91)
where
  "[]⟨i⟩ = None"
| "(x # xs)⟨i⟩ = (case i of 0 ==> Some x | Suc j ==> xs ⟨j⟩)"

inductive nth_el1 :: "'a list ==> nat ==> 'a ==> bool"
where
  "nth_el1 (x # xs) 0 x"
| "nth_el1 xs i y ==> nth_el1 (x # xs) (Suc i) y"

inductive typing :: "type list ==> dB ==> type ==> bool"  (‹_ ⊨ _ : _› [50, 50, 50] 50)
  where
    Var [intro!]: "nth_el1 env x T ==> env ⊨ Var x : T"
  | Abs [intro!]: "T # env ⊨ t : U ==> env ⊨ Abs T t : (T ==> U)"
  | App [intro!]: "env ⊨ s : U ==> T ==> env ⊨ t : T ==> env ⊨ (s 🍋 t) : U"

primrec
  lift :: "[dB, nat] => dB"
where
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
  | "lift (s 🍋 t) k = lift s k 🍋 lift t k"
  | "lift (Abs T s) k = Abs T (lift s (k + 1))"

primrec pred :: "nat => nat"
where
  "pred (Suc i) = i"

primrec
  subst :: "[dB, dB, nat] => dB"  (‹_[_'/_]› [300, 0, 0] 300)
where
    subst_Var: "(Var i)[s/k] =
      (if k < i then Var (pred i) else if i = k then s else Var i)"
  | subst_App: "(t 🍋 u)[s/k] = t[s/k] 🍋 u[s/k]"
  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"

inductive beta :: "[dB, dB] => bool"  (infixl ‹→🪙β› 50)
  where
    beta [simp, intro!]: "Abs T s 🍋 t →🪙β s[t/0]"
  | appL [simp, intro!]: "s →🪙β t ==> s 🍋 u →🪙β t 🍋 u"
  | appR [simp, intro!]: "s →🪙β t ==> u 🍋 s →🪙β u 🍋 t"
  | abs [simp, intro!]: "s →🪙β t ==> Abs T s →🪙β Abs T t"

subsection ‹Inductive definitions for ordering on naturals›

inductive less_nat
where
  "less_nat 0 (Suc y)"
| "less_nat x y ==> less_nat (Suc x) (Suc y)"

lemma less_nat[code_pred_inline]:
  "x < y = less_nat x y"
apply (rule iffI)
apply (induct x arbitrary: y)
apply (case_tac y) apply (auto intro: less_nat.intros)
apply (case_tac y)
apply (auto intro: less_nat.intros)
apply (induct rule: less_nat.induct)
apply auto
done

lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
by simp

section ‹Manual setup to find counterexample›

setup ‹
  Context.theory_map
  (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
 ›

setup ‹Code_Prolog.map_code_options (K
  { ensure_groundness = true,
  limit_globally = NONE,
  limited_types = [(🍋‹nat›, 1), (🍋‹type›, 1), (🍋‹dB›, 1), (🍋‹type list›, 1)],
  limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
  replacing = [(("typing", "limited_typing"), "quickcheck"),
  (("nthel1", "limited_nthel1"), "lim_typing")],
  manual_reorder = []})›

lemma
  "Γ ⊨ t : U ==> t →🪙β t' ==> Γ ⊨ t' : U"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

text ‹Verifying that the found counterexample really is one by means of a proof›

lemma
assumes
  "t' = Var 0"
  "U = Atom 0"
  "Γ = [Atom 1]"
  "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
shows
  "Γ ⊨ t : U"
  "t →🪙β t'"
  "¬ Γ ⊨ t' : U"
proof -
  from assms show "Γ ⊨ t : U"
    by (auto intro!: typing.intros nth_el1.intros)
next
  from assms have "t →🪙β (Var 1)[Var 0/0]"
    by (auto simp only: intro: beta.intros)
  moreover
  from assms have "(Var 1)[Var 0/0] = t'" by simp
  ultimately show "t →🪙β t'" by simp
next
  from assms show "¬ Γ ⊨ t' : U"
    by (auto elim: typing.cases nth_el1.cases)
qed


end