--- a/NEWS Thu Sep 17 11:57:36 2009 +0200
+++ b/NEWS Thu Sep 17 11:58:21 2009 +0200
@@ -41,14 +41,6 @@
semidefinite programming solvers. For more information and examples
see src/HOL/Library/Sum_Of_Squares.
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.
-INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.
-INCOMPATIBILITY:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
-
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
@@ -57,16 +49,14 @@
* New class "boolean_algebra".
-* Refinements to lattices classes:
- - added boolean_algebra type class
+* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
- renamed ACI to inf_sup_aci
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants renamed:
-
+ corresponding constants (and abbreviations) renamed:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -75,6 +65,14 @@
Set.Union ~> Complete_Lattice.Union
Set.INTER ~> Complete_Lattice.INTER
Set.UNION ~> Complete_Lattice.UNION
+ - more convenient names for set intersection and union:
+ Set.Int ~> Set.inter
+ Set.Un ~> Set.union
+ - mere abbreviations:
+ Set.empty (for bot)
+ Set.UNIV (for top)
+ Complete_Lattice.Inter (for Inf)
+ Complete_Lattice.Union (for Sup)
INCOMPATIBILITY.
@@ -87,7 +85,7 @@
INCOMPATIBILITY.
* Power operations on relations and functions are now one dedicate
-constant compow with infix syntax "^^". Power operations on
+constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
--- a/src/HOL/Complete_Lattice.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Thu Sep 17 11:58:21 2009 +0200
@@ -203,8 +203,8 @@
subsection {* Union *}
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> \<Squnion>S"
notation (xsymbols)
Union ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
- by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+ by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
qed
lemma Union_iff [simp, noatp]:
@@ -314,7 +314,7 @@
lemma UNION_eq_Union_image:
"(\<Union>x\<in>A. B x) = \<Union>(B`A)"
- by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
+ by (simp add: SUPR_def SUPR_set_eq [symmetric])
lemma Union_def:
"\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
subsection {* Inter *}
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> \<Sqinter>S"
notation (xsymbols)
Inter ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+ by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -541,7 +541,7 @@
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
+ by (simp add: INFI_def INFI_set_eq [symmetric])
lemma Inter_def:
"\<Inter>S = (\<Inter>x\<in>S. x)"
--- a/src/HOL/Imperative_HOL/Array.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Thu Sep 17 11:58:21 2009 +0200
@@ -176,12 +176,11 @@
code_type array (OCaml "_/ array")
code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
+code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
+code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
code_reserved OCaml Array
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Thu Sep 17 11:58:21 2009 +0200
@@ -1,4 +1,3 @@
-(* $Id$ *)
header {* Slices of lists *}
@@ -6,7 +5,6 @@
imports Multiset
begin
-
lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
apply (induct xs arbitrary: i j k)
apply simp
--- a/src/HOL/Inductive.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Inductive.thy Thu Sep 17 11:58:21 2009 +0200
@@ -111,8 +111,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms unfolding Sup_set_eq [symmetric]
- by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct [where P=P])
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
--- a/src/HOL/Library/Executable_Set.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Thu Sep 17 11:58:21 2009 +0200
@@ -8,7 +8,7 @@
imports Main Fset
begin
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
declare member [code]
@@ -24,9 +24,7 @@
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
[code del]: "eq_set = op ="
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
lemma [code]:
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]
-
-subsection {* Rewrites for primitive operations *}
-
declare List_Set.project_def [symmetric, code_unfold]
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter = Complete_Lattice.Inter"
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
ML {*
nonfix inter;
@@ -75,8 +80,8 @@
"op \<union>" ("{*Fset.union*}")
"op \<inter>" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
- "Complete_Lattice.Union" ("{*Fset.Union*}")
- "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+ "Union" ("{*Fset.Union*}")
+ "Inter" ("{*Fset.Inter*}")
card ("{*Fset.card*}")
fold ("{*foldl o flip*}")
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 17 11:58:21 2009 +0200
@@ -23,6 +23,7 @@
datatype sh_data = ShData of {
calls: int,
success: int,
+ lemmas: int,
time_isa: int,
time_atp: int,
time_atp_fail: int}
@@ -38,7 +39,8 @@
datatype min_data = MinData of {
calls: int,
- ratios: int
+ ratios: int,
+ lemmas: int
}
(* The first me_data component is only used if "minimize" is on.
@@ -46,30 +48,30 @@
*)
datatype data = Data of sh_data * me_data * min_data * me_data
-fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) =
- ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
- time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}
+fun make_sh_data (calls,success,lemmas,time_isa,time_atp,time_atp_fail) =
+ ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa,
+ time_atp=time_atp, time_atp_fail=time_atp_fail}
-fun make_min_data (calls, ratios) =
- MinData{calls=calls, ratios=ratios}
+fun make_min_data (calls, ratios, lemmas) =
+ MinData{calls=calls, ratios=ratios, lemmas=lemmas}
fun make_me_data (calls, success, time, timeout, lemmas, posns) =
MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
val empty_data =
- Data(make_sh_data (0, 0, 0, 0, 0),
+ Data(make_sh_data (0, 0, 0, 0, 0, 0),
make_me_data(0, 0, 0, 0, 0, []),
- MinData{calls=0, ratios=0},
+ MinData{calls=0, ratios=0, lemmas=0},
make_me_data(0, 0, 0, 0, 0, []))
fun map_sh_data f
- (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
- Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)),
+ (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) =
+ Data (make_sh_data (f (calls, success, lemmas, time_isa, time_atp, time_atp_fail)),
meda0, minda, meda)
fun map_min_data f
- (Data(shda, meda0, MinData{calls,ratios}, meda)) =
- Data(shda, meda0, make_min_data(f(calls,ratios)), meda)
+ (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) =
+ Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda)
fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
@@ -78,30 +80,34 @@
Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
val inc_sh_calls =
- map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
- => (calls + 1, success, time_isa, time_atp, time_atp_fail))
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls + 1, success, lemmas, time_isa, time_atp, time_atp_fail))
val inc_sh_success =
- map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
- => (calls, success + 1, time_isa, time_atp, time_atp_fail))
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success + 1, lemmas, time_isa, time_atp, time_atp_fail))
+
+fun inc_sh_lemmas n =
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas + n, time_isa, time_atp, time_atp_fail))
fun inc_sh_time_isa t =
- map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
- => (calls, success, time_isa + t, time_atp, time_atp_fail))
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa + t, time_atp, time_atp_fail))
fun inc_sh_time_atp t =
- map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
- => (calls, success, time_isa, time_atp + t, time_atp_fail))
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa, time_atp + t, time_atp_fail))
fun inc_sh_time_atp_fail t =
- map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail)
- => (calls, success, time_isa, time_atp, time_atp_fail + t))
+ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
+ => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t))
val inc_min_calls =
- map_min_data (fn (calls, ratios) => (calls + 1, ratios))
+ map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas))
fun inc_min_ratios n =
- map_min_data (fn (calls, ratios) => (calls, ratios + n))
+ map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas))
val inc_metis_calls = map_me_data
(fn (calls, success, time, timeout, lemmas,posns)
@@ -160,9 +166,10 @@
fun avg_time t n =
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
-fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail =
+fun log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail =
(log ("Total number of sledgehammer calls: " ^ str sh_calls);
log ("Number of successful sledgehammer calls: " ^ str sh_success);
+ log ("Number of sledgehammer lemmas: " ^ str sh_lemmas);
log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
@@ -188,7 +195,7 @@
log ("Number of " ^ tag ^ "metis exceptions: " ^
str (sh_success - metis_success - metis_timeout));
log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
- log ("Number of " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
+ log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
log ("Total time for successful metis calls: " ^ str3 (time metis_time));
log ("Average time for successful metis calls: " ^
str3 (avg_time metis_time metis_success));
@@ -205,19 +212,19 @@
in
fun log_data id log (Data
- (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
- time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail},
+ (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success,
+ time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail},
MeData{calls=metis_calls0,
success=metis_success0, time=metis_time0, timeout=metis_timeout0,
lemmas=metis_lemmas0,posns=metis_posns0},
- MinData{calls=min_calls, ratios=min_ratios},
+ MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas},
MeData{calls=metis_calls,
success=metis_success, time=metis_time, timeout=metis_timeout,
lemmas=metis_lemmas,posns=metis_posns})) =
if sh_calls > 0
then
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
- log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail;
+ log_sh_data log sh_calls sh_success sh_lemmas sh_time_isa sh_time_atp sh_time_atp_fail;
log "";
if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls
metis_success metis_time metis_timeout metis_lemmas metis_posns else ();
@@ -321,6 +328,7 @@
SH_OK (time_isa, time_atp, names) =>
let
val _ = change_data id inc_sh_success
+ val _ = change_data id (inc_sh_lemmas (length names))
val _ = change_data id (inc_sh_time_isa time_isa)
val _ = change_data id (inc_sh_time_atp time_atp)
@@ -374,6 +382,7 @@
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
| with_time (true, t) = (change_data id inc_metis_success;
+ change_data id (inc_metis_lemmas (length named_thms));
change_data id (inc_metis_time t);
change_data id (inc_metis_posns pos);
"succeeded (" ^ string_of_int t ^ ")")
@@ -383,7 +392,6 @@
val _ = log separator
val _ = change_data id inc_metis_calls
- val _ = change_data id (inc_metis_lemmas (length named_thms))
in
maps snd named_thms
|> timed_metis
--- a/src/HOL/Nominal/Examples/Class.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Sep 17 11:58:21 2009 +0200
@@ -11134,7 +11134,6 @@
shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
and "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
--- a/src/HOL/Predicate.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/Predicate.thy Thu Sep 17 11:58:21 2009 +0200
@@ -366,7 +366,7 @@
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
"P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
-instantiation pred :: (type) complete_lattice
+instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
begin
definition
@@ -393,10 +393,16 @@
definition
[code del]: "\<Squnion>A = Pred (SUPR A eval)"
-instance by default
- (auto simp add: less_eq_pred_def less_pred_def
+definition
+ "- P = Pred (- eval P)"
+
+definition
+ "P - Q = Pred (eval P - eval Q)"
+
+instance proof
+qed (auto simp add: less_eq_pred_def less_pred_def
inf_pred_def sup_pred_def bot_pred_def top_pred_def
- Inf_pred_def Sup_pred_def,
+ Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
eval_inject mem_def)
@@ -464,6 +470,127 @@
lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
unfolding sup_pred_def by auto
+lemma single_not_bot [simp]:
+ "single x \<noteq> \<bottom>"
+ by (auto simp add: single_def bot_pred_def expand_fun_eq)
+
+lemma not_bot:
+ assumes "A \<noteq> \<bottom>"
+ obtains x where "eval A x"
+using assms by (cases A)
+ (auto simp add: bot_pred_def, auto simp add: mem_def)
+
+
+subsubsection {* Emptiness check and definite choice *}
+
+definition is_empty :: "'a pred \<Rightarrow> bool" where
+ "is_empty A \<longleftrightarrow> A = \<bottom>"
+
+lemma is_empty_bot:
+ "is_empty \<bottom>"
+ by (simp add: is_empty_def)
+
+lemma not_is_empty_single:
+ "\<not> is_empty (single x)"
+ by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
+
+lemma is_empty_sup:
+ "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
+ by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
+
+definition singleton :: "'a pred \<Rightarrow> 'a" where
+ "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
+
+lemma singleton_eqI:
+ "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x"
+ by (auto simp add: singleton_def)
+
+lemma eval_singletonI:
+ "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
+proof -
+ assume assm: "\<exists>!x. eval A x"
+ then obtain x where "eval A x" ..
+ moreover with assm have "singleton A = x" by (rule singleton_eqI)
+ ultimately show ?thesis by simp
+qed
+
+lemma single_singleton:
+ "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
+proof -
+ assume assm: "\<exists>!x. eval A x"
+ then have "eval A (singleton A)"
+ by (rule eval_singletonI)
+ moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
+ by (rule singleton_eqI)
+ ultimately have "eval (single (singleton A)) = eval A"
+ by (simp (no_asm_use) add: single_def expand_fun_eq) blast
+ then show ?thesis by (simp add: eval_inject)
+qed
+
+lemma singleton_undefinedI:
+ "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
+ by (simp add: singleton_def)
+
+lemma singleton_bot:
+ "singleton \<bottom> = undefined"
+ by (auto simp add: bot_pred_def intro: singleton_undefinedI)
+
+lemma singleton_single:
+ "singleton (single x) = x"
+ by (auto simp add: intro: singleton_eqI singleI elim: singleE)
+
+lemma singleton_sup_single_single:
+ "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
+proof (cases "x = y")
+ case True then show ?thesis by (simp add: singleton_single)
+next
+ case False
+ have "eval (single x \<squnion> single y) x"
+ and "eval (single x \<squnion> single y) y"
+ by (auto intro: supI1 supI2 singleI)
+ with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
+ by blast
+ then have "singleton (single x \<squnion> single y) = undefined"
+ by (rule singleton_undefinedI)
+ with False show ?thesis by simp
+qed
+
+lemma singleton_sup_aux:
+ "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+ else if B = \<bottom> then singleton A
+ else singleton
+ (single (singleton A) \<squnion> single (singleton B)))"
+proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
+ case True then show ?thesis by (simp add: single_singleton)
+next
+ case False
+ from False have A_or_B:
+ "singleton A = undefined \<or> singleton B = undefined"
+ by (auto intro!: singleton_undefinedI)
+ then have rhs: "singleton
+ (single (singleton A) \<squnion> single (singleton B)) = undefined"
+ by (auto simp add: singleton_sup_single_single singleton_single)
+ from False have not_unique:
+ "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
+ show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
+ case True
+ then obtain a b where a: "eval A a" and b: "eval B b"
+ by (blast elim: not_bot)
+ with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
+ by (auto simp add: sup_pred_def bot_pred_def)
+ then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
+ with True rhs show ?thesis by simp
+ next
+ case False then show ?thesis by auto
+ qed
+qed
+
+lemma singleton_sup:
+ "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+ else if B = \<bottom> then singleton A
+ else if singleton A = singleton B then singleton A else undefined)"
+using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
+
subsubsection {* Derived operations *}
@@ -630,6 +757,46 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
"map f P = P \<guillemotright>= (single o f)"
+primrec null :: "'a seq \<Rightarrow> bool" where
+ "null Empty \<longleftrightarrow> True"
+ | "null (Insert x P) \<longleftrightarrow> False"
+ | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
+
+lemma null_is_empty:
+ "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
+ by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
+
+lemma is_empty_code [code]:
+ "is_empty (Seq f) \<longleftrightarrow> null (f ())"
+ by (simp add: null_is_empty Seq_def)
+
+primrec the_only :: "'a seq \<Rightarrow> 'a" where
+ [code del]: "the_only Empty = undefined"
+ | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
+ | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
+ else let x = singleton P; y = the_only xq in
+ if x = y then x else undefined)"
+
+lemma the_only_singleton:
+ "the_only xq = singleton (pred_of_seq xq)"
+ by (induct xq)
+ (auto simp add: singleton_bot singleton_single is_empty_def
+ null_is_empty Let_def singleton_sup)
+
+lemma singleton_code [code]:
+ "singleton (Seq f) = (case f ()
+ of Empty \<Rightarrow> undefined
+ | Insert x P \<Rightarrow> if is_empty P then x
+ else let y = singleton P in
+ if x = y then x else undefined
+ | Join P xq \<Rightarrow> if is_empty P then the_only xq
+ else if null xq then singleton P
+ else let x = singleton P; y = the_only xq in
+ if x = y then x else undefined)"
+ by (cases "f ()")
+ (auto simp add: Seq_def the_only_singleton is_empty_def
+ null_is_empty singleton_bot singleton_single singleton_sup Let_def)
+
ML {*
signature PREDICATE =
sig
@@ -707,7 +874,7 @@
bind (infixl "\<guillemotright>=" 70)
hide (open) type pred seq
-hide (open) const Pred eval single bind if_pred not_pred
- Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+ Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
end
--- a/src/HOL/UNITY/Transformers.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Thu Sep 17 11:58:21 2009 +0200
@@ -88,7 +88,7 @@
done
lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def, blast)
text{*These two theorems justify the claim that @{term wens} returns the
weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Sup_set_eq, blast)
+ ensures_def transient_def, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -120,7 +120,7 @@
text{*Assertion 4.17 in the thesis*}
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
--{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
lemma wens_single_eq:
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOL/ex/CTL.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/ex/CTL.thy Thu Sep 17 11:58:21 2009 +0200
@@ -95,7 +95,7 @@
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
- by (auto simp add: gfp_def Sup_set_eq)
+ by (auto simp add: gfp_def)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Sep 17 11:57:36 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Sep 17 11:58:21 2009 +0200
@@ -157,4 +157,13 @@
values 3 "{(a,q). step (par nil nil) a q}"
*)
+
+inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+ "k < l \<Longrightarrow> divmod_rel k l 0 k"
+ | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
+
+code_pred divmod_rel ..
+
+value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+
end
\ No newline at end of file
--- a/src/Pure/Concurrent/future.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Sep 17 11:58:21 2009 +0200
@@ -84,7 +84,7 @@
fun group_of (Future {group, ...}) = group;
fun result_of (Future {result, ...}) = result;
-fun peek x = Synchronized.peek (result_of x);
+fun peek x = Synchronized.value (result_of x);
fun is_finished x = is_some (peek x);
fun value x = Future
--- a/src/Pure/Concurrent/synchronized.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Thu Sep 17 11:58:21 2009 +0200
@@ -8,7 +8,6 @@
sig
type 'a var
val var: string -> 'a -> 'a var
- val peek: 'a var -> 'a
val value: 'a var -> 'a
val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -33,9 +32,7 @@
cond = ConditionVar.conditionVar (),
var = ref x};
-fun peek (Var {var, ...}) = ! var; (*unsynchronized!*)
-
-fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
+fun value (Var {var, ...}) = ! var;
(* synchronized access *)
--- a/src/Pure/General/binding.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/General/binding.ML Thu Sep 17 11:58:21 2009 +0200
@@ -30,18 +30,19 @@
val str_of: binding -> string
end;
-structure Binding:> BINDING =
+structure Binding: BINDING =
struct
(** representation **)
(* datatype *)
-datatype binding = Binding of
+abstype binding = Binding of
{prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ pos: Position.T} (*source position*)
+with
fun make_binding (prefix, qualifier, name, pos) =
Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
end;
+end;
type binding = Binding.binding;
--- a/src/Pure/General/linear_set.scala Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/General/linear_set.scala Thu Sep 17 11:58:21 2009 +0200
@@ -1,22 +1,22 @@
/* Title: Pure/General/linear_set.scala
Author: Makarius
- Author: Fabian Immler TU Munich
+ Author: Fabian Immler, TU Munich
Sets with canonical linear order, or immutable linked-lists.
*/
+
package isabelle
object Linear_Set
{
private case class Rep[A](
- val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
-
- private def empty_rep[A] = Rep[A](None, None, Map())
+ val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
- private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
- new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
+ private def empty_rep[A] = Rep[A](None, None, Map(), Map())
+ private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+ : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
def empty[A]: Linear_Set[A] = new Linear_Set
def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
@@ -35,48 +35,74 @@
/* auxiliary operations */
- def next(elem: A) = rep.body.get(elem)
- def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1) // slow
+ def next(elem: A): Option[A] = rep.nexts.get(elem)
+ def prev(elem: A): Option[A] = rep.prevs.get(elem)
- private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
+ def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
- else hook match {
- case Some(hook) =>
- if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
- else if (rep.body.isDefinedAt(hook))
- Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
- else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
+ else
+ hook match {
+ case None =>
+ rep.first match {
+ case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+ case Some(elem1) =>
+ Linear_Set.make(Some(elem), rep.last,
+ rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem),
+ rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+ case Some(elem2) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts + (elem1 -> elem) + (elem -> elem2),
+ rep.prevs + (elem2 -> elem) + (elem -> elem1))
+ }
+ }
+
+ def delete_after(hook: Option[A]): Linear_Set[A] =
+ hook match {
case None =>
- if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
- else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
+ rep.first match {
+ case None => throw new Linear_Set.Undefined("")
+ case Some(elem1) =>
+ rep.nexts.get(elem1) match {
+ case None => empty
+ case Some(elem2) =>
+ Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+ }
+ }
+ case Some(elem1) =>
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ else
+ rep.nexts.get(elem1) match {
+ case None => throw new Linear_Set.Undefined("")
+ case Some(elem2) =>
+ rep.nexts.get(elem2) match {
+ case None =>
+ Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ case Some(elem3) =>
+ Linear_Set.make(rep.first, rep.last,
+ rep.nexts - elem2 + (elem1 -> elem3),
+ rep.prevs - elem2 + (elem3 -> elem1))
+ }
+ }
}
- def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
- elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
+ def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+ (elems :\ this)((elem, set) => set.insert_after(hook, elem))
- def delete_after(elem: Option[A]): Linear_Set[A] =
- elem match {
- case Some(elem) =>
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
- else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
- else if (rep.body(elem) == rep.last_elem.get)
- Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
- else Linear_Set.make(rep.first_elem, rep.last_elem,
- rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
- case None =>
- if (isEmpty) throw new Linear_Set.Undefined(null)
- else if (size == 1) empty
- else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
- }
-
- def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
- if(!rep.first_elem.isDefined) this
+ def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
+ {
+ if (isEmpty) this
else {
val next =
- if (from == rep.last_elem) None
- else if (from == None) rep.first_elem
- else from.map(rep.body(_))
+ if (from == rep.last) None
+ else if (from == None) rep.first
+ else from.map(rep.nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
}
@@ -89,23 +115,23 @@
def empty[B]: Linear_Set[B] = Linear_Set.empty
- override def isEmpty: Boolean = !rep.last_elem.isDefined
- def size: Int = if (isEmpty) 0 else rep.body.size + 1
+ override def isEmpty: Boolean = !rep.first.isDefined
+ def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
def elements = new Iterator[A] {
- private var next_elem = rep.first_elem
+ private var next_elem = rep.first
def hasNext = next_elem.isDefined
def next = {
val elem = next_elem.get
- next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
+ next_elem = rep.nexts.get(elem)
elem
}
}
def contains(elem: A): Boolean =
- !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+ !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
- def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+ def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
this + elem1 + elem2 ++ elems
--- a/src/Pure/General/position.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/General/position.ML Thu Sep 17 11:58:21 2009 +0200
@@ -21,6 +21,7 @@
val line: int -> T
val line_file: int -> string -> T
val id: string -> T
+ val id_only: string -> T
val get_id: T -> string option
val put_id: string -> T -> T
val of_properties: Properties.T -> T
@@ -97,8 +98,8 @@
fun line_file i name = Pos ((i, 0, 0), file_name name);
fun line i = line_file i "";
-
fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
--- a/src/Pure/Isar/isar_document.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML Thu Sep 17 11:58:21 2009 +0200
@@ -278,6 +278,7 @@
val _ =
OuterSyntax.internal_command "Isar.define_command"
(P.string -- P.string >> (fn (id, text) =>
+ Toplevel.position (Position.id_only id) o
Toplevel.imperative (fn () =>
define_command id (OuterSyntax.prepare_command (Position.id id) text))));
--- a/src/Pure/thm.ML Thu Sep 17 11:57:36 2009 +0200
+++ b/src/Pure/thm.ML Thu Sep 17 11:58:21 2009 +0200
@@ -153,7 +153,7 @@
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
-structure Thm:> THM =
+structure Thm: THM =
struct
structure Pt = Proofterm;
@@ -163,11 +163,12 @@
(** certified types **)
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
{thy_ref: theory_ref,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
fun rep_ctyp (Ctyp args) = args;
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
@@ -189,12 +190,13 @@
(** certified terms **)
(*certified terms with checked typ, maxidx, and sorts*)
-datatype cterm = Cterm of
+abstype cterm = Cterm of
{thy_ref: theory_ref,
t: term,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
exception CTERM of string * cterm list;
@@ -337,7 +339,7 @@
(*** Derivations and Theorems ***)
-datatype thm = Thm of
+abstype thm = Thm of
deriv * (*derivation*)
{thy_ref: theory_ref, (*dynamic reference to theory*)
tags: Properties.T, (*additional annotations/comments*)
@@ -348,7 +350,8 @@
prop: term} (*conclusion*)
and deriv = Deriv of
{promises: (serial * thm future) OrdList.T,
- body: Pt.proof_body};
+ body: Pt.proof_body}
+with
type conv = cterm -> thm;
@@ -1718,6 +1721,10 @@
end
end;
+end;
+end;
+end;
+
(* authentic derivation names *)