src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40924 a9be7f26b4e6
child 41956 c15ef1b85035
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     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 {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    83 
    84 setup {* Code_Prolog.map_code_options (K 
    85   { ensure_groundness = true,
    86     limit_globally = NONE,
    87     limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
    88     limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
    89     replacing = [(("typing", "limited_typing"), "quickcheck"),
    90                  (("nthel1", "limited_nthel1"), "lim_typing")],
    91     manual_reorder = []}) *}
    92 
    93 lemma
    94   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
    95 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
    96 oops
    97 
    98 text {* Verifying that the found counterexample really is one by means of a proof *}
    99 
   100 lemma
   101 assumes
   102   "t' = Var 0"
   103   "U = Atom 0"
   104   "\<Gamma> = [Atom 1]"
   105   "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
   106 shows
   107   "\<Gamma> \<turnstile> t : U"
   108   "t \<rightarrow>\<^sub>\<beta> t'"
   109   "\<not> \<Gamma> \<turnstile> t' : U"
   110 proof -
   111   from assms show "\<Gamma> \<turnstile> t : U"
   112     by (auto intro!: typing.intros nth_el1.intros)
   113 next
   114   from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
   115     by (auto simp only: intro: beta.intros)
   116   moreover
   117   from assms have "(Var 1)[Var 0/0] = t'" by simp
   118   ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
   119 next
   120   from assms show "\<not> \<Gamma> \<turnstile> t' : U"
   121     by (auto elim: typing.cases nth_el1.cases)
   122 qed
   123 
   124 
   125 end
   126