# HG changeset patch # User blanchet # Date 1392761335 -3600 # Node ID d7f411651bed54db6f08825558edf92abcff7137 # Parent 260e18aa306fca008ed3b6c570b2bb35e68a1032# Parent f663fc1e653ba3a8ec6adada0b5ee03519e2261b merged diff -r 260e18aa306f -r d7f411651bed NEWS --- a/NEWS Tue Feb 18 17:52:28 2014 +0100 +++ b/NEWS Tue Feb 18 23:08:55 2014 +0100 @@ -358,6 +358,13 @@ pass runtime Proof.context (and ensure that the simplified entity actually belongs to it). +* Subtle change of semantics of Thm.eq_thm: theory stamps are not +compared (according to Thm.thm_ord), but assumed to be covered by the +current background theory. Thus equivalent data produced in different +branches of the theory graph usually coincides (e.g. relevant for +theory merge). Note that the softer Thm.eq_thm_prop is often more +appropriate than Thm.eq_thm. + *** System *** diff -r 260e18aa306f -r d7f411651bed etc/symbols --- a/etc/symbols Tue Feb 18 17:52:28 2014 +0100 +++ b/etc/symbols Tue Feb 18 23:08:55 2014 +0100 @@ -350,6 +350,7 @@ \ code: 0x0023ce \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> +\ code: 0x002302 font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText diff -r 260e18aa306f -r d7f411651bed lib/fonts/IsabelleText.sfd --- a/lib/fonts/IsabelleText.sfd Tue Feb 18 17:52:28 2014 +0100 +++ b/lib/fonts/IsabelleText.sfd Tue Feb 18 23:08:55 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050361371 -ModificationTime: 1389823475 +ModificationTime: 1392668982 PfmFamily: 17 TTFWeight: 400 TTFWidth: 5 @@ -2240,9 +2240,9 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 9104 16 10 +WinInfo: 8912 16 10 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144 -BeginChars: 1114189 1095 +BeginChars: 1114189 1096 StartChar: u10000 Encoding: 65536 65536 0 @@ -55572,5 +55572,27 @@ 893 663 l 1,9,-1 EndSplineSet EndChar + +StartChar: house +Encoding: 8962 8962 1095 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +146.5 0 m 9,0,-1 + 146.5 647 l 25,1,-1 + 616 1220 l 25,2,-1 + 1086.5 647 l 25,3,-1 + 1086.5 0 l 17,4,-1 + 146.5 0 l 9,0,-1 +268.5 122 m 17,5,-1 + 964.5 122 l 9,6,-1 + 964.5 591 l 25,7,-1 + 616 1018 l 25,8,-1 + 268.5 591 l 25,9,-1 + 268.5 122 l 17,5,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 260e18aa306f -r d7f411651bed lib/fonts/IsabelleText.ttf Binary file lib/fonts/IsabelleText.ttf has changed diff -r 260e18aa306f -r d7f411651bed lib/fonts/IsabelleTextBold.sfd --- a/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 17:52:28 2014 +0100 +++ b/lib/fonts/IsabelleTextBold.sfd Tue Feb 18 23:08:55 2014 +0100 @@ -19,7 +19,7 @@ OS2_WeightWidthSlopeOnly: 0 OS2_UseTypoMetrics: 1 CreationTime: 1050374980 -ModificationTime: 1389823579 +ModificationTime: 1392669044 PfmFamily: 17 TTFWeight: 700 TTFWidth: 5 @@ -1674,8 +1674,8 @@ DisplaySize: -48 AntiAlias: 1 FitToEm: 1 -WinInfo: 9072 16 10 -BeginChars: 1114112 1084 +WinInfo: 8928 16 10 +BeginChars: 1114112 1085 StartChar: u10000 Encoding: 65536 65536 0 @@ -58502,5 +58502,27 @@ 1067 1072 l 1,9,-1 EndSplineSet EndChar + +StartChar: house +Encoding: 8962 8962 1084 +Width: 1233 +Flags: W +LayerCount: 2 +Fore +SplineSet +110 0 m 9,0,-1 + 110 682 l 25,1,-1 + 616 1220 l 25,2,-1 + 1123 682 l 25,3,-1 + 1123 0 l 17,4,-1 + 110 0 l 9,0,-1 +298 187 m 17,5,-1 + 935 187 l 9,6,-1 + 935 625 l 25,7,-1 + 616 959 l 25,8,-1 + 298 625 l 25,9,-1 + 298 187 l 17,5,-1 +EndSplineSet +EndChar EndChars EndSplineFont diff -r 260e18aa306f -r d7f411651bed lib/fonts/IsabelleTextBold.ttf Binary file lib/fonts/IsabelleTextBold.ttf has changed diff -r 260e18aa306f -r d7f411651bed src/Doc/IsarImplementation/Tactic.thy --- a/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Doc/IsarImplementation/Tactic.thy Tue Feb 18 23:08:55 2014 +0100 @@ -920,9 +920,8 @@ "thm"} has fewer than @{text "n"} premises. \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text - "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have - compatible background theories. Both theorems must have the same - conclusions, the same set of hypotheses, and the same set of sort + "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the + same conclusions, the same set of hypotheses, and the same set of sort hypotheses. Names of bound variables are ignored as usual. \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether diff -r 260e18aa306f -r d7f411651bed src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 23:08:55 2014 +0100 @@ -1761,7 +1761,7 @@ "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory. \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows - that a relator respects reflexivity, left-totality and left_uniqueness. For examples + that a relator respects left-totality and left_uniqueness. For examples see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files in the same directory. The property is used in a reflexivity prover, which is used for discharging respectfulness diff -r 260e18aa306f -r d7f411651bed src/HOL/BNF_GFP.thy --- a/src/HOL/BNF_GFP.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/BNF_GFP.thy Tue Feb 18 23:08:55 2014 +0100 @@ -51,21 +51,6 @@ (* Operators: *) definition image2 where "image2 A f g = {(f a, g a) | a. a \ A}" -lemma Id_onD: "(a, b) \ Id_on A \ a = b" -unfolding Id_on_def by simp - -lemma Id_onD': "x \ Id_on A \ fst x = snd x" -unfolding Id_on_def by auto - -lemma Id_on_fst: "x \ Id_on A \ fst x \ A" -unfolding Id_on_def by auto - -lemma Id_on_UNIV: "Id_on UNIV = Id" -unfolding Id_on_def by auto - -lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A" -unfolding Id_on_def by auto - lemma Id_on_Gr: "Id_on A = Gr A id" unfolding Id_on_def Gr_def by auto @@ -102,9 +87,6 @@ lemma Collect_split_in_rel_leE: "X \ Collect (split (in_rel Y)) \ (X \ Y \ R) \ R" by force -lemma Collect_split_in_relI: "x \ X \ x \ Collect (split (in_rel X))" -by auto - lemma conversep_in_rel: "(in_rel R)\\ = in_rel (R\)" unfolding fun_eq_iff by auto @@ -114,9 +96,6 @@ lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" unfolding Gr_def Grp_def fun_eq_iff by auto -lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op =" -unfolding fun_eq_iff by auto - definition relImage where "relImage R f \ {(f a1, f a2) | a1 a2. (a1,a2) \ R}" diff -r 260e18aa306f -r d7f411651bed src/HOL/IMP/Abs_Int2_ivl.thy --- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 23:08:55 2014 +0100 @@ -30,8 +30,7 @@ lemma \_ivl_nice: "\_ivl[l,h] = {i. l \ Fin i \ Fin i \ h}" by transfer (simp add: \_rep_def) -lift_definition num_ivl :: "int \ ivl" is "\i. (Fin i, Fin i)" -by(auto simp: eq_ivl_def) +lift_definition num_ivl :: "int \ ivl" is "\i. (Fin i, Fin i)" . lift_definition in_ivl :: "int \ ivl \ bool" is "\i (l,h). l \ Fin i \ Fin i \ h" diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:08:55 2014 +0100 @@ -69,7 +69,7 @@ rcset[Transfer.transferred, unfolded mem_Collect_eq, simp] lift_definition cin :: "'a \ 'a cset \ bool" is "op \" parametric member_transfer - .. + . lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer by (rule countable_empty) lift_definition cinsert :: "'a \ 'a cset \ 'a cset" is insert parametric Lifting_Set.insert_transfer diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/DAList.thy Tue Feb 18 23:08:55 2014 +0100 @@ -39,7 +39,7 @@ subsection {* Primitive operations *} -lift_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" is map_of .. +lift_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" is map_of . lift_definition empty :: "('key, 'value) alist" is "[]" by simp diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/FSet.thy Tue Feb 18 23:08:55 2014 +0100 @@ -34,7 +34,7 @@ lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp lift_definition less_eq_fset :: "'a fset \ 'a fset \ bool" is subset_eq parametric subset_transfer - by simp + . definition less_fset :: "'a fset \ 'a fset \ bool" where "xs < ys \ xs \ ys \ xs \ (ys::'a fset)" @@ -164,7 +164,7 @@ "{|x|}" == "CONST finsert x {||}" lift_definition fmember :: "'a \ 'a fset \ bool" (infix "|\|" 50) is Set.member - parametric member_transfer by simp + parametric member_transfer . abbreviation notin_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" @@ -187,12 +187,12 @@ by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq) -lift_definition fcard :: "'a fset \ nat" is card parametric card_transfer by simp +lift_definition fcard :: "'a fset \ nat" is card parametric card_transfer . lift_definition fimage :: "('a \ 'b) \ 'a fset \ 'b fset" (infixr "|`|" 90) is image parametric image_transfer by simp -lift_definition fthe_elem :: "'a fset \ 'a" is the_elem .. +lift_definition fthe_elem :: "'a fset \ 'a" is the_elem . (* FIXME why is not invariant here unfolded ? *) lift_definition fbind :: "'a fset \ ('a \ 'b fset) \ 'b fset" is Set.bind parametric bind_transfer @@ -202,10 +202,10 @@ by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def) -lift_definition fBall :: "'a fset \ ('a \ bool) \ bool" is Ball parametric Ball_transfer .. -lift_definition fBex :: "'a fset \ ('a \ bool) \ bool" is Bex parametric Bex_transfer .. +lift_definition fBall :: "'a fset \ ('a \ bool) \ bool" is Ball parametric Ball_transfer . +lift_definition fBex :: "'a fset \ ('a \ bool) \ bool" is Bex parametric Bex_transfer . -lift_definition ffold :: "('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" is Finite_Set.fold .. +lift_definition ffold :: "('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" is Finite_Set.fold . subsection {* Transferred lemmas from Set.thy *} @@ -774,7 +774,7 @@ subsubsection {* Relator and predicator properties *} lift_definition fset_rel :: "('a \ 'b \ bool) \ 'a fset \ 'b fset \ bool" is set_rel -parametric set_rel_transfer .. +parametric set_rel_transfer . lemma fset_rel_alt_def: "fset_rel R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) \ (\y. \x. y|\|B \ x|\|A \ R x y))" @@ -837,8 +837,6 @@ by (rename_tac A, rule_tac x="f |`| A" in exI, blast) qed -lemmas reflp_fset_rel[reflexivity_rule] = reflp_set_rel[Transfer.transferred] - lemma right_total_fset_rel[transfer_rule]: "right_total A \ right_total (fset_rel A)" unfolding right_total_def apply transfer diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/FinFun.thy Tue Feb 18 23:08:55 2014 +0100 @@ -411,7 +411,7 @@ qed lift_definition finfun_default :: "'a \f 'b \ 'b" -is "finfun_default_aux" .. +is "finfun_default_aux" . lemma finite_finfun_default: "finite {a. finfun_apply f a \ finfun_default f}" by transfer (erule finite_finfun_default_aux) diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Float.thy Tue Feb 18 23:08:55 2014 +0100 @@ -161,11 +161,11 @@ lift_definition sgn_float :: "float \ float" is sgn by simp declare sgn_float.rep_eq[simp] -lift_definition equal_float :: "float \ float \ bool" is "op = :: real \ real \ bool" .. +lift_definition equal_float :: "float \ float \ bool" is "op = :: real \ real \ bool" . -lift_definition less_eq_float :: "float \ float \ bool" is "op \" .. +lift_definition less_eq_float :: "float \ float \ bool" is "op \" . declare less_eq_float.rep_eq[simp] -lift_definition less_float :: "float \ float \ bool" is "op <" .. +lift_definition less_float :: "float \ float \ bool" is "op <" . declare less_float.rep_eq[simp] instance @@ -466,7 +466,7 @@ by transfer (simp add: sgn_times) hide_fact (open) compute_float_sgn -lift_definition is_float_pos :: "float \ bool" is "op < 0 :: real \ bool" .. +lift_definition is_float_pos :: "float \ bool" is "op < 0 :: real \ bool" . lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \ 0 < m" by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0]) @@ -476,7 +476,7 @@ by transfer (simp add: field_simps) hide_fact (open) compute_float_less -lift_definition is_float_nonneg :: "float \ bool" is "op \ 0 :: real \ bool" .. +lift_definition is_float_nonneg :: "float \ bool" is "op \ 0 :: real \ bool" . lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \ 0 \ m" by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0]) @@ -486,7 +486,7 @@ by transfer (simp add: field_simps) hide_fact (open) compute_float_le -lift_definition is_float_zero :: "float \ bool" is "op = 0 :: real \ bool" by simp +lift_definition is_float_zero :: "float \ bool" is "op = 0 :: real \ bool" . lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \ 0 = m" by transfer (auto simp add: is_float_zero_def) @@ -1533,7 +1533,7 @@ lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)" unfolding nprt_def inf_float_def min_def inf_real_def by auto -lift_definition int_floor_fl :: "float \ int" is floor by simp +lift_definition int_floor_fl :: "float \ int" is floor . lemma compute_int_floor_fl[code]: "int_floor_fl (Float m e) = (if 0 \ e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))" diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Feb 18 23:08:55 2014 +0100 @@ -268,8 +268,8 @@ instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le begin -lift_definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" is "\ A B. (\a. A a \ B a)" -by simp +lift_definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" is "\ A B. (\a. A a \ B a)" . + lemmas mset_le_def = less_eq_multiset_def definition less_multiset :: "'a multiset \ 'a multiset \ bool" where diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Quotient_List.thy Tue Feb 18 23:08:55 2014 +0100 @@ -22,6 +22,16 @@ by (induct xs ys rule: list_induct2') simp_all qed +lemma reflp_list_all2: + assumes "reflp R" + shows "reflp (list_all2 R)" +proof (rule reflpI) + from assms have *: "\xs. R xs xs" by (rule reflpE) + fix xs + show "list_all2 R xs xs" + by (induct xs) (simp_all add: *) +qed + lemma list_symp: assumes "symp R" shows "symp (list_all2 R)" diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Quotient_Option.thy Tue Feb 18 23:08:55 2014 +0100 @@ -22,6 +22,10 @@ map_option.id [id_simps] rel_option_eq [id_simps] +lemma reflp_rel_option: + "reflp R \ reflp (rel_option R)" + unfolding reflp_def split_option_all by simp + lemma option_symp: "symp R \ symp (rel_option R)" unfolding symp_def split_option_all diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 23:08:55 2014 +0100 @@ -26,6 +26,10 @@ "sum_rel (op =) (op =) = (op =)" by (simp add: sum_rel_def fun_eq_iff split: sum.split) +lemma reflp_sum_rel: + "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" + unfolding reflp_def split_sum_all sum_rel_simps by fast + lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" unfolding symp_def split_sum_all sum_rel_simps by fast diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/RBT.thy Tue Feb 18 23:08:55 2014 +0100 @@ -38,8 +38,7 @@ setup_lifting type_definition_rbt print_theorems -lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" -by simp +lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" . lift_definition empty :: "('a\linorder, 'b) rbt" is RBT_Impl.Empty by (simp add: empty_def) @@ -50,29 +49,25 @@ lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_delete" by simp -lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries -by simp +lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries . + +lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys . -lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys -by simp +lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "rbt_bulkload" .. -lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "rbt_bulkload" -by simp - -lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is rbt_map_entry +lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is rbt_map_entry by simp lift_definition map :: "('a \ 'b \ 'c) \ ('a\linorder, 'b) rbt \ ('a, 'c) rbt" is RBT_Impl.map by simp -lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is RBT_Impl.fold -by simp +lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is RBT_Impl.fold . lift_definition union :: "('a\linorder, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_union" by (simp add: rbt_union_is_rbt) lift_definition foldi :: "('c \ bool) \ ('a \ 'b \ 'c \ 'c) \ ('a :: linorder, 'b) rbt \ 'c \ 'c" - is RBT_Impl.foldi by simp + is RBT_Impl.foldi . subsection {* Derived operations *} diff -r 260e18aa306f -r d7f411651bed src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Library/RBT_Set.thy Tue Feb 18 23:08:55 2014 +0100 @@ -423,7 +423,7 @@ (** abstract **) lift_definition fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) rbt \ 'a" - is rbt_fold1_keys by simp + is rbt_fold1_keys . lemma fold1_keys_def_alt: "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))" @@ -441,9 +441,9 @@ (* minimum *) -lift_definition r_min :: "('a :: linorder, unit) rbt \ 'a" is rbt_min by simp +lift_definition r_min :: "('a :: linorder, unit) rbt \ 'a" is rbt_min . -lift_definition r_min_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_min_opt by simp +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_min_opt . lemma r_min_alt_def: "r_min t = fold1_keys min t" by transfer (simp add: rbt_min_def) @@ -479,9 +479,9 @@ (* maximum *) -lift_definition r_max :: "('a :: linorder, unit) rbt \ 'a" is rbt_max by simp +lift_definition r_max :: "('a :: linorder, unit) rbt \ 'a" is rbt_max . -lift_definition r_max_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_max_opt by simp +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_max_opt . lemma r_max_alt_def: "r_max t = fold1_keys max t" by transfer (simp add: rbt_max_def) diff -r 260e18aa306f -r d7f411651bed src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Lifting.thy Tue Feb 18 23:08:55 2014 +0100 @@ -439,39 +439,23 @@ text {* Proving reflexivity *} -definition reflp' :: "('a \ 'a \ bool) \ bool" where "reflp' R \ reflp R" - lemma Quotient_to_left_total: assumes q: "Quotient R Abs Rep T" and r_R: "reflp R" shows "left_total T" using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) -lemma reflp_Quotient_composition: - assumes "left_total R" - assumes "reflp T" - shows "reflp (R OO T OO R\\)" -using assms unfolding reflp_def left_total_def by fast - -lemma reflp_fun1: - assumes "is_equality R" - assumes "reflp' S" - shows "reflp (R ===> S)" -using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast +lemma Quotient_composition_ge_eq: + assumes "left_total T" + assumes "R \ op=" + shows "(T OO R OO T\\) \ op=" +using assms unfolding left_total_def by fast -lemma reflp_fun2: - assumes "is_equality R" - assumes "is_equality S" - shows "reflp (R ===> S)" -using assms unfolding is_equality_def reflp_def fun_rel_def by blast - -lemma is_equality_Quotient_composition: - assumes "is_equality T" - assumes "left_total R" - assumes "left_unique R" - shows "is_equality (R OO T OO R\\)" -using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff -by fastforce +lemma Quotient_composition_le_eq: + assumes "left_unique T" + assumes "R \ op=" + shows "(T OO R OO T\\) \ op=" +using assms unfolding left_unique_def by fast lemma left_total_composition: "left_total R \ left_total S \ left_total (R OO S)" unfolding left_total_def OO_def by fast @@ -479,8 +463,14 @@ lemma left_unique_composition: "left_unique R \ left_unique S \ left_unique (R OO S)" unfolding left_unique_def OO_def by fast -lemma reflp_equality: "reflp (op =)" -by (auto intro: reflpI) +lemma invariant_le_eq: + "invariant P \ op=" unfolding invariant_def by blast + +lemma reflp_ge_eq: + "reflp R \ R \ op=" unfolding reflp_def by blast + +lemma ge_eq_refl: + "R \ op= \ R x x" by blast text {* Proving a parametrized correspondence relation *} @@ -649,19 +639,10 @@ setup Lifting_Info.setup lemmas [reflexivity_rule] = - reflp_equality reflp_Quotient_composition is_equality_Quotient_composition - left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition - left_unique_composition - -text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML - because we don't want to get reflp' variant of these theorems *} - -setup{* -Context.theory_map - (fold - (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) - [@{thm reflp_fun1}, @{thm reflp_fun2}]) -*} + order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq + Quotient_composition_ge_eq + left_total_eq left_unique_eq left_total_composition left_unique_composition + left_total_fun left_unique_fun (* setup for the function type *) declare fun_quotient[quot_map] @@ -674,6 +655,6 @@ ML_file "Tools/Lifting/lifting_setup.ML" -hide_const (open) invariant POS NEG reflp' +hide_const (open) invariant POS NEG end diff -r 260e18aa306f -r d7f411651bed src/HOL/Lifting_Option.thy --- a/src/HOL/Lifting_Option.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Lifting_Option.thy Tue Feb 18 23:08:55 2014 +0100 @@ -39,10 +39,6 @@ using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def] by (auto iff: fun_eq_iff split: option.split) -lemma reflp_rel_option[reflexivity_rule]: - "reflp R \ reflp (rel_option R)" - unfolding reflp_def split_option_all by simp - lemma left_total_rel_option[reflexivity_rule]: "left_total R \ left_total (rel_option R)" unfolding left_total_def split_option_all split_option_ex by simp diff -r 260e18aa306f -r d7f411651bed src/HOL/Lifting_Product.thy --- a/src/HOL/Lifting_Product.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Lifting_Product.thy Tue Feb 18 23:08:55 2014 +0100 @@ -30,12 +30,6 @@ shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)" using assms unfolding prod_rel_def prod_pred_def by blast -lemma reflp_prod_rel [reflexivity_rule]: - assumes "reflp R1" - assumes "reflp R2" - shows "reflp (prod_rel R1 R2)" -using assms by (auto intro!: reflpI elim: reflpE) - lemma left_total_prod_rel [reflexivity_rule]: assumes "left_total R1" assumes "left_total R2" diff -r 260e18aa306f -r d7f411651bed src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Lifting_Set.thy Tue Feb 18 23:08:55 2014 +0100 @@ -54,9 +54,6 @@ apply (rename_tac A, rule_tac x="{y. \x\A. T x y}" in exI, fast) done -lemma reflp_set_rel[reflexivity_rule]: "reflp R \ reflp (set_rel R)" - unfolding reflp_def set_rel_def by fast - lemma left_total_set_rel[reflexivity_rule]: "left_total A \ left_total (set_rel A)" unfolding left_total_def set_rel_def diff -r 260e18aa306f -r d7f411651bed src/HOL/Lifting_Sum.thy --- a/src/HOL/Lifting_Sum.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Lifting_Sum.thy Tue Feb 18 23:08:55 2014 +0100 @@ -26,10 +26,6 @@ using assms by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split) -lemma reflp_sum_rel[reflexivity_rule]: - "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" - unfolding reflp_def split_sum_all sum_rel_simps by fast - lemma left_total_sum_rel[reflexivity_rule]: "left_total R1 \ left_total R2 \ left_total (sum_rel R1 R2)" using assms unfolding left_total_def split_sum_all split_sum_ex by simp diff -r 260e18aa306f -r d7f411651bed src/HOL/List.thy --- a/src/HOL/List.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/List.thy Tue Feb 18 23:08:55 2014 +0100 @@ -6582,16 +6582,6 @@ by (auto iff: fun_eq_iff) qed -lemma reflp_list_all2[reflexivity_rule]: - assumes "reflp R" - shows "reflp (list_all2 R)" -proof (rule reflpI) - from assms have *: "\xs. R xs xs" by (rule reflpE) - fix xs - show "list_all2 R xs xs" - by (induct xs) (simp_all add: *) -qed - lemma left_total_list_all2[reflexivity_rule]: "left_total R \ left_total (list_all2 R)" unfolding left_total_def diff -r 260e18aa306f -r d7f411651bed src/HOL/Predicate_Compile.thy --- a/src/HOL/Predicate_Compile.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Predicate_Compile.thy Tue Feb 18 23:08:55 2014 +0100 @@ -81,6 +81,7 @@ Core_Data.PredData.map (Graph.new_node (@{const_name contains}, Core_Data.PredData { + pos = Position.thread_data (), intros = [(NONE, @{thm containsI})], elim = SOME @{thm containsE}, preprocessed = true, diff -r 260e18aa306f -r d7f411651bed src/HOL/Quotient_Examples/Lift_DList.thy --- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 23:08:55 2014 +0100 @@ -35,20 +35,15 @@ text {* Derived operations: *} -lift_definition null :: "'a dlist \ bool" is List.null -by simp +lift_definition null :: "'a dlist \ bool" is List.null . -lift_definition member :: "'a dlist \ 'a \ bool" is List.member -by simp +lift_definition member :: "'a dlist \ 'a \ bool" is List.member . -lift_definition length :: "'a dlist \ nat" is List.length -by simp +lift_definition length :: "'a dlist \ nat" is List.length . -lift_definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.fold -by simp +lift_definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.fold . -lift_definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.foldr -by simp +lift_definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.foldr . lift_definition concat :: "'a dlist dlist \ 'a dlist" is "remdups o List.concat" proof - diff -r 260e18aa306f -r d7f411651bed src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Feb 18 23:08:55 2014 +0100 @@ -31,7 +31,7 @@ let fun intro_reflp_tac (ct, i) = let - val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD} + val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm ge_eq_refl} val concl_pat = Drule.strip_imp_concl (cprop_of rule) val insts = Thm.first_order_match (concl_pat, ct) in diff -r 260e18aa306f -r d7f411651bed src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Feb 18 23:08:55 2014 +0100 @@ -28,7 +28,6 @@ val get_invariant_commute_rules: Proof.context -> thm list val get_reflexivity_rules: Proof.context -> thm list - val add_reflexivity_rule_raw_attribute: attribute val add_reflexivity_rule_attribute: attribute type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, @@ -276,33 +275,14 @@ (* info about reflexivity rules *) fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) - -(* Conversion to create a reflp' variant of a reflexivity rule *) -fun safe_reflp_conv ct = - Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct - -fun prep_reflp_conv ct = ( - Conv.implies_conv safe_reflp_conv prep_reflp_conv - else_conv - safe_reflp_conv - else_conv - Conv.all_conv) ct - -fun add_reflexivity_rule_raw thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) -val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw - -fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #> - add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm) +fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule - val relfexivity_rule_setup = let val name = @{binding reflexivity_rule} - fun del_thm_raw thm = Data.map (map_reflexivity_rules (Item_Net.remove thm)) - fun del_thm thm = del_thm_raw thm #> - del_thm_raw (Conv.fconv_rule prep_reflp_conv thm) + fun del_thm thm = Data.map (map_reflexivity_rules (Item_Net.remove thm)) val del = Thm.declaration_attribute del_thm val text = "rules that are used to prove that a relation is reflexive" val content = Item_Net.content o get_reflexivity_rules' @@ -370,19 +350,42 @@ Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule end; +fun add_reflexivity_rules mono_rule ctxt = + let + fun find_eq_rule thm ctxt = + let + val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o concl_of) thm; + val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs; + in + find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules + end + + val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt); + val eq_rule = if is_some eq_rule then the eq_rule else error + "No corresponding rule that the relator preserves equality was found." + in + ctxt + |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) + |> add_reflexivity_rule + (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule])) + end + fun add_mono_rule mono_rule ctxt = let - val mono_rule = introduce_polarities mono_rule + val pol_mono_rule = introduce_polarities mono_rule val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o - dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule + dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) pol_mono_rule val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") else () - val neg_mono_rule = negate_mono_rule mono_rule - val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, + val neg_mono_rule = negate_mono_rule pol_mono_rule + val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, pos_distr_rules = [], neg_distr_rules = []} in - Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt + ctxt + |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) + |> add_reflexivity_rules mono_rule end; local diff -r 260e18aa306f -r d7f411651bed src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Feb 18 23:08:55 2014 +0100 @@ -252,7 +252,7 @@ val lthy = case opt_reflp_thm of SOME reflp_thm => lthy |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), - [reflp_thm]) + [reflp_thm RS @{thm reflp_ge_eq}]) |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}]) |> define_code_constr gen_code quot_thm diff -r 260e18aa306f -r d7f411651bed src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 18 23:08:55 2014 +0100 @@ -18,6 +18,7 @@ }; datatype pred_data = PredData of { + pos : Position.T, intros : (string option * thm) list, elim : thm option, preprocessed : bool, @@ -100,6 +101,7 @@ PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro} datatype pred_data = PredData of { + pos: Position.T, intros : (string option * thm) list, elim : thm option, preprocessed : bool, @@ -109,13 +111,17 @@ }; fun rep_pred_data (PredData data) = data; +val pos_of = #pos o rep_pred_data; -fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) = - PredData {intros = intros, elim = elim, preprocessed = preprocessed, +fun mk_pred_data + (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) = + PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed, function_names = function_names, predfun_data = predfun_data, needs_random = needs_random} -fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) = - mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) +fun map_pred_data f + (PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) = + mk_pred_data + (f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))) fun eq_option eq (NONE, NONE) = true | eq_option eq (SOME x, SOME y) = eq (x, y) @@ -130,7 +136,13 @@ type T = pred_data Graph.T; val empty = Graph.empty; val extend = I; - val merge = Graph.merge eq_pred_data; + val merge = + Graph.join (fn key => fn (x, y) => + if eq_pred_data (x, y) + then raise Graph.SAME + else + error ("Duplicate predicate declarations for " ^ quote key ^ + Position.here (pos_of x) ^ Position.here (pos_of y))); ); @@ -260,11 +272,13 @@ (case try (Inductive.the_inductive ctxt) name of SOME (info as (_, result)) => let + val thy = Proof_Context.theory_of ctxt + + val pos = Position.thread_data () fun is_intro_of intro = let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val thy = Proof_Context.theory_of ctxt val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index @@ -273,13 +287,13 @@ val nparams = length (Inductive.params_of (#raw_induct result)) val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t in - mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation) + mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation)) end | NONE => error ("No such predicate: " ^ quote name)) fun add_predfun_data name mode data = let - val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) + val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) in PredData.map (Graph.map_node name (map_pred_data add)) end fun is_inductive_predicate ctxt name = @@ -305,17 +319,21 @@ (case try (Graph.get_node gr) name of SOME _ => Graph.map_node name (map_pred_data - (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr + (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr | NONE => Graph.new_node - (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr) + (name, + mk_pred_data (Position.thread_data (), + (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr) in PredData.map cons_intro thy end fun set_elim thm = let val (name, _) = dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) - in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end + in + PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm)))))))) + end fun register_predicate (constname, intros, elim) thy = let @@ -324,7 +342,8 @@ if not (member (op =) (Graph.keys (PredData.get thy)) constname) then PredData.map (Graph.new_node (constname, - mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy + mk_pred_data (Position.thread_data (), + (((named_intros, SOME elim), false), no_compilation)))) thy else thy end @@ -345,14 +364,14 @@ fun defined_function_of compilation pred = let - val set = (apsnd o apfst) (cons (compilation, [])) + val set = (apsnd o apsnd o apfst) (cons (compilation, [])) in PredData.map (Graph.map_node pred (map_pred_data set)) end fun set_function_name compilation pred mode name = let - val set = (apsnd o apfst) + val set = (apsnd o apsnd o apfst) (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name))) in PredData.map (Graph.map_node pred (map_pred_data set)) @@ -360,7 +379,7 @@ fun set_needs_random name modes = let - val set = (apsnd o apsnd o apsnd) (K modes) + val set = (apsnd o apsnd o apsnd o apsnd) (K modes) in PredData.map (Graph.map_node name (map_pred_data set)) end @@ -389,7 +408,7 @@ end fun preprocess_intros name thy = - PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) => + PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) => if preprocessed then (rules, preprocessed) else let @@ -401,7 +420,7 @@ val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t in ((named_intros', SOME elim'), true) - end)))) + end))))) thy @@ -422,7 +441,7 @@ AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode -fun force_modes_and_compilations pred_name compilations = +fun force_modes_and_compilations pred_name compilations thy = let (* thm refl is a dummy thm *) val modes = map fst compilations @@ -435,11 +454,14 @@ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations val alt_compilations = map (apsnd fst) compilations in + thy |> PredData.map (Graph.new_node (pred_name, - mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))) - #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) + mk_pred_data + (Position.thread_data (), + ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))) + |> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) end fun functional_compilation fun_name mode compfuns T = diff -r 260e18aa306f -r d7f411651bed src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Tools/transfer.ML Tue Feb 18 23:08:55 2014 +0100 @@ -12,6 +12,7 @@ val prep_conv: conv val get_transfer_raw: Proof.context -> thm list + val get_relator_eq_item_net: Proof.context -> thm Item_Net.T val get_relator_eq: Proof.context -> thm list val get_sym_relator_eq: Proof.context -> thm list val get_relator_eq_raw: Proof.context -> thm list @@ -40,6 +41,8 @@ (** Theory Data **) val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst); +val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq + o HOLogic.dest_Trueprop o Thm.concl_of); structure Data = Generic_Data ( @@ -56,7 +59,7 @@ known_frees = [], compound_lhs = compound_xhs_empty_net, compound_rhs = compound_xhs_empty_net, - relator_eq = Thm.full_rules, + relator_eq = rewr_rules, relator_eq_raw = Thm.full_rules, relator_domain = Thm.full_rules } val extend = I @@ -90,6 +93,8 @@ fun get_compound_rhs ctxt = ctxt |> (#compound_rhs o Data.get o Context.Proof) +fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt + fun get_relator_eq ctxt = ctxt |> (Item_Net.content o #relator_eq o Data.get o Context.Proof) |> map safe_mk_meta_eq diff -r 260e18aa306f -r d7f411651bed src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Feb 18 17:52:28 2014 +0100 +++ b/src/HOL/Topological_Spaces.thy Tue Feb 18 23:08:55 2014 +0100 @@ -2375,10 +2375,6 @@ unfolding filter_rel_eventually[abs_def] by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) -lemma reflp_filter_rel [reflexivity_rule]: "reflp R \ reflp (filter_rel R)" -unfolding filter_rel_eventually[abs_def] -by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD) - lemma filter_rel_conversep [simp]: "filter_rel A\\ = (filter_rel A)\\" by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def) diff -r 260e18aa306f -r d7f411651bed src/Pure/General/path.scala --- a/src/Pure/General/path.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/General/path.scala Tue Feb 18 23:08:55 2014 +0100 @@ -94,7 +94,7 @@ else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) - new Path(norm_elems(elems.reverse ++ roots)) + new Path(norm_elems(elems.reverse ::: roots)) } def is_ok(str: String): Boolean = diff -r 260e18aa306f -r d7f411651bed src/Pure/General/position.ML --- a/src/Pure/General/position.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/General/position.ML Tue Feb 18 23:08:55 2014 +0100 @@ -192,7 +192,7 @@ (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")" | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")" | (NONE, SOME name) => "(file " ^ quote name ^ ")" - | _ => ""); + | _ => if is_reported pos then "\\" else ""); in if null props then "" else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s diff -r 260e18aa306f -r d7f411651bed src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/General/position.scala Tue Feb 18 23:08:55 2014 +0100 @@ -50,7 +50,7 @@ object Range { - def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) + def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop) def unapply(pos: T): Option[Text.Range] = (pos, pos) match { case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop)) diff -r 260e18aa306f -r d7f411651bed src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/General/pretty.scala Tue Feb 18 23:08:55 2014 +0100 @@ -45,12 +45,11 @@ object Block { def apply(i: Int, body: XML.Body): XML.Tree = - XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) + XML.Elem(Markup.Block(i), body) def unapply(tree: XML.Tree): Option[(Int, XML.Body)] = tree match { - case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => - Some((i, body)) + case XML.Elem(Markup.Block(i), body) => Some((i, body)) case _ => None } } @@ -58,12 +57,11 @@ object Break { def apply(w: Int): XML.Tree = - XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), - List(XML.Text(spaces(w)))) + XML.Elem(Markup.Break(w), List(XML.Text(spaces(w)))) def unapply(tree: XML.Tree): Option[Int] = tree match { - case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w) + case XML.Elem(Markup.Break(w), _) => Some(w) case _ => None } } diff -r 260e18aa306f -r d7f411651bed src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Tue Feb 18 23:08:55 2014 +0100 @@ -300,7 +300,7 @@ fun read pos txt = let - val _ = Position.report pos Markup.ML_source; + val _ = Position.report pos Markup.language_ML; val syms = Symbol_Pos.explode (txt, pos); val termination = if null syms then [] diff -r 260e18aa306f -r d7f411651bed src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/PIDE/command.scala Tue Feb 18 23:08:55 2014 +0100 @@ -108,19 +108,17 @@ if id == command.id || id == alt_id => command.chunks.get(file_name) match { case Some(chunk) => - val range = chunk.decode(raw_range) - if (chunk.range.contains(range)) { - val props = Position.purge(atts) - val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(file_name, info) + chunk.decode(raw_range).try_restrict(chunk.range) match { + case Some(range) => + if (!range.is_singularity) { + val props = Position.purge(atts) + state.add_markup(file_name, + Text.Info(range, XML.Elem(Markup(name, props), args))) + } + else state + case None => bad(); state } - else { - bad() - state - } - case None => - bad() - state + case None => bad(); state } case XML.Elem(Markup(name, atts), args) @@ -130,9 +128,7 @@ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) state.add_markup("", info) - case _ => - // FIXME bad() - state + case _ => /* FIXME bad(); */ state } }) case XML.Elem(Markup(name, props), body) => diff -r 260e18aa306f -r d7f411651bed src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Feb 18 23:08:55 2014 +0100 @@ -20,6 +20,14 @@ val name: string -> T -> T val kindN: string val instanceN: string + val languageN: string val language: string -> T + val language_sort: T + val language_type: T + val language_term: T + val language_prop: T + val language_ML: T + val language_document: T + val language_text: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val get_entity_kind: T -> string option @@ -62,10 +70,6 @@ val inner_cartoucheN: string val inner_cartouche: T val inner_commentN: string val inner_comment: T val token_rangeN: string val token_range: T - val sortN: string val sort: T - val typN: string val typ: T - val termN: string val term: T - val propN: string val prop: T val sortingN: string val sorting: T val typingN: string val typing: T val ML_keyword1N: string val ML_keyword1: T @@ -81,8 +85,6 @@ val ML_openN: string val ML_structN: string val ML_typingN: string val ML_typing: T - val ML_sourceN: string val ML_source: T - val document_sourceN: string val document_source: T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val ML_antiquotationN: string @@ -163,6 +165,12 @@ val command_timing: Properties.entry val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option + val simp_trace_logN: string + val simp_trace_stepN: string + val simp_trace_recurseN: string + val simp_trace_hintN: string + val simp_trace_ignoreN: string + val simp_trace_cancel: serial -> Properties.T val no_output: Output.output * Output.output val default_output: T -> Output.output * Output.output val add_mode: string -> (T -> Output.output * Output.output) -> unit @@ -220,9 +228,9 @@ fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); -fun markup_elem elem = (elem, (elem, []): T); -fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T); -fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T); +fun markup_elem name = (name, (name, []): T); +fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); +fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T); (* misc properties *) @@ -235,6 +243,20 @@ val instanceN = "instance"; +(* embedded languages *) + +val (languageN, language) = markup_string "language" nameN; + +val language_sort = language "sort"; +val language_type = language "type"; +val language_term = language "term"; +val language_prop = language "prop"; + +val language_ML = language "ML"; +val language_document = language "document"; +val language_text = language "text"; + + (* formal entities *) val (bindingN, binding) = markup_elem "binding"; @@ -317,11 +339,6 @@ val (token_rangeN, token_range) = markup_elem "token_range"; -val (sortN, sort) = markup_elem "sort"; -val (typN, typ) = markup_elem "typ"; -val (termN, term) = markup_elem "term"; -val (propN, prop) = markup_elem "prop"; - val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; @@ -344,10 +361,7 @@ val (ML_typingN, ML_typing) = markup_elem "ML_typing"; -(* embedded source text *) - -val (ML_sourceN, ML_source) = markup_elem "ML_source"; -val (document_sourceN, document_source) = markup_elem "document_source"; +(* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; @@ -510,6 +524,16 @@ | dest_loading_theory _ = NONE; +(* simplifier trace *) + +val simp_trace_logN = "simp_trace_log"; +val simp_trace_stepN = "simp_trace_step"; +val simp_trace_recurseN = "simp_trace_recurse"; +val simp_trace_hintN = "simp_trace_hint"; +val simp_trace_ignoreN = "simp_trace_ignore"; + +fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)]; + (** print mode operations **) diff -r 260e18aa306f -r d7f411651bed src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Feb 18 23:08:55 2014 +0100 @@ -27,6 +27,24 @@ val Empty = Markup("", Nil) val Broken = Markup("broken", Nil) + class Markup_String(val name: String, prop: String) + { + private val Prop = new Properties.String(prop) + + def apply(s: String): Markup = Markup(name, Prop(s)) + def unapply(markup: Markup): Option[String] = + if (markup.name == name) Prop.unapply(markup.properties) else None + } + + class Markup_Int(val name: String, prop: String) + { + private val Prop = new Properties.Int(prop) + + def apply(i: Int): Markup = Markup(name, Prop(i)) + def unapply(markup: Markup): Option[Int] = + if (markup.name == name) Prop.unapply(markup.properties) else None + } + /* formal entities */ @@ -39,9 +57,9 @@ { def unapply(markup: Markup): Option[(String, String)] = markup match { - case Markup(ENTITY, props @ Kind(kind)) => - props match { - case Name(name) => Some(kind, name) + case Markup(ENTITY, props) => + (props, props) match { + case (Kind(kind), Name(name)) => Some(kind, name) case _ => None } case _ => None @@ -67,38 +85,25 @@ val POSITION = "position" + /* embedded languages */ + + val LANGUAGE = "language" + val Language = new Markup_String(LANGUAGE, NAME) + + /* external resources */ val PATH = "path" - - object Path - { - def unapply(markup: Markup): Option[String] = - markup match { - case Markup(PATH, Name(name)) => Some(name) - case _ => None - } - } + val Path = new Markup_String(PATH, NAME) val URL = "url" - - object Url - { - def unapply(markup: Markup): Option[String] = - markup match { - case Markup(URL, Name(name)) => Some(name) - case _ => None - } - } + val Url = new Markup_String(URL, NAME) /* pretty printing */ - val Indent = new Properties.Int("indent") - val BLOCK = "block" - - val Width = new Properties.Int("width") - val BREAK = "break" + val Block = new Markup_Int("block", "indent") + val Break = new Markup_Int("break", "width") val ITEM = "item" val BULLET = "bullet" @@ -138,11 +143,6 @@ val TOKEN_RANGE = "token_range" - val SORT = "sort" - val TYP = "typ" - val TERM = "term" - val PROP = "prop" - val SORTING = "sorting" val TYPING = "typing" @@ -150,10 +150,7 @@ val METHOD = "method" - /* embedded source text */ - - val ML_SOURCE = "ML_source" - val DOCUMENT_SOURCE = "document_source" + /* antiquotations */ val ANTIQUOTED = "antiquoted" val ANTIQUOTE = "antiquote" @@ -392,82 +389,26 @@ } } + /* simplifier trace */ - val TEXT = "text" - val Text = new Properties.String(TEXT) - - val PARENT = "parent" - val Parent = new Properties.Long(PARENT) + val SIMP_TRACE = "simp_trace" - val SUCCESS = "success" - val Success = new Properties.Boolean(SUCCESS) + val SIMP_TRACE_LOG = "simp_trace_log" + val SIMP_TRACE_STEP = "simp_trace_step" + val SIMP_TRACE_RECURSE = "simp_trace_recurse" + val SIMP_TRACE_HINT = "simp_trace_hint" + val SIMP_TRACE_IGNORE = "simp_trace_ignore" - val MEMORY = "memory" - val Memory = new Properties.Boolean(MEMORY) - - val CANCEL_SIMP_TRACE = "simp_trace_cancel" - object Cancel_Simp_Trace + val SIMP_TRACE_CANCEL = "simp_trace_cancel" + object Simp_Trace_Cancel { def unapply(props: Properties.T): Option[Long] = props match { - case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id) + case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i) case _ => None } } - - val SIMP_TRACE = "simp_trace" - object Simp_Trace - { - def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] = - tree match { - case XML.Elem(Markup(SIMP_TRACE, props), _) => - (props, props) match { - case (Serial(serial), Name(name)) => - Simplifier_Trace.all_answers.find(_.name == name).map((serial, _)) - case _ => - None - } - case _ => - None - } - } - - /* trace items from the prover */ - - object Simp_Trace_Item - { - - def unapply(tree: XML.Tree): Option[(String, Data)] = - tree match { - case XML.Elem(Markup(RESULT, Serial(serial)), List( - XML.Elem(Markup(markup, props), content) - )) if markup.startsWith("simp_trace_") => - (props, props) match { - case (Text(text), Parent(parent)) => - Some((markup, Data(serial, markup, text, parent, props, content))) - case _ => - None - } - case _ => - None - } - - val LOG = "simp_trace_log" - val STEP = "simp_trace_step" - val RECURSE = "simp_trace_recurse" - val HINT = "simp_trace_hint" - val IGNORE = "simp_trace_ignore" - - case class Data(serial: Long, markup: String, text: String, - parent: Long, props: Properties.T, content: XML.Body) - { - def memory: Boolean = - Memory.unapply(props) getOrElse true - } - - } - } diff -r 260e18aa306f -r d7f411651bed src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/PIDE/protocol.scala Tue Feb 18 23:08:55 2014 +0100 @@ -282,10 +282,12 @@ { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { - case Position.Reported(id, file_name, range) + case Position.Reported(id, file_name, raw_range) if (id == command_id || id == alt_id) && file_name == chunk.file_name => - val range1 = chunk.decode(range).restrict(chunk.range) - if (range1.is_singularity) set else set + range1 + chunk.decode(raw_range).try_restrict(chunk.range) match { + case Some(range) if !range.is_singularity => set + range + case _ => set + } case _ => set } diff -r 260e18aa306f -r d7f411651bed src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/PIDE/yxml.scala Tue Feb 18 23:08:55 2014 +0100 @@ -33,7 +33,7 @@ def tree(t: XML.Tree): Unit = t match { case XML.Elem(Markup(name, atts), ts) => - s += X; s += Y; s++= name; atts.foreach(attrib); s += X + s += X; s += Y; s ++= name; atts.foreach(attrib); s += X ts.foreach(tree) s += X; s += Y; s += X case XML.Text(text) => s ++= text @@ -120,7 +120,7 @@ /* failsafe parsing */ private def markup_broken(source: CharSequence) = - XML.elem(Markup.Broken.name, List(XML.Text(source.toString))) + XML.Elem(Markup.Broken, List(XML.Text(source.toString))) def parse_body_failsafe(source: CharSequence): XML.Body = { diff -r 260e18aa306f -r d7f411651bed src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Feb 18 23:08:55 2014 +0100 @@ -342,7 +342,7 @@ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); fun parse_sort ctxt = - Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort + Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort (fn (syms, pos) => parse_tree ctxt "sort" (syms, pos) |> uncurry (report_result ctxt pos) @@ -351,7 +351,7 @@ handle ERROR msg => parse_failed ctxt pos msg "sort"); fun parse_typ ctxt = - Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ + Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type (fn (syms, pos) => parse_tree ctxt "type" (syms, pos) |> uncurry (report_result ctxt pos) @@ -362,8 +362,8 @@ let val (markup, kind, root, constrain) = if is_prop - then (Markup.prop, "proposition", "prop", Type.constraint propT) - else (Markup.term, "term", Config.get ctxt Syntax.root, I); + then (Markup.language_prop, "prop", "prop", Type.constraint propT) + else (Markup.language_term, "term", Config.get ctxt Syntax.root, I); val decode = constrain o Term_XML.Decode.term; in Syntax.parse_token ctxt decode markup @@ -749,8 +749,8 @@ in -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort; -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ; +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort; +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type; fun unparse_term ctxt = let @@ -760,7 +760,7 @@ in unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn)) (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) - Markup.term ctxt + Markup.language_term ctxt end; end; diff -r 260e18aa306f -r d7f411651bed src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/System/isabelle_system.scala Tue Feb 18 23:08:55 2014 +0100 @@ -267,7 +267,7 @@ def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = { val cmdline = - if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args + if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList else args val env1 = if (env == null) settings else settings ++ env raw_execute(cwd, env1, redirect, cmdline: _*) @@ -283,7 +283,7 @@ { private val params = List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script") - private val proc = execute_env(cwd, env, redirect, (params ++ args):_*) + private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*) // channels @@ -414,7 +414,7 @@ } match { case Some(dir) => val file = standard_path(dir + Path.basic(name)) - process_output(execute(true, (List(file) ++ args): _*)) + process_output(execute(true, (List(file) ::: args.toList): _*)) case None => ("Unknown Isabelle tool: " + name, 2) } } diff -r 260e18aa306f -r d7f411651bed src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Feb 18 23:08:55 2014 +0100 @@ -188,7 +188,7 @@ fun check_text (txt, pos) state = - (Position.report pos Markup.document_source; + (Position.report pos Markup.language_document; if Toplevel.is_skipped_proof state then () else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); @@ -470,6 +470,9 @@ fun pretty_text ctxt = Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines; +fun pretty_text_report ctxt (s, pos) = + (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s); + fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; @@ -574,7 +577,7 @@ basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #> basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #> basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #> - basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #> + basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #> basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #> basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #> basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory); diff -r 260e18aa306f -r d7f411651bed src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 23:08:55 2014 +0100 @@ -13,7 +13,7 @@ structure Simplifier_Trace: SIMPLIFIER_TRACE = struct -(** background data **) +(** context data **) datatype mode = Disabled | Normal | Full @@ -23,7 +23,7 @@ | merge_modes Full _ = Full val empty_breakpoints = - (Item_Net.init (op =) single (* FIXME equality on terms? *), + (Item_Net.init (op aconv) single, Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = @@ -49,10 +49,11 @@ parent = 0, breakpoints = empty_breakpoints} val extend = I - fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, - memory = memory1, breakpoints = breakpoints1, ...}: T, - {max_depth = max_depth2, mode = mode2, interactive = interactive2, - memory = memory2, breakpoints = breakpoints2, ...}: T) = + fun merge + ({max_depth = max_depth1, mode = mode1, interactive = interactive1, + memory = memory1, breakpoints = breakpoints1, ...}: T, + {max_depth = max_depth2, mode = mode2, interactive = interactive2, + memory = memory2, breakpoints = breakpoints2, ...}: T) = {max_depth = Int.max (max_depth1, max_depth2), depth = 0, mode = merge_modes mode1 mode2, @@ -97,14 +98,17 @@ (term_matches, thm_matches) end + + (** config and attributes **) fun config raw_mode interactive max_depth memory = let - val mode = case raw_mode of - "normal" => Normal - | "full" => Full - | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode) + val mode = + (case raw_mode of + "normal" => Normal + | "full" => Full + | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)) val update = Data.map (fn {depth, parent, breakpoints, ...} => {max_depth = max_depth, @@ -122,11 +126,15 @@ val thm_breakpoint = Thm.declaration_attribute add_thm_breakpoint + + (** tracing state **) val futures = Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) + + (** markup **) fun output_result (id, data) = @@ -138,14 +146,6 @@ val memoryN = "memory" val successN = "success" -val logN = "simp_trace_log" -val stepN = "simp_trace_step" -val recurseN = "simp_trace_recurse" -val hintN = "simp_trace_hint" -val ignoreN = "simp_trace_ignore" - -val cancelN = "simp_trace_cancel" - type payload = {props: Properties.T, pretty: Pretty.T} @@ -158,15 +158,17 @@ val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt) val eligible = - case mode of + (case mode of Disabled => false | Normal => triggered - | Full => true + | Full => true) - val markup' = if markup = stepN andalso not interactive then logN else markup + val markup' = + if markup = Markup.simp_trace_stepN andalso not interactive + then Markup.simp_trace_logN + else markup in - if not eligible orelse depth > max_depth then - NONE + if not eligible orelse depth > max_depth then NONE else let val {props = more_props, pretty} = payload () @@ -181,15 +183,14 @@ end end + + (** tracing output **) fun send_request (result_id, content) = let fun break () = - (Output.protocol_message - [(Markup.functionN, cancelN), - (serialN, Markup.print_int result_id)] - ""; + (Output.protocol_message (Markup.simp_trace_cancel result_id) ""; Synchronized.change futures (Inttab.delete_safe result_id)) val promise = Future.promise break : string future in @@ -209,10 +210,8 @@ val term_triggered = not (null matching_terms) val text = - if unconditional then - "Apply rewrite rule?" - else - "Apply conditional rewrite rule?" + if unconditional then "Apply rewrite rule?" + else "Apply conditional rewrite rule?" fun payload () = let @@ -233,8 +232,7 @@ in if not (null matching_terms) then [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] - else - [] + else [] end val pretty = @@ -269,14 +267,14 @@ in if not interactive then (output_result result; Future.value (SOME (put mode false))) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of + (case mk_generic_result Markup.simp_trace_stepN text + (thm_triggered orelse term_triggered) payload ctxt of NONE => Future.value (SOME ctxt) - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun recurse text term ctxt = @@ -298,11 +296,9 @@ breakpoints = breakpoints} (Context.Proof ctxt) val context' = - case mk_generic_result recurseN text true payload ctxt of - NONE => - put 0 - | SOME res => - (output_result res; put (#1 res)) + (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of + NONE => put 0 + | SOME res => (output_result res; put (#1 res))) in Context.the_proof context' end fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = @@ -336,24 +332,21 @@ let val result_id = #1 result - fun to_response "exit" = - false + fun to_response "exit" = false | to_response "redo" = (Option.app output_result - (mk_generic_result ignoreN "Ignore" true empty_payload ctxt'); + (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt'); true) - | to_response _ = - raise Fail "Simplifier_Trace.indicate_failure: invalid message" + | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message" in if not interactive then (output_result result; Future.value false) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result hintN "Step failed" true payload ctxt' of + (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of NONE => Future.value false - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun indicate_success thm ctxt = @@ -362,9 +355,12 @@ {props = [(successN, "true")], pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} in - Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt) + Option.app output_result + (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt) end + + (** setup **) fun simp_apply args ctxt cont = @@ -377,21 +373,17 @@ thm = thm, rrule = rrule} in - case Future.join (step data) of - NONE => - NONE + (case Future.join (step data) of + NONE => NONE | SOME ctxt' => let val res = cont ctxt' in - case res of + (case res of NONE => if Future.join (indicate_failure data ctxt') then simp_apply args ctxt cont - else - NONE - | SOME (thm, _) => - (indicate_success thm ctxt'; - res) - end + else NONE + | SOME (thm, _) => (indicate_success thm ctxt'; res)) + end) end val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" @@ -402,7 +394,7 @@ trace_apply = simp_apply}) val _ = - Isabelle_Process.protocol_command "Document.simp_trace_reply" + Isabelle_Process.protocol_command "Simplifier_Trace.reply" (fn [s, r] => let val serial = Markup.parse_int s @@ -415,20 +407,19 @@ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn end) + + (** attributes **) -val pat_parser = - Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic - -val mode_parser: string parser = +val mode_parser = Scan.optional (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) "normal" -val interactive_parser: bool parser = +val interactive_parser = Scan.optional (Args.$$$ "interactive" >> K true) false -val memory_parser: bool parser = +val memory_parser = Scan.optional (Args.$$$ "no_memory" >> K false) true val depth_parser = @@ -440,7 +431,7 @@ val _ = Theory.setup (Attrib.setup @{binding break_term} - ((Scan.repeat1 pat_parser) >> term_breakpoint) + (Scan.repeat1 Args.term_pattern >> term_breakpoint) "declaration of a term breakpoint" #> Attrib.setup @{binding break_thm} (Scan.succeed thm_breakpoint) diff -r 260e18aa306f -r d7f411651bed src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Feb 18 23:08:55 2014 +0100 @@ -6,6 +6,7 @@ package isabelle + import scala.actors.Actor._ import scala.annotation.tailrec import scala.collection.immutable.SortedMap @@ -13,8 +14,42 @@ object Simplifier_Trace { + /* trace items from the prover */ - import Markup.Simp_Trace_Item + val TEXT = "text" + val Text = new Properties.String(TEXT) + + val PARENT = "parent" + val Parent = new Properties.Long(PARENT) + + val SUCCESS = "success" + val Success = new Properties.Boolean(SUCCESS) + + val MEMORY = "memory" + val Memory = new Properties.Boolean(MEMORY) + + object Item + { + case class Data( + serial: Long, markup: String, text: String, + parent: Long, props: Properties.T, content: XML.Body) + { + def memory: Boolean = Memory.unapply(props) getOrElse true + } + + def unapply(tree: XML.Tree): Option[(String, Data)] = + tree match { + case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), + List(XML.Elem(Markup(markup, props), content))) + if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants + (props, props) match { + case (Text(text), Parent(parent)) => + Some((markup, Data(serial, markup, text, parent, props, content))) + case _ => None + } + case _ => None + } + } /* replies to the prover */ @@ -23,7 +58,6 @@ object Answer { - object step { val skip = Answer("skip", "Skip") @@ -44,10 +78,23 @@ val default = exit val all = List(redo, exit) } - } - val all_answers = Answer.step.all ++ Answer.hint_fail.all + val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all + + object Active + { + def unapply(tree: XML.Tree): Option[(Long, Answer)] = + tree match { + case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) => + (props, props) match { + case (Markup.Serial(serial), Markup.Name(name)) => + all_answers.find(_.name == name).map((serial, _)) + case _ => None + } + case _ => None + } + } /* GUI interaction */ @@ -64,7 +111,7 @@ private object Stop case class Reply(session: Session, serial: Long, answer: Answer) - case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer) + case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer) case class Context( last_serial: Long = 0L, @@ -83,13 +130,13 @@ } - case class Trace(entries: List[Simp_Trace_Item.Data]) + case class Trace(entries: List[Item.Data]) case class Index(text: String, content: XML.Body) object Index { - def of_data(data: Simp_Trace_Item.Data): Index = + def of_data(data: Item.Data): Index = Index(data.text, data.content) } @@ -128,7 +175,7 @@ def do_reply(session: Session, serial: Long, answer: Answer) { - session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name) + session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name) } loop { @@ -140,14 +187,12 @@ for ((serial, result) <- results.entries if serial > new_context.last_serial) { result match { - case Simp_Trace_Item(markup, data) => - import Simp_Trace_Item._ - + case Item(markup, data) => memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) markup match { - case STEP => + case Markup.SIMP_TRACE_STEP => val index = Index.of_data(data) memory.get(index) match { case Some(answer) if data.memory => @@ -156,11 +201,11 @@ new_context += Question(data, Answer.step.all, Answer.step.default) } - case HINT => + case Markup.SIMP_TRACE_HINT => data.props match { - case Markup.Success(false) => + case Success(false) => results.get(data.parent) match { - case Some(Simp_Trace_Item(STEP, _)) => + case Some(Item(Markup.SIMP_TRACE_STEP, _)) => new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default) case _ => // unknown, better send a default reply @@ -169,7 +214,7 @@ case _ => } - case IGNORE => + case Markup.SIMP_TRACE_IGNORE => // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP' // entry, and that that 'STEP' entry is about to be replayed. Hence, we need // to selectively purge the replies which have been memorized, going down from @@ -179,7 +224,7 @@ def purge(queue: Vector[Long]): Unit = queue match { case s +: rest => - for (Simp_Trace_Item(STEP, data) <- results.get(s)) + for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) memory -= Index.of_data(data) val children = memory_children.getOrElse(s, Set.empty) memory_children -= s @@ -208,7 +253,7 @@ // current results. val items = - for { (_, Simp_Trace_Item(_, data)) <- results.entries } + for { (_, Item(_, data)) <- results.entries } yield data reply(Trace(items.toList)) @@ -232,7 +277,7 @@ case Reply(session, serial, answer) => find_question(serial) match { case Some((id, Question(data, _, _))) => - if (data.markup == Markup.Simp_Trace_Item.STEP && data.memory) + if (data.markup == Markup.SIMP_TRACE_STEP && data.memory) { val index = Index.of_data(data) memory += (index -> answer) @@ -256,10 +301,9 @@ class Handler extends Session.Protocol_Handler { - private def cancel( - prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = + private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = msg.properties match { - case Markup.Cancel_Simp_Trace(serial) => + case Markup.Simp_Trace_Cancel(serial) => manager ! Cancel(serial) true case _ => @@ -272,8 +316,6 @@ manager ! Stop } - val functions = Map( - Markup.CANCEL_SIMP_TRACE -> cancel _) + val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _) } - } diff -r 260e18aa306f -r d7f411651bed src/Pure/context.ML --- a/src/Pure/context.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/context.ML Tue Feb 18 23:08:55 2014 +0100 @@ -43,7 +43,6 @@ val this_theory: theory -> string -> theory val eq_thy: theory * theory -> bool val subthy: theory * theory -> bool - val joinable: theory * theory -> bool val merge: theory * theory -> theory val finish_thy: theory -> theory val begin_thy: (theory -> pretty) -> string -> theory list -> theory @@ -246,8 +245,6 @@ fun subthy thys = eq_thy thys orelse proper_subthy thys; -fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); - (* consistent ancestors *) diff -r 260e18aa306f -r d7f411651bed src/Pure/defs.ML --- a/src/Pure/defs.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/defs.ML Tue Feb 18 23:08:55 2014 +0100 @@ -11,7 +11,11 @@ val plain_args: typ list -> bool type T type spec = - {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list} + {def: string option, + description: string, + pos: Position.T, + lhs: typ list, + rhs: (string * typ list) list} val all_specifications_of: T -> (string * spec list) list val specifications_of: T -> string -> spec list val dest: T -> @@ -53,11 +57,15 @@ (* datatype defs *) type spec = - {def: string option, description: string, lhs: args, rhs: (string * args) list}; + {def: string option, + description: string, + pos: Position.T, + lhs: args, + rhs: (string * args) list}; type def = - {specs: spec Inttab.table, (*source specifications*) - restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) + {specs: spec Inttab.table, (*source specifications*) + restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) reducts: (args * (string * args) list) list}; (*specifications as reduction system*) fun make_def (specs, restricts, reducts) = @@ -97,11 +105,12 @@ (* specifications *) -fun disjoint_specs c (i, {lhs = Ts, description = a, ...}: spec) = - Inttab.forall (fn (j, {lhs = Us, description = b, ...}: spec) => +fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = + Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => i = j orelse disjoint_args (Ts, Us) orelse - error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^ - " for constant " ^ quote c)); + error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^ + " " ^ quote a ^ Position.here pos_a ^ "\n" ^ + " " ^ quote b ^ Position.here pos_b)); fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = let @@ -204,12 +213,13 @@ fun define ctxt unchecked def description (c, args) deps (Defs defs) = let + val pos = Position.thread_data (); val restr = if plain_args args orelse (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false) then [] else [(args, description)]; val spec = - (serial (), {def = def, description = description, lhs = args, rhs = deps}); + (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); val defs' = defs |> update_specs c spec; in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end; diff -r 260e18aa306f -r d7f411651bed src/Pure/goal.ML --- a/src/Pure/goal.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/goal.ML Tue Feb 18 23:08:55 2014 +0100 @@ -187,10 +187,10 @@ val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled (); val pos = Position.thread_data (); - fun err msg = cat_error msg - ("The error(s) above occurred for the goal statement:\n" ^ - Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^ - (case Position.here pos of "" => "" | s => "\n" ^ s)); + fun err msg = + cat_error msg + ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^ + Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props))); fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; diff -r 260e18aa306f -r d7f411651bed src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Pure/more_thm.ML Tue Feb 18 23:08:55 2014 +0100 @@ -37,7 +37,6 @@ val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool - val eq_thm_thy: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: thm * thm -> bool @@ -191,17 +190,17 @@ fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; -fun eq_thm ths = - Context.joinable (pairself Thm.theory_of_thm ths) andalso - is_equal (thm_ord ths); +val eq_thm = is_equal o thm_ord; -val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm; val eq_thm_prop = op aconv o pairself Thm.full_prop_of; fun eq_thm_strict ths = - eq_thm_thy ths andalso eq_thm ths andalso - let val (rep1, rep2) = pairself Thm.rep_thm ths - in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end; + eq_thm ths andalso + let val (rep1, rep2) = pairself Thm.rep_thm ths in + Theory.eq_thy (#thy rep1, #thy rep2) andalso + #maxidx rep1 = #maxidx rep2 andalso + #tags rep1 = #tags rep2 + end; (* pattern equivalence *) diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Feb 18 23:08:55 2014 +0100 @@ -27,48 +27,48 @@ options.isabelle-rendering.label=Rendering options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2(); -#menu actions +#menu actions and dockables plugin.isabelle.jedit.Plugin.menu.label=Isabelle plugin.isabelle.jedit.Plugin.menu= \ - isabelle.documentation-panel \ - isabelle.find-panel \ - isabelle.monitor-panel \ - isabelle.output-panel \ - isabelle.protocol-panel \ - isabelle.raw-output-panel \ - isabelle.sledgehammer-panel \ - isabelle.simp-trace-panel \ - isabelle.symbols-panel \ - isabelle.syslog-panel \ - isabelle.theories-panel \ - isabelle.timing-panel -isabelle.documentation-panel.label=Documentation panel -isabelle.find-panel.label=Find panel -isabelle.monitor-panel.label=Monitor panel -isabelle.output-panel.label=Output panel -isabelle.protocol-panel.label=Protocol panel -isabelle.raw-output-panel.label=Raw Output panel -isabelle.simp-trace-panel.label=Simplifier trace panel -isabelle.sledgehammer-panel.label=Sledgehammer panel -isabelle.symbols-panel.label=Symbols panel -isabelle.syslog-panel.label=Syslog panel -isabelle.theories-panel.label=Theories panel -isabelle.timing-panel.label=Timing panel - -#dockables + isabelle-documentation \ + isabelle-find \ + isabelle-monitor \ + isabelle-output \ + isabelle-protocol \ + isabelle-raw-output \ + isabelle-simplifier-trace \ + isabelle-sledgehammer \ + isabelle-symbols \ + isabelle-syslog \ + isabelle-theories \ + isabelle-timing +isabelle-documentation.label=Documentation panel +isabelle-documentation.title=Documentation +isabelle-find.label=Find panel isabelle-find.title=Find +isabelle-graphview.label=Graphview panel isabelle-graphview.title=Graphview +isabelle-info.label=Info panel isabelle-info.title=Info +isabelle-monitor.label=Monitor panel isabelle-monitor.title=Monitor +isabelle-output.label=Output panel isabelle-output.title=Output -isabelle-simp-trace.title=Simplifier trace +isabelle-protocol.label=Protocol panel isabelle-protocol.title=Protocol +isabelle-raw-output.label=Raw Output panel isabelle-raw-output.title=Raw Output -isabelle-documentation.title=Documentation +isabelle-simplifier-trace.label=Simplifier Trace panel +isabelle-simplifier-trace.title=Simplifier Trace +isabelle-sledgehammer.label=Sledgehammer panel isabelle-sledgehammer.title=Sledgehammer +isabelle-symbols.label=Symbols panel isabelle-symbols.title=Symbols +isabelle-syslog.label=Syslog panel isabelle-syslog.title=Syslog +isabelle-theories.label=Theories panel isabelle-theories.title=Theories +isabelle-timing.label=Timing panel isabelle-timing.title=Timing #SideKick diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/actions.xml Tue Feb 18 23:08:55 2014 +0100 @@ -2,66 +2,6 @@ - - - wm.addDockableWindow("isabelle-theories"); - - - - - wm.addDockableWindow("isabelle-timing"); - - - - - wm.addDockableWindow("isabelle-syslog"); - - - - - wm.addDockableWindow("isabelle-documentation"); - - - - - wm.addDockableWindow("isabelle-find"); - - - - - wm.addDockableWindow("isabelle-sledgehammer"); - - - - - wm.addDockableWindow("isabelle-output"); - - - - - wm.addDockableWindow("isabelle-raw-output"); - - - - - wm.addDockableWindow("isabelle-simp-trace"); - - - - - wm.addDockableWindow("isabelle-protocol"); - - - - - wm.addDockableWindow("isabelle-monitor"); - - - - - wm.addDockableWindow("isabelle-symbols"); - - isabelle.jedit.Isabelle.set_continuous_checking(); diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/active.scala Tue Feb 18 23:08:55 2014 +0100 @@ -61,7 +61,7 @@ else text_area.setSelectedText(text) } - case Markup.Simp_Trace(serial, answer) => + case Simplifier_Trace.Active(serial, answer) => Simplifier_Trace.send_reply(PIDE.session, serial, answer) case Protocol.Dialog(id, serial, result) => diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/dockables.xml Tue Feb 18 23:08:55 2014 +0100 @@ -2,46 +2,46 @@ - - new isabelle.jedit.Theories_Dockable(view, position); - - - new isabelle.jedit.Timing_Dockable(view, position); - - - new isabelle.jedit.Syslog_Dockable(view, position); - new isabelle.jedit.Documentation_Dockable(view, position); - - new isabelle.jedit.Output_Dockable(view, position); - new isabelle.jedit.Find_Dockable(view, position); - - new isabelle.jedit.Sledgehammer_Dockable(view, position); - new isabelle.jedit.Info_Dockable(view, position); new isabelle.jedit.Graphview_Dockable(view, position); - - new isabelle.jedit.Raw_Output_Dockable(view, position); + + new isabelle.jedit.Monitor_Dockable(view, position); + + + new isabelle.jedit.Output_Dockable(view, position); new isabelle.jedit.Protocol_Dockable(view, position); - - new isabelle.jedit.Monitor_Dockable(view, position); + + new isabelle.jedit.Raw_Output_Dockable(view, position); + + + new isabelle.jedit.Simplifier_Trace_Dockable(view, position); + + + new isabelle.jedit.Sledgehammer_Dockable(view, position); new isabelle.jedit.Symbols_Dockable(view, position); - - new isabelle.jedit.Simplifier_Trace_Dockable(view, position); + + new isabelle.jedit.Syslog_Dockable(view, position); + + + new isabelle.jedit.Theories_Dockable(view, position); + + + new isabelle.jedit.Timing_Dockable(view, position); diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 18 23:08:55 2014 +0100 @@ -58,45 +58,75 @@ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager - def docked_theories(view: View): Option[Theories_Dockable] = - wm(view).getDockableWindow("isabelle-theories") match { - case dockable: Theories_Dockable => Some(dockable) + def documentation_dockable(view: View): Option[Documentation_Dockable] = + wm(view).getDockableWindow("isabelle-documentation") match { + case dockable: Documentation_Dockable => Some(dockable) case _ => None } - def docked_timing(view: View): Option[Timing_Dockable] = - wm(view).getDockableWindow("isabelle-timing") match { - case dockable: Timing_Dockable => Some(dockable) + def find_dockable(view: View): Option[Find_Dockable] = + wm(view).getDockableWindow("isabelle-find") match { + case dockable: Find_Dockable => Some(dockable) case _ => None } - def docked_output(view: View): Option[Output_Dockable] = + def monitor_dockable(view: View): Option[Monitor_Dockable] = + wm(view).getDockableWindow("isabelle-monitor") match { + case dockable: Monitor_Dockable => Some(dockable) + case _ => None + } + + def output_dockable(view: View): Option[Output_Dockable] = wm(view).getDockableWindow("isabelle-output") match { case dockable: Output_Dockable => Some(dockable) case _ => None } - def docked_raw_output(view: View): Option[Raw_Output_Dockable] = + def protocol_dockable(view: View): Option[Protocol_Dockable] = + wm(view).getDockableWindow("isabelle-protocol") match { + case dockable: Protocol_Dockable => Some(dockable) + case _ => None + } + + def raw_output_dockable(view: View): Option[Raw_Output_Dockable] = wm(view).getDockableWindow("isabelle-raw-output") match { case dockable: Raw_Output_Dockable => Some(dockable) case _ => None } - def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] = - wm(view).getDockableWindow("isabelle-simp-trace") match { + def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] = + wm(view).getDockableWindow("isabelle-simplifier-trace") match { case dockable: Simplifier_Trace_Dockable => Some(dockable) case _ => None } - def docked_protocol(view: View): Option[Protocol_Dockable] = - wm(view).getDockableWindow("isabelle-protocol") match { - case dockable: Protocol_Dockable => Some(dockable) + def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] = + wm(view).getDockableWindow("isabelle-sledgehammer") match { + case dockable: Sledgehammer_Dockable => Some(dockable) + case _ => None + } + + def symbols_dockable(view: View): Option[Symbols_Dockable] = + wm(view).getDockableWindow("isabelle-symbols") match { + case dockable: Symbols_Dockable => Some(dockable) case _ => None } - def docked_monitor(view: View): Option[Monitor_Dockable] = - wm(view).getDockableWindow("isabelle-monitor") match { - case dockable: Monitor_Dockable => Some(dockable) + def syslog_dockable(view: View): Option[Syslog_Dockable] = + wm(view).getDockableWindow("isabelle-syslog") match { + case dockable: Syslog_Dockable => Some(dockable) + case _ => None + } + + def theories_dockable(view: View): Option[Theories_Dockable] = + wm(view).getDockableWindow("isabelle-theories") match { + case dockable: Theories_Dockable => Some(dockable) + case _ => None + } + + def timing_dockable(view: View): Option[Timing_Dockable] = + wm(view).getDockableWindow("isabelle-timing") match { + case dockable: Timing_Dockable => Some(dockable) case _ => None } diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Tue Feb 18 23:08:55 2014 +0100 @@ -188,8 +188,8 @@ isabelle-output.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 +isabelle-simplifier-trace.dock-position=bottom isabelle-sledgehammer.dock-position=bottom -isabelle-simp-trace.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right isabelle.complete.label=Complete Isabelle text diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 23:08:55 2014 +0100 @@ -222,9 +222,10 @@ try { val p = text_area.offsetToXY(range.start) val (q, r) = - if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) - else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") + if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) + else if (stop >= end) + (text_area.offsetToXY(end), char_width * (stop - end)) else (text_area.offsetToXY(stop), 0) (p, q, r) } diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 18 23:08:55 2014 +0100 @@ -241,10 +241,10 @@ /* markup selectors */ private val highlight_include = - Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, - Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE, - Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, - Markup.DOCUMENT_SOURCE) + Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, + Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, + Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, + Markup.VAR, Markup.TFREE, Markup.TVAR) def highlight(range: Text.Range): Option[Text.Info[Color]] = { @@ -258,7 +258,21 @@ } - private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL) + private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) + + private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] = + if (Path.is_ok(name)) + Isabelle_System.source_file(Path.explode(name)).map(path => + PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line)) + else None + + private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset) + : Option[PIDE.editor.Hyperlink] = + snapshot.state.find_command(snapshot.version, id) match { + case Some((node, command)) => + PIDE.editor.hyperlink_command(snapshot, command, offset) + case None => None + } def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { @@ -281,26 +295,22 @@ case (Markup.KIND, Markup.ML_STRUCT) => true case _ => false }) => - props match { - case Position.Def_Line_File(line, name) if Path.is_ok(name) => - Isabelle_System.source_file(Path.explode(name)) match { - case Some(path) => - val jedit_file = Isabelle_System.platform_path(path) - val link = PIDE.editor.hyperlink_file(jedit_file, line) - Some(Text.Info(snapshot.convert(info_range), link) :: links) - case None => None - } + val opt_link = + props match { + case Position.Def_Line_File(line, name) => hyperlink_file(line, name) + case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset) + case _ => None + } + opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) - case Position.Def_Id_Offset(id, offset) => - snapshot.state.find_command(snapshot.version, id) match { - case Some((node, command)) => - PIDE.editor.hyperlink_command(snapshot, command, offset) - .map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) - case None => None - } - - case _ => None - } + case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => + val opt_link = + props match { + case Position.Line_File(line, name) => hyperlink_file(line, name) + case Position.Id_Offset(id, offset) => hyperlink_command(id, offset) + case _ => None + } + opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) case _ => None }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None } @@ -365,23 +375,18 @@ private val tooltips: Map[String, String] = Map( - Markup.SORT -> "sort", - Markup.TYP -> "type", - Markup.TERM -> "term", - Markup.PROP -> "proposition", Markup.TOKEN_RANGE -> "inner syntax token", Markup.FREE -> "free variable", Markup.SKOLEM -> "skolem variable", Markup.BOUND -> "bound variable", Markup.VAR -> "schematic variable", Markup.TFREE -> "free type variable", - Markup.TVAR -> "schematic type variable", - Markup.ML_SOURCE -> "ML source", - Markup.DOCUMENT_SOURCE -> "document source") + Markup.TVAR -> "schematic type variable") private val tooltip_elements = - Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, - Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys + Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING, + Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ + tooltips.keys private def pretty_typing(kind: String, body: XML.Body): XML.Tree = Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body) @@ -424,6 +429,8 @@ Some(add(prev, r, (true, pretty_typing("::", body)))) case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(add(prev, r, (false, pretty_typing("ML:", body)))) + case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) => + Some(add(prev, r, (true, XML.Text("language: " + name)))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => if (tooltips.isDefinedAt(name)) Some(add(prev, r, (true, XML.Text(tooltips(name))))) diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 23:08:55 2014 +0100 @@ -10,7 +10,6 @@ import isabelle._ import scala.actors.Actor._ - import scala.swing.{Button, CheckBox, Orientation, Separator} import scala.swing.event.ButtonClicked @@ -19,6 +18,7 @@ import org.gjt.sp.jedit.View + class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) { Swing_Thread.require() diff -r 260e18aa306f -r d7f411651bed src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 17:52:28 2014 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 23:08:55 2014 +0100 @@ -10,12 +10,9 @@ import isabelle._ import scala.annotation.tailrec - import scala.collection.immutable.SortedMap - import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField} import scala.swing.event.{Key, KeyPressed} - import scala.util.matching.Regex import java.awt.BorderLayout @@ -25,17 +22,15 @@ import org.gjt.sp.jedit.View + private object Simplifier_Trace_Window { - - import Markup.Simp_Trace_Item - sealed trait Trace_Tree { var children: SortedMap[Long, Elem_Tree] = SortedMap.empty val serial: Long val parent: Option[Trace_Tree] - var hints: List[Simp_Trace_Item.Data] + var hints: List[Simplifier_Trace.Item.Data] def set_interesting(): Unit } @@ -43,17 +38,19 @@ { val parent = None val hints = Nil - def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints") + def hints_=(xs: List[Simplifier_Trace.Item.Data]) = + throw new IllegalStateException("Root_Tree.hints") def set_interesting() = () def format(regex: Option[Regex]): XML.Body = Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut)) } - final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree + final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree]) + extends Trace_Tree { val serial = data.serial - var hints = List.empty[Simp_Trace_Item.Data] + var hints = List.empty[Simplifier_Trace.Item.Data] var interesting: Boolean = false def set_interesting(): Unit = @@ -76,7 +73,7 @@ Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res))) } - def format_hint(data: Simp_Trace_Item.Data): XML.Tree = + def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree = Pretty.block(Pretty.separate( XML.Text(data.text) :: data.content @@ -111,19 +108,19 @@ } @tailrec - def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit = + def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit = rest match { case Nil => () case head :: tail => lookup.get(head.parent) match { case Some(parent) => - if (head.markup == Simp_Trace_Item.HINT) + if (head.markup == Markup.SIMP_TRACE_HINT) { parent.hints ::= head walk_trace(tail, lookup) } - else if (head.markup == Simp_Trace_Item.IGNORE) + else if (head.markup == Markup.SIMP_TRACE_IGNORE) { parent.parent match { case None => @@ -137,7 +134,7 @@ { val entry = new Elem_Tree(head, Some(parent)) parent.children += ((head.serial, entry)) - if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG) + if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG) entry.set_interesting() walk_trace(tail, lookup + (head.serial -> entry)) } @@ -149,11 +146,10 @@ } -class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame + +class Simplifier_Trace_Window( + view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame { - - import Simplifier_Trace_Window._ - Swing_Thread.require() val area = new Pretty_Text_Area(view) @@ -165,11 +161,11 @@ private val tree = trace.entries.headOption match { case Some(first) => - val tree = new Root_Tree(first.parent) - walk_trace(trace.entries, Map(first.parent -> tree)) + val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) + Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree)) tree case None => - new Root_Tree(0) + new Simplifier_Trace_Window.Root_Tree(0) } do_update(None)