--- a/Admin/isatest/settings/mac-poly64-M8 Fri Feb 24 08:49:36 2012 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Fri Feb 24 09:40:02 2012 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.4.1"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 2000 --gcthreads 4"
+ ML_OPTIONS="-H 2000 --gcthreads 8"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 09:40:02 2012 +0100
@@ -1648,7 +1648,7 @@
\end{matharray}
@{rail "
- @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
+ @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
;
@@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -1662,11 +1662,11 @@
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
- @@{command (HOL) quickcheck_generator} typeconstructor \\
+ @@{command (HOL) quickcheck_generator} @{syntax nameref} \\
'operations:' ( @{syntax term} +)
;
- @@{command (HOL) find_unused_assms} theoryname?
+ @@{command (HOL) find_unused_assms} @{syntax name}?
;
modes: '(' (@{syntax name} +) ')'
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 08:49:36 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 09:40:02 2012 +0100
@@ -2351,7 +2351,7 @@
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
-\rail@nont{\isa{name}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
\rail@endbar
\rail@bar
@@ -2408,7 +2408,7 @@
\rail@end
\rail@begin{4}{}
\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
-\rail@nont{\isa{typeconstructor}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@cr{2}
\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@plus
@@ -2420,7 +2420,7 @@
\rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{theoryname}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endbar
\rail@end
\rail@begin{2}{\isa{modes}}
--- a/src/HOL/Code_Evaluation.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Code_Evaluation.thy Fri Feb 24 09:40:02 2012 +0100
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Evaluation
-imports Plain Typerep Code_Numeral Predicate
+imports Plain Typerep Code_Numeral
uses ("Tools/code_evaluation.ML")
begin
--- a/src/HOL/Code_Numeral.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Code_Numeral.thy Fri Feb 24 09:40:02 2012 +0100
@@ -281,7 +281,18 @@
qed
-hide_const (open) of_nat nat_of Suc subtract int_of
+text {* Lazy Evaluation of an indexed function *}
+
+function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
+where
+ "iterate_upto f n m =
+ Predicate.Seq (%u. if n > m then Predicate.Empty
+ else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
+by pat_completeness auto
+
+termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
+
+hide_const (open) of_nat nat_of Suc subtract int_of iterate_upto
subsection {* Code generator setup *}
@@ -366,4 +377,3 @@
Code_Numeral Arith
end
-
--- a/src/HOL/IsaMakefile Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/IsaMakefile Fri Feb 24 09:40:02 2012 +0100
@@ -197,6 +197,7 @@
Partial_Function.thy \
Plain.thy \
Power.thy \
+ Predicate.thy \
Product_Type.thy \
Relation.thy \
Rings.thy \
@@ -293,7 +294,6 @@
Nitpick.thy \
Numeral_Simprocs.thy \
Presburger.thy \
- Predicate.thy \
Predicate_Compile.thy \
Quickcheck.thy \
Quickcheck_Exhaustive.thy \
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Fri Feb 24 09:40:02 2012 +0100
@@ -249,9 +249,9 @@
by hoare auto
-subsection{* Time *}
+subsection {* Time *}
-text{* A simple embedding of time in Hoare logic: function @{text
+text {* A simple embedding of time in Hoare logic: function @{text
timeit} inserts an extra variable to keep track of the elapsed time. *}
record tstate = time :: nat
--- a/src/HOL/List.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/List.thy Fri Feb 24 09:40:02 2012 +0100
@@ -2662,6 +2662,7 @@
by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
+declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
lemma (in complete_lattice) INF_set_foldr [code]:
"INFI (set xs) f = foldr (inf \<circ> f) xs top"
@@ -2671,6 +2672,29 @@
"SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
+(* FIXME: better implement conversion by bisection *)
+
+lemma pred_of_set_fold_sup:
+ assumes "finite A"
+ shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
+proof (rule sym)
+ interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+ by (fact comp_fun_idem_sup)
+ from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
+qed
+
+lemma pred_of_set_set_fold_sup:
+ "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
+proof -
+ interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+ by (fact comp_fun_idem_sup)
+ show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
+qed
+
+lemma pred_of_set_set_foldr_sup [code]:
+ "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
+ by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
+
subsubsection {* @{text upt} *}
--- a/src/HOL/Predicate.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Predicate.thy Fri Feb 24 09:40:02 2012 +0100
@@ -1,11 +1,11 @@
(* Title: HOL/Predicate.thy
- Author: Lukas Bulwahn and Florian Haftmann, TU Muenchen
+ Author: Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
*)
-header {* Predicates as enumerations *}
+header {* Predicates as relations and enumerations *}
theory Predicate
-imports List
+imports Inductive Relation
begin
notation
@@ -22,7 +22,261 @@
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-subsection {* The type of predicate enumerations (a monad) *}
+
+subsection {* Classical rules for reasoning on predicates *}
+
+declare predicate1D [Pure.dest?, dest?]
+declare predicate2I [Pure.intro!, intro!]
+declare predicate2D [Pure.dest, dest]
+declare bot1E [elim!]
+declare bot2E [elim!]
+declare top1I [intro!]
+declare top2I [intro!]
+declare inf1I [intro!]
+declare inf2I [intro!]
+declare inf1E [elim!]
+declare inf2E [elim!]
+declare sup1I1 [intro?]
+declare sup2I1 [intro?]
+declare sup1I2 [intro?]
+declare sup2I2 [intro?]
+declare sup1E [elim!]
+declare sup2E [elim!]
+declare sup1CI [intro!]
+declare sup2CI [intro!]
+declare INF1_I [intro!]
+declare INF2_I [intro!]
+declare INF1_D [elim]
+declare INF2_D [elim]
+declare INF1_E [elim]
+declare INF2_E [elim]
+declare SUP1_I [intro]
+declare SUP2_I [intro]
+declare SUP1_E [elim!]
+declare SUP2_E [elim!]
+
+
+subsection {* Conversion between set and predicate relations *}
+
+subsubsection {* Equality *}
+
+lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
+ by (simp add: set_eq_iff fun_eq_iff)
+
+lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
+ by (simp add: set_eq_iff fun_eq_iff)
+
+
+subsubsection {* Order relation *}
+
+lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+ by (simp add: subset_iff le_fun_def)
+
+lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+ by (simp add: subset_iff le_fun_def)
+
+
+subsubsection {* Top and bottom elements *}
+
+lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
+ by (auto simp add: fun_eq_iff)
+
+lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
+ by (auto simp add: fun_eq_iff)
+
+
+subsubsection {* Binary intersection *}
+
+lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+ by (simp add: inf_fun_def)
+
+lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
+ by (simp add: inf_fun_def)
+
+
+subsubsection {* Binary union *}
+
+lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
+ by (simp add: sup_fun_def)
+
+lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
+ by (simp add: sup_fun_def)
+
+
+subsubsection {* Intersections of families *}
+
+lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
+ by (simp add: INF_apply fun_eq_iff)
+
+lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
+ by (simp add: INF_apply fun_eq_iff)
+
+
+subsubsection {* Unions of families *}
+
+lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
+ by (simp add: SUP_apply fun_eq_iff)
+
+lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
+ by (simp add: SUP_apply fun_eq_iff)
+
+
+subsection {* Predicates as relations *}
+
+subsubsection {* Composition *}
+
+inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
+ pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
+
+inductive_cases pred_compE [elim!]: "(r OO s) a c"
+
+lemma pred_comp_rel_comp_eq [pred_set_conv]:
+ "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
+ by (auto simp add: fun_eq_iff)
+
+
+subsubsection {* Converse *}
+
+inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ conversepI: "r a b \<Longrightarrow> r^--1 b a"
+
+notation (xsymbols)
+ conversep ("(_\<inverse>\<inverse>)" [1000] 1000)
+
+lemma conversepD:
+ assumes ab: "r^--1 a b"
+ shows "r b a" using ab
+ by cases simp
+
+lemma conversep_iff [iff]: "r^--1 a b = r b a"
+ by (iprover intro: conversepI dest: conversepD)
+
+lemma conversep_converse_eq [pred_set_conv]:
+ "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
+ by (auto simp add: fun_eq_iff)
+
+lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
+ by (iprover intro: order_antisym conversepI dest: conversepD)
+
+lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
+ by (iprover intro: order_antisym conversepI pred_compI
+ elim: pred_compE dest: conversepD)
+
+lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
+ by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
+
+lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
+ by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
+
+lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
+ by (auto simp add: fun_eq_iff)
+
+lemma conversep_eq [simp]: "(op =)^--1 = op ="
+ by (auto simp add: fun_eq_iff)
+
+
+subsubsection {* Domain *}
+
+inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
+
+inductive_cases DomainPE [elim!]: "DomainP r a"
+
+lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
+ by (blast intro!: Orderings.order_antisym predicate1I)
+
+
+subsubsection {* Range *}
+
+inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
+
+inductive_cases RangePE [elim!]: "RangeP r b"
+
+lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
+ by (blast intro!: Orderings.order_antisym predicate1I)
+
+
+subsubsection {* Inverse image *}
+
+definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+ "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
+
+lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
+ by (simp add: inv_image_def inv_imagep_def)
+
+lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
+ by (simp add: inv_imagep_def)
+
+
+subsubsection {* Powerset *}
+
+definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
+
+lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
+ by (auto simp add: Powp_def fun_eq_iff)
+
+lemmas Powp_mono [mono] = Pow_mono [to_pred]
+
+
+subsubsection {* Properties of relations *}
+
+abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "antisymP r \<equiv> antisym {(x, y). r x y}"
+
+abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transP r \<equiv> trans {(x, y). r x y}"
+
+abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+ "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
+
+(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
+
+definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
+
+definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "symp r \<longleftrightarrow> sym {(x, y). r x y}"
+
+definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transp r \<longleftrightarrow> trans {(x, y). r x y}"
+
+lemma reflpI:
+ "(\<And>x. r x x) \<Longrightarrow> reflp r"
+ by (auto intro: refl_onI simp add: reflp_def)
+
+lemma reflpE:
+ assumes "reflp r"
+ obtains "r x x"
+ using assms by (auto dest: refl_onD simp add: reflp_def)
+
+lemma sympI:
+ "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
+ by (auto intro: symI simp add: symp_def)
+
+lemma sympE:
+ assumes "symp r" and "r x y"
+ obtains "r y x"
+ using assms by (auto dest: symD simp add: symp_def)
+
+lemma transpI:
+ "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
+ by (auto intro: transI simp add: transp_def)
+
+lemma transpE:
+ assumes "transp r" and "r x y" and "r y z"
+ obtains "r x z"
+ using assms by (auto dest: transD simp add: transp_def)
+
+
+subsection {* Predicates as enumerations *}
+
+subsubsection {* The type of predicate enumerations (a monad) *}
datatype 'a pred = Pred "'a \<Rightarrow> bool"
@@ -211,7 +465,7 @@
using assms by (cases A) (auto simp add: bot_pred_def)
-subsection {* Emptiness check and definite choice *}
+subsubsection {* Emptiness check and definite choice *}
definition is_empty :: "'a pred \<Rightarrow> bool" where
"is_empty A \<longleftrightarrow> A = \<bottom>"
@@ -324,7 +578,7 @@
using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
-subsection {* Derived operations *}
+subsubsection {* Derived operations *}
definition if_pred :: "bool \<Rightarrow> unit pred" where
if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
@@ -414,7 +668,7 @@
by (rule ext, rule pred_eqI, auto)+
-subsection {* Implementation *}
+subsubsection {* Implementation *}
datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
@@ -508,12 +762,6 @@
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
qed
-lemma [code]:
- "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
-
-lemma [code]:
- "pred_size f P = 0" by (cases P) simp
-
primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
"contained Empty Q \<longleftrightarrow> True"
| "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
@@ -689,44 +937,6 @@
"set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq"
by auto
-text {* Lazy Evaluation of an indexed function *}
-
-function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
-where
- "iterate_upto f n m =
- Predicate.Seq (%u. if n > m then Predicate.Empty
- else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
-by pat_completeness auto
-
-termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
-
-text {* Misc *}
-
-declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
-
-(* FIXME: better implement conversion by bisection *)
-
-lemma pred_of_set_fold_sup:
- assumes "finite A"
- shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
-proof (rule sym)
- interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
- by (fact comp_fun_idem_sup)
- from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
-qed
-
-lemma pred_of_set_set_fold_sup:
- "pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot"
-proof -
- interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
- by (fact comp_fun_idem_sup)
- show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
-qed
-
-lemma pred_of_set_set_foldr_sup [code]:
- "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot"
- by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
-
no_notation
bot ("\<bottom>") and
top ("\<top>") and
@@ -745,7 +955,5 @@
hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
- iterate_upto
end
-
--- a/src/HOL/Predicate_Compile.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Predicate_Compile.thy Fri Feb 24 09:40:02 2012 +0100
@@ -5,7 +5,7 @@
header {* A compiler for predicates defined by introduction rules *}
theory Predicate_Compile
-imports Predicate New_Random_Sequence Quickcheck_Exhaustive
+imports New_Random_Sequence Quickcheck_Exhaustive
uses
"Tools/Predicate_Compile/predicate_compile_aux.ML"
"Tools/Predicate_Compile/predicate_compile_compilations.ML"
--- a/src/HOL/Quickcheck.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Quickcheck.thy Fri Feb 24 09:40:02 2012 +0100
@@ -233,7 +233,7 @@
definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
where
- "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
+ "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
where
--- a/src/HOL/Relation.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Relation.thy Fri Feb 24 09:40:02 2012 +0100
@@ -1,107 +1,15 @@
(* Title: HOL/Relation.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
*)
-header {* Relations – as sets of pairs, and binary predicates *}
+header {* Relations *}
theory Relation
imports Datatype Finite_Set
begin
-notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-
-subsection {* Classical rules for reasoning on predicates *}
-
-declare predicate1D [Pure.dest?, dest?]
-declare predicate2I [Pure.intro!, intro!]
-declare predicate2D [Pure.dest, dest]
-declare bot1E [elim!]
-declare bot2E [elim!]
-declare top1I [intro!]
-declare top2I [intro!]
-declare inf1I [intro!]
-declare inf2I [intro!]
-declare inf1E [elim!]
-declare inf2E [elim!]
-declare sup1I1 [intro?]
-declare sup2I1 [intro?]
-declare sup1I2 [intro?]
-declare sup2I2 [intro?]
-declare sup1E [elim!]
-declare sup2E [elim!]
-declare sup1CI [intro!]
-declare sup2CI [intro!]
-declare INF1_I [intro!]
-declare INF2_I [intro!]
-declare INF1_D [elim]
-declare INF2_D [elim]
-declare INF1_E [elim]
-declare INF2_E [elim]
-declare SUP1_I [intro]
-declare SUP2_I [intro]
-declare SUP1_E [elim!]
-declare SUP2_E [elim!]
-
-
-subsection {* Conversions between set and predicate relations *}
-
-lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
- by (simp add: set_eq_iff fun_eq_iff)
-
-lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
- by (simp add: set_eq_iff fun_eq_iff)
-
-lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
- by (simp add: subset_iff le_fun_def)
-
-lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
- by (simp add: subset_iff le_fun_def)
-
-lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
- by (auto simp add: fun_eq_iff)
-
-lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
- by (auto simp add: fun_eq_iff)
-
-lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
- by (simp add: inf_fun_def)
-
-lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
- by (simp add: inf_fun_def)
-
-lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
- by (simp add: sup_fun_def)
-
-lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
- by (simp add: sup_fun_def)
-
-lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
- by (simp add: INF_apply fun_eq_iff)
-
-lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
- by (simp add: INF_apply fun_eq_iff)
-
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
- by (simp add: SUP_apply fun_eq_iff)
-
-lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
- by (simp add: SUP_apply fun_eq_iff)
-
-
-subsection {* Relations as sets of pairs *}
+subsection {* Definitions *}
type_synonym 'a rel = "('a * 'a) set"
@@ -182,7 +90,7 @@
"inv_image r f = {(x, y). (f x, f y) : r}"
-subsubsection {* The identity relation *}
+subsection {* The identity relation *}
lemma IdI [intro]: "(a, a) : Id"
by (simp add: Id_def)
@@ -207,7 +115,7 @@
by (simp add: trans_def)
-subsubsection {* Diagonal: identity over a set *}
+subsection {* Diagonal: identity over a set *}
lemma Id_on_empty [simp]: "Id_on {} = {}"
by (simp add: Id_on_def)
@@ -234,7 +142,7 @@
by blast
-subsubsection {* Composition of two relations *}
+subsection {* Composition of two relations *}
lemma rel_compI [intro]:
"(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
@@ -286,7 +194,7 @@
by auto
-subsubsection {* Reflexivity *}
+subsection {* Reflexivity *}
lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
by (unfold refl_on_def) (iprover intro!: ballI)
@@ -324,8 +232,7 @@
"refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
-
-subsubsection {* Antisymmetry *}
+subsection {* Antisymmetry *}
lemma antisymI:
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
@@ -344,7 +251,7 @@
by (unfold antisym_def) blast
-subsubsection {* Symmetry *}
+subsection {* Symmetry *}
lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
by (unfold sym_def) iprover
@@ -368,7 +275,7 @@
by (rule symI) clarify
-subsubsection {* Transitivity *}
+subsection {* Transitivity *}
lemma trans_join [code]:
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
@@ -393,8 +300,7 @@
lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
unfolding antisym_def trans_def by blast
-
-subsubsection {* Irreflexivity *}
+subsection {* Irreflexivity *}
lemma irrefl_distinct [code]:
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
@@ -404,7 +310,7 @@
by(simp add:irrefl_def)
-subsubsection {* Totality *}
+subsection {* Totality *}
lemma total_on_empty[simp]: "total_on {} r"
by(simp add:total_on_def)
@@ -412,8 +318,7 @@
lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
by(simp add: total_on_def)
-
-subsubsection {* Converse *}
+subsection {* Converse *}
lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
by (simp add: converse_def)
@@ -478,7 +383,7 @@
by (auto simp: total_on_def)
-subsubsection {* Domain *}
+subsection {* Domain *}
declare Domain_def [no_atp]
@@ -539,7 +444,7 @@
by auto
-subsubsection {* Range *}
+subsection {* Range *}
lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
by (simp add: Domain_def Range_def)
@@ -588,7 +493,7 @@
by force
-subsubsection {* Field *}
+subsection {* Field *}
lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
by(auto simp:Field_def Domain_def Range_def)
@@ -609,7 +514,7 @@
by(auto simp:Field_def)
-subsubsection {* Image of a set under a relation *}
+subsection {* Image of a set under a relation *}
declare Image_def [no_atp]
@@ -683,7 +588,7 @@
by blast
-subsubsection {* Single valued relations *}
+subsection {* Single valued relations *}
lemma single_valuedI:
"ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
@@ -708,7 +613,7 @@
by (unfold single_valued_def) blast
-subsubsection {* Graphs given by @{text Collect} *}
+subsection {* Graphs given by @{text Collect} *}
lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
by auto
@@ -720,7 +625,7 @@
by auto
-subsubsection {* Inverse image *}
+subsection {* Inverse image *}
lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
by (unfold sym_def inv_image_def) blast
@@ -738,7 +643,7 @@
unfolding inv_image_def converse_def by auto
-subsubsection {* Finiteness *}
+subsection {* Finiteness *}
lemma finite_converse [iff]: "finite (r^-1) = finite r"
apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
@@ -766,7 +671,7 @@
done
-subsubsection {* Miscellaneous *}
+subsection {* Miscellaneous *}
text {* Version of @{thm[source] lfp_induct} for binary relations *}
@@ -778,171 +683,4 @@
lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
by auto
-
-subsection {* Relations as binary predicates *}
-
-subsubsection {* Composition *}
-
-inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
- for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
- pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
-
-inductive_cases pred_compE [elim!]: "(r OO s) a c"
-
-lemma pred_comp_rel_comp_eq [pred_set_conv]:
- "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
- by (auto simp add: fun_eq_iff)
-
-
-subsubsection {* Converse *}
-
-inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
- for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
- conversepI: "r a b \<Longrightarrow> r^--1 b a"
-
-notation (xsymbols)
- conversep ("(_\<inverse>\<inverse>)" [1000] 1000)
-
-lemma conversepD:
- assumes ab: "r^--1 a b"
- shows "r b a" using ab
- by cases simp
-
-lemma conversep_iff [iff]: "r^--1 a b = r b a"
- by (iprover intro: conversepI dest: conversepD)
-
-lemma conversep_converse_eq [pred_set_conv]:
- "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
- by (auto simp add: fun_eq_iff)
-
-lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
- by (iprover intro: order_antisym conversepI dest: conversepD)
-
-lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
- by (iprover intro: order_antisym conversepI pred_compI
- elim: pred_compE dest: conversepD)
-
-lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
- by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
-
-lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
- by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
-
-lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
- by (auto simp add: fun_eq_iff)
-
-lemma conversep_eq [simp]: "(op =)^--1 = op ="
- by (auto simp add: fun_eq_iff)
-
-
-subsubsection {* Domain *}
-
-inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
- for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
- DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
-
-inductive_cases DomainPE [elim!]: "DomainP r a"
-
-lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
- by (blast intro!: Orderings.order_antisym predicate1I)
-
-
-subsubsection {* Range *}
-
-inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
- for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
- RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
-
-inductive_cases RangePE [elim!]: "RangeP r b"
-
-lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
- by (blast intro!: Orderings.order_antisym predicate1I)
-
-
-subsubsection {* Inverse image *}
-
-definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
- "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
-
-lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
- by (simp add: inv_image_def inv_imagep_def)
-
-lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
- by (simp add: inv_imagep_def)
-
-
-subsubsection {* Powerset *}
-
-definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
- "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
-
-lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
- by (auto simp add: Powp_def fun_eq_iff)
-
-lemmas Powp_mono [mono] = Pow_mono [to_pred]
-
-
-subsubsection {* Properties of predicate relations *}
-
-abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "antisymP r \<equiv> antisym {(x, y). r x y}"
-
-abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "transP r \<equiv> trans {(x, y). r x y}"
-
-abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
- "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
-
-(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
-
-definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
-
-definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "symp r \<longleftrightarrow> sym {(x, y). r x y}"
-
-definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "transp r \<longleftrightarrow> trans {(x, y). r x y}"
-
-lemma reflpI:
- "(\<And>x. r x x) \<Longrightarrow> reflp r"
- by (auto intro: refl_onI simp add: reflp_def)
-
-lemma reflpE:
- assumes "reflp r"
- obtains "r x x"
- using assms by (auto dest: refl_onD simp add: reflp_def)
-
-lemma sympI:
- "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
- by (auto intro: symI simp add: symp_def)
-
-lemma sympE:
- assumes "symp r" and "r x y"
- obtains "r y x"
- using assms by (auto dest: symD simp add: symp_def)
-
-lemma transpI:
- "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
- by (auto intro: transI simp add: transp_def)
-
-lemma transpE:
- assumes "transp r" and "r x y" and "r y z"
- obtains "r x z"
- using assms by (auto dest: transD simp add: transp_def)
-
-no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-no_syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 24 09:40:02 2012 +0100
@@ -186,7 +186,7 @@
| map2_optional f [] [] = []
fun find_indices f xs =
- map_filter (fn (i, true) => SOME i | (_, false) => NONE) (map_index (apsnd f) xs)
+ map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
(* mode *)
@@ -253,7 +253,7 @@
raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
end
| all_modes_of_typ @{typ bool} = [Bool]
- | all_modes_of_typ _ =
+ | all_modes_of_typ T =
raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
fun all_smodes_of_typ (T as Type ("fun", _)) =
@@ -394,7 +394,7 @@
fun split_modeT mode Ts =
let
- fun split_arg_mode (Fun _) _ = ([], [])
+ fun split_arg_mode (Fun _) T = ([], [])
| split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
let
val (i1, o1) = split_arg_mode m1 T1
@@ -481,6 +481,8 @@
fun is_intro constname t = is_intro_term constname (prop_of t)
+fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
+
fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
| is_predT _ = false
@@ -502,6 +504,12 @@
| _ => false)
in check end;
+fun is_funtype (Type ("fun", [_, _])) = true
+ | is_funtype _ = false;
+
+fun is_Type (Type _) = true
+ | is_Type _ = false
+
(* returns true if t is an application of an datatype constructor *)
(* which then consequently would be splitted *)
(* else false *)
@@ -557,7 +565,7 @@
fun fold_atoms f intro s =
let
- val (literals, _) = Logic.strip_horn intro
+ val (literals, head) = Logic.strip_horn intro
fun appl t s = (case t of
(@{term Not} $ t') => f t' s
| _ => f t s)
@@ -574,6 +582,13 @@
(Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
end;
+fun map_premises f intro =
+ let
+ val (premises, head) = Logic.strip_horn intro
+ in
+ Logic.list_implies (map f premises, head)
+ end
+
fun map_filter_premises f intro =
let
val (premises, head) = Logic.strip_horn intro
@@ -608,7 +623,7 @@
|> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
-fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
+fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
| find_split_thm thy _ = NONE
(* lifting term operations to theorems *)
@@ -811,7 +826,7 @@
fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
| rewrite_args (arg::args) (pats, intro_t, ctxt) =
(case HOLogic.strip_tupleT (fastype_of arg) of
- (_ :: _ :: _) =>
+ (Ts as _ :: _ :: _) =>
let
fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
@@ -853,7 +868,7 @@
fun dest_conjunct_prem th =
case HOLogic.dest_Trueprop (prop_of th) of
- (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
+ (Const (@{const_name HOL.conj}, _) $ t $ t') =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
| _ => [th]
@@ -864,9 +879,10 @@
val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
val intro_t = prop_of intro'
val concl = Logic.strip_imp_concl intro_t
- val (_, args) = strip_comb (HOLogic.dest_Trueprop concl)
+ val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
- val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
+ val (pats', intro_t', ctxt3) =
+ fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
fun rewrite_pat (ct1, ct2) =
(ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
val t_insts' = map rewrite_pat t_insts
@@ -931,6 +947,7 @@
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
+ val T = TFree (tname, HOLogic.typeS)
val T' = TFree (tname', HOLogic.typeS)
val U = TFree (uname, HOLogic.typeS)
val y = Free (yname, U)
@@ -963,6 +980,11 @@
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
| _ => Conv.all_conv ct
+fun all_params_conv cv ctxt ct =
+ if Logic.is_all (Thm.term_of ct)
+ then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
+ else cv ctxt ct;
+
(** eta contract higher-order arguments **)
fun eta_contract_ho_arguments thy intro =
@@ -1040,7 +1062,7 @@
val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
val T = fastype_of outp_pred
val paramTs = ho_argsT_of_typ (binder_types T)
- val (param_names, _) = Variable.variant_fixes
+ val (param_names, ctxt'') = Variable.variant_fixes
(map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
val params = map2 (curry Free) param_names paramTs
in
@@ -1175,8 +1197,8 @@
fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B
- | strip_imp_concl A = A;
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
+ | strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Fri Feb 24 09:40:02 2012 +0100
@@ -30,7 +30,7 @@
HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
fun mk_iterate_upto T (f, from, to) =
- list_comb (Const (@{const_name Predicate.iterate_upto},
+ list_comb (Const (@{const_name Code_Numeral.iterate_upto},
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
[f, from, to])
--- a/src/HOL/Transitive_Closure.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Feb 24 09:40:02 2012 +0100
@@ -6,7 +6,7 @@
header {* Reflexive and Transitive closure of a relation *}
theory Transitive_Closure
-imports Relation
+imports Predicate
uses "~~/src/Provers/trancl.ML"
begin
--- a/src/HOL/Wellfounded.thy Fri Feb 24 08:49:36 2012 +0100
+++ b/src/HOL/Wellfounded.thy Fri Feb 24 09:40:02 2012 +0100
@@ -858,4 +858,10 @@
declare "prod.size" [no_atp]
+lemma [code]:
+ "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
+
+lemma [code]:
+ "pred_size f P = 0" by (cases P) simp
+
end
--- a/src/Pure/General/graph.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/General/graph.scala Fri Feb 24 09:40:02 2012 +0100
@@ -17,7 +17,8 @@
class Undefined[Key](x: Key) extends Exception
class Cycles[Key](cycles: List[List[Key]]) extends Exception
- def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)
+ private val empty_val: Graph[Any, Nothing] = new Graph[Any, Nothing](Map.empty)
+ def empty[Key, A]: Graph[Key, A] = empty_val.asInstanceOf[Graph[Key, A]]
}
--- a/src/Pure/General/linear_set.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/General/linear_set.scala Fri Feb 24 09:40:02 2012 +0100
@@ -14,16 +14,10 @@
object Linear_Set extends ImmutableSetFactory[Linear_Set]
{
- protected case class Rep[A](
- val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
-
- private def empty_rep[A] = Rep[A](None, None, Map(), Map())
-
- private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
- : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
+ private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
+ override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
- override def empty[A] = new Linear_Set[A]
class Duplicate[A](x: A) extends Exception
class Undefined[A](x: A) extends Exception
@@ -31,7 +25,8 @@
}
-class Linear_Set[A]
+class Linear_Set[A] private(
+ start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
extends scala.collection.immutable.Set[A]
with GenericSetTemplate[A, Linear_Set]
with SetLike[A, Linear_Set[A]]
@@ -39,20 +34,15 @@
override def companion: GenericCompanion[Linear_Set] = Linear_Set
- /* representation */
-
- protected val rep = Linear_Set.empty_rep[A]
-
-
/* relative addressing */
// FIXME check definedness??
- def next(elem: A): Option[A] = rep.nexts.get(elem)
- def prev(elem: A): Option[A] = rep.prevs.get(elem)
+ def next(elem: A): Option[A] = nexts.get(elem)
+ def prev(elem: A): Option[A] = prevs.get(elem)
def get_after(hook: Option[A]): Option[A] =
hook match {
- case None => rep.start
+ case None => start
case Some(elem) =>
if (!contains(elem)) throw new Linear_Set.Undefined(elem)
next(elem)
@@ -63,51 +53,51 @@
else
hook match {
case None =>
- rep.start match {
- case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+ start match {
+ case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map())
case Some(elem1) =>
- Linear_Set.make(Some(elem), rep.end,
- rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+ new Linear_Set[A](Some(elem), end,
+ nexts + (elem -> elem1), prevs + (elem1 -> elem))
}
case Some(elem1) =>
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
- rep.nexts.get(elem1) match {
+ nexts.get(elem1) match {
case None =>
- Linear_Set.make(rep.start, Some(elem),
- rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+ new Linear_Set[A](start, Some(elem),
+ nexts + (elem1 -> elem), prevs + (elem -> elem1))
case Some(elem2) =>
- Linear_Set.make(rep.start, rep.end,
- rep.nexts + (elem1 -> elem) + (elem -> elem2),
- rep.prevs + (elem2 -> elem) + (elem -> elem1))
+ new Linear_Set[A](start, end,
+ nexts + (elem1 -> elem) + (elem -> elem2),
+ prevs + (elem2 -> elem) + (elem -> elem1))
}
}
def delete_after(hook: Option[A]): Linear_Set[A] =
hook match {
case None =>
- rep.start match {
+ start match {
case None => throw new Linear_Set.Next_Undefined[A](None)
case Some(elem1) =>
- rep.nexts.get(elem1) match {
+ nexts.get(elem1) match {
case None => empty
case Some(elem2) =>
- Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
+ new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
}
}
case Some(elem1) =>
if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
- rep.nexts.get(elem1) match {
+ nexts.get(elem1) match {
case None => throw new Linear_Set.Next_Undefined(Some(elem1))
case Some(elem2) =>
- rep.nexts.get(elem2) match {
+ nexts.get(elem2) match {
case None =>
- Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
case Some(elem3) =>
- Linear_Set.make(rep.start, rep.end,
- rep.nexts - elem2 + (elem1 -> elem3),
- rep.prevs - elem2 + (elem3 -> elem1))
+ new Linear_Set[A](start, end,
+ nexts - elem2 + (elem1 -> elem3),
+ prevs - elem2 + (elem3 -> elem1))
}
}
}
@@ -122,9 +112,9 @@
if (isEmpty) this
else {
val next =
- if (from == rep.end) None
- else if (from == None) rep.start
- else from.map(rep.nexts(_))
+ if (from == end) None
+ else if (from == None) start
+ else from.map(nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
}
@@ -135,14 +125,14 @@
override def stringPrefix = "Linear_Set"
- override def isEmpty: Boolean = !rep.start.isDefined
- override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+ override def isEmpty: Boolean = !start.isDefined
+ override def size: Int = if (isEmpty) 0 else nexts.size + 1
def contains(elem: A): Boolean =
- !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
+ !isEmpty && (end.get == elem || nexts.isDefinedAt(elem))
- private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
- private var next_elem = start
+ private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
+ private var next_elem = from
def hasNext(): Boolean = next_elem.isDefined
def next(): A =
next_elem match {
@@ -153,17 +143,17 @@
}
}
- override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts)
+ override def iterator: Iterator[A] = make_iterator(start, nexts)
def iterator(elem: A): Iterator[A] =
- if (contains(elem)) make_iterator(Some(elem), rep.nexts)
+ if (contains(elem)) make_iterator(Some(elem), nexts)
else throw new Linear_Set.Undefined(elem)
def reverse_iterator(elem: A): Iterator[A] =
- if (contains(elem)) make_iterator(Some(elem), rep.prevs)
+ if (contains(elem)) make_iterator(Some(elem), prevs)
else throw new Linear_Set.Undefined(elem)
- def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
+ def + (elem: A): Linear_Set[A] = insert_after(end, elem)
def - (elem: A): Linear_Set[A] =
if (!contains(elem)) throw new Linear_Set.Undefined(elem)
--- a/src/Pure/General/scan.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/General/scan.scala Fri Feb 24 09:40:02 2012 +0100
@@ -7,8 +7,7 @@
package isabelle
-import scala.collection.generic.Addable
-import scala.collection.IndexedSeq
+import scala.collection.{IndexedSeq, TraversableOnce}
import scala.collection.immutable.PagedSeq
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
import scala.util.parsing.combinator.RegexParsers
@@ -41,8 +40,7 @@
def apply(elems: String*): Lexicon = empty ++ elems
}
- class Lexicon private(private val main_tree: Lexicon.Tree)
- extends Addable[String, Lexicon] with RegexParsers
+ class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
{
import Lexicon.Tree
@@ -93,9 +91,7 @@
}
- /* Addable methods */
-
- def repr = this
+ /* add elements */
def + (elem: String): Lexicon =
if (contains(elem)) this
@@ -115,10 +111,11 @@
}
}
else tree
- val old = this
- new Lexicon(extend(old.main_tree, 0))
+ new Lexicon(extend(main_tree, 0))
}
+ def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
+
/** RegexParsers methods **/
--- a/src/Pure/Isar/outer_syntax.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Feb 24 09:40:02 2012 +0100
@@ -33,29 +33,22 @@
result += '"'
result.toString
}
+
+ def init(): Outer_Syntax = new Outer_Syntax()
}
-class Outer_Syntax
+class Outer_Syntax private(
+ keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
+ lexicon: Scan.Lexicon = Scan.Lexicon.empty,
+ val completion: Completion = Completion.init())
{
- protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
- protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
- lazy val completion: Completion = (new Completion).add_symbols // FIXME odd initialization
-
def keyword_kind(name: String): Option[String] = keywords.get(name)
def + (name: String, kind: String, replace: String): Outer_Syntax =
- {
- val new_keywords = keywords + (name -> kind)
- val new_lexicon = lexicon + name
- val new_completion =
- if (Keyword.control(kind)) completion
- else completion + (name, replace)
- new Outer_Syntax {
- override val lexicon = new_lexicon
- override val keywords = new_keywords
- override lazy val completion = new_completion
- }
- }
+ new Outer_Syntax(
+ keywords + (name -> kind),
+ lexicon + name,
+ if (Keyword.control(kind)) completion else completion + (name, replace))
def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
--- a/src/Pure/System/session.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/System/session.scala Fri Feb 24 09:40:02 2012 +0100
@@ -116,7 +116,7 @@
@volatile var verbose: Boolean = false
- @volatile private var syntax = new Outer_Syntax
+ @volatile private var syntax = Outer_Syntax.init()
def current_syntax(): Outer_Syntax = syntax
@volatile private var reverse_syslog = List[XML.Elem]()
--- a/src/Pure/Thy/completion.scala Fri Feb 24 08:49:36 2012 +0100
+++ b/src/Pure/Thy/completion.scala Fri Feb 24 09:40:02 2012 +0100
@@ -10,14 +10,18 @@
import scala.util.parsing.combinator.RegexParsers
-private object Completion
+object Completion
{
+ val empty: Completion = new Completion()
+ def init(): Completion = empty.add_symbols()
+
+
/** word completion **/
- val word_regex = "[a-zA-Z0-9_']+".r
- def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+ private val word_regex = "[a-zA-Z0-9_']+".r
+ private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
- object Parse extends RegexParsers
+ private object Parse extends RegexParsers
{
override val whiteSpace = "".r
@@ -36,33 +40,24 @@
}
}
-class Completion
+class Completion private(
+ words_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ words_map: Map[String, String] = Map.empty,
+ abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ abbrevs_map: Map[String, (String, String)] = Map.empty)
{
- /* representation */
-
- protected val words_lex = Scan.Lexicon()
- protected val words_map = Map[String, String]()
-
- protected val abbrevs_lex = Scan.Lexicon()
- protected val abbrevs_map = Map[String, (String, String)]()
-
-
/* adding stuff */
def + (keyword: String, replace: String): Completion =
- {
- val old = this
- new Completion {
- override val words_lex = old.words_lex + keyword
- override val words_map = old.words_map + (keyword -> replace)
- override val abbrevs_lex = old.abbrevs_lex
- override val abbrevs_map = old.abbrevs_map
- }
- }
+ new Completion(
+ words_lex + keyword,
+ words_map + (keyword -> replace),
+ abbrevs_lex,
+ abbrevs_map)
def + (keyword: String): Completion = this + (keyword, keyword)
- def add_symbols: Completion =
+ private def add_symbols(): Completion =
{
val words =
(for ((x, _) <- Symbol.names) yield (x, x)).toList :::
@@ -73,13 +68,11 @@
(for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
yield (y.reverse.toString, (y, x))).toList
- val old = this
- new Completion {
- override val words_lex = old.words_lex ++ words.map(_._1)
- override val words_map = old.words_map ++ words
- override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
- override val abbrevs_map = old.abbrevs_map ++ abbrs
- }
+ new Completion(
+ words_lex ++ words.map(_._1),
+ words_map ++ words,
+ abbrevs_lex ++ abbrs.map(_._1),
+ abbrevs_map ++ abbrs)
}