Theory Lambda_Example

theory Lambda_Example
  imports "HOL-Library.Code_Prolog"
  options [condition = "$ISABELLE_SWIPL"]
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 = [(\<^typ>‹nat›, 1), (\<^typ>‹type›, 1), (\<^typ>‹dB›, 1), (\<^typ>‹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