--- a/src/HOL/IsaMakefile Tue Aug 31 08:00:50 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 31 08:00:51 2010 +0200
@@ -1322,7 +1322,8 @@
Predicate_Compile_Examples/Predicate_Compile_Examples.thy \
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
Predicate_Compile_Examples/Code_Prolog_Examples.thy \
- Predicate_Compile_Examples/Hotel_Example.thy
+ Predicate_Compile_Examples/Hotel_Example.thy \
+ Predicate_Compile_Examples/Lambda_Example.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Aug 31 08:00:51 2010 +0200
@@ -0,0 +1,125 @@
+theory Lambda_Example
+imports Code_Prolog
+begin
+
+subsection {* Lambda *}
+
+datatype type =
+ Atom nat
+ | Fun type type (infixr "\<Rightarrow>" 200)
+
+datatype dB =
+ Var nat
+ | App dB dB (infixl "\<degree>" 200)
+ | Abs type dB
+
+primrec
+ nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
+where
+ "[]\<langle>i\<rangle> = None"
+| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
+
+inductive nth_el1 :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "nth_el1 (x # xs) 0 x"
+| "nth_el1 xs i y \<Longrightarrow> nth_el1 (x # xs) (Suc i) y"
+
+inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ where
+ Var [intro!]: "nth_el1 env x T \<Longrightarrow> env \<turnstile> Var x : T"
+ | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
+ | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+
+primrec
+ lift :: "[dB, nat] => dB"
+where
+ "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
+ | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
+ | "lift (Abs T s) k = Abs T (lift s (k + 1))"
+
+primrec pred :: "nat => nat"
+where
+ "pred (Suc i) = i"
+
+primrec
+ subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
+where
+ subst_Var: "(Var i)[s/k] =
+ (if k < i then Var (pred i) else if i = k then s else Var i)"
+ | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
+ | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
+
+inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ where
+ beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+ | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+ | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+ | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
+
+subsection {* Inductive definitions for ordering on naturals *}
+
+inductive less_nat
+where
+ "less_nat 0 (Suc y)"
+| "less_nat x y ==> less_nat (Suc x) (Suc y)"
+
+lemma less_nat[code_pred_inline]:
+ "x < y = less_nat x y"
+apply (rule iffI)
+apply (induct x arbitrary: y)
+apply (case_tac y) apply (auto intro: less_nat.intros)
+apply (case_tac y)
+apply (auto intro: less_nat.intros)
+apply (induct rule: less_nat.induct)
+apply auto
+done
+
+lemma [code_pred_inline]: "(x::nat) + 1 = Suc x"
+by simp
+
+section {* Manual setup to find counterexample *}
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+ML {* Code_Prolog.options :=
+ { ensure_groundness = true,
+ limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
+ limited_predicates = [("typing", 2), ("nth_el1", 2)],
+ replacing = [(("typing", "limited_typing"), "quickcheck"),
+ (("nth_el1", "limited_nth_el1"), "lim_typing")],
+ prolog_system = Code_Prolog.SWI_PROLOG} *}
+
+lemma
+ "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+text {* Verifying that the found counterexample really is one by means of a proof *}
+
+lemma
+assumes
+ "t' = Var 0"
+ "U = Atom 0"
+ "\<Gamma> = [Atom 1]"
+ "t = App (Abs (Atom 0) (Var 1)) (Var 0)"
+shows
+ "\<Gamma> \<turnstile> t : U"
+ "t \<rightarrow>\<^sub>\<beta> t'"
+ "\<not> \<Gamma> \<turnstile> t' : U"
+proof -
+ from assms show "\<Gamma> \<turnstile> t : U"
+ by (auto intro!: typing.intros nth_el1.intros)
+next
+ from assms have "t \<rightarrow>\<^sub>\<beta> (Var 1)[Var 0/0]"
+ by (auto simp only: intro: beta.intros)
+ moreover
+ from assms have "(Var 1)[Var 0/0] = t'" by simp
+ ultimately show "t \<rightarrow>\<^sub>\<beta> t'" by simp
+next
+ from assms show "\<not> \<Gamma> \<turnstile> t' : U"
+ by (auto elim: typing.cases nth_el1.cases)
+qed
+
+
+end
+
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Aug 31 08:00:50 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Aug 31 08:00:51 2010 +0200
@@ -1,2 +1,2 @@
use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 08:00:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Aug 31 08:00:51 2010 +0200
@@ -13,7 +13,7 @@
limited_predicates : (string * int) list,
replacing : ((string * string) * string) list,
prolog_system : prolog_system}
- val options : code_options ref
+ val options : code_options Unsynchronized.ref
datatype arith_op = Plus | Minus
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list