|
theory Lambda_Example
imports "HOL-Library.Code_Prolog"
begin
subsection \<open>Lambda\<close>
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 "\\<^sub>\" 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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
