--- 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 =