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