Quelle Lambda_Example.thy Sprache: Isabelle

theory Lambda_Example
imports "HOL-Library.Code_Prolog"
begin

subsection \<open>Lambda\<close>

datatype type =
    Atom nat
  | Fun type type    (infixr \<open>\<Rightarrow>\<close> 200)

datatype dB =
    Var nat
  | App dB dB (infixl \<open>\<degree>\<close> 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"  (\<open>_[_'/_]\<close> [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 \<open>\<rightarrow>\<^sub>\<beta>\<close> 50)
  where
    beta [simp, intro!]: "Abs T s \ t \\<^sub>\ s[t/0]"
  | appL [simp, intro!]: "s \\<^sub>\ t ==> s \ u \\<^sub>\ t \ u"
  | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t"
  | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t"

subsection \<open>Inductive definitions for ordering on naturals\<close>

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 \<open>Manual setup to find counterexample\<close>

setup \<open>
  Context.theory_map
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
\<close>

setup \<open>Code_Prolog.map_code_options (K
  { ensure_groundness = true,
    limit_globally = NONE,
    limited_types = [(\<^typ>\<open>nat\<close>, 1), (\<^typ>\<open>type\<close>, 1), (\<^typ>\<open>dB\<close>, 1), (\<^typ>\<open>type list\<close>, 1)],
    limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
    replacing = [(("typing", "limited_typing"), "quickcheck"),
                 (("nthel1", "limited_nthel1"), "lim_typing")],
    manual_reorder = []})\<close>

lemma
  "\ \ t : U \ t \\<^sub>\ t' \ \ \ t' : U"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

text \<open>Verifying that the found counterexample really is one by means of a proof\<close>

lemma
assumes
  "t' = Var 0"
  "U = Atom 0"
  "\ = [Atom 1]"
  "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
shows
  "\ \ t : U"
  "t \\<^sub>\ t'"
  "\ \ \ t' : U"
proof -
  from assms show "\ \ t : U"
    by (auto intro!: typing.intros nth_el1.intros)
next
  from assms have "t \\<^sub>\ (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 \\<^sub>\ t'" by simp
next
  from assms show "\ \ \ t' : U"
    by (auto elim: typing.cases nth_el1.cases)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.