merged
authorbulwahn
Wed, 01 Sep 2010 07:53:31 +0200
changeset 38965 45e4d3a855ad
parent 38964 b1a7bef0907a (diff)
parent 38946 da5e4f182f69 (current diff)
child 38966 68853347ba37
merged
src/HOL/IsaMakefile
--- a/src/HOL/Auth/Event.thy	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Auth/Event.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -22,14 +22,6 @@
        
 consts 
   bad    :: "agent set"                         -- {* compromised agents *}
-  knows  :: "agent => event list => msg set"
-
-
-text{*The constant "spies" is retained for compatibility's sake*}
-
-abbreviation (input)
-  spies  :: "event list => msg set" where
-  "spies == knows Spy"
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}
 specification (bad)
@@ -37,9 +29,10 @@
   Server_not_bad [iff]: "Server \<notin> bad"
     by (rule exI [of _ "{Spy}"], simp)
 
-primrec
+primrec knows :: "agent => event list => msg set"
+where
   knows_Nil:   "knows A [] = initState A"
-  knows_Cons:
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then 
         (case ev of
@@ -62,14 +55,20 @@
   therefore the oops case must use Notes
 *)
 
-consts
-  (*Set of items that might be visible to somebody:
+text{*The constant "spies" is retained for compatibility's sake*}
+
+abbreviation (input)
+  spies  :: "event list => msg set" where
+  "spies == knows Spy"
+
+
+(*Set of items that might be visible to somebody:
     complement of the set of fresh items*)
-  used :: "event list => msg set"
 
-primrec
+primrec used :: "event list => msg set"
+where
   used_Nil:   "used []         = (UN B. parts (initState B))"
-  used_Cons:  "used (ev # evs) =
+| used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs
--- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -203,7 +203,7 @@
 apply clarify
 apply (frule_tac A' = A in 
        Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
-apply (rename_tac C B' evs3)
+apply (rename_tac evs3 B' C)
 txt{*This is the attack!
 @{subgoals[display,indent=0,margin=65]}
 *}
--- a/src/HOL/IsaMakefile	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 01 07:53:31 2010 +0200
@@ -1323,7 +1323,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
 
 
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -10,17 +10,35 @@
   "append [] ys ys"
 | "append xs ys zs ==> append (x # xs) ys (x # zs)"
 
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = false,
+   limited_types = [],
+   limited_predicates = [],
+   replacing = [],
+   manual_reorder = [],
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values "{(x, y, z). append x y z}"
 
 values 3 "{(x, y, z). append x y z}"
 
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = false,
+   limited_types = [],
+   limited_predicates = [],
+   replacing = [],
+   manual_reorder = [],
+   prolog_system = Code_Prolog.YAP}) *}
 
 values "{(x, y, z). append x y z}"
 
-ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = false,
+   limited_types = [],
+   limited_predicates = [],
+   replacing = [],
+   manual_reorder = [],
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
 section {* Example queens *}
@@ -183,7 +201,13 @@
 where
   "y \<noteq> B \<Longrightarrow> notB y"
 
-ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+   limited_types = [],
+   limited_predicates = [],
+   replacing = [],
+   manual_reorder = [], 
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values 2 "{y. notB y}"
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -0,0 +1,169 @@
+theory Context_Free_Grammar_Example
+imports Code_Prolog
+begin
+
+declare mem_def[code_pred_inline]
+
+
+subsection {* Alternative rules for length *}
+
+definition size_list :: "'a list => nat"
+where "size_list = size"
+
+lemma size_list_simps:
+  "size_list [] = 0"
+  "size_list (x # xs) = Suc (size_list xs)"
+by (auto simp add: size_list_def)
+
+declare size_list_simps[code_pred_def]
+declare size_list_def[symmetric, code_pred_inline]
+
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+datatype alphabet = a | b
+
+inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
+  "[] \<in> S\<^isub>1"
+| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
+| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
+| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
+
+lemma
+  "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+definition "filter_a = filter (\<lambda>x. x = a)"
+
+lemma [code_pred_def]: "filter_a [] = []"
+unfolding filter_a_def by simp
+
+lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
+unfolding filter_a_def by simp
+
+declare filter_a_def[symmetric, code_pred_inline]
+
+definition "filter_b = filter (\<lambda>x. x = b)"
+
+lemma [code_pred_def]: "filter_b [] = []"
+unfolding filter_b_def by simp
+
+lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
+unfolding filter_b_def by simp
+
+declare filter_b_def[symmetric, code_pred_inline]
+
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [(["s1", "a1", "b1"], 2)],
+  replacing = [(("s1", "limited_s1"), "quickcheck")],
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>1_sound:
+"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, iterations=1, expect = counterexample]
+oops
+
+
+inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
+  "[] \<in> S\<^isub>2"
+| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
+| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
+| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
+| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
+
+
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [(["s2", "a2", "b2"], 3)],
+  replacing = [(("s2", "limited_s2"), "quickcheck")],
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>2_sound:
+"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, expect = counterexample]
+oops
+
+inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
+  "[] \<in> S\<^isub>3"
+| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
+| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
+| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
+| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
+
+
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [(["s3", "a3", "b3"], 6)],
+  replacing = [(("s3", "limited_s3"), "quickcheck")],
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma S\<^isub>3_sound:
+"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+oops
+
+
+(*
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [],
+  replacing = [],
+  manual_reorder = [],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>3_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+quickcheck[generator = prolog, size=1, iterations=1]
+oops
+*)
+
+inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
+  "[] \<in> S\<^isub>4"
+| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
+| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
+| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
+| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
+| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
+
+
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [(["s4", "a4", "b4"], 6)],
+  replacing = [(("s4", "limited_s4"), "quickcheck")],
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+
+theorem S\<^isub>4_sound:
+"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+oops
+
+(*
+theorem S\<^isub>4_complete:
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
+oops
+*)
+
+hide_const a b
+
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -84,18 +84,46 @@
 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
 by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
 
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+setup {* Code_Prolog.map_code_options (K
+  {ensure_groundness = true,
+  limited_types = [],
+  limited_predicates = [],
+  replacing = [],
+  manual_reorder = [],
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values 40 "{s. hotel s}"
 
 
 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
-ML {* set Code_Prolog.trace *}
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
 quickcheck[generator = code, iterations = 100000, report]
-quickcheck[generator = prolog, iterations = 1]
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
 oops
 
 
+definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
+[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
+
+
+definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
+where
+  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
+   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+
+setup {* Code_Prolog.map_code_options (K 
+  {ensure_groundness = true,
+   limited_types = [],
+   limited_predicates = [(["hotel"], 5)],
+   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+   manual_reorder = [],
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
 end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Wed Sep 01 07:53:31 2010 +0200
@@ -0,0 +1,126 @@
+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) *}
+
+setup {* Code_Prolog.map_code_options (K 
+  { ensure_groundness = true,
+    limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
+    limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
+    replacing = [(("typing", "limited_typing"), "quickcheck"),
+                 (("nthel1", "limited_nthel1"), "lim_typing")],
+    manual_reorder = [],
+    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 21:17:19 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Sep 01 07:53:31 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 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 01 07:53:31 2010 +0200
@@ -8,8 +8,14 @@
 sig
   datatype prolog_system = SWI_PROLOG | YAP
   type code_options =
-    {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
-  val options : code_options ref
+    {ensure_groundness : bool,
+     limited_types : (typ * int) list,
+     limited_predicates : (string list * int) list,
+     replacing : ((string * string) * string) list,
+     manual_reorder : ((string * int) * int list) list,
+     prolog_system : prolog_system}
+  val code_options_of : theory -> code_options 
+  val map_code_options : (code_options -> code_options) -> theory -> theory
 
   datatype arith_op = Plus | Minus
   datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
@@ -31,6 +37,8 @@
   val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
 
   val trace : bool Unsynchronized.ref
+  
+  val replace : ((string * string) * string) -> logic_program -> logic_program
 end;
 
 structure Code_Prolog : CODE_PROLOG =
@@ -47,10 +55,38 @@
 datatype prolog_system = SWI_PROLOG | YAP
 
 type code_options =
-  {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+  {ensure_groundness : bool,
+   limited_types : (typ * int) list,
+   limited_predicates : (string list * int) list,
+   replacing : ((string * string) * string) list,
+   manual_reorder : ((string * int) * int list) list,
+   prolog_system : prolog_system}
 
-val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
-  prolog_system = SWI_PROLOG};
+structure Options = Theory_Data
+(
+  type T = code_options
+  val empty = {ensure_groundness = false,
+    limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [],
+    prolog_system = SWI_PROLOG}
+  val extend = I;
+  fun merge
+    ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
+      limited_predicates = limited_predicates1, replacing = replacing1,
+      manual_reorder = manual_reorder1, prolog_system = prolog_system1},
+     {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
+      limited_predicates = limited_predicates2, replacing = replacing2,
+      manual_reorder = manual_reorder2, prolog_system = prolog_system2}) =
+    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+     limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
+     limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
+     manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
+     replacing = Library.merge (op =) (replacing1, replacing2),
+     prolog_system = prolog_system1};
+);
+
+val code_options_of = Options.get
+
+val map_code_options = Options.map
 
 (* general string functions *)
 
@@ -124,16 +160,32 @@
 
 (* translation from introduction rules to internal representation *)
 
+fun mk_conform f empty avoid name =
+  let
+    fun dest_Char (Symbol.Char c) = c
+    val name' = space_implode "" (map (dest_Char o Symbol.decode)
+      (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
+        (Symbol.explode name)))
+    val name'' = f (if name' = "" then empty else name')
+  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+
 (** constant table **)
 
 type constant_table = (string * string) list
 
 (* assuming no clashing *)
-fun mk_constant_table consts =
-  AList.make (first_lower o Long_Name.base_name) consts
-
 fun declare_consts consts constant_table =
-  fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table
+  let
+    fun update' c table =
+      if AList.defined (op =) table c then table else
+        let
+          val c' = mk_conform first_lower "pred" (map snd table) (Long_Name.base_name c)
+        in
+          AList.update (op =) (c, c') table
+        end
+  in
+    fold update' consts constant_table
+  end
   
 fun translate_const constant_table c =
   case AList.lookup (op =) constant_table c of
@@ -234,7 +286,8 @@
         val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
         val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
       in clause end
-  in (map translate_intro intros', constant_table') end
+    val res = (map translate_intro intros', constant_table')
+  in res end
 
 fun depending_preds_of (key, intros) =
   fold Term.add_const_names (map Thm.prop_of intros) []
@@ -263,7 +316,7 @@
     val gr = Predicate_Compile_Core.intros_graph_of ctxt
     val gr' = add_edges depending_preds_of const gr
     val scc = strong_conn_of gr' [const]
-    val constant_table = mk_constant_table (flat scc)
+    val constant_table = declare_consts (flat scc) []
   in
     apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
   end
@@ -347,28 +400,88 @@
     ((flat grs) @ p', constant_table')
   end
 
+(* make depth-limited version of predicate *)
+
+fun mk_lim_rel_name rel_name = "lim_" ^ rel_name
+
+fun mk_depth_limited rel_names ((rel_name, ts), prem) =
+  let
+    fun has_positive_recursive_prems (Conj prems) = exists has_positive_recursive_prems prems
+      | has_positive_recursive_prems (Rel (rel, ts)) = member (op =) rel_names rel
+      | has_positive_recursive_prems _ = false
+    fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems)
+      | mk_lim_prem (p as Rel (rel, ts)) =
+        if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p
+      | mk_lim_prem p = p
+  in
+    if has_positive_recursive_prems prem then
+      ((mk_lim_rel_name rel_name, (AppF ("suc", [Var "Lim"]))  :: ts), mk_lim_prem prem)
+    else
+      ((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
+  end
+
+fun add_limited_predicates limited_predicates =
+  let                                     
+    fun add (rel_names, limit) (p, constant_table) = 
+      let
+        val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
+        val clauses' = map (mk_depth_limited rel_names) clauses
+        fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+        fun mk_entry_clause rel_name =
+          let
+            val nargs = length (snd (fst
+              (the (find_first (fn ((rel, _), _) => rel = rel_name) clauses))))
+            val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)        
+          in
+            (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+          end
+      in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+  in
+    fold add limited_predicates
+  end
+
+
+(* replace predicates in clauses *)
+
+(* replace (A, B, C) p = replace A by B in clauses of C *)
+fun replace ((from, to), location) p =
+  let
+    fun replace_prem (Conj prems) = Conj (map replace_prem prems)
+      | replace_prem (r as Rel (rel, ts)) =
+          if rel = from then Rel (to, ts) else r
+      | replace_prem r = r
+  in
+    map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p
+  end
+
   
+(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *)
+
+fun reorder_manually reorder p =
+  let
+    fun reorder' (clause as ((rel, args), prem)) seen =
+      let
+        val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen
+        val i = the (AList.lookup (op =) seen' rel)
+        val perm = AList.lookup (op =) reorder (rel, i)
+        val prem' = (case perm of 
+          SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
+        | NONE => prem)
+      in (((rel, args), prem'), seen') end
+  in
+    fst (fold_map reorder' p [])
+  end
 (* rename variables to prolog-friendly names *)
 
 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
 
 fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming)
 
-fun dest_Char (Symbol.Char c) = c
-
 fun is_prolog_conform v =
   forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
-
-fun mk_conform avoid v =
-  let 
-    val v' = space_implode "" (map (dest_Char o Symbol.decode)
-      (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
-        (Symbol.explode v)))
-    val v' = if v' = "" then "var" else v'
-  in Name.variant avoid (first_upper v') end
   
 fun mk_renaming v renaming =
-  (v, mk_conform (map snd renaming) v) :: renaming
+  (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
 
 fun rename_vars_clause ((rel, args), prem) =
   let
@@ -377,7 +490,7 @@
   in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
   
 val rename_vars_program = map rename_vars_clause
-  
+
 (* code printer *)
 
 fun write_arith_op Plus = "+"
@@ -460,7 +573,7 @@
   let
     val cmd =
       case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
-  in bash_output (cmd ^ file_name) end
+  in fst (bash_output (cmd ^ file_name)) end
 
 (* parsing prolog solution *)
 
@@ -508,24 +621,23 @@
         (l :: r :: []) => parse_term (unprefix " " r)
       | _ => raise Fail "unexpected equation in prolog output"
     fun parse_solution s = map dest_eq (space_explode ";" s)
+    val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)  
   in
-    map parse_solution (fst (split_last (space_explode "\n" sol)))
+    map parse_solution sols
   end 
   
 (* calling external interpreter and getting results *)
 
 fun run system p query_rel vnames nsols =
   let
-    val cmd = Path.named_root
     val p' = rename_vars_program p
     val _ = tracing "Renaming variable names..."
     val renaming = fold mk_renaming vnames [] 
     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
     val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
     val _ = tracing ("Generated prolog program:\n" ^ prog)
-    val prolog_file = File.tmp_path (Path.basic "prolog_file")
-    val _ = File.write prolog_file prog
-    val (solution, _) = invoke system (File.shell_path prolog_file)
+    val solution = Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
+      (File.write prolog_file prog; invoke system (Path.implode prolog_file)))
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution
   in
@@ -577,7 +689,7 @@
 
 fun values ctxt soln t_compr =
   let
-    val options = !options
+    val options = code_options_of (ProofContext.theory_of ctxt)
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
     val (body, Ts, fp) = HOLogic.strip_psplits split;
@@ -605,6 +717,9 @@
       |> (if #ensure_groundness options then
           add_ground_predicates ctxt' (#limited_types options)
         else I)
+      |> add_limited_predicates (#limited_predicates options)
+      |> apfst (fold replace (#replacing options))
+      |> apfst (reorder_manually (#manual_reorder options))
     val _ = tracing "Running prolog program..."
     val tss = run (#prolog_system options)
       p (translate_const constant_table name) (map first_upper vnames) soln
@@ -675,6 +790,7 @@
 
 fun quickcheck ctxt report t size =
   let
+    val options = code_options_of (ProofContext.theory_of ctxt)
     val thy = Theory.copy (ProofContext.theory_of ctxt)
     val (vs, t') = strip_abs t
     val vs' = Variable.variant_frees ctxt [] vs
@@ -696,12 +812,18 @@
     val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate true ctxt' full_constname
-      |> add_ground_predicates ctxt' (#limited_types (!options))
+      |> add_ground_predicates ctxt' (#limited_types options)
+      |> add_limited_predicates (#limited_predicates options)
+      |> apfst (fold replace (#replacing options))
+      |> apfst (reorder_manually (#manual_reorder options))
     val _ = tracing "Running prolog program..."
-    val [ts] = run (#prolog_system (!options))
+    val tss = run (#prolog_system options)
       p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."
-    val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+    val res =
+      case tss of
+        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+      | _ => NONE
     val empty_report = ([], false)
   in
     (res, empty_report)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 01 07:53:31 2010 +0200
@@ -63,6 +63,19 @@
   val add_random_dseq_equations : options -> string list -> theory -> theory
   val add_new_random_dseq_equations : options -> string list -> theory -> theory
   val mk_tracing : string -> term -> term
+  val prepare_intrs : options -> compilation -> theory -> string list -> thm list ->
+    ((string * typ) list * string list * string list * (string * mode list) list *
+      (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
+  type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}  
+  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
+  | Mode_Pair of mode_derivation * mode_derivation | Term of mode
+  type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
+  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
+
+  val infer_modes : 
+    mode_analysis_options -> options -> compilation -> (string * typ) list -> (string * mode list) list ->
+      string list -> (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
+      theory -> ((moded_clause list pred_mode_table * string list) * theory)
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 01 07:53:31 2010 +0200
@@ -351,13 +351,17 @@
         |> map (fn (resargs, (names', prems')) =>
           let
             val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
-          in (prem'::prems', names') end)
+          in (prems' @ [prem'], names') end)
       end
     val intro_ts' = folds_map rewrite prems frees
       |> maps (fn (prems', frees') =>
         rewrite concl frees'
-        |> map (fn (concl'::conclprems, _) =>
-          Logic.list_implies ((flat prems') @ conclprems, concl')))
+        |> map (fn (conclprems, _) =>
+          let
+            val (conclprems', concl') = split_last conclprems
+          in
+            Logic.list_implies ((flat prems') @ conclprems', concl')
+          end))
     (*val _ = tracing ("Rewritten intro to " ^
       commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
   in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Sep 01 07:53:31 2010 +0200
@@ -259,7 +259,8 @@
 
 fun rewrite_intros thy =
   Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
-  #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+  #> Simplifier.full_simplify
+    (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
   #> map_term thy (maps_premises (split_conjs thy))
 
 fun print_specs options thy msg ths =