38948
|
1 |
theory Lambda_Example
|
|
2 |
imports Code_Prolog
|
|
3 |
begin
|
|
4 |
|
|
5 |
subsection {* Lambda *}
|
|
6 |
|
|
7 |
datatype type =
|
|
8 |
Atom nat
|
|
9 |
| Fun type type (infixr "\<Rightarrow>" 200)
|
|
10 |
|
|
11 |
datatype dB =
|
|
12 |
Var nat
|
|
13 |
| App dB dB (infixl "\<degree>" 200)
|
|
14 |
| Abs type dB
|
|
15 |
|
|
16 |
primrec
|
|
17 |
nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
|
|
18 |
where
|
|
19 |
"[]\<langle>i\<rangle> = None"
|
|
20 |
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
|
|
21 |
|
|
22 |
inductive nth_el1 :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
|
|
23 |
where
|
|
24 |
"nth_el1 (x # xs) 0 x"
|
|
25 |
| "nth_el1 xs i y \<Longrightarrow> nth_el1 (x # xs) (Suc i) y"
|
|
26 |
|
|
27 |
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
|
|
28 |
where
|
|
29 |
Var [intro!]: "nth_el1 env x T \<Longrightarrow> env \<turnstile> Var x : T"
|
|
30 |
| Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
|
|
31 |
| App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
|
|
32 |
|
|
33 |
primrec
|
|
34 |
lift :: "[dB, nat] => dB"
|
|
35 |
where
|
|
36 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))"
|
|
37 |
| "lift (s \<degree> t) k = lift s k \<degree> lift t k"
|
|
38 |
| "lift (Abs T s) k = Abs T (lift s (k + 1))"
|
|
39 |
|
|
40 |
primrec pred :: "nat => nat"
|
|
41 |
where
|
|
42 |
"pred (Suc i) = i"
|
|
43 |
|
|
44 |
primrec
|
|
45 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
|
|
46 |
where
|
|
47 |
subst_Var: "(Var i)[s/k] =
|
|
48 |
(if k < i then Var (pred i) else if i = k then s else Var i)"
|
|
49 |
| subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
|
|
50 |
| subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
|
|
51 |
|
|
52 |
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
|
|
53 |
where
|
|
54 |
beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
|
|
55 |
| appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
|
|
56 |
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
|
|
57 |
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
|
|
58 |
|
|
59 |
subsection {* Inductive definitions for ordering on naturals *}
|
|
60 |
|
|
61 |
inductive less_nat
|
|
62 |
where
|
|
63 |
"less_nat 0 (Suc y)"
|
|
64 |
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
|
|
65 |
|
|
66 |
lemma less_nat[code_pred_inline]:
|
|
67 |
"x < y = less_nat x y"
|
|
68 |
apply (rule iffI)
|
|
69 |
apply (induct x arbitrary: y)
|
|
70 |
apply (case_tac y) apply (auto intro: less_nat.intros)
|
|
71 |
apply (case_tac y)
|
|
72 |
apply (auto intro: less_nat.intros)
|
|
73 |
apply (induct rule: less_nat.induct)
|
|
74 |
apply auto
|
|
75 |
done
|
|
76 |
|
|
77 |
lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
|
|
78 |
by simp
|
|
79 |
|
|
80 |
section {* Manual setup to find counterexample *}
|
|
81 |
|
|
82 |
setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
|
|
83 |
|
|
84 |
ML {* Code_Prolog.options :=
|
|
85 |
{ ensure_groundness = true,
|
|
86 |
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
|
|
87 |
limited_predicates = [("typing", 2), ("nth_el1", 2)],
|
|
88 |
replacing = [(("typing", "limited_typing"), "quickcheck"),
|
|
89 |
(("nth_el1", "limited_nth_el1"), "lim_typing")],
|
|
90 |
prolog_system = Code_Prolog.SWI_PROLOG} *}
|
|
91 |
|
|
92 |
lemma
|
|
93 |
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
|
|
94 |
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
|
|
95 |
oops
|
|
96 |
|
|
97 |
text {* Verifying that the found counterexample really is one by means of a proof *}
|
|
98 |
|
|
99 |
lemma
|
|
100 |
assumes
|
|
101 |
"t' = Var 0"
|
|
102 |
"U = Atom 0"
|
|
103 |
"\<Gamma> = [Atom 1]"
|
|
104 |
"t = App (Abs (Atom 0) (Var 1)) (Var 0)"
|
|
105 |
shows
|
|
106 |
"\<Gamma> \<turnstile> t : U"
|
|
107 |
"t \<rightarrow>\<^sub>\<beta> t'"
|
|
108 |
"\<not> \<Gamma> \<turnstile> t' : U"
|
|
109 |
proof -
|
|
110 |
from assms show "\<Gamma> \<turnstile> t : U"
|
|
111 |
by (auto intro!: typing.intros nth_el1.intros)
|
|
112 |
next
|
|
113 |
from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
|
|
114 |
by (auto simp only: intro: beta.intros)
|
|
115 |
moreover
|
|
116 |
from assms have "(Var 1)[Var 0/0] = t'" by simp
|
|
117 |
ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
|
|
118 |
next
|
|
119 |
from assms show "\<not> \<Gamma> \<turnstile> t' : U"
|
|
120 |
by (auto elim: typing.cases nth_el1.cases)
|
|
121 |
qed
|
|
122 |
|
|
123 |
|
|
124 |
end
|
|
125 |
|