|
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 |