# HG changeset patch # User haftmann # Date 1330072802 -3600 # Node ID fc315796794ea35649b3b32f32bfcb461014daf2 # Parent f14eaac189e820f180c846eaaaa0e1ab01ec544a# Parent 0bd7c16a420024756048fde7037d07871101b8f2 given up disfruitful branch diff -r 0bd7c16a4200 -r fc315796794e Admin/isatest/settings/mac-poly64-M8 --- 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 diff -r 0bd7c16a4200 -r fc315796794e doc-src/IsarRef/Thy/HOL_Specific.thy --- 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} +) ')' diff -r 0bd7c16a4200 -r fc315796794e doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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}} diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Code_Evaluation.thy --- 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 diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Code_Numeral.thy --- 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 \ 'a) \ code_numeral \ code_numeral \ '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 - diff -r 0bd7c16a4200 -r fc315796794e src/HOL/IsaMakefile --- 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 \ diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Isar_Examples/Hoare_Ex.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 diff -r 0bd7c16a4200 -r fc315796794e src/HOL/List.thy --- 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 \ f) xs top" @@ -2671,6 +2672,29 @@ "SUPR (set xs) f = foldr (sup \ 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 \ 'a Predicate.pred \ '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 \ 'a Predicate.pred \ '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} *} diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Predicate.thy --- 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 \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [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]: "((\x. x \ R) = (\x. x \ S)) \ (R = S)" + by (simp add: set_eq_iff fun_eq_iff) + +lemma pred_equals_eq2 [pred_set_conv]: "((\x y. (x, y) \ R) = (\x y. (x, y) \ S)) \ (R = S)" + by (simp add: set_eq_iff fun_eq_iff) + + +subsubsection {* Order relation *} + +lemma pred_subset_eq [pred_set_conv]: "((\x. x \ R) \ (\x. x \ S)) \ (R \ S)" + by (simp add: subset_iff le_fun_def) + +lemma pred_subset_eq2 [pred_set_conv]: "((\x y. (x, y) \ R) \ (\x y. (x, y) \ S)) \ (R \ S)" + by (simp add: subset_iff le_fun_def) + + +subsubsection {* Top and bottom elements *} + +lemma bot_empty_eq: "\ = (\x. x \ {})" + by (auto simp add: fun_eq_iff) + +lemma bot_empty_eq2: "\ = (\x y. (x, y) \ {})" + by (auto simp add: fun_eq_iff) + + +subsubsection {* Binary intersection *} + +lemma inf_Int_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" + by (simp add: inf_fun_def) + +lemma inf_Int_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" + by (simp add: inf_fun_def) + + +subsubsection {* Binary union *} + +lemma sup_Un_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" + by (simp add: sup_fun_def) + +lemma sup_Un_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" + by (simp add: sup_fun_def) + + +subsubsection {* Intersections of families *} + +lemma INF_INT_eq: "(\i. (\x. x \ r i)) = (\x. x \ (\i. r i))" + by (simp add: INF_apply fun_eq_iff) + +lemma INF_INT_eq2: "(\i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i. r i))" + by (simp add: INF_apply fun_eq_iff) + + +subsubsection {* Unions of families *} + +lemma SUP_UN_eq [pred_set_conv]: "(\i. (\x. x \ r i)) = (\x. x \ (\i. r i))" + by (simp add: SUP_apply fun_eq_iff) + +lemma SUP_UN_eq2 [pred_set_conv]: "(\i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i. r i))" + by (simp add: SUP_apply fun_eq_iff) + + +subsection {* Predicates as relations *} + +subsubsection {* Composition *} + +inductive pred_comp :: "['a \ 'b \ bool, 'b \ 'c \ bool] \ 'a \ 'c \ bool" (infixr "OO" 75) + for r :: "'a \ 'b \ bool" and s :: "'b \ 'c \ bool" where + pred_compI [intro]: "r a b \ s b c \ (r OO s) a c" + +inductive_cases pred_compE [elim!]: "(r OO s) a c" + +lemma pred_comp_rel_comp_eq [pred_set_conv]: + "((\x y. (x, y) \ r) OO (\x y. (x, y) \ s)) = (\x y. (x, y) \ r O s)" + by (auto simp add: fun_eq_iff) + + +subsubsection {* Converse *} + +inductive conversep :: "('a \ 'b \ bool) \ 'b \ 'a \ bool" ("(_^--1)" [1000] 1000) + for r :: "'a \ 'b \ bool" where + conversepI: "r a b \ r^--1 b a" + +notation (xsymbols) + conversep ("(_\\)" [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]: + "(\x y. (x, y) \ r)^--1 = (\x y. (x, y) \ 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 \ s)^--1 = r^--1 \ s^--1" + by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) + +lemma converse_join: "(r \ s)^--1 = r^--1 \ s^--1" + by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) + +lemma conversep_noteq [simp]: "(op \)^--1 = op \" + 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 \ 'b \ bool) \ 'a \ bool" + for r :: "'a \ 'b \ bool" where + DomainPI [intro]: "r a b \ DomainP r a" + +inductive_cases DomainPE [elim!]: "DomainP r a" + +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\x y. (x, y) \ r) = (\x. x \ Domain r)" + by (blast intro!: Orderings.order_antisym predicate1I) + + +subsubsection {* Range *} + +inductive RangeP :: "('a \ 'b \ bool) \ 'b \ bool" + for r :: "'a \ 'b \ bool" where + RangePI [intro]: "r a b \ RangeP r b" + +inductive_cases RangePE [elim!]: "RangeP r b" + +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\x y. (x, y) \ r) = (\x. x \ Range r)" + by (blast intro!: Orderings.order_antisym predicate1I) + + +subsubsection {* Inverse image *} + +definition inv_imagep :: "('b \ 'b \ bool) \ ('a \ 'b) \ 'a \ 'a \ bool" where + "inv_imagep r f = (\x y. r (f x) (f y))" + +lemma [pred_set_conv]: "inv_imagep (\x y. (x, y) \ r) f = (\x y. (x, y) \ 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 \ bool) \ 'a set \ bool" where + "Powp A = (\B. \x \ B. A x)" + +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\x. x \ A) = (\x. x \ 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 \ 'a \ bool) \ bool" where + "antisymP r \ antisym {(x, y). r x y}" + +abbreviation transP :: "('a \ 'a \ bool) \ bool" where + "transP r \ trans {(x, y). r x y}" + +abbreviation single_valuedP :: "('a \ 'b \ bool) \ bool" where + "single_valuedP r \ single_valued {(x, y). r x y}" + +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*) + +definition reflp :: "('a \ 'a \ bool) \ bool" where + "reflp r \ refl {(x, y). r x y}" + +definition symp :: "('a \ 'a \ bool) \ bool" where + "symp r \ sym {(x, y). r x y}" + +definition transp :: "('a \ 'a \ bool) \ bool" where + "transp r \ trans {(x, y). r x y}" + +lemma reflpI: + "(\x. r x x) \ 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: + "(\x y. r x y \ r y x) \ 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: + "(\x y z. r x y \ r y z \ r x z) \ 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 \ 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 \ bool" where "is_empty A \ A = \" @@ -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 \ unit pred" where if_pred_eq: "if_pred b = (if b then single () else \)" @@ -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 \ 'a pred \ bool" where "contained Empty Q \ True" | "contained (Insert x P) Q \ eval Q x \ P \ Q" @@ -689,44 +937,6 @@ "set_of_seq (Predicate.Join P xq) = set_of_pred P \ set_of_seq xq" by auto -text {* Lazy Evaluation of an indexed function *} - -function iterate_upto :: "(code_numeral \ 'a) \ code_numeral \ code_numeral \ '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 \ 'a Predicate.pred \ '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 \ 'a Predicate.pred \ '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 ("\") and 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 - diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Predicate_Compile.thy --- 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" diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Quickcheck.thy --- 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 \ unit randompred" where diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Relation.thy --- 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 ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\_" [900] 900) and - Sup ("\_" [900] 900) - -syntax (xsymbols) - "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [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]: "((\x. x \ R) = (\x. x \ S)) \ (R = S)" - by (simp add: set_eq_iff fun_eq_iff) - -lemma pred_equals_eq2 [pred_set_conv]: "((\x y. (x, y) \ R) = (\x y. (x, y) \ S)) \ (R = S)" - by (simp add: set_eq_iff fun_eq_iff) - -lemma pred_subset_eq [pred_set_conv]: "((\x. x \ R) \ (\x. x \ S)) \ (R \ S)" - by (simp add: subset_iff le_fun_def) - -lemma pred_subset_eq2 [pred_set_conv]: "((\x y. (x, y) \ R) \ (\x y. (x, y) \ S)) \ (R \ S)" - by (simp add: subset_iff le_fun_def) - -lemma bot_empty_eq: "\ = (\x. x \ {})" - by (auto simp add: fun_eq_iff) - -lemma bot_empty_eq2: "\ = (\x y. (x, y) \ {})" - by (auto simp add: fun_eq_iff) - -lemma inf_Int_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" - by (simp add: inf_fun_def) - -lemma inf_Int_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" - by (simp add: inf_fun_def) - -lemma sup_Un_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)" - by (simp add: sup_fun_def) - -lemma sup_Un_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)" - by (simp add: sup_fun_def) - -lemma INF_INT_eq: "(\i. (\x. x \ r i)) = (\x. x \ (\i. r i))" - by (simp add: INF_apply fun_eq_iff) - -lemma INF_INT_eq2: "(\i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i. r i))" - by (simp add: INF_apply fun_eq_iff) - -lemma SUP_UN_eq [pred_set_conv]: "(\i. (\x. x \ r i)) = (\x. x \ (\i. r i))" - by (simp add: SUP_apply fun_eq_iff) - -lemma SUP_UN_eq2 [pred_set_conv]: "(\i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\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 \ A \ 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 = ((\(x, y) \ r. x : A \ y : A) \ (\x \ 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 \ (\(x, y1) \ r. \(y2, z) \ r. y1 = y2 \ (x, z) \ r)" @@ -393,8 +300,7 @@ lemma trans_diff_Id: " trans r \ antisym r \ trans (r-Id)" unfolding antisym_def trans_def by blast - -subsubsection {* Irreflexivity *} +subsection {* Irreflexivity *} lemma irrefl_distinct [code]: "irrefl r \ (\(x, y) \ r. x \ 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 \ s \ Field r \ 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: "(\x y. (x, y) \ r \ (x, y) \ s) \ r \ s" by auto - -subsection {* Relations as binary predicates *} - -subsubsection {* Composition *} - -inductive pred_comp :: "['a \ 'b \ bool, 'b \ 'c \ bool] \ 'a \ 'c \ bool" (infixr "OO" 75) - for r :: "'a \ 'b \ bool" and s :: "'b \ 'c \ bool" where - pred_compI [intro]: "r a b \ s b c \ (r OO s) a c" - -inductive_cases pred_compE [elim!]: "(r OO s) a c" - -lemma pred_comp_rel_comp_eq [pred_set_conv]: - "((\x y. (x, y) \ r) OO (\x y. (x, y) \ s)) = (\x y. (x, y) \ r O s)" - by (auto simp add: fun_eq_iff) - - -subsubsection {* Converse *} - -inductive conversep :: "('a \ 'b \ bool) \ 'b \ 'a \ bool" ("(_^--1)" [1000] 1000) - for r :: "'a \ 'b \ bool" where - conversepI: "r a b \ r^--1 b a" - -notation (xsymbols) - conversep ("(_\\)" [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]: - "(\x y. (x, y) \ r)^--1 = (\x y. (x, y) \ 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 \ s)^--1 = r^--1 \ s^--1" - by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) - -lemma converse_join: "(r \ s)^--1 = r^--1 \ s^--1" - by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) - -lemma conversep_noteq [simp]: "(op \)^--1 = op \" - 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 \ 'b \ bool) \ 'a \ bool" - for r :: "'a \ 'b \ bool" where - DomainPI [intro]: "r a b \ DomainP r a" - -inductive_cases DomainPE [elim!]: "DomainP r a" - -lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\x y. (x, y) \ r) = (\x. x \ Domain r)" - by (blast intro!: Orderings.order_antisym predicate1I) - - -subsubsection {* Range *} - -inductive RangeP :: "('a \ 'b \ bool) \ 'b \ bool" - for r :: "'a \ 'b \ bool" where - RangePI [intro]: "r a b \ RangeP r b" - -inductive_cases RangePE [elim!]: "RangeP r b" - -lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\x y. (x, y) \ r) = (\x. x \ Range r)" - by (blast intro!: Orderings.order_antisym predicate1I) - - -subsubsection {* Inverse image *} - -definition inv_imagep :: "('b \ 'b \ bool) \ ('a \ 'b) \ 'a \ 'a \ bool" where - "inv_imagep r f = (\x y. r (f x) (f y))" - -lemma [pred_set_conv]: "inv_imagep (\x y. (x, y) \ r) f = (\x y. (x, y) \ 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 \ bool) \ 'a set \ bool" where - "Powp A = (\B. \x \ B. A x)" - -lemma Powp_Pow_eq [pred_set_conv]: "Powp (\x. x \ A) = (\x. x \ 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 \ 'a \ bool) \ bool" where - "antisymP r \ antisym {(x, y). r x y}" - -abbreviation transP :: "('a \ 'a \ bool) \ bool" where - "transP r \ trans {(x, y). r x y}" - -abbreviation single_valuedP :: "('a \ 'b \ bool) \ bool" where - "single_valuedP r \ single_valued {(x, y). r x y}" - -(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*) - -definition reflp :: "('a \ 'a \ bool) \ bool" where - "reflp r \ refl {(x, y). r x y}" - -definition symp :: "('a \ 'a \ bool) \ bool" where - "symp r \ sym {(x, y). r x y}" - -definition transp :: "('a \ 'a \ bool) \ bool" where - "transp r \ trans {(x, y). r x y}" - -lemma reflpI: - "(\x. r x x) \ 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: - "(\x y. r x y \ r y x) \ 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: - "(\x y z. r x y \ r y z \ r x z) \ 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 ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\_" [900] 900) and - Sup ("\_" [900] 900) - -no_syntax (xsymbols) - "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - end diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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); diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- 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]) diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Transitive_Closure.thy --- 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 diff -r 0bd7c16a4200 -r fc315796794e src/HOL/Wellfounded.thy --- 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 diff -r 0bd7c16a4200 -r fc315796794e src/Pure/General/graph.scala --- 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]] } diff -r 0bd7c16a4200 -r fc315796794e src/Pure/General/linear_set.scala --- 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) diff -r 0bd7c16a4200 -r fc315796794e src/Pure/General/scan.scala --- 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 **/ diff -r 0bd7c16a4200 -r fc315796794e src/Pure/Isar/outer_syntax.scala --- 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) diff -r 0bd7c16a4200 -r fc315796794e src/Pure/System/session.scala --- 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]() diff -r 0bd7c16a4200 -r fc315796794e src/Pure/Thy/completion.scala --- 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) }