--- a/CONTRIBUTORS Thu Nov 12 14:31:11 2009 -0800
+++ b/CONTRIBUTORS Thu Nov 12 14:31:29 2009 -0800
@@ -6,7 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
-
+* November 2009: Lukas Bulwahn, TUM
+ Predicate Compiler: a compiler for inductive predicates to equational specfications
+
* November 2009: Sascha Boehme, TUM
HOL-Boogie: an interactive prover back-end for Boogie and VCC
--- a/NEWS Thu Nov 12 14:31:11 2009 -0800
+++ b/NEWS Thu Nov 12 14:31:29 2009 -0800
@@ -37,6 +37,9 @@
*** HOL ***
+* New commands "code_pred" and "values" to invoke the predicate compiler
+and to enumerate values of inductive predicates.
+
* Combined former theories Divides and IntDiv to one theory Divides
in the spirit of other number theory theories in HOL; some constants
(and to a lesser extent also facts) have been suffixed with _nat und _int
@@ -91,6 +94,9 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
+* Added theorem List.map_map as [simp]. Removed List.map_compose.
+INCOMPATIBILITY.
+
* New testing tool "Mirabelle" for automated (proof) tools. Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
every proof step in a theory. To be used in batch mode via the
--- a/src/FOL/ex/LocaleTest.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/FOL/ex/LocaleTest.thy Thu Nov 12 14:31:29 2009 -0800
@@ -453,8 +453,7 @@
subsection {* Interpretation in theory, then sublocale *}
-interpretation (* fol: *) logic "op +" "minus"
-(* FIXME declaration of qualified names *)
+interpretation fol: logic "op +" "minus"
by unfold_locales (rule int_assoc int_minus2)+
locale logic2 =
@@ -464,17 +463,15 @@
and notnot: "-- (-- x) = x"
begin
-(* FIXME interpretation below fails
definition lor (infixl "||" 50) where
"x || y = --(-- x && -- y)"
-*)
end
sublocale logic < two: logic2
by unfold_locales (rule assoc notnot)+
-thm two.assoc
+thm fol.two.assoc
subsection {* Declarations and sublocale *}
--- a/src/HOL/Code_Evaluation.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Code_Evaluation.thy Thu Nov 12 14:31:29 2009 -0800
@@ -145,7 +145,7 @@
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
code_const "term_of \<Colon> String.literal \<Rightarrow> term"
- (Eval "HOLogic.mk'_message'_string")
+ (Eval "HOLogic.mk'_literal")
code_reserved Eval HOLogic
--- a/src/HOL/Datatype.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Datatype.thy Thu Nov 12 14:31:29 2009 -0800
@@ -562,6 +562,14 @@
Sumr :: "('b => 'c) => 'a + 'b => 'c"
"Sumr == sum_case undefined"
+lemma [code]:
+ "Suml f (Inl x) = f x"
+ by (simp add: Suml_def)
+
+lemma [code]:
+ "Sumr f (Inr x) = f x"
+ by (simp add: Sumr_def)
+
lemma Suml_inject: "Suml f = Suml g ==> f = g"
by (unfold Suml_def) (erule sum_case_inject)
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 14:31:29 2009 -0800
@@ -1928,7 +1928,8 @@
{ fix t n assume tnY: "(t,n) \<in> set ?Y"
hence "(t,n) \<in> set ?SS" by simp
hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
- by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
+ by (auto simp add: split_def simp del: map_map)
+ (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
from simp_num_pair_l[OF tnb np tns]
--- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 14:31:29 2009 -0800
@@ -1522,7 +1522,7 @@
also fix y have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"
using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
also have "\<dots> = (Ifm bs (decr ?cyes) \<and> Ifm bs (E ?cno))"
- by (auto simp add: decr[OF yes_nb])
+ by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv)
also have "\<dots> = (Ifm bs (conj (decr ?cyes) (qe ?cno)))"
using qe[rule_format, OF no_qf] by auto
finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)"
@@ -5298,7 +5298,8 @@
{ fix t n assume tnY: "(t,n) \<in> set ?Y"
hence "(t,n) \<in> set ?SS" by simp
hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
- by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
+ by (auto simp add: split_def simp del: map_map)
+ (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
from simp_num_pair_l[OF tnb np tns]
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 12 14:31:29 2009 -0800
@@ -1233,7 +1233,7 @@
also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
- by (auto simp add: decr0[OF yes_nb])
+ by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
using qe[rule_format, OF no_qf] by auto
finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"
--- a/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 14:31:29 2009 -0800
@@ -231,7 +231,7 @@
the literature? *}
lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
- by (simp add: get_array_def set_array_def)
+ by (simp add: get_array_def set_array_def o_def)
lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
by (simp add: noteq_arrs_def get_array_def set_array_def)
--- a/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 14:31:29 2009 -0800
@@ -130,7 +130,7 @@
"MAP_o" > "HOL4Base.rich_list.MAP_o"
"MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC"
"MAP_REVERSE" > "List.rev_map"
- "MAP_MAP_o" > "List.map_compose"
+ "MAP_MAP_o" > "List.map_map"
"MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR"
"MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL"
"MAP_FLAT" > "List.map_concat"
--- a/src/HOL/Integration.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Integration.thy Thu Nov 12 14:31:29 2009 -0800
@@ -542,7 +542,7 @@
apply (erule subst)
apply (subst listsum_subtractf [symmetric])
apply (rule listsum_abs [THEN order_trans])
- apply (subst map_compose [symmetric, unfolded o_def])
+ apply (subst map_map [unfolded o_def])
apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
apply (erule ssubst)
apply (simp add: abs_minus_commute)
--- a/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 14:31:29 2009 -0800
@@ -186,7 +186,7 @@
by (rule typing.App)
qed
with Cons True show ?thesis
- by (simp add: map_compose [symmetric] comp_def)
+ by (simp add: comp_def)
qed
next
case False
--- a/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 14:31:29 2009 -0800
@@ -148,7 +148,7 @@
hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
by (rule lift_types)
thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
- by (simp_all add: map_compose [symmetric] o_def)
+ by (simp_all add: o_def)
qed
with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
by (rule subject_reduction')
@@ -167,7 +167,7 @@
also note rred
finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
with rnf Cons eq show ?thesis
- by (simp add: map_compose [symmetric] o_def) iprover
+ by (simp add: o_def) iprover
qed
next
assume neq: "x \<noteq> i"
--- a/src/HOL/Library/Countable.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Library/Countable.thy Thu Nov 12 14:31:29 2009 -0800
@@ -165,7 +165,7 @@
text {* Lists *}
lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
- by (simp add: comp_def map_compose [symmetric])
+ by (simp add: comp_def)
primrec
list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
--- a/src/HOL/Library/Enum.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Library/Enum.thy Thu Nov 12 14:31:29 2009 -0800
@@ -10,7 +10,7 @@
class enum =
fixes enum :: "'a list"
- assumes UNIV_enum [code]: "UNIV = set enum"
+ assumes UNIV_enum: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
@@ -72,7 +72,7 @@
by (induct n) simp_all
lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
- by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv)
+ by (induct n) (auto simp add: length_concat o_def listsum_triv)
lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
by (induct n arbitrary: ys) auto
@@ -114,10 +114,6 @@
by (simp add: length_n_lists)
qed
-lemma map_of_zip_map: (*FIXME move to Map.thy*)
- "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
- by (induct xs) (simp_all add: expand_fun_eq)
-
lemma map_of_zip_enum_is_Some:
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
@@ -250,7 +246,7 @@
by (auto simp add: image_def)
have "set (map set (sublists xs)) = Pow (set xs)"
by (induct xs)
- (simp_all add: aux Let_def Pow_insert Un_commute)
+ (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
then show ?thesis by simp
qed
--- a/src/HOL/Library/Mapping.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Library/Mapping.thy Thu Nov 12 14:31:29 2009 -0800
@@ -128,7 +128,7 @@
lemma bulkload_tabulate:
"bulkload xs = tabulate [0..<length xs] (nth xs)"
by (rule sym)
- (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
+ (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def)
subsection {* Some technical code lemmas *}
--- a/src/HOL/List.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/List.thy Thu Nov 12 14:31:29 2009 -0800
@@ -272,13 +272,16 @@
"sorted [x] \<longleftrightarrow> True" |
"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
-primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort x [] = [x]" |
-"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
-
-primrec sort :: "'a list \<Rightarrow> 'a list" where
-"sort [] = []" |
-"sort (x#xs) = insort x (sort xs)"
+primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"insort_key f x [] = [x]" |
+"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
+
+primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"sort_key f [] = []" |
+"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+
+abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
+abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
end
@@ -698,8 +701,8 @@
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
by (induct xs) auto
-lemma map_compose: "map (f o g) xs = map f (map g xs)"
-by (induct xs) (auto simp add: o_def)
+lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
+by (induct xs) auto
lemma rev_map: "rev (map f xs) = map f (rev xs)"
by (induct xs) auto
@@ -1183,6 +1186,12 @@
then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
qed
+lemma partition_filter_conv[simp]:
+ "partition f xs = (filter f xs,filter (Not o f) xs)"
+unfolding partition_filter2[symmetric]
+unfolding partition_filter1[symmetric] by simp
+
+declare partition.simps[simp del]
subsubsection {* @{text concat} *}
@@ -1722,6 +1731,9 @@
subsubsection {* @{text takeWhile} and @{text dropWhile} *}
+lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
+ by (induct xs) auto
+
lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
by (induct xs) auto
@@ -1736,6 +1748,15 @@
lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
by (induct xs) auto
+lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
+apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
+
+lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
+apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
+
+lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
+by (induct xs) auto
+
lemma dropWhile_append1 [simp]:
"[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
by (induct xs) auto
@@ -1765,6 +1786,66 @@
lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
by (induct xs) auto
+lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
+by (induct xs) auto
+
+lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
+by (induct xs) auto
+
+lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
+by (induct xs) auto
+
+lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
+by (induct xs) auto
+
+lemma hd_dropWhile:
+ "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
+using assms by (induct xs) auto
+
+lemma takeWhile_eq_filter:
+ assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
+ shows "takeWhile P xs = filter P xs"
+proof -
+ have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"
+ by simp
+ have B: "filter P (dropWhile P xs) = []"
+ unfolding filter_empty_conv using assms by blast
+ have "filter P xs = takeWhile P xs"
+ unfolding A filter_append B
+ by (auto simp add: filter_id_conv dest: set_takeWhileD)
+ thus ?thesis ..
+qed
+
+lemma takeWhile_eq_take_P_nth:
+ "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
+ takeWhile P xs = take n xs"
+proof (induct xs arbitrary: n)
+ case (Cons x xs)
+ thus ?case
+ proof (cases n)
+ case (Suc n') note this[simp]
+ have "P x" using Cons.prems(1)[of 0] by simp
+ moreover have "takeWhile P xs = take n' xs"
+ proof (rule Cons.hyps)
+ case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
+ next case goal2 thus ?case using Cons by auto
+ qed
+ ultimately show ?thesis by simp
+ qed simp
+qed simp
+
+lemma nth_length_takeWhile:
+ "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
+by (induct xs) auto
+
+lemma length_takeWhile_less_P_nth:
+ assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
+ shows "j \<le> length (takeWhile P xs)"
+proof (rule classical)
+ assume "\<not> ?thesis"
+ hence "length (takeWhile P xs) < length xs" using assms by simp
+ thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
+qed
text{* The following two lemmmas could be generalized to an arbitrary
property. *}
@@ -1838,19 +1919,32 @@
"length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
by (induct rule:list_induct2, simp_all)
+lemma zip_map_map:
+ "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs) note Cons_x_xs = Cons.hyps
+ show ?case
+ proof (cases ys)
+ case (Cons y ys')
+ show ?thesis unfolding Cons using Cons_x_xs by simp
+ qed simp
+qed simp
+
+lemma zip_map1:
+ "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
+using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
+
+lemma zip_map2:
+ "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
+using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
+
lemma map_zip_map:
- "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
-apply(induct xs arbitrary:ys) apply simp
-apply(case_tac ys)
-apply simp_all
-done
+ "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
+unfolding zip_map1 by auto
lemma map_zip_map2:
- "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
-apply(induct xs arbitrary:ys) apply simp
-apply(case_tac ys)
-apply simp_all
-done
+ "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
+unfolding zip_map2 by auto
text{* Courtesy of Andreas Lochbihler: *}
lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
@@ -1867,6 +1961,9 @@
"set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
by(simp add: set_conv_nth cong: rev_conj_cong)
+lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
+by(induct xs) auto
+
lemma zip_update:
"zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
by(rule sym, simp add: update_zip)
@@ -1893,6 +1990,16 @@
apply (case_tac ys, simp_all)
done
+lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs) thus ?case by (cases ys) auto
+qed simp
+
+lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs) thus ?case by (cases ys) auto
+qed simp
+
lemma set_zip_leftD:
"(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
by (induct xs ys rule:list_induct2') auto
@@ -1913,6 +2020,35 @@
"length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
by (auto simp add: zip_map_fst_snd)
+lemma distinct_zipI1:
+ "distinct xs \<Longrightarrow> distinct (zip xs ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs)
+ show ?case
+ proof (cases ys)
+ case (Cons y ys')
+ have "(x, y) \<notin> set (zip xs ys')"
+ using Cons.prems by (auto simp: set_zip)
+ thus ?thesis
+ unfolding Cons zip_Cons_Cons distinct.simps
+ using Cons.hyps Cons.prems by simp
+ qed simp
+qed simp
+
+lemma distinct_zipI2:
+ "distinct xs \<Longrightarrow> distinct (zip xs ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs)
+ show ?case
+ proof (cases ys)
+ case (Cons y ys')
+ have "(x, y) \<notin> set (zip xs ys')"
+ using Cons.prems by (auto simp: set_zip)
+ thus ?thesis
+ unfolding Cons zip_Cons_Cons distinct.simps
+ using Cons.hyps Cons.prems by simp
+ qed simp
+qed simp
subsubsection {* @{text list_all2} *}
@@ -2259,6 +2395,12 @@
lemma length_concat: "length (concat xss) = listsum (map length xss)"
by (induct xss) simp_all
+lemma listsum_map_filter:
+ fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
+ assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
+ shows "listsum (map f (filter P xs)) = listsum (map f xs)"
+using assms by (induct xs) auto
+
text{* For efficient code generation ---
@{const listsum} is not tail recursive but @{const foldl} is. *}
lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
@@ -2640,6 +2782,11 @@
"length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
by(simp add: set_concat distinct_card[symmetric])
+lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
+proof -
+ have xs: "concat[xs] = xs" by simp
+ from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
+qed
subsubsection {* @{text remove1} *}
@@ -3083,6 +3230,12 @@
context linorder
begin
+lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
+by (induct xs, auto)
+
+lemma length_sort[simp]: "length (sort_key f xs) = length xs"
+by (induct xs, auto)
+
lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
apply(induct xs arbitrary: x) apply simp
by simp (blast intro: order_trans)
@@ -3092,37 +3245,88 @@
by (induct xs) (auto simp add:sorted_Cons)
lemma sorted_nth_mono:
- "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
+ "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
-lemma set_insort: "set(insort x xs) = insert x (set xs)"
+lemma sorted_rev_nth_mono:
+ "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
+using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
+ rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
+by auto
+
+lemma sorted_nth_monoI:
+ "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
+proof (induct xs)
+ case (Cons x xs)
+ have "sorted xs"
+ proof (rule Cons.hyps)
+ fix i j assume "i \<le> j" and "j < length xs"
+ with Cons.prems[of "Suc i" "Suc j"]
+ show "xs ! i \<le> xs ! j" by auto
+ qed
+ moreover
+ {
+ fix y assume "y \<in> set xs"
+ then obtain j where "j < length xs" and "xs ! j = y"
+ unfolding in_set_conv_nth by blast
+ with Cons.prems[of 0 "Suc j"]
+ have "x \<le> y"
+ by auto
+ }
+ ultimately
+ show ?case
+ unfolding sorted_Cons by auto
+qed simp
+
+lemma sorted_equals_nth_mono:
+ "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
+by (auto intro: sorted_nth_monoI sorted_nth_mono)
+
+lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
by (induct xs) auto
-lemma set_sort[simp]: "set(sort xs) = set xs"
+lemma set_sort[simp]: "set(sort_key f xs) = set xs"
by (induct xs) (simp_all add:set_insort)
-lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
+lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
by(induct xs)(auto simp:set_insort)
-lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
+lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
by(induct xs)(simp_all add:distinct_insort set_sort)
+lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
+by(induct xs)(auto simp:sorted_Cons set_insort)
+
lemma sorted_insort: "sorted (insort x xs) = sorted xs"
-apply (induct xs)
- apply(auto simp:sorted_Cons set_insort)
-done
+using sorted_insort_key[where f="\<lambda>x. x"] by simp
+
+theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
+by(induct xs)(auto simp:sorted_insort_key)
theorem sorted_sort[simp]: "sorted (sort xs)"
-by (induct xs) (auto simp:sorted_insort)
-
-lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
+by(induct xs)(auto simp:sorted_insort)
+
+lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
by (cases xs) auto
lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
-by (induct xs, auto simp add: sorted_Cons)
+by(induct xs)(auto simp add: sorted_Cons)
+
+lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
+ \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
+proof (induct xs)
+ case (Cons x xs)
+ thus ?case
+ proof (cases "x = a")
+ case False
+ hence "f x \<noteq> f a" using Cons.prems by auto
+ hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+ thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+ qed (auto simp: sorted_Cons insort_is_Cons)
+qed simp
lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
-by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
+using insort_key_remove1[where f="\<lambda>x. x"] by simp
lemma sorted_remdups[simp]:
"sorted l \<Longrightarrow> sorted (remdups l)"
@@ -3178,6 +3382,11 @@
case 3 then show ?case by (cases n) simp_all
qed
+lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
+ unfolding dropWhile_eq_drop by (rule sorted_drop)
+
+lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
+ apply (subst takeWhile_eq_take) by (rule sorted_take)
end
@@ -3772,6 +3981,12 @@
| "length_unique (x#xs) =
(if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
+primrec
+ concat_map :: "('a => 'b list) => 'a list => 'b list"
+where
+ "concat_map f [] = []"
+ | "concat_map f (x#xs) = f x @ concat_map f xs"
+
text {*
Only use @{text mem} for generating executable code. Otherwise use
@{prop "x : set xs"} instead --- it is much easier to reason about.
@@ -3865,7 +4080,11 @@
lemma length_remdups_length_unique [code_unfold]:
"length (remdups xs) = length_unique xs"
- by (induct xs) simp_all
+by (induct xs) simp_all
+
+lemma concat_map_code[code_unfold]:
+ "concat(map f xs) = concat_map f xs"
+by (induct xs) simp_all
declare INFI_def [code_unfold]
declare SUPR_def [code_unfold]
@@ -3923,6 +4142,11 @@
"setsum f (set [m..<n]) = listsum (map f [m..<n])"
by (rule setsum_set_distinct_conv_listsum) simp
+text {* General equivalence between @{const listsum} and @{const setsum} *}
+lemma listsum_setsum_nth:
+ "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
+using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"]
+by (simp add: map_nth)
text {* Code for summation over ints. *}
--- a/src/HOL/Map.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Map.thy Thu Nov 12 14:31:29 2009 -0800
@@ -218,6 +218,10 @@
ultimately show ?case by simp
qed
+lemma map_of_zip_map:
+ "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
+ by (induct xs) (simp_all add: expand_fun_eq)
+
lemma finite_range_map_of: "finite (range (map_of xys))"
apply (induct xys)
apply (simp_all add: image_constant)
--- a/src/HOL/MicroJava/BV/JVM.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/BV/JVM.thy Thu Nov 12 14:31:29 2009 -0800
@@ -117,11 +117,7 @@
from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
also from w have "phi' = map OK (map ok_val phi')"
- apply (clarsimp simp add: wt_step_def not_Err_eq)
- apply (rule map_id [symmetric])
- apply (erule allE, erule impE, assumption)
- apply clarsimp
- done
+ by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
finally
have check_types:
"check_types G maxs maxr (map OK (map ok_val phi'))" .
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Thu Nov 12 14:31:29 2009 -0800
@@ -166,7 +166,7 @@
by (simp add: check_types_def)
also from step
have [symmetric]: "map OK (map ok_val phi) = phi"
- by (auto intro!: map_id simp add: wt_step_def)
+ by (auto intro!: nth_equalityI simp add: wt_step_def)
finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
}
moreover {
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Nov 12 14:31:29 2009 -0800
@@ -269,12 +269,6 @@
(states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
-
-lemma map_id [rule_format]:
- "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
- by (induct xs, auto)
-
-
lemma is_type_pTs:
"\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
\<Longrightarrow> set pTs \<subseteq> types G"
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Thu Nov 12 14:31:29 2009 -0800
@@ -552,7 +552,7 @@
apply (simp only: wf_java_mdecl_def)
apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
-apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
+apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
apply (intro strip)
apply (simp (no_asm_simp) only: append_Cons [THEN sym])
apply (rule progression_lvar_init_aux)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 14:31:29 2009 -0800
@@ -132,7 +132,7 @@
apply (case_tac "vname = This")
apply (simp add: inited_LT_def)
apply (simp add: inited_LT_def)
-apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
+apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric])
apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
@@ -166,7 +166,7 @@
lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
\<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
apply (simp only: inited_LT_def)
-apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
+apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map)
apply (simp only: nth_map)
apply simp
done
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 14:31:29 2009 -0800
@@ -68,7 +68,7 @@
with fst_eq Cons
show "unique (map f (a # list)) = unique (a # list)"
- by (simp add: unique_def fst_set)
+ by (simp add: unique_def fst_set image_compose)
qed
qed
@@ -292,7 +292,7 @@
apply (simp add: method_def)
apply (frule wf_subcls1)
apply (simp add: comp_class_rec)
-apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
+apply (simp add: split_iter split_compose map_map[symmetric] del: map_map)
apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b).
(D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))"
in class_rec_relation)
@@ -311,7 +311,7 @@
apply (simp add: split_beta compMethod_def)
apply (simp add: map_of_map [THEN sym])
apply (simp add: split_beta)
-apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
+apply (simp add: Fun.comp_def split_beta)
apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
(fst x, Object,
snd (compMethod G Object
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 14:31:29 2009 -0800
@@ -284,8 +284,7 @@
apply (frule fields_rec, assumption)
apply (rule HOL.trans)
apply (simp add: o_def)
-apply (simp (no_asm_use)
- add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
+apply (simp (no_asm_use) add: split_beta split_def o_def)
done
lemma method_Object [simp]:
--- a/src/HOL/Predicate.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Predicate.thy Thu Nov 12 14:31:29 2009 -0800
@@ -828,28 +828,6 @@
code_abort not_unique
-text {* dummy setup for @{text code_pred} and @{text values} keywords *}
-
-ML {*
-local
-
-structure P = OuterParse;
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-in
-
-val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
- OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
- OuterKeyword.diag ((opt_modes -- P.term)
- >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
- (K ())));
-
-end
-*}
-
no_notation
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
--- a/src/HOL/Product_Type.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Product_Type.thy Thu Nov 12 14:31:29 2009 -0800
@@ -777,7 +777,7 @@
"apfst f (x, y) = (f x, y)"
by (simp add: apfst_def)
-lemma upd_snd_conv [simp, code]:
+lemma apsnd_conv [simp, code]:
"apsnd f (x, y) = (x, f y)"
by (simp add: apsnd_def)
@@ -829,6 +829,9 @@
"apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
by (cases x) simp
+lemma apsnd_apfst_commute:
+ "apsnd f (apfst g p) = apfst g (apsnd f p)"
+ by simp
text {*
Disjoint union of a family of sets -- Sigma.
--- a/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 14:31:29 2009 -0800
@@ -10,7 +10,7 @@
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
- * Fixed soundness bug related to sets of sets
+ * Fixed soundness bugs related to sets and sets of sets
* Fixed monotonicity check
* Fixed error in display of uncurried constants
* Speeded up scope enumeration
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 14:31:29 2009 -0800
@@ -1448,7 +1448,7 @@
fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
| Op2 (Apply, _, R, u1, u2) =>
if is_Cst Unrep u2 andalso is_set_type (type_of u1)
- andalso not (is_opt_rep (rep_of u1)) then
+ andalso is_FreeName u1 then
false_atom
else
to_apply R u1 u2
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 14:31:29 2009 -0800
@@ -96,6 +96,7 @@
val nickname_of : nut -> string
val is_skolem_name : nut -> bool
val is_eval_name : nut -> bool
+ val is_FreeName : nut -> bool
val is_Cst : cst -> nut -> bool
val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
val map_nut : (nut -> nut) -> nut -> nut
@@ -367,6 +368,8 @@
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
+fun is_FreeName (FreeName _) = true
+ | is_FreeName _ = false
(* cst -> nut -> bool *)
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
@@ -764,9 +767,8 @@
(* A nut is said to be constructive if whenever it evaluates to unknown in our
three-valued logic, it would evaluate to a unrepresentable value ("unrep")
- according to the HOL semantics. For example, "Suc n" is
- constructive if "n" is representable or "Unrep", because unknown implies
- unrep. *)
+ according to the HOL semantics. For example, "Suc n" is constructive if "n"
+ is representable or "Unrep", because unknown implies unrep. *)
(* nut -> bool *)
fun is_constructive u =
is_Cst Unrep u orelse
@@ -830,13 +832,9 @@
else if is_Cst Unrep u2 then
if is_constructive u1 then
Cst (Unrep, T, R)
- else if is_boolean_type T andalso not (is_opt_rep (rep_of u1)) then
- (* Selectors are an unfortunate exception to the rule that non-"Opt"
- predicates return "False" for unrepresentable domain values. *)
- case u1 of
- ConstName (s, _, _) => if is_sel s then unknown_boolean T R
- else Cst (False, T, Formula Neut)
- | _ => Cst (False, T, Formula Neut)
+ else if is_boolean_type T then
+ if is_FreeName u1 then Cst (False, T, Formula Neut)
+ else unknown_boolean T R
else case u1 of
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
Cst (Unrep, T, R)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 14:31:29 2009 -0800
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML
Author: Lukas Bulwahn, TU Muenchen
-FIXME.
+Entry point for the predicate compiler; definition of Toplevel commands code_pred and values
*)
signature PREDICATE_COMPILE =
@@ -10,7 +10,7 @@
val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
end;
-structure Predicate_Compile : PREDICATE_COMPILE =
+structure Predicate_Compile (*: PREDICATE_COMPILE*) =
struct
(* options *)
@@ -105,12 +105,16 @@
(Graph.strong_conn gr) thy
end
-fun extract_options ((modes, raw_options), const) =
+fun extract_options (((expected_modes, proposed_modes), raw_options), const) =
let
fun chk s = member (op =) raw_options s
in
Options {
- expected_modes = Option.map (pair const) modes,
+ expected_modes = Option.map (pair const) expected_modes,
+ proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [],
+ proposed_names =
+ map_filter
+ (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes,
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
@@ -125,17 +129,18 @@
}
end
-fun code_pred_cmd ((modes, raw_options), raw_const) lthy =
+fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy =
let
val thy = ProofContext.theory_of lthy
val const = Code.read_const thy raw_const
- val options = extract_options ((modes, raw_options), const)
+ val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
in
if (is_inductify options) then
let
val lthy' = LocalTheory.theory (preprocess options const) lthy
|> LocalTheory.checkpoint
- val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
+ val const =
+ case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
SOME c => c
| NONE => const
val _ = print_step options "Starting Predicate Compile Core..."
@@ -146,7 +151,7 @@
Predicate_Compile_Core.code_pred_cmd options raw_const lthy
end
-val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
+val setup = Predicate_Compile_Core.setup
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
@@ -157,35 +162,25 @@
(* Parser for mode annotations *)
-(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
-datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
-
-val parse_argmode' =
- ((Args.$$$ "i" || Args.$$$ "o") >> Argmode) ||
- (Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple)
-
-fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss)
+fun parse_mode_basic_expr xs =
+ (Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
+ Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
+and parse_mode_tuple_expr xs =
+ (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
+ xs
+and parse_mode_expr xs =
+ (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
-val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]"
- >> (fn m => flat (map_index
- (fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else []
- | (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m))
-
-val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
- >> map (rpair (NONE : int list option))
-
-fun gen_parse_mode smode_parser =
- (Scan.optional
- ((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") [])
- -- smode_parser
-
-val parse_mode = gen_parse_mode parse_smode
-
-val parse_mode' = gen_parse_mode parse_smode'
+val mode_and_opt_proposal = parse_mode_expr --
+ Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
val opt_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
+ P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") []
+
+val opt_expected_modes =
+ Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
+ P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
(* Parser for options *)
@@ -198,10 +193,10 @@
val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME)
+val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE
+ P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
val value_options =
let
@@ -217,7 +212,8 @@
val _ = OuterSyntax.local_theory_to_proof "code_pred"
"prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+ OuterKeyword.thy_goal
+ (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
(opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 14:31:29 2009 -0800
@@ -21,6 +21,7 @@
(fn (i, is) =>
string_of_int i ^ (case is of NONE => ""
| SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js)
+(* FIXME: remove! *)
fun string_of_mode (iss, is) = space_implode " -> " (map
(fn NONE => "X"
@@ -28,10 +29,118 @@
(iss @ [SOME is]));
fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
- "predmode: " ^ (string_of_mode predmode) ^
+ "predmode: " ^ (string_of_mode predmode) ^
(if null param_modes then "" else
"; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
+(* new datatype for mode *)
+
+datatype mode' = Bool | Input | Output | Pair of mode' * mode' | Fun of mode' * mode'
+
+(* equality of instantiatedness with respect to equivalences:
+ Pair Input Input == Input and Pair Output Output == Output *)
+fun eq_mode' (Fun (m1, m2), Fun (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4)
+ | eq_mode' (Pair (m1, m2), Pair (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4)
+ | eq_mode' (Pair (m1, m2), Input) = eq_mode' (m1, Input) andalso eq_mode' (m2, Input)
+ | eq_mode' (Pair (m1, m2), Output) = eq_mode' (m1, Output) andalso eq_mode' (m2, Output)
+ | eq_mode' (Input, Pair (m1, m2)) = eq_mode' (Input, m1) andalso eq_mode' (Input, m2)
+ | eq_mode' (Output, Pair (m1, m2)) = eq_mode' (Output, m1) andalso eq_mode' (Output, m2)
+ | eq_mode' (Input, Input) = true
+ | eq_mode' (Output, Output) = true
+ | eq_mode' (Bool, Bool) = true
+ | eq_mode' _ = false
+
+(* name: binder_modes? *)
+fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
+ | strip_fun_mode Bool = []
+ | strip_fun_mode _ = error "Bad mode for strip_fun_mode"
+
+fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode'
+ | dest_fun_mode mode = [mode]
+
+fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
+ | dest_tuple_mode _ = []
+
+fun string_of_mode' mode' =
+ let
+ fun string_of_mode1 Input = "i"
+ | string_of_mode1 Output = "o"
+ | string_of_mode1 Bool = "bool"
+ | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")"
+ and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^ string_of_mode2 m2
+ | string_of_mode2 mode = string_of_mode1 mode
+ and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2
+ | string_of_mode3 mode = string_of_mode2 mode
+ in string_of_mode3 mode' end
+
+fun ascii_string_of_mode' mode' =
+ let
+ fun ascii_string_of_mode' Input = "i"
+ | ascii_string_of_mode' Output = "o"
+ | ascii_string_of_mode' Bool = "b"
+ | ascii_string_of_mode' (Pair (m1, m2)) =
+ "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+ | ascii_string_of_mode' (Fun (m1, m2)) =
+ "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
+ and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
+ ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
+ | ascii_string_of_mode'_Fun Bool = "B"
+ | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m
+ and ascii_string_of_mode'_Pair (Pair (m1, m2)) =
+ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
+ | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
+ in ascii_string_of_mode'_Fun mode' end
+
+fun translate_mode T (iss, is) =
+ let
+ val Ts = binder_types T
+ val (Ts1, Ts2) = chop (length iss) Ts
+ fun translate_smode Ts is =
+ let
+ fun translate_arg (i, T) =
+ case AList.lookup (op =) is (i + 1) of
+ SOME NONE => Input
+ | SOME (SOME its) =>
+ let
+ fun translate_tuple (i, T) = if member (op =) its (i + 1) then Input else Output
+ in
+ foldr1 Pair (map_index translate_tuple (HOLogic.strip_tupleT T))
+ end
+ | NONE => Output
+ in map_index translate_arg Ts end
+ fun mk_mode arg_modes = foldr1 Fun (arg_modes @ [Bool])
+ val param_modes =
+ map (fn (T, NONE) => Input | (T, SOME is) => mk_mode (translate_smode (binder_types T) is))
+ (Ts1 ~~ iss)
+ in
+ mk_mode (param_modes @ translate_smode Ts2 is)
+ end;
+
+fun translate_mode' nparams mode' =
+ let
+ fun err () = error "translate_mode': given mode cannot be translated"
+ val (m1, m2) = chop nparams (strip_fun_mode mode')
+ val translate_to_tupled_mode =
+ (map_filter I) o (map_index (fn (i, m) =>
+ if eq_mode' (m, Input) then SOME (i + 1)
+ else if eq_mode' (m, Output) then NONE
+ else err ()))
+ val translate_to_smode =
+ (map_filter I) o (map_index (fn (i, m) =>
+ if eq_mode' (m, Input) then SOME (i + 1, NONE)
+ else if eq_mode' (m, Output) then NONE
+ else SOME (i + 1, SOME (translate_to_tupled_mode (dest_tuple_mode m)))))
+ fun translate_to_param_mode m =
+ case rev (dest_fun_mode m) of
+ Bool :: _ :: _ => SOME (translate_to_smode (strip_fun_mode m))
+ | _ => if eq_mode' (m, Input) then NONE else err ()
+ in
+ (map translate_to_param_mode m1, translate_to_smode m2)
+ end
+
+fun string_of_mode thy constname mode =
+ string_of_mode' (translate_mode (Sign.the_const_type thy constname) mode)
+
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
@@ -40,8 +149,6 @@
fun conjuncts t = conjuncts_aux t [];
-(* syntactic functions *)
-
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
| is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
| is_equationlike_term _ = false
@@ -70,8 +177,23 @@
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
| is_predT _ = false
-
+(* guessing number of parameters *)
+fun find_indexes pred xs =
+ let
+ fun find is n [] = is
+ | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
+ in rev (find [] 0 xs) end;
+
+fun guess_nparams T =
+ let
+ val argTs = binder_types T
+ val nparams = fold Integer.max
+ (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
+ in nparams end;
+
(*** check if a term contains only constructor functions ***)
+(* FIXME: constructor terms are supposed to be seen in the way the code generator
+ sees constructors.*)
fun is_constrt thy =
let
val cnstrs = flat (maps
@@ -159,7 +281,9 @@
(* Different options for compiler *)
datatype options = Options of {
- expected_modes : (string * mode list) option,
+ expected_modes : (string * mode' list) option,
+ proposed_modes : (string * mode' list) list,
+ proposed_names : ((string * mode') * string) list,
show_steps : bool,
show_proof_trace : bool,
show_intermediate_results : bool,
@@ -175,6 +299,10 @@
};
fun expected_modes (Options opt) = #expected_modes opt
+fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name
+fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode')
+ (#proposed_names opt) (name, mode)
+
fun show_steps (Options opt) = #show_steps opt
fun show_intermediate_results (Options opt) = #show_intermediate_results opt
fun show_proof_trace (Options opt) = #show_proof_trace opt
@@ -190,6 +318,8 @@
val default_options = Options {
expected_modes = NONE,
+ proposed_modes = [],
+ proposed_names = [],
show_steps = false,
show_intermediate_results = false,
show_proof_trace = false,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 14:31:29 2009 -0800
@@ -9,7 +9,7 @@
val setup : theory -> theory
val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
- val values_cmd : string list -> Predicate_Compile_Aux.smode option list option
+ val values_cmd : string list -> Predicate_Compile_Aux.mode' option list option
-> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
val register_predicate : (string * thm list * thm * int) -> theory -> theory
val register_intros : string * thm list -> theory -> theory
@@ -36,7 +36,7 @@
val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
option Unsynchronized.ref
- val code_pred_intros_attrib : attribute
+ val code_pred_intro_attrib : attribute
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
datatype compilation_funs = CompilationFuns of {
@@ -128,32 +128,25 @@
(* destruction of intro rules *)
(* FIXME: look for other place where this functionality was used before *)
-fun strip_intro_concl nparams intro = let
- val _ $ u = Logic.strip_imp_concl intro
- val (pred, all_args) = strip_comb u
- val (params, args) = chop nparams all_args
-in (pred, (params, args)) end
+fun strip_intro_concl nparams intro =
+ let
+ val _ $ u = Logic.strip_imp_concl intro
+ val (pred, all_args) = strip_comb u
+ val (params, args) = chop nparams all_args
+ in (pred, (params, args)) end
(** data structures **)
-(* new datatype for modes: *)
-(*
-datatype instantiation = Input | Output
-type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode
-type mode = arg_mode list
-type tmode = Mode of mode *
-*)
-
fun gen_split_smode (mk_tuple, strip_tuple) smode ts =
let
fun split_tuple' _ _ [] = ([], [])
| split_tuple' is i (t::ts) =
- (if i mem is then apfst else apsnd) (cons t)
+ (if member (op =) is i then apfst else apsnd) (cons t)
(split_tuple' is (i+1) ts)
fun split_tuple is t = split_tuple' is 1 (strip_tuple t)
fun split_smode' _ _ [] = ([], [])
| split_smode' smode i (t::ts) =
- (if i mem (map fst smode) then
+ (if member (op =) (map fst smode) i then
case (the (AList.lookup (op =) smode i)) of
NONE => apfst (cons t)
| SOME is =>
@@ -274,7 +267,7 @@
(AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode)
fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
- of NONE => error ("No function defined for mode " ^ string_of_mode mode ^
+ of NONE => error ("No function defined for mode " ^ string_of_mode thy name mode ^
" of predicate " ^ name)
| SOME data => data;
@@ -291,7 +284,7 @@
(AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode)
fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of
- NONE => error ("No random function defined for mode " ^ string_of_mode mode ^
+ NONE => error ("No random function defined for mode " ^ string_of_mode thy name mode ^
" of predicate " ^ name)
| SOME data => data
@@ -310,7 +303,7 @@
fun the_depth_limited_function_data thy name mode =
case lookup_depth_limited_function_data thy name mode of
- NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
+ NONE => error ("No depth-limited function defined for mode " ^ string_of_mode thy name mode
^ " of predicate " ^ name)
| SOME data => data
@@ -325,7 +318,7 @@
(AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode)
fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode
- of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode
+ of NONE => error ("No annotated function defined for mode " ^ string_of_mode thy name mode
^ " of predicate " ^ name)
| SOME data => data
@@ -337,17 +330,17 @@
(* diagnostic display functions *)
-fun print_modes options modes =
+fun print_modes options thy modes =
if show_modes options then
tracing ("Inferred modes:\n" ^
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- string_of_mode ms)) modes))
+ (string_of_mode thy s) ms)) modes))
else ()
fun print_pred_mode_table string_of_entry thy pred_mode_table =
let
- fun print_mode pred (mode, entry) = "mode : " ^ (string_of_mode mode)
- ^ (string_of_entry pred mode entry)
+ fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode thy pred mode
+ ^ string_of_entry pred mode entry
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
val _ = tracing (cat_lines (map print_pred pred_mode_table))
@@ -417,25 +410,29 @@
fun print (pred, modes) u =
let
val _ = writeln ("predicate: " ^ pred)
- val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
- in u end
+ val _ = writeln ("modes: " ^ (commas (map (string_of_mode thy pred) modes)))
+ in u end
in
fold print (all_modes_of thy) ()
end
(* validity checks *)
-fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =
- case expected_modes options of
- SOME (s, ms) => (case AList.lookup (op =) modes s of
- SOME modes =>
- if not (eq_set (op =) (ms, modes)) then
- error ("expected modes were not inferred:\n"
- ^ "inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes)
- ^ "\n expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
- else ()
- | NONE => ())
- | NONE => ()
+fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes =
+ case expected_modes options of
+ SOME (s, ms) => (case AList.lookup (op =) modes s of
+ SOME modes =>
+ let
+ val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
+ in
+ if not (eq_set eq_mode' (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ()
(* importing introduction rules *)
@@ -464,7 +461,7 @@
val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred))
val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i))
(1 upto nparams)) ctxt'
- val params = map Free (param_names ~~ paramTs)
+ val params = map2 (curry Free) param_names paramTs
in (((outp_pred, params), []), ctxt') end
| import_intros inp_pred nparams (th :: ths) ctxt =
let
@@ -511,7 +508,7 @@
let
val (_, (_, args)) = strip_intro_concl nparams intro
val prems = Logic.strip_imp_prems intro
- val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+ val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
val frees = (fold o fold_aterms)
(fn t as Free _ =>
if member (op aconv) params t then I else insert (op aconv) t
@@ -567,25 +564,6 @@
Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
end;
-(* special case: predicate with no introduction rule *)
-fun noclause thy predname elim = let
- val T = (Logic.unvarifyT o Sign.the_const_type thy) predname
- val Ts = binder_types T
- val names = Name.variant_list []
- (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))
- val vs = map2 (curry Free) names Ts
- val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs))
- val intro_t = Logic.mk_implies (@{prop False}, clausehd)
- val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
- val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
- val intro = Goal.prove (ProofContext.init thy) names [] intro_t
- (fn _ => etac @{thm FalseE} 1)
- val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
- (fn _ => etac elim 1)
-in
- ([intro], elim)
-end
-
fun expand_tuples_elim th = th
(* updaters *)
@@ -617,7 +595,6 @@
val elim =
(Drule.standard o Skip_Proof.make_thm thy)
(mk_casesrule (ProofContext.init thy) pred nparams intros)
- val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
in
mk_pred_data ((intros, SOME elim, nparams), no_compilation)
end
@@ -653,23 +630,10 @@
end;
*)
-(* guessing number of parameters *)
-fun find_indexes pred xs =
- let
- fun find is n [] = is
- | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
- in rev (find [] 0 xs) end;
-
-fun guess_nparams T =
+fun add_intro thm thy =
let
- val argTs = binder_types T
- val nparams = fold Integer.max
- (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
- in nparams end;
-
-fun add_intro thm thy = let
- val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
- fun cons_intro gr =
+ val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
+ fun cons_intro gr =
case try (Graph.get_node gr) name of
SOME pred_data => Graph.map_node name (map_pred_data
(apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
@@ -680,13 +644,15 @@
in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end;
in PredData.map cons_intro thy end
-fun set_elim thm = let
+fun set_elim thm =
+ let
val (name, _) = dest_Const (fst
(strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
fun set (intros, _, nparams) = (intros, SOME thm, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-fun set_nparams name nparams = let
+fun set_nparams name nparams =
+ let
fun set (intros, elim, _ ) = (intros, elim, nparams)
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
@@ -974,7 +940,6 @@
(iss ~~ args1)))
end
end)) (AList.lookup op = modes name)
-
in
case strip_comb (Envir.eta_contract t) of
(Const (name, _), args) => the_default default (mk_modes name args)
@@ -1081,7 +1046,7 @@
if show_mode_inference options then
let
val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m)
+ p ^ " violates mode " ^ string_of_mode thy p m)
val _ = tracing (string_of_clause thy p (nth rs i))
in () end
else ()
@@ -1170,10 +1135,6 @@
| mk_Eval_of additional_arguments ((x, T), SOME mode) names =
let
val Ts = binder_types T
- (*val argnames = Name.variant_list names
- (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- val args = map Free (argnames ~~ Ts)
- val (inargs, outargs) = split_smode mode args*)
fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
| mk_split_lambda [x] t = lambda x t
| mk_split_lambda xs t =
@@ -1200,7 +1161,7 @@
val vnames = Name.variant_list names
(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
(1 upto length Ts))
- val args = map Free (vnames ~~ Ts)
+ val args = map2 (curry Free) vnames Ts
fun split_args (i, arg) (ins, outs) =
if member (op =) pis i then
(arg::ins, outs)
@@ -1289,18 +1250,18 @@
let
val names = Term.add_free_names t [];
val Ts = binder_types (fastype_of t);
- val vs = map Free
- (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
+ val vs = map2 (curry Free)
+ (Name.variant_list names (replicate (length Ts) "x")) Ts
in
fold_rev lambda vs (f (list_comb (t, vs)))
end;
-fun compile_param compilation_modifiers compfuns thy (NONE, t) = t
- | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) =
+fun compile_param compilation_modifiers compfuns thy NONE t = t
+ | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms))) t =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, args') = chop (length ms) args
- val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+ val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params
val f' =
case f of
Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode,
@@ -1316,7 +1277,7 @@
case strip_comb t of
(Const (name, T), params) =>
let
- val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+ val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params
val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode
val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T
in
@@ -1428,8 +1389,12 @@
val vnames = Name.variant_list (all_vs @ param_vs)
(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
pis)
- in if null pis then []
- else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
+ in
+ if null pis then
+ []
+ else
+ [HOLogic.mk_tuple (map2 (curry Free) vnames (map (fn j => nth Ts (j - 1)) pis))]
+ end
val in_ts = maps mk_input_term (snd mode)
val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
@@ -1472,7 +1437,7 @@
map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
- val params = map Free (param_names ~~ Ts1')
+ val params = map2 (curry Free) param_names Ts1'
fun mk_args (i, T) argnames =
let
val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
@@ -1490,17 +1455,17 @@
val vnames = Name.variant_list (param_names @ argnames)
(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
(1 upto (length Ts)))
- in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ argnames) end
+ in (HOLogic.mk_tuple (map2 (curry Free) vnames Ts), vnames @ argnames) end
end
val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
val (inargs, outargs) = split_smode is args
val param_names' = Name.variant_list (param_names @ argnames)
(map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
- val param_vs = map Free (param_names' ~~ Ts1)
+ val param_vs = map2 (curry Free) param_names' Ts1
val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) []
val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args))
val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args))
- val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
+ val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) param_vs params'
val funargs = params @ inargs
val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
@@ -1520,24 +1485,20 @@
(introthm, elimthm)
end;
-fun create_constname_of_mode thy prefix name mode =
+fun create_constname_of_mode options thy prefix name T mode =
let
- fun string_of_mode mode = if null mode then "0"
- else space_implode "_"
- (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
- ^ space_implode "p" (map string_of_int pis)) mode)
- val HOmode = space_implode "_and_"
- (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
+ val system_proposal = prefix ^ (Long_Name.base_name name)
+ ^ "_" ^ ascii_string_of_mode' (translate_mode T mode)
+ val name = the_default system_proposal (proposed_names options name (translate_mode T mode))
in
- (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
- (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
+ Sign.full_bname thy name
end;
fun split_tupleT is T =
let
fun split_tuple' _ _ [] = ([], [])
| split_tuple' is i (T::Ts) =
- (if i mem is then apfst else apsnd) (cons T)
+ (if member (op =) is i then apfst else apsnd) (cons T)
(split_tuple' is (i+1) Ts)
in
split_tuple' is 1 (HOLogic.strip_tupleT T)
@@ -1550,7 +1511,8 @@
fun mk_proj i j t =
(if i = j then I else HOLogic.mk_fst)
(funpow (i - 1) HOLogic.mk_snd t)
- fun mk_arg' i (si, so) = if i mem pis then
+ fun mk_arg' i (si, so) =
+ if member (op =) pis i then
(mk_proj si ni xin, (si+1, so))
else
(mk_proj so (n - ni) xout, (si, so+1))
@@ -1559,12 +1521,12 @@
HOLogic.mk_tuple args
end
-fun create_definitions preds (name, modes) thy =
+fun create_definitions options preds (name, modes) thy =
let
val compfuns = PredicateCompFuns.compfuns
val T = AList.lookup (op =) preds name |> the
fun create_definition (mode as (iss, is)) thy = let
- val mode_cname = create_constname_of_mode thy "" name mode
+ val mode_cname = create_constname_of_mode options thy "" name T mode
val mode_cbasename = Long_Name.base_name mode_cname
val Ts = binder_types T
val (Ts1, Ts2) = chop (length iss) Ts
@@ -1573,16 +1535,9 @@
val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
val names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
- (* old *)
- (*
- val xs = map Free (names ~~ (Ts1' @ Ts2))
- val (xparams, xargs) = chop (length iss) xs
- val (xins, xouts) = split_smode is xargs
- *)
- (* new *)
val param_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
- val xparams = map Free (param_names ~~ Ts1')
+ val xparams = map2 (curry Free) param_names Ts1'
fun mk_vars (i, T) names =
let
val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
@@ -1634,13 +1589,13 @@
fold create_definition modes thy
end;
-fun define_functions comp_modifiers compfuns preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
let
val T = AList.lookup (op =) preds name |> the
fun create_definition mode thy =
let
val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
- val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+ val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
in
thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
@@ -1672,8 +1627,8 @@
(* MAJOR FIXME: prove_params should be simple
- different form of introrule for parameters ? *)
-fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1)
- | prove_param thy (m as SOME (Mode (mode, is, ms)), t) =
+fun prove_param thy NONE t = TRY (rtac @{thm refl} 1)
+ | prove_param thy (m as SOME (Mode (mode, is, ms))) t =
let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, _) = chop (length ms) args
@@ -1690,7 +1645,7 @@
THEN print_tac "prove_param"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- THEN (EVERY (map (prove_param thy) (ms ~~ params)))
+ THEN (EVERY (map2 (prove_param thy) ms params))
THEN (REPEAT_DETERM (atac 1))
end
@@ -1711,7 +1666,7 @@
(* work with parameter arguments *)
THEN (atac 1)
THEN (print_tac "parameter goal")
- THEN (EVERY (map (prove_param thy) (ms ~~ args1)))
+ THEN (EVERY (map2 (prove_param thy) ms args1))
THEN (REPEAT_DETERM (atac 1))
end
| _ => rtac @{thm bindI} 1
@@ -1804,8 +1759,7 @@
THEN rtac @{thm not_predI} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
THEN (REPEAT_DETERM (atac 1))
- (* FIXME: work with parameter arguments *)
- THEN (EVERY (map (prove_param thy) (param_modes ~~ params)))
+ THEN (EVERY (map2 (prove_param thy) param_modes params))
else
rtac @{thm not_predI'} 1)
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
@@ -1888,8 +1842,9 @@
*)
(* TODO: remove function *)
-fun prove_param2 thy (NONE, t) = all_tac
- | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let
+fun prove_param2 thy NONE t = all_tac
+ | prove_param2 thy (m as SOME (Mode (mode, is, ms))) t =
+ let
val (f, args) = strip_comb (Envir.eta_contract t)
val (params, _) = chop (length ms) args
val f_tac = case f of
@@ -1898,11 +1853,11 @@
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term"
- in
+ in
print_tac "before simplification in prove_args:"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- THEN (EVERY (map (prove_param2 thy) (ms ~~ params)))
+ THEN (EVERY (map2 (prove_param2 thy) ms params))
end
@@ -1916,7 +1871,7 @@
(prop_of (predfun_elim_of thy name mode))))
THEN (etac (predfun_elim_of thy name mode) 1)
THEN print_tac "prove_expr2"
- THEN (EVERY (map (prove_param2 thy) (ms ~~ args)))
+ THEN (EVERY (map2 (prove_param2 thy) ms args))
THEN print_tac "finished prove_expr2"
| _ => etac @{thm bindE} 1)
@@ -1987,7 +1942,7 @@
[predfun_definition_of thy (the name) (iss, is)]) 1
THEN etac @{thm not_predE} 1
THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
- THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
+ THEN (EVERY (map2 (prove_param2 thy) param_modes params))
else
etac @{thm not_predE'} 1)
THEN rec_tac
@@ -2078,7 +2033,7 @@
fun dest_prem thy params t =
(case strip_comb t of
- (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
+ (v as Free _, ts) => if member (op =) params v then Prem (ts, v) else Sidecond t
| (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of
Prem (ts, t) => Negprem (ts, t)
| Negprem _ => error ("Double negation not allowed in premise: " ^
@@ -2091,7 +2046,7 @@
else Sidecond t
| _ => Sidecond t)
-fun prepare_intrs thy prednames intros =
+fun prepare_intrs options thy prednames intros =
let
val intrs = map prop_of intros
val nparams = nparams_of thy (hd prednames)
@@ -2108,7 +2063,7 @@
val (paramTs, _) = chop nparams (binder_types (snd (hd preds)))
val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
(1 upto length paramTs))
- in map Free (param_names ~~ paramTs) end
+ in map2 (curry Free) param_names paramTs end
| intr :: _ => fst (chop nparams
(snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))))
val param_vs = maps term_vs params
@@ -2151,7 +2106,11 @@
(Rs as _ :: _, Type ("bool", [])) =>
map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
end
- val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
+ val all_modes = map (fn (s, T) =>
+ case proposed_modes options s of
+ NONE => (s, modes_of_typ T)
+ | SOME modes' => (s, map (translate_mode' nparams) modes'))
+ preds
in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
(* sanity check of introduction rules *)
@@ -2160,14 +2119,15 @@
let
val concl = Logic.strip_imp_concl (prop_of intro)
val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
- val params = List.take (args, nparams_of thy (fst (dest_Const p)))
+ val params = fst (chop (nparams_of thy (fst (dest_Const p))) args)
fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
- if (length (HOLogic.strip_tuple arg) = length Ts) then true
+ if length (HOLogic.strip_tuple arg) = length Ts then
+ true
else
- error ("Format of introduction rule is invalid: tuples must be expanded:"
- ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
- (Display.string_of_thm_global thy intro))
+ error ("Format of introduction rule is invalid: tuples must be expanded:"
+ ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
+ (Display.string_of_thm_global thy intro))
| _ => true
val prems = Logic.strip_imp_prems (prop_of intro)
fun check_prem (Prem (args, _)) = forall check_arg args
@@ -2201,7 +2161,7 @@
fun add_code_equations thy nparams preds result_thmss =
let
- fun add_code_equation ((predname, T), (pred, result_thms)) =
+ fun add_code_equation (predname, T) (pred, result_thms) =
let
val full_mode = (replicate nparams NONE,
map (rpair NONE) (1 upto (length (binder_types T) - nparams)))
@@ -2211,7 +2171,7 @@
val Ts = binder_types T
val arg_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
- val args = map Free (arg_names ~~ Ts)
+ val args = map2 (curry Free) arg_names Ts
val predfun = Const (predfun_name_of thy predname full_mode,
Ts ---> PredicateCompFuns.mk_predT @{typ unit})
val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
@@ -2228,7 +2188,7 @@
(pred, result_thms)
end
in
- map add_code_equation (preds ~~ result_thmss)
+ map2 add_code_equation preds result_thmss
end
(** main function of predicate compiler **)
@@ -2237,7 +2197,7 @@
{
compile_preds : theory -> string list -> string list -> (string * typ) list
-> (moded_clause list) pred_mode_table -> term pred_mode_table,
- define_functions : (string * typ) list -> string * mode list -> theory -> theory,
+ define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
-> string list -> (string * (term list * indprem list) list) list
-> moded_clause list pred_mode_table,
@@ -2259,16 +2219,16 @@
(*val _ = check_intros_elim_match thy prednames*)
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
- prepare_intrs thy prednames (maps (intros_of thy) prednames)
+ prepare_intrs options thy prednames (maps (intros_of thy) prednames)
val _ = print_step options "Infering modes..."
val moded_clauses =
#infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
- val _ = check_expected_modes options modes
- val _ = print_modes options modes
+ val _ = check_expected_modes preds options modes
+ val _ = print_modes options thy modes
(*val _ = print_moded_clauses thy moded_clauses*)
val _ = print_step options "Defining executable functions..."
- val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
+ val thy' = fold (#define_functions (dest_steps steps) options preds) modes thy
|> Theory.checkpoint
val _ = print_step options "Compiling equations..."
val compiled_terms =
@@ -2373,7 +2333,7 @@
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
{function_name_of = random_function_name_of,
set_function_name = set_random_function_name,
- function_name_prefix = "random",
+ function_name_prefix = "random_",
funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
wrap_compilation = K (K (K (K (K I))))
@@ -2384,12 +2344,13 @@
val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
{function_name_of = annotated_function_name_of,
set_function_name = set_annotated_function_name,
- function_name_prefix = "annotated",
+ function_name_prefix = "annotated_",
funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
additional_arguments = K [],
wrap_compilation =
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
- mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation,
+ mk_tracing ("calling predicate " ^ s ^
+ " with mode " ^ string_of_mode' (translate_mode T mode)) compilation,
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
@@ -2435,19 +2396,16 @@
fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-val code_pred_intros_attrib = attrib add_intro;
+val code_pred_intro_attrib = attrib add_intro;
(*FIXME
- Naming of auxiliary rules necessary?
-- add default code equations P x y z = P_i_i_i x y z
*)
val setup = PredData.put (Graph.empty) #>
- Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
+ Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro))
"adding alternative introduction rules for code generation of inductive predicates"
- (*FIXME name discrepancy in attribs and ML code*)
- (*FIXME intros should be better named intro*)
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
fun generic_code_pred prep_const options raw_const lthy =
@@ -2519,7 +2477,7 @@
val user_mode' = map (rpair NONE) user_mode
val all_modes_of = if random then all_random_modes_of else all_modes_of
fun fits_to is NONE = true
- | fits_to is (SOME pm) = (is = pm)
+ | fits_to is (SOME pm) = (is = (snd (translate_mode' 0 pm)))
fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) =
fits_to is pm andalso valid (ms @ ms') pms
| valid (NONE :: ms') pms = valid ms' pms
@@ -2593,14 +2551,7 @@
in if k = ~1 orelse length ts < k then elemsT
else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont
end;
- (*
-fun random_values ctxt k t =
- let
- val thy = ProofContext.theory_of ctxt
- val _ =
- in
- end;
- *)
+
fun values_cmd print_modes param_user_modes options k raw_t state =
let
val ctxt = Toplevel.context_of state;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 14:31:29 2009 -0800
@@ -186,9 +186,11 @@
@{const_name "False"},
@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
@{const_name Nat.one_nat_inst.one_nat},
-@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
+@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
+@{const_name "HOL.zero_class.zero"},
@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus},
@{const_name Nat.ord_nat_inst.less_eq_nat},
+@{const_name Nat.ord_nat_inst.less_nat},
@{const_name number_nat_inst.number_of_nat},
@{const_name Int.Bit0},
@{const_name Int.Bit1},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:31:29 2009 -0800
@@ -6,29 +6,14 @@
signature PREDICATE_COMPILE_FUN =
sig
-val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
+ val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
val rewrite_intro : theory -> thm -> thm list
- val setup_oracle : theory -> theory
val pred_of_function : theory -> string -> string option
end;
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
struct
-
-(* Oracle for preprocessing *)
-
-val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
-
-fun the_oracle () =
- case !oracle of
- NONE => error "Oracle is not setup"
- | SOME (_, oracle) => oracle
-
-val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
- (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
-
-
fun is_funtype (Type ("fun", [_, _])) = true
| is_funtype _ = false;
@@ -393,9 +378,6 @@
in ([], thy) end
end
-(* preprocessing intro rules - uses oracle *)
-
-(* theory -> thm -> thm *)
fun rewrite_intro thy intro =
let
fun lookup_pred (Const (name, T)) =
@@ -435,7 +417,7 @@
|> map (fn (concl'::conclprems, _) =>
Logic.list_implies ((flat prems') @ conclprems, concl')))
in
- map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
- end;
+ map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
+ end
end;
--- a/src/HOL/Tools/res_atp.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Tools/res_atp.ML Thu Nov 12 14:31:29 2009 -0800
@@ -352,20 +352,32 @@
filter (not o known) c_clauses
end;
-fun valid_facts facts =
- Facts.fold_static (fn (name, ths) =>
- if Facts.is_concealed facts name orelse
- (run_blacklist_filter andalso is_package_def name) then I
- else
- let val xname = Facts.extern facts name in
- if Name_Space.is_hidden xname then I
- else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
- end) facts [];
-
fun all_valid_thms ctxt =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
+ val full_space =
+ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
+
+ fun valid_facts facts =
+ (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
+ let
+ fun check_thms a =
+ (case try (ProofContext.get_thms ctxt) a of
+ NONE => false
+ | SOME ths1 => Thm.eq_thms (ths0, ths1));
+
+ val name1 = Facts.extern facts name;
+ val name2 = Name_Space.extern full_space name;
+ val ths = filter_out Res_Axioms.bad_for_atp ths0;
+ in
+ if Facts.is_concealed facts name orelse null ths orelse
+ run_blacklist_filter andalso is_package_def name then I
+ else
+ (case find_first check_thms [name1, name2, name] of
+ NONE => I
+ | SOME a => cons (a, ths))
+ end);
in valid_facts global_facts @ valid_facts local_facts end;
fun multi_name a th (n, pairs) =
--- a/src/HOL/Word/WordShift.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/Word/WordShift.thy Thu Nov 12 14:31:29 2009 -0800
@@ -1102,7 +1102,7 @@
apply simp
apply (rule bin_nth_rsplit)
apply simp_all
- apply (simp add : word_size rev_map map_compose [symmetric])
+ apply (simp add : word_size rev_map)
apply (rule trans)
defer
apply (rule map_ident [THEN fun_cong])
@@ -1113,7 +1113,7 @@
lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
unfolding word_rcat_def to_bl_def' of_bl_def
- by (clarsimp simp add : bin_rcat_bl map_compose)
+ by (clarsimp simp add : bin_rcat_bl)
lemma size_rcat_lem':
"size (concat (map to_bl wl)) = length wl * size (hd wl)"
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 14:31:29 2009 -0800
@@ -3,35 +3,21 @@
begin
section {* Set operations *}
-(*
-definition Empty where "Empty == {}"
-declare empty_def[symmetric, code_pred_inline]
-*)
+
declare eq_reflection[OF empty_def, code_pred_inline]
-(*
-definition Union where "Union A B == A Un B"
-
-lemma [code_pred_intros]: "A x ==> Union A B x"
-and [code_pred_intros] : "B x ==> Union A B x"
-unfolding Union_def Un_def Collect_def mem_def by auto
-
-code_pred Union
-unfolding Union_def Un_def Collect_def mem_def by auto
-
-declare Union_def[symmetric, code_pred_inline]
-*)
declare eq_reflection[OF Un_def, code_pred_inline]
+declare eq_reflection[OF UNION_def, code_pred_inline]
section {* Alternative list definitions *}
subsection {* Alternative rules for set *}
-lemma set_ConsI1 [code_pred_intros]:
+lemma set_ConsI1 [code_pred_intro]:
"set (x # xs) x"
unfolding mem_def[symmetric, of _ x]
by auto
-lemma set_ConsI2 [code_pred_intros]:
+lemma set_ConsI2 [code_pred_intro]:
"set xs x ==> set (x' # xs) x"
unfolding mem_def[symmetric, of _ x]
by auto
@@ -49,13 +35,12 @@
done
qed
-
subsection {* Alternative rules for list_all2 *}
-lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
by auto
-lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
by auto
code_pred list_all2
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 14:31:11 2009 -0800
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 14:31:29 2009 -0800
@@ -6,31 +6,35 @@
inductive False' :: "bool"
-code_pred (mode : []) False' .
+code_pred (expected_modes: bool) False' .
code_pred [depth_limited] False' .
code_pred [random] False' .
inductive EmptySet :: "'a \<Rightarrow> bool"
-code_pred (mode: [], [1]) EmptySet .
+code_pred (expected_modes: o => bool, i => bool) EmptySet .
definition EmptySet' :: "'a \<Rightarrow> bool"
where "EmptySet' = {}"
-code_pred (mode: [], [1]) [inductify] EmptySet' .
+code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
+code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
code_pred
- (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2],
- [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2],
- [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2],
- [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2])
+ (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
+ (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
+ (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
+ (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
+ (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
+ (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
+ (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
+ (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
EmptyClosure .
thm EmptyClosure.equation
@@ -39,20 +43,21 @@
where
"False \<Longrightarrow> False''"
-code_pred (mode: []) False'' .
+code_pred (expected_modes: []) False'' .
inductive EmptySet'' :: "'a \<Rightarrow> bool"
where
"False \<Longrightarrow> EmptySet'' x"
-code_pred (mode: [1]) EmptySet'' .
-code_pred (mode: [], [1]) [inductify] EmptySet'' .
+code_pred (expected_modes: [1]) EmptySet'' .
+code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
*)
+
inductive True' :: "bool"
where
"True \<Longrightarrow> True'"
-code_pred (mode: []) True' .
+code_pred (expected_modes: bool) True' .
consts a' :: 'a
@@ -60,15 +65,29 @@
where
"Fact a' a'"
-code_pred (mode: [], [1], [2], [1, 2]) Fact .
+code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
inductive zerozero :: "nat * nat => bool"
where
"zerozero (0, 0)"
-code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero .
+code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
code_pred [random] zerozero .
+inductive JamesBond :: "nat => int => code_numeral => bool"
+where
+ "JamesBond 0 0 7"
+
+code_pred JamesBond .
+
+values "{(a, b, c). JamesBond a b c}"
+values "{(a, c, b). JamesBond a b c}"
+values "{(b, a, c). JamesBond a b c}"
+values "{(b, c, a). JamesBond a b c}"
+values "{(c, a, b). JamesBond a b c}"
+values "{(c, b, a). JamesBond a b c}"
+
+
subsection {* Alternative Rules *}
datatype char = C | D | E | F | G | H
@@ -77,22 +96,22 @@
where
"(x = C) \<or> (x = D) ==> is_C_or_D x"
-code_pred (mode: [1]) is_C_or_D .
+code_pred (expected_modes: i => bool) is_C_or_D .
thm is_C_or_D.equation
inductive is_D_or_E
where
"(x = D) \<or> (x = E) ==> is_D_or_E x"
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_D_or_E D"
by (auto intro: is_D_or_E.intros)
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_D_or_E E"
by (auto intro: is_D_or_E.intros)
-code_pred (mode: [], [1]) is_D_or_E
+code_pred (expected_modes: o => bool, i => bool) is_D_or_E
proof -
case is_D_or_E
from this(1) show thesis
@@ -115,11 +134,11 @@
where
"x = F \<or> x = G ==> is_F_or_G x"
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_F_or_G F"
by (auto intro: is_F_or_G.intros)
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"is_F_or_G G"
by (auto intro: is_F_or_G.intros)
@@ -130,7 +149,7 @@
text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
-code_pred (mode: [], [1]) is_FGH
+code_pred (expected_modes: o => bool, i => bool) is_FGH
proof -
case is_F_or_G
from this(1) show thesis
@@ -156,7 +175,7 @@
inductive zerozero' :: "nat * nat => bool" where
"equals (x, y) (0, 0) ==> zerozero' (x, y)"
-code_pred (mode: [1]) zerozero' .
+code_pred (expected_modes: i => bool) zerozero' .
lemma zerozero'_eq: "zerozero' x == zerozero x"
proof -
@@ -176,7 +195,7 @@
text {* if preprocessing fails, zerozero'' will not have all modes. *}
-code_pred (mode: [o], [(i, o)], [(o,i)], [i]) [inductify] zerozero'' .
+code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
subsection {* Numerals *}
@@ -214,7 +233,7 @@
| "even n \<Longrightarrow> odd (Suc n)"
| "odd n \<Longrightarrow> even (Suc n)"
-code_pred (mode: [], [1]) even .
+code_pred (expected_modes: i => bool, o => bool) even .
code_pred [depth_limited] even .
code_pred [random] even .
@@ -237,7 +256,7 @@
definition odd' where "odd' x == \<not> even x"
-code_pred (mode: [1]) [inductify] odd' .
+code_pred (expected_modes: i => bool) [inductify] odd' .
code_pred [inductify, depth_limited] odd' .
code_pred [inductify, random] odd' .
@@ -249,7 +268,7 @@
where
"n mod 2 = 0 \<Longrightarrow> is_even n"
-code_pred (mode: [1]) is_even .
+code_pred (expected_modes: i => bool) is_even .
subsection {* append predicate *}
@@ -257,7 +276,8 @@
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
+ i => o => i => bool as suffix) append .
code_pred [depth_limited] append .
code_pred [random] append .
code_pred [annotated] append .
@@ -270,11 +290,12 @@
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
-values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
-values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}"
-value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
-value [code] "Predicate.the (append_3 ([]::int list))"
+values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}"
+
+value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
+value [code] "Predicate.the (slice ([]::int list))"
text {* tricky case with alternative rules *}
@@ -287,9 +308,10 @@
lemma append2_Nil: "append2 [] (xs::'b list) xs"
by (simp add: append2.intros(1))
-lemmas [code_pred_intros] = append2_Nil append2.intros(2)
+lemmas [code_pred_intro] = append2_Nil append2.intros(2)
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2
+code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
+ i => o => i => bool, i => i => i => bool) append2
proof -
case append2
from append2(1) show thesis
@@ -309,13 +331,13 @@
"tupled_append ([], xs, xs)"
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) tupled_append .
code_pred [random] tupled_append .
thm tupled_append.equation
-(*
-TODO: values with tupled modes
-values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
-*)
+
+(*TODO: values with tupled modes*)
+(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*)
inductive tupled_append'
where
@@ -323,7 +345,8 @@
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) tupled_append' .
thm tupled_append'.equation
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -331,7 +354,8 @@
"tupled_append'' ([], xs, xs)"
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' .
thm tupled_append''.equation
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -339,7 +363,8 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' .
+code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' .
thm tupled_append'''.equation
subsection {* map_ofP predicate *}
@@ -349,7 +374,7 @@
"map_ofP ((a, b)#xs) a b"
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
-code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
+code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
thm map_ofP.equation
subsection {* filter predicate *}
@@ -361,7 +386,7 @@
| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
-code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 .
+code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
code_pred [depth_limited] filter1 .
code_pred [random] filter1 .
@@ -373,7 +398,7 @@
| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
-code_pred (mode: [1, 2, 3], [1, 2]) filter2 .
+code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 .
code_pred [depth_limited] filter2 .
code_pred [random] filter2 .
thm filter2.equation
@@ -384,7 +409,7 @@
where
"List.filter P xs = ys ==> filter3 P xs ys"
-code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 .
+code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 .
code_pred [depth_limited] filter3 .
thm filter3.depth_limited_equation
@@ -392,7 +417,7 @@
where
"List.filter P xs = ys ==> filter4 P xs ys"
-code_pred (mode: [1, 2], [1, 2, 3]) filter4 .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
code_pred [depth_limited] filter4 .
code_pred [random] filter4 .
@@ -402,7 +427,7 @@
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-code_pred (mode: [1], [2], [1, 2]) rev .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
thm rev.equation
@@ -412,7 +437,7 @@
"tupled_rev ([], [])"
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
-code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev .
+code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
thm tupled_rev.equation
subsection {* partition predicate *}
@@ -423,7 +448,8 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition .
+code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
+ (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) partition .
code_pred [depth_limited] partition .
code_pred [random] partition .
@@ -438,18 +464,21 @@
| "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
| "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
-code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition .
+code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
+ (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
thm tupled_partition.equation
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
"r a b \<Longrightarrow> tranclp r a b"
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
by auto
subsection {* transitive predicate *}
-code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp
+code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
+ (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
+ (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
proof -
case tranclp
from this converse_tranclpE[OF this(1)] show thesis by metis
@@ -476,11 +505,10 @@
text {* values command needs mode annotation of the parameter succ
to disambiguate which mode is to be chosen. *}
-values [mode: [1]] 20 "{n. tranclp succ 10 n}"
-values [mode: [2]] 10 "{n. tranclp succ n 10}"
+values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
+values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
values 20 "{(n, m). tranclp succ n m}"
-
subsection {* IMP *}
types
@@ -548,9 +576,8 @@
values 5
"{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
-(* FIXME:
values 3 "{(a,q). step (par nil nil) a q}"
-*)
+
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
where
@@ -570,8 +597,8 @@
| "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
code_pred divmod_rel ..
-
-value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
+thm divmod_rel.equation
+value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
subsection {* Minimum *}
@@ -657,7 +684,7 @@
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-code_pred (mode: [1], [1, 2]) [inductify] set_of .
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
thm set_of.equation
code_pred [inductify] is_ord .
@@ -673,19 +700,15 @@
thm rel_comp.equation
code_pred [inductify] Image .
thm Image.equation
-(*TODO: *)
-
-declare Id_on_def[unfolded UNION_def, code_pred_def]
-
-code_pred [inductify] Id_on .
+code_pred (expected_modes: (o => bool) => o => bool, (o => bool) => i * o => bool,
+ (o => bool) => o * i => bool, (o => bool) => i => bool) [inductify] Id_on .
thm Id_on.equation
code_pred [inductify] Domain .
thm Domain.equation
code_pred [inductify] Range .
thm Range.equation
code_pred [inductify] Field .
-declare Sigma_def[unfolded UNION_def, code_pred_def]
-declare refl_on_def[unfolded UNION_def, code_pred_def]
+thm Field.equation
code_pred [inductify] refl_on .
thm refl_on.equation
code_pred [inductify] total_on .
@@ -708,21 +731,82 @@
(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
-code_pred [inductify] concat .
-code_pred [inductify] hd .
-code_pred [inductify] tl .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
+thm concatP.equation
+
+values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
+values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
+
+code_pred [inductify, depth_limited] List.concat .
+thm concatP.depth_limited_equation
+
+values [depth_limit = 3] 3
+ "{xs. concatP xs ([0] :: nat list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs ([1] :: int list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs ([1] :: nat list)}"
+
+values [depth_limit = 5] 3
+ "{xs. concatP xs [(1::int), 2]}"
+
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
+thm hdP.equation
+values "{x. hdP [1, 2, (3::int)] x}"
+values "{(xs, x). hdP [1, 2, (3::int)] 1}"
+
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
+thm tlP.equation
+values "{x. tlP [1, 2, (3::nat)] x}"
+values "{x. tlP [1, 2, (3::int)] [3]}"
+
code_pred [inductify] last .
+thm lastP.equation
+
code_pred [inductify] butlast .
+thm butlastP.equation
+
code_pred [inductify] take .
+thm takeP.equation
+
code_pred [inductify] drop .
+thm dropP.equation
code_pred [inductify] zip .
+thm zipP.equation
+
(*code_pred [inductify] upt .*)
code_pred [inductify] remdups .
+thm remdupsP.equation
+code_pred [inductify, depth_limited] remdups .
+values [depth_limit = 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
+
code_pred [inductify] remove1 .
+thm remove1P.equation
+values "{xs. remove1P 1 xs [2, (3::int)]}"
+
code_pred [inductify] removeAll .
+thm removeAllP.equation
+code_pred [inductify, depth_limited] removeAll .
+
+values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
+
code_pred [inductify] distinct .
+thm distinct.equation
+
code_pred [inductify] replicate .
+thm replicateP.equation
+values 5 "{(n, xs). replicateP n (0::int) xs}"
+
code_pred [inductify] splice .
+thm splice.simps
+thm spliceP.equation
+
+values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
+(* TODO: correct error messages:*)
+(* values {(xs, ys, zs). spliceP xs ... } *)
+
code_pred [inductify] List.rev .
code_pred [inductify] map .
code_pred [inductify] foldr .
@@ -786,7 +870,7 @@
| "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"
-code_pred (mode: [], [1]) S\<^isub>4p .
+code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
subsection {* Lambda *}
@@ -838,10 +922,58 @@
| 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"
-code_pred (mode: [1, 2], [1, 2, 3]) typing .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
thm typing.equation
-code_pred (mode: [1], [1, 2]) beta .
+code_pred (modes: i => o => bool as reduce') beta .
thm beta.equation
+values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
+
+definition "reduce t = Predicate.the (reduce' t)"
+
+value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
+
+code_pred [random] typing .
+
+values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
+
+subsection {* A minimal example of yet another semantics *}
+
+text {* thanks to Elke Salecker *}
+
+types
+vname = nat
+vvalue = int
+var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
+
+datatype ir_expr =
+ IrConst vvalue
+| ObjAddr vname
+| Add ir_expr ir_expr
+
+datatype val =
+ IntVal vvalue
+
+record configuration =
+Env :: var_assign
+
+inductive eval_var ::
+"ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
+where
+ irconst: "eval_var (IrConst i) conf (IntVal i)"
+| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
+| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
+
+(* TODO: breaks if code_pred_intro is used? *)
+(*
+lemmas [code_pred_intro] = irconst objaddr plus
+*)
+thm eval_var.cases
+
+code_pred eval_var . (*by (rule eval_var.cases)*)
+thm eval_var.equation
+
+values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
+
end
\ No newline at end of file
--- a/src/Tools/Code/code_ml.ML Thu Nov 12 14:31:11 2009 -0800
+++ b/src/Tools/Code/code_ml.ML Thu Nov 12 14:31:29 2009 -0800
@@ -1,4 +1,4 @@
-(* Title: Tools/code/code_ml.ML
+(* Title: Tools/code/code_ml.ML_
Author: Florian Haftmann, TU Muenchen
Serializer for SML and OCaml.
@@ -25,29 +25,34 @@
val target_OCaml = "OCaml";
val target_Eval = "Eval";
-datatype ml_stmt =
- MLExc of string * int
- | MLVal of string * ((typscheme * iterm) * (thm * bool))
- | MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list * string list
- | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
- | MLClass of string * (vname * ((class * string) list * (string * itype) list))
- | MLClassinst of string * ((class * (string * (vname * sort) list))
+datatype ml_binding =
+ ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ | ML_Instance of string * ((class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
* ((string * const) * (thm * bool)) list));
-fun stmt_names_of (MLExc (name, _)) = [name]
- | stmt_names_of (MLVal (name, _)) = [name]
- | stmt_names_of (MLFuns (fs, _)) = map fst fs
- | stmt_names_of (MLDatas ds) = map fst ds
- | stmt_names_of (MLClass (name, _)) = [name]
- | stmt_names_of (MLClassinst (name, _)) = [name];
+datatype ml_stmt =
+ ML_Exc of string * int
+ | ML_Val of ml_binding
+ | ML_Funs of ml_binding list * string list
+ | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
+ | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
+
+fun stmt_name_of_binding (ML_Function (name, _)) = name
+ | stmt_name_of_binding (ML_Instance (name, _)) = name;
+
+fun stmt_names_of (ML_Exc (name, _)) = [name]
+ | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
+ | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
+ | stmt_names_of (ML_Datas ds) = map fst ds
+ | stmt_names_of (ML_Class (name, _)) = [name];
(** SML serailizer **)
fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
let
- fun pr_dicts fxy ds =
+ fun pr_dicts is_pseudo_fun fxy ds =
let
fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
| pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
@@ -58,7 +63,9 @@
| pr_proj (ps as _ :: _) p =
brackets [Pretty.enum " o" "(" ")" ps, p];
fun pr_dict fxy (DictConst (inst, dss)) =
- brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+ brackify fxy ((str o deresolve) inst ::
+ (if is_pseudo_fun inst then [str "()"]
+ else map (pr_dicts is_pseudo_fun BR) dss))
| pr_dict fxy (DictVar (classrels, v)) =
pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
in case ds
@@ -66,11 +73,11 @@
| [d] => pr_dict fxy d
| _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
end;
- fun pr_tyvar_dicts vs =
+ fun pr_tyvar_dicts is_pseudo_fun vs =
vs
|> map (fn (v, sort) => map_index (fn (i, _) =>
DictVar ([], (v, (i, length sort)))) sort)
- |> map (pr_dicts BR);
+ |> map (pr_dicts is_pseudo_fun BR);
fun pr_tycoexpr fxy (tyco, tys) =
let
val tyco' = (str o deresolve) tyco
@@ -83,144 +90,155 @@
of NONE => pr_tycoexpr fxy (tyco, tys)
| SOME (i, pr) => pr pr_typ fxy tys)
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term is_closure thm vars fxy (IConst c) =
- pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar NONE) =
+ fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
+ pr_app is_pseudo_fun thm vars fxy (c, [])
+ | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
str "_"
- | pr_term is_closure thm vars fxy (IVar (SOME v)) =
+ | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
- | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
+ | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => pr_app is_closure thm vars fxy c_ts
+ of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
| NONE => brackify fxy
- [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
- | pr_term is_closure thm vars fxy (t as _ `|=> _) =
+ [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
+ | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
fun pr (pat, ty) =
- pr_bind is_closure thm NOBR pat
+ pr_bind is_pseudo_fun thm NOBR pat
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map pr binds vars;
- in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
- | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) =
+ in brackets (ps @ [pr_term is_pseudo_fun thm vars' NOBR t']) end
+ | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then pr_case is_closure thm vars fxy cases
- else pr_app is_closure thm vars fxy c_ts
- | NONE => pr_case is_closure thm vars fxy cases)
- and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ then pr_case is_pseudo_fun thm vars fxy cases
+ else pr_app is_pseudo_fun thm vars fxy c_ts
+ | NONE => pr_case is_pseudo_fun thm vars fxy cases)
+ and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
let
val k = length tys
in if k < 2 then
- (str o deresolve) c :: map (pr_term is_closure thm vars BR) ts
+ (str o deresolve) c :: map (pr_term is_pseudo_fun thm vars BR) ts
else if k = length ts then
- [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_closure thm vars NOBR) ts)]
- else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand k app)] end
- else if is_closure c
+ [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
+ else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] end
+ else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
else
(str o deresolve) c
- :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
- and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
+ :: (map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts
+ and pr_app is_pseudo_fun thm vars = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
syntax_const thm vars
- and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
- and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
+ and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
+ and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR pat
- |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
+ |> pr_bind is_pseudo_fun thm NOBR pat
+ |>> (fn p => semicolon [str "val", p, str "=", pr_term is_pseudo_fun thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
Pretty.chunks [
[str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
- [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR body] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term is_pseudo_fun thm vars' NOBR body] |> Pretty.block,
str ("end")
]
end
- | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
+ | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR pat vars;
+ val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
in
- concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
+ concat [str delim, p, str "=>", pr_term is_pseudo_fun thm vars' NOBR body]
end;
in
brackets (
str "case"
- :: pr_term is_closure thm vars NOBR t
+ :: pr_term is_pseudo_fun thm vars NOBR t
:: pr "of" clause
:: map (pr "|") clauses
)
end
- | pr_case is_closure thm vars fxy ((_, []), _) =
+ | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
(concat o map str) ["raise", "Fail", "\"empty case\""];
- fun pr_stmt (MLExc (name, n)) =
+ fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs as eq :: eqs'))) =
let
- val exc_str =
- (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
+ val vs_dict = filter_out (null o snd) vs;
+ val shift = if null eqs' then I else
+ map (Pretty.block o single o Pretty.block o single);
+ fun pr_eq definer ((ts, t), (thm, _)) =
+ let
+ val consts = fold Code_Thingol.add_constnames (t :: ts) [];
+ val vars = reserved
+ |> intro_base_names
+ (is_none o syntax_const) deresolve consts
+ |> intro_vars ((fold o Code_Thingol.fold_varnames)
+ (insert (op =)) ts []);
+ val prolog = if needs_typ then
+ concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
+ else Pretty.strs [definer, deresolve name];
+ in
+ concat (
+ prolog
+ :: (if is_pseudo_fun name then [str "()"]
+ else pr_tyvar_dicts is_pseudo_fun vs_dict
+ @ map (pr_term is_pseudo_fun thm vars BR) ts)
+ @ str "="
+ @@ pr_term is_pseudo_fun thm vars NOBR t
+ )
+ end
in
- (concat o map str) (
- (if n = 0 then "val" else "fun")
- :: deresolve name
- :: replicate n "_"
- @ "="
- :: "raise"
- :: "Fail"
- @@ exc_str
+ (Pretty.block o Pretty.fbreaks o shift) (
+ pr_eq definer eq
+ :: map (pr_eq "|") eqs'
)
end
- | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
- let
- val consts = Code_Thingol.add_constnames t [];
- val vars = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts;
- in
- concat [
- str "val",
- (str o deresolve) name,
- str ":",
- pr_typ NOBR ty,
- str "=",
- pr_term (K false) thm vars NOBR t
- ]
- end
- | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
+ | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
let
- fun pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
- let
- val vs_dict = filter_out (null o snd) vs;
- val shift = if null eqs' then I else
- map (Pretty.block o single o Pretty.block o single);
- fun pr_eq definer ((ts, t), (thm, _)) =
- let
- val consts = fold Code_Thingol.add_constnames (t :: ts) [];
- val vars = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts
- |> intro_vars ((fold o Code_Thingol.fold_varnames)
- (insert (op =)) ts []);
- in
- concat (
- str definer
- :: (str o deresolve) name
- :: (if member (op =) pseudo_funs name then [str "()"]
- else pr_tyvar_dicts vs_dict
- @ map (pr_term (member (op =) pseudo_funs) thm vars BR) ts)
- @ str "="
- @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t
- )
- end
- in
- (Pretty.block o Pretty.fbreaks o shift) (
- pr_eq definer eq
- :: map (pr_eq "|") eqs'
- )
- end;
+ fun pr_superclass (_, (classrel, dss)) =
+ concat [
+ (str o Long_Name.base_name o deresolve) classrel,
+ str "=",
+ pr_dicts is_pseudo_fun NOBR [DictConst dss]
+ ];
+ fun pr_classparam ((classparam, c_inst), (thm, _)) =
+ concat [
+ (str o Long_Name.base_name o deresolve) classparam,
+ str "=",
+ pr_app (K false) thm reserved NOBR (c_inst, [])
+ ];
+ in
+ concat (
+ str definer
+ :: (str o deresolve) inst
+ :: (if is_pseudo_fun inst then [str "()"]
+ else pr_tyvar_dicts is_pseudo_fun arity)
+ @ str "="
+ :: Pretty.enum "," "{" "}"
+ (map pr_superclass superarities @ map pr_classparam classparam_insts)
+ :: str ":"
+ @@ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ )
+ end;
+ fun pr_stmt (ML_Exc (name, n)) =
+ (concat o map str) (
+ (if n = 0 then "val" else "fun")
+ :: deresolve name
+ :: replicate n "_"
+ @ "="
+ :: "raise"
+ :: "Fail"
+ @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";"
+ )
+ | pr_stmt (ML_Val binding) =
+ semicolon [pr_binding (K false) true "val" binding]
+ | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+ let
+ val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
fun pr_pseudo_fun name = concat [
str "val",
(str o deresolve) name,
@@ -228,10 +246,11 @@
(str o deresolve) name,
str "();"
];
- val (ps, p) = split_last (pr_funn "fun" funn :: map (pr_funn "and") funns);
+ val (ps, p) = split_last
+ (pr_binding' "fun" binding :: map (pr_binding' "and") bindings);
val pseudo_ps = map pr_pseudo_fun pseudo_funs;
in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end
- | pr_stmt (MLDatas (datas as (data :: datas'))) =
+ | pr_stmt (ML_Datas (datas as (data :: datas'))) =
let
fun pr_co (co, []) =
str (deresolve co)
@@ -258,7 +277,7 @@
val (ps, p) = split_last
(pr_data "datatype" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
- | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+ | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
let
val w = first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
@@ -300,32 +319,6 @@
:: map pr_superclass_proj superclasses
@ map pr_classparam_proj classparams
)
- end
- | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
- let
- fun pr_superclass (_, (classrel, dss)) =
- concat [
- (str o Long_Name.base_name o deresolve) classrel,
- str "=",
- pr_dicts NOBR [DictConst dss]
- ];
- fun pr_classparam ((classparam, c_inst), (thm, _)) =
- concat [
- (str o Long_Name.base_name o deresolve) classparam,
- str "=",
- pr_app (K false) thm reserved NOBR (c_inst, [])
- ];
- in
- semicolon ([
- str (if null arity then "val" else "fun"),
- (str o deresolve) inst ] @
- pr_tyvar_dicts arity @ [
- str "=",
- Pretty.enum "," "{" "}"
- (map pr_superclass superarities @ map pr_classparam classparam_insts),
- str ":",
- pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ])
end;
in pr_stmt end;
@@ -354,14 +347,16 @@
fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
let
- fun pr_dicts fxy ds =
+ fun pr_dicts is_pseudo_fun fxy ds =
let
fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
| pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
fun pr_proj ps p =
fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
fun pr_dict fxy (DictConst (inst, dss)) =
- brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+ brackify fxy ((str o deresolve) inst ::
+ (if is_pseudo_fun inst then [str "()"]
+ else map (pr_dicts is_pseudo_fun BR) dss))
| pr_dict fxy (DictVar (classrels, v)) =
pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
in case ds
@@ -369,11 +364,11 @@
| [d] => pr_dict fxy d
| _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
end;
- fun pr_tyvar_dicts vs =
+ fun pr_tyvar_dicts is_pseudo_fun vs =
vs
|> map (fn (v, sort) => map_index (fn (i, _) =>
DictVar ([], (v, (i, length sort)))) sort)
- |> map (pr_dicts BR);
+ |> map (pr_dicts is_pseudo_fun BR);
fun pr_tycoexpr fxy (tyco, tys) =
let
val tyco' = (str o deresolve) tyco
@@ -386,103 +381,73 @@
of NONE => pr_tycoexpr fxy (tyco, tys)
| SOME (i, pr) => pr pr_typ fxy tys)
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term is_closure thm vars fxy (IConst c) =
- pr_app is_closure thm vars fxy (c, [])
- | pr_term is_closure thm vars fxy (IVar NONE) =
+ fun pr_term is_pseudo_fun thm vars fxy (IConst c) =
+ pr_app is_pseudo_fun thm vars fxy (c, [])
+ | pr_term is_pseudo_fun thm vars fxy (IVar NONE) =
str "_"
- | pr_term is_closure thm vars fxy (IVar (SOME v)) =
+ | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
- | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
+ | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => pr_app is_closure thm vars fxy c_ts
+ of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts
| NONE =>
- brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
- | pr_term is_closure thm vars fxy (t as _ `|=> _) =
+ brackify fxy [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2])
+ | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
- val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) binds vars;
- in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
- | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
+ val (ps, vars') = fold_map (pr_bind is_pseudo_fun thm BR o fst) binds vars;
+ in brackets (str "fun" :: ps @ str "->" @@ pr_term is_pseudo_fun thm vars' NOBR t') end
+ | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then pr_case is_closure thm vars fxy cases
- else pr_app is_closure thm vars fxy c_ts
- | NONE => pr_case is_closure thm vars fxy cases)
- and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ then pr_case is_pseudo_fun thm vars fxy cases
+ else pr_app is_pseudo_fun thm vars fxy c_ts
+ | NONE => pr_case is_pseudo_fun thm vars fxy cases)
+ and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
if length tys = length ts
then case ts
of [] => [(str o deresolve) c]
- | [t] => [(str o deresolve) c, pr_term is_closure thm vars BR t]
+ | [t] => [(str o deresolve) c, pr_term is_pseudo_fun thm vars BR t]
| _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
- (map (pr_term is_closure thm vars NOBR) ts)]
- else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand (length tys) app)]
- else if is_closure c
+ (map (pr_term is_pseudo_fun thm vars NOBR) ts)]
+ else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand (length tys) app)]
+ else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
else (str o deresolve) c
- :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
- and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
+ :: ((map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts)
+ and pr_app is_pseudo_fun = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun)
syntax_const
- and pr_bind is_closure = gen_pr_bind (pr_term is_closure)
- and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
+ and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun)
+ and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
- |> pr_bind is_closure thm NOBR pat
+ |> pr_bind is_pseudo_fun thm NOBR pat
|>> (fn p => concat
- [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
+ [str "let", p, str "=", pr_term is_pseudo_fun thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
in
brackify_block fxy (Pretty.chunks ps) []
- (pr_term is_closure thm vars' NOBR body)
+ (pr_term is_pseudo_fun thm vars' NOBR body)
end
- | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
+ | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun pr delim (pat, body) =
let
- val (p, vars') = pr_bind is_closure thm NOBR pat vars;
- in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
+ val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars;
+ in concat [str delim, p, str "->", pr_term is_pseudo_fun thm vars' NOBR body] end;
in
brackets (
str "match"
- :: pr_term is_closure thm vars NOBR t
+ :: pr_term is_pseudo_fun thm vars NOBR t
:: pr "with" clause
:: map (pr "|") clauses
)
end
- | pr_case is_closure thm vars fxy ((_, []), _) =
+ | pr_case is_pseudo_fun thm vars fxy ((_, []), _) =
(concat o map str) ["failwith", "\"empty case\""];
- fun pr_stmt (MLExc (name, n)) =
- let
- val exc_str =
- (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
- in
- (concat o map str) (
- "let"
- :: deresolve name
- :: replicate n "_"
- @ "="
- :: "failwith"
- @@ exc_str
- )
- end
- | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
- let
- val consts = Code_Thingol.add_constnames t [];
- val vars = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts;
- in
- concat [
- str "let",
- (str o deresolve) name,
- str ":",
- pr_typ NOBR ty,
- str "=",
- pr_term (K false) thm vars NOBR t
- ]
- end
- | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
+ fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs))) =
let
fun pr_eq ((ts, t), (thm, _)) =
let
@@ -494,9 +459,9 @@
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
- (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts),
+ (map (pr_term is_pseudo_fun thm vars NOBR) ts),
str "->",
- pr_term (member (op =) pseudo_funs) thm vars NOBR t
+ pr_term is_pseudo_fun thm vars NOBR t
] end;
fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
let
@@ -509,9 +474,9 @@
in
concat (
(if is_pseudo then [str "()"]
- else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts)
+ else map (pr_term is_pseudo_fun thm vars BR) ts)
@ str "="
- @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t
+ @@ pr_term is_pseudo_fun thm vars NOBR t
)
end
| pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') =
@@ -548,13 +513,58 @@
o single o pr_eq) eqs'
)
end;
- fun pr_funn definer (name, ((vs, ty), eqs)) =
- concat (
- str definer
- :: (str o deresolve) name
- :: pr_tyvar_dicts (filter_out (null o snd) vs)
- @| pr_eqs (member (op =) pseudo_funs name) eqs
- );
+ val prolog = if needs_typ then
+ concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty]
+ else Pretty.strs [definer, deresolve name];
+ in
+ concat (
+ prolog
+ :: pr_tyvar_dicts is_pseudo_fun (filter_out (null o snd) vs)
+ @| pr_eqs (is_pseudo_fun name) eqs
+ )
+ end
+ | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
+ let
+ fun pr_superclass (_, (classrel, dss)) =
+ concat [
+ (str o deresolve) classrel,
+ str "=",
+ pr_dicts is_pseudo_fun NOBR [DictConst dss]
+ ];
+ fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
+ concat [
+ (str o deresolve) classparam,
+ str "=",
+ pr_app (K false) thm reserved NOBR (c_inst, [])
+ ];
+ in
+ concat (
+ str definer
+ :: (str o deresolve) inst
+ :: pr_tyvar_dicts is_pseudo_fun arity
+ @ str "="
+ @@ brackets [
+ enum_default "()" ";" "{" "}" (map pr_superclass superarities
+ @ map pr_classparam_inst classparam_insts),
+ str ":",
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ]
+ )
+ end;
+ fun pr_stmt (ML_Exc (name, n)) =
+ (concat o map str) (
+ "let"
+ :: deresolve name
+ :: replicate n "_"
+ @ "="
+ :: "failwith"
+ @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";;"
+ )
+ | pr_stmt (ML_Val binding) =
+ Pretty.block [pr_binding (K false) true "let" binding, str ";;"]
+ | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
+ let
+ val pr_binding' = pr_binding (member (op =) pseudo_funs) false;
fun pr_pseudo_fun name = concat [
str "let",
(str o deresolve) name,
@@ -563,10 +573,10 @@
str "();;"
];
val (ps, p) = split_last
- (pr_funn "let rec" funn :: map (pr_funn "and") funns);
+ (pr_binding' "let rec" binding :: map (pr_binding' "and") bindings);
val pseudo_ps = map pr_pseudo_fun pseudo_funs;
in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end
- | pr_stmt (MLDatas (datas as (data :: datas'))) =
+ | pr_stmt (ML_Datas (datas as (data :: datas'))) =
let
fun pr_co (co, []) =
str (deresolve co)
@@ -593,7 +603,7 @@
val (ps, p) = split_last
(pr_data "type" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
- | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+ | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
let
val w = "_" ^ first_upper v;
fun pr_superclass_field (class, classrel) =
@@ -623,36 +633,8 @@
)
]
:: map pr_classparam_proj classparams
- ) end
- | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
- let
- fun pr_superclass (_, (classrel, dss)) =
- concat [
- (str o deresolve) classrel,
- str "=",
- pr_dicts NOBR [DictConst dss]
- ];
- fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
- concat [
- (str o deresolve) classparam,
- str "=",
- pr_app (K false) thm reserved NOBR (c_inst, [])
- ];
- in
- concat (
- str "let"
- :: (str o deresolve) inst
- :: pr_tyvar_dicts arity
- @ str "="
- @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
- enum_default "()" ";" "{" "}" (map pr_superclass superarities
- @ map pr_classparam_inst classparam_insts),
- str ":",
- pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ]
- )
- end;
- in pr_stmt end;
+ ) end;
+ in pr_stmt end;
fun pr_ocaml_module name content =
Pretty.chunks (
@@ -744,32 +726,41 @@
val base' = if upper then first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
- fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
+ fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
+ let
+ val eqs = filter (snd o snd) raw_eqs;
+ val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
+ of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
+ then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
+ else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+ | _ => (eqs, NONE)
+ else (eqs, NONE)
+ in (ML_Function (name, (tysm, eqs')), is_value) end
+ | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, arity)), _))) =
+ (ML_Instance (name, stmt), if null arity then SOME (name, false) else NONE)
+ | ml_binding_of_stmt (name, _) =
+ error ("Binding block containing illegal statement: " ^ labelled_name name)
+ fun add_fun (name, stmt) =
let
- val eqs = filter (snd o snd) raw_eqs;
- val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
- of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
- then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
- else (eqs, not (member (op =) (Code_Thingol.add_constnames t []) name))
- | _ => (eqs, false)
- else (eqs, false)
- in ((name, (tysm, eqs')), is_value) end;
- fun check_kind [((name, (tysm, [(([], t), thm)])), true)] = MLVal (name, ((tysm, t), thm))
- | check_kind [((name, ((vs, ty), [])), _)] =
- MLExc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)
- | check_kind funns =
- MLFuns (map fst funns, map_filter
- (fn ((name, ((vs, _), [(([], _), _)])), _) =>
- if null (filter_out (null o snd) vs) then SOME name else NONE
- | _ => NONE) funns);
- fun add_funs stmts = fold_map
- (fn (name, Code_Thingol.Fun (_, stmt)) =>
- map_nsp_fun_yield (mk_name_stmt false name)
- #>> rpair (rearrange_fun name stmt)
- | (name, _) =>
- error ("Function block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd check_kind);
+ val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+ val ml_stmt = case binding
+ of ML_Function (name, ((vs, ty), [])) =>
+ ML_Exc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)
+ | _ => case some_value_name
+ of NONE => ML_Funs ([binding], [])
+ | SOME (name, true) => ML_Funs ([binding], [name])
+ | SOME (name, false) => ML_Val binding
+ in
+ map_nsp_fun_yield (mk_name_stmt false name)
+ #>> (fn name' => ([name'], ml_stmt))
+ end;
+ fun add_funs stmts =
+ let
+ val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
+ in
+ fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
+ #>> rpair ml_stmt
+ end;
fun add_datatypes stmts =
fold_map
(fn (name, Code_Thingol.Datatype (_, stmt)) =>
@@ -782,7 +773,7 @@
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Datatype block without data statement: "
^ (commas o map (labelled_name o fst)) stmts)
- | stmts => MLDatas stmts)));
+ | stmts => ML_Datas stmts)));
fun add_class stmts =
fold_map
(fn (name, Code_Thingol.Class (_, stmt)) =>
@@ -797,11 +788,10 @@
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Class block without class statement: "
^ (commas o map (labelled_name o fst)) stmts)
- | [stmt] => MLClass stmt)));
- fun add_inst [(name, Code_Thingol.Classinst stmt)] =
- map_nsp_fun_yield (mk_name_stmt false name)
- #>> (fn base => ([base], MLClassinst (name, stmt)));
- fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+ | [stmt] => ML_Class stmt)));
+ fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
+ add_fun stmt
+ | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
add_funs stmts
| add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
add_datatypes stmts
@@ -813,8 +803,10 @@
add_class stmts
| add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
add_class stmts
- | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =
- add_inst stmts
+ | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
+ add_fun stmt
+ | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+ add_funs stmts
| add_stmts stmts = error ("Illegal mutual dependencies: " ^
(commas o map (labelled_name o fst)) stmts);
fun add_stmts' stmts nsp_nodes =