src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
changeset 38948 c4e6afaa8dcd
child 38950 62578950e748
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 08:00:51 2010 +0200
     1.3 @@ -0,0 +1,125 @@
     1.4 +theory Lambda_Example
     1.5 +imports Code_Prolog
     1.6 +begin
     1.7 +
     1.8 +subsection {* Lambda *}
     1.9 +
    1.10 +datatype type =
    1.11 +    Atom nat
    1.12 +  | Fun type type    (infixr "\<Rightarrow>" 200)
    1.13 +
    1.14 +datatype dB =
    1.15 +    Var nat
    1.16 +  | App dB dB (infixl "\<degree>" 200)
    1.17 +  | Abs type dB
    1.18 +
    1.19 +primrec
    1.20 +  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
    1.21 +where
    1.22 +  "[]\<langle>i\<rangle> = None"
    1.23 +| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
    1.24 +
    1.25 +inductive nth_el1 :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
    1.26 +where
    1.27 +  "nth_el1 (x # xs) 0 x"
    1.28 +| "nth_el1 xs i y \<Longrightarrow> nth_el1 (x # xs) (Suc i) y"
    1.29 +
    1.30 +inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    1.31 +  where
    1.32 +    Var [intro!]: "nth_el1 env x T \<Longrightarrow> env \<turnstile> Var x : T"
    1.33 +  | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
    1.34 +  | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
    1.35 +
    1.36 +primrec
    1.37 +  lift :: "[dB, nat] => dB"
    1.38 +where
    1.39 +    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
    1.40 +  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
    1.41 +  | "lift (Abs T s) k = Abs T (lift s (k + 1))"
    1.42 +
    1.43 +primrec pred :: "nat => nat"
    1.44 +where
    1.45 +  "pred (Suc i) = i"
    1.46 +
    1.47 +primrec
    1.48 +  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
    1.49 +where
    1.50 +    subst_Var: "(Var i)[s/k] =
    1.51 +      (if k < i then Var (pred i) else if i = k then s else Var i)"
    1.52 +  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
    1.53 +  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
    1.54 +
    1.55 +inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    1.56 +  where
    1.57 +    beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
    1.58 +  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
    1.59 +  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
    1.60 +  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
    1.61 +
    1.62 +subsection {* Inductive definitions for ordering on naturals *}
    1.63 +
    1.64 +inductive less_nat
    1.65 +where
    1.66 +  "less_nat 0 (Suc y)"
    1.67 +| "less_nat x y ==> less_nat (Suc x) (Suc y)"
    1.68 +
    1.69 +lemma less_nat[code_pred_inline]:
    1.70 +  "x < y = less_nat x y"
    1.71 +apply (rule iffI)
    1.72 +apply (induct x arbitrary: y)
    1.73 +apply (case_tac y) apply (auto intro: less_nat.intros)
    1.74 +apply (case_tac y)
    1.75 +apply (auto intro: less_nat.intros)
    1.76 +apply (induct rule: less_nat.induct)
    1.77 +apply auto
    1.78 +done
    1.79 +
    1.80 +lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
    1.81 +by simp
    1.82 +
    1.83 +section {* Manual setup to find counterexample *}
    1.84 +
    1.85 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    1.86 +
    1.87 +ML {* Code_Prolog.options :=
    1.88 +  { ensure_groundness = true,
    1.89 +    limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
    1.90 +    limited_predicates = [("typing", 2), ("nth_el1", 2)],
    1.91 +    replacing = [(("typing", "limited_typing"), "quickcheck"),
    1.92 +                 (("nth_el1", "limited_nth_el1"), "lim_typing")],
    1.93 +    prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.94 +
    1.95 +lemma
    1.96 +  "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
    1.97 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.98 +oops
    1.99 +
   1.100 +text {* Verifying that the found counterexample really is one by means of a proof *}
   1.101 +
   1.102 +lemma
   1.103 +assumes
   1.104 +  "t' = Var 0"
   1.105 +  "U = Atom 0"
   1.106 +  "\<Gamma> = [Atom 1]"
   1.107 +  "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
   1.108 +shows
   1.109 +  "\<Gamma> \<turnstile> t : U"
   1.110 +  "t \<rightarrow>\<^sub>\<beta> t'"
   1.111 +  "\<not> \<Gamma> \<turnstile> t' : U"
   1.112 +proof -
   1.113 +  from assms show "\<Gamma> \<turnstile> t : U"
   1.114 +    by (auto intro!: typing.intros nth_el1.intros)
   1.115 +next
   1.116 +  from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
   1.117 +    by (auto simp only: intro: beta.intros)
   1.118 +  moreover
   1.119 +  from assms have "(Var 1)[Var 0/0] = t'" by simp
   1.120 +  ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
   1.121 +next
   1.122 +  from assms show "\<not> \<Gamma> \<turnstile> t' : U"
   1.123 +    by (auto elim: typing.cases nth_el1.cases)
   1.124 +qed
   1.125 +
   1.126 +
   1.127 +end
   1.128 +