--- a/etc/isar-keywords.el Wed Aug 28 23:41:21 2013 +0200
+++ b/etc/isar-keywords.el Wed Aug 28 23:48:45 2013 +0200
@@ -195,10 +195,10 @@
"print_methods"
"print_options"
"print_orders"
+ "print_quot_maps"
"print_quotconsts"
"print_quotients"
"print_quotientsQ3"
- "print_quotmaps"
"print_quotmapsQ3"
"print_rules"
"print_simpset"
@@ -422,10 +422,10 @@
"print_methods"
"print_options"
"print_orders"
+ "print_quot_maps"
"print_quotconsts"
"print_quotients"
"print_quotientsQ3"
- "print_quotmaps"
"print_quotmapsQ3"
"print_rules"
"print_simpset"
--- a/src/Doc/IsarRef/HOL_Specific.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Wed Aug 28 23:48:45 2013 +0200
@@ -1550,7 +1550,7 @@
\begin{matharray}{rcl}
@{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
@{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
- @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
+ @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
@{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
@@ -1626,7 +1626,7 @@
Integration with code: For total quotients, @{command
(HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
- \item @{command (HOL) "print_quotmaps"} prints stored quotient map
+ \item @{command (HOL) "print_quot_maps"} prints stored quotient map
theorems.
\item @{command (HOL) "print_quotients"} prints stored quotient
--- a/src/Doc/Sledgehammer/document/root.tex Wed Aug 28 23:41:21 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Aug 28 23:48:45 2013 +0200
@@ -601,14 +601,15 @@
\point{A strange error occurred---what should I do?}
Sledgehammer tries to give informative error messages. Please report any strange
-error to the author at \authoremail. This applies double if you get the message
+error to the author at \authoremail. This applies doubly if you get the message
\prew
\slshape
-The prover found a type-unsound proof involving ``\textit{foo\/}'',
-``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
-encoding was used (or, less likely, your axioms are inconsistent). You might
-want to report this to the Isabelle developers.
+The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
+``\textit{bar\/}'', and ``\textit{baz\/}''.
+This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
+a bug in Sledgehammer. If the problem persists, please contact the
+Isabelle developers.
\postw
\point{Auto can solve it---why not Sledgehammer?}
--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Aug 28 23:48:45 2013 +0200
@@ -14,8 +14,11 @@
type unfold_set
val empty_unfolds: unfold_set
+ exception BAD_DEAD of typ * typ
+
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
- ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
+ ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> typ ->
+ unfold_set * Proof.context ->
(BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
val default_comp_sort: (string * sort) list list -> (string * sort) list
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
@@ -645,10 +648,18 @@
((bnf', deads), lthy')
end;
-fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
- | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
- | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
+exception BAD_DEAD of typ * typ;
+
+fun bnf_of_typ _ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
+ | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+ | bnf_of_typ const_policy qualify' sort Xs (T as Type (C, Ts)) (unfold_set, lthy) =
let
+ fun check_bad_dead ((_, (deads, _)), _) =
+ let val Ds = fold Term.add_tfreesT deads [] in
+ (case Library.inter (op =) Ds Xs of [] => ()
+ | X :: _ => raise BAD_DEAD (TFree X, T))
+ end;
+
val tfrees = Term.add_tfreesT T [];
val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
in
@@ -679,11 +690,12 @@
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
apfst (apsnd split_list o split_list)
- (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
+ (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs)
(if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
in
compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
end)
+ |> tap check_bad_dead
end;
end;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 28 23:48:45 2013 +0200
@@ -97,6 +97,7 @@
open BNF_Util
open BNF_Ctr_Sugar
+open BNF_Comp
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
@@ -1103,12 +1104,14 @@
quote (Syntax.string_of_typ fake_lthy T)))
| eq_fpT_check _ _ = false;
- fun freeze_fp (T as Type (s, Us)) =
+ fun freeze_fp (T as Type (s, Ts)) =
(case find_index (eq_fpT_check T) fake_Ts of
- ~1 => Type (s, map freeze_fp Us)
+ ~1 => Type (s, map freeze_fp Ts)
| kk => nth Xs kk)
| freeze_fp T = T;
+ val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts);
+
val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
@@ -1120,7 +1123,33 @@
dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
- no_defs_lthy0;
+ no_defs_lthy0
+ handle BAD_DEAD (X, X_backdrop) =>
+ (case X_backdrop of
+ Type (bad_tc, _) =>
+ let
+ val qsoty = quote o Syntax.string_of_typ fake_lthy;
+ val fake_T = qsoty (unfreeze_fp X);
+ val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
+ fun register_hint () =
+ "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^
+ quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
+ \it";
+ in
+ if is_some (bnf_of no_defs_lthy bad_tc) orelse
+ is_some (fp_sugar_of no_defs_lthy bad_tc) then
+ error ("Non-strictly-positive " ^ co_prefix fp ^ "recursive occurrence of type " ^
+ fake_T ^ " in type expression " ^ fake_T_backdrop)
+ else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+ bad_tc) then
+ error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+ " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^
+ fake_T_backdrop ^ register_hint ())
+ else
+ error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
+ " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^
+ register_hint ())
+ end);
val time = time lthy;
val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 28 23:48:45 2013 +0200
@@ -352,7 +352,7 @@
fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
fun add_components_of_typ (Type (s, Ts)) =
- fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
+ cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
| add_components_of_typ _ = I;
fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
@@ -571,18 +571,18 @@
|> unfold_thms ctxt unfolds
end;
-fun fp_bnf construct_fp bs resBs eqs lthy =
+fun fp_bnf construct_fp bs resBs fp_eqs lthy =
let
val time = time lthy;
val timer = time (Timer.startRealTimer ());
- val (lhss, rhss) = split_list eqs;
+ val (Xs, rhsXs) = split_list fp_eqs;
- (* FIXME: because of "@ lhss", the output could contain type variables that are not in the
+ (* FIXME: because of "@ Xs", the output could contain type variables that are not in the
input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
fun fp_sort Ass =
- subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss;
+ subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
- val name = mk_common_name (map Binding.name_of bs);
+ val common_name = mk_common_name (map Binding.name_of bs);
fun raw_qualify b =
let val s = Binding.name_of b in
@@ -590,21 +590,17 @@
end;
val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
- (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss
+ (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
(empty_unfolds, lthy));
fun qualify i =
- let val namei = name ^ nonzero_string_of_int i;
+ let val namei = common_name ^ nonzero_string_of_int i;
in Binding.qualify true namei end;
val Ass = map (map dest_TFree) livess;
val resDs = fold (subtract (op =)) Ass resBs;
val Ds = fold (fold Term.add_tfreesT) deadss [];
- val _ = (case Library.inter (op =) Ds lhss of [] => ()
- | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
- \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
-
val timer = time (timer "Construction of BNFs");
val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Aug 28 23:48:45 2013 +0200
@@ -246,7 +246,7 @@
end
-class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
+class linear_continuum = conditionally_complete_linorder + dense_linorder +
assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
begin
@@ -283,22 +283,22 @@
lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq_non_empty intro: dense_le)
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = x"
by (auto intro!: cSup_eq intro: dense_le_bounded)
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, dense_linorder} <..} = x"
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, unbounded_dense_linorder} <..} = x"
by (auto intro!: cInf_eq intro: dense_ge)
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, unbounded_dense_linorder}} = y"
by (auto intro!: cInf_eq intro: dense_ge_bounded)
end
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 28 23:48:45 2013 +0200
@@ -243,7 +243,7 @@
section {* The classical QE after Langford for dense linear orders *}
-context dense_linorder
+context unbounded_dense_linorder
begin
lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
@@ -299,7 +299,8 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
+ by (rule unbounded_dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
@@ -452,7 +453,7 @@
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
and between_same: "between x x = x"
-sublocale constr_dense_linorder < dlo: dense_linorder
+sublocale constr_dense_linorder < dlo: unbounded_dense_linorder
apply unfold_locales
using gt_ex lt_ex between_less
apply auto
--- a/src/HOL/Fields.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Fields.thy Wed Aug 28 23:48:45 2013 +0200
@@ -842,7 +842,7 @@
lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
by (simp add: field_simps zero_less_two)
-subclass dense_linorder
+subclass unbounded_dense_linorder
proof
fix x y :: 'a
from less_add_one show "\<exists>y. x < y" ..
--- a/src/HOL/Library/Extended_Real.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Aug 28 23:48:45 2013 +0200
@@ -293,7 +293,7 @@
lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y"
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
-instance ereal :: inner_dense_linorder
+instance ereal :: dense_linorder
by default (blast dest: ereal_dense2)
instance ereal :: ordered_ab_semigroup_add
--- a/src/HOL/Library/Float.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Float.thy Wed Aug 28 23:48:45 2013 +0200
@@ -180,7 +180,7 @@
and real_of_float_max: "real (max x y) = max (real x) (real y)"
by (simp_all add: min_def max_def)
-instance float :: dense_linorder
+instance float :: unbounded_dense_linorder
proof
fix a b :: float
show "\<exists>c. a < c"
--- a/src/HOL/Library/Liminf_Limsup.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Wed Aug 28 23:48:45 2013 +0200
@@ -9,13 +9,13 @@
begin
lemma le_Sup_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
unfolding le_SUP_iff
by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
lemma Inf_le_iff_less:
- fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+ fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
unfolding INF_le_iff
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
--- a/src/HOL/Library/While_Combinator.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy Wed Aug 28 23:48:45 2013 +0200
@@ -242,4 +242,55 @@
shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
unfolding while_def using assms by (rule lfp_the_while_option) blast
+
+text{* Computing the reflexive, transitive closure by iterating a successor
+function. Stops when an element is found that dos not satisfy the test.
+
+More refined (and hence more efficient) versions can be found in ITP 2011 paper
+by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
+and the AFP article Executable Transitive Closures by René Thiemann. *}
+
+definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
+ \<Rightarrow> ('a list * 'a set) option"
+where "rtrancl_while p f x =
+ while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
+ ((%(ws,Z).
+ let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+ in (new @ tl ws, set new \<union> insert x Z)))
+ ([x],{x})"
+
+lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
+shows "if ws = []
+ then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
+ else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
+proof-
+ let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
+ let ?step = "(%(ws,Z).
+ let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+ in (new @ tl ws, set new \<union> insert x Z))"
+ let ?R = "{(x,y). y \<in> set(f x)}"
+ let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
+ Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z)"
+ { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
+ from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
+ have "?Inv(?step (ws,Z))" using 1 2
+ by (auto intro: rtrancl.rtrancl_into_rtrancl)
+ } note inv = this
+ hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
+ apply(tactic {* split_all_tac @{context} 1 *})
+ using inv by iprover
+ moreover have "?Inv ([x],{x})" by (simp)
+ ultimately have I: "?Inv (ws,Z)"
+ by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
+ { assume "ws = []"
+ hence ?thesis using I
+ by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
+ } moreover
+ { assume "ws \<noteq> []"
+ hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
+ by (simp add: subset_iff)
+ }
+ ultimately show ?thesis by simp
+qed
+
end
--- a/src/HOL/Lifting.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Lifting.thy Wed Aug 28 23:48:45 2013 +0200
@@ -9,7 +9,7 @@
imports Equiv_Relations Transfer
keywords
"parametric" and
- "print_quotmaps" "print_quotients" :: diag and
+ "print_quot_maps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
"setup_lifting" :: thy_decl
begin
--- a/src/HOL/Orderings.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Orderings.thy Wed Aug 28 23:48:45 2013 +0200
@@ -1230,10 +1230,10 @@
subsection {* Dense orders *}
-class inner_dense_order = order +
+class dense_order = order +
assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
-class inner_dense_linorder = linorder + inner_dense_order
+class dense_linorder = linorder + dense_order
begin
lemma dense_le:
@@ -1312,7 +1312,7 @@
class no_bot = order +
assumes lt_ex: "\<exists>y. y < x"
-class dense_linorder = inner_dense_linorder + no_top + no_bot
+class unbounded_dense_linorder = dense_linorder + no_top + no_bot
subsection {* Wellorders *}
--- a/src/HOL/Probability/Borel_Space.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Aug 28 23:48:45 2013 +0200
@@ -251,7 +251,7 @@
by (blast intro: borel_open borel_closed)+
lemma open_Collect_less:
- fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+ fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
assumes "continuous_on UNIV f"
assumes "continuous_on UNIV g"
shows "open {x. f x < g x}"
@@ -264,14 +264,14 @@
qed
lemma closed_Collect_le:
- fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+ fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
assumes f: "continuous_on UNIV f"
assumes g: "continuous_on UNIV g"
shows "closed {x. f x \<le> g x}"
using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
lemma borel_measurable_less[measurable]:
- fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+ fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -285,7 +285,7 @@
qed
lemma
- fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+ fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
assumes f[measurable]: "f \<in> borel_measurable M"
assumes g[measurable]: "g \<in> borel_measurable M"
shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -755,11 +755,11 @@
by (simp add: field_divide_inverse)
lemma borel_measurable_max[measurable (raw)]:
- "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+ "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
by (simp add: max_def)
lemma borel_measurable_min[measurable (raw)]:
- "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
+ "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
by (simp add: min_def)
lemma borel_measurable_abs[measurable (raw)]:
--- a/src/HOL/Set_Interval.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Set_Interval.thy Wed Aug 28 23:48:45 2013 +0200
@@ -373,7 +373,7 @@
end
-context inner_dense_linorder
+context dense_linorder
begin
lemma greaterThanLessThan_empty_iff[simp]:
@@ -519,7 +519,7 @@
end
lemma
- fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}"
+ fixes x y :: "'a :: {complete_lattice, dense_linorder}"
shows Sup_lessThan[simp]: "Sup {..< y} = y"
and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y"
and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y"
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 23:48:45 2013 +0200
@@ -25,7 +25,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- OldSPASS |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -81,7 +80,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- OldSPASS |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -103,8 +101,7 @@
fun involving [] = ""
| involving ss =
- "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
- " "
+ " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
fun string_of_failure Unprovable = "The generated problem is unprovable."
| string_of_failure GaveUp = "The prover gave up."
@@ -114,27 +111,18 @@
"The prover claims the conjecture is a theorem but provided an incomplete \
\(or unparsable) proof."
| string_of_failure (UnsoundProof (false, ss)) =
- "The prover found an unsound proof " ^ involving ss ^
- "(or, less likely, your axioms are inconsistent). Specify a sound type \
- \encoding or omit the \"type_enc\" option."
+ "The prover derived \"False\" using" ^ involving ss ^
+ ". Specify a sound type encoding or omit the \"type_enc\" option."
| string_of_failure (UnsoundProof (true, ss)) =
- "The prover found an unsound proof " ^ involving ss ^
- "(or, less likely, your axioms are inconsistent). Please report this to \
- \the Isabelle developers."
+ "The prover derived \"False\" using" ^ involving ss ^
+ ". This could be due to inconsistent axioms (including \"sorry\"s) or to \
+ \a bug in Sledgehammer. If the problem persists, please contact the \
+ \Isabelle developers."
| string_of_failure CantConnect = "Cannot connect to remote server."
| string_of_failure TimedOut = "Timed out."
| string_of_failure Inappropriate =
"The generated problem lies outside the prover's scope."
| string_of_failure OutOfResources = "The prover ran out of resources."
- | string_of_failure OldSPASS =
- "The version of SPASS you are using is obsolete. Please upgrade to \
- \SPASS 3.8ds. To install it, download and extract the package \
- \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
- \\"spass-3.8ds\" directory's absolute path to " ^
- quote (Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"])))) ^
- " on a line of its own."
| string_of_failure NoPerl = "Perl" ^ missing_message_tail
| string_of_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 28 23:48:45 2013 +0200
@@ -529,8 +529,7 @@
|> extra_options <> "" ? prefix (extra_options ^ " "),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
- [(OldSPASS, "Unrecognized option Isabelle"),
- (GaveUp, "SPASS beiseite: Completion found"),
+ [(GaveUp, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
--- a/src/HOL/Tools/Lifting/lifting_info.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed Aug 28 23:48:45 2013 +0200
@@ -6,18 +6,15 @@
signature LIFTING_INFO =
sig
- type quotmaps = {rel_quot_thm: thm}
- val lookup_quotmaps: Proof.context -> string -> quotmaps option
- val lookup_quotmaps_global: theory -> string -> quotmaps option
- val print_quotmaps: Proof.context -> unit
-
- type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
- type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
- val transform_quotients: morphism -> quotients -> quotients
- val lookup_quotients: Proof.context -> string -> quotients option
- val lookup_quotients_global: theory -> string -> quotients option
- val update_quotients: string -> quotients -> Context.generic -> Context.generic
- val dest_quotients: Proof.context -> quotients list
+ type quot_map = {rel_quot_thm: thm}
+ val lookup_quot_maps: Proof.context -> string -> quot_map option
+ val print_quot_maps: Proof.context -> unit
+
+ type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
+ type quotient = {quot_thm: thm, pcr_info: pcr option}
+ val transform_quotient: morphism -> quotient -> quotient
+ val lookup_quotients: Proof.context -> string -> quotient option
+ val update_quotients: string -> quotient -> Context.generic -> Context.generic
val print_quotients: Proof.context -> unit
val get_invariant_commute_rules: Proof.context -> thm list
@@ -29,7 +26,10 @@
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
pos_distr_rules: thm list, neg_distr_rules: thm list}
val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
- val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
+
+ val get_quot_maps : Proof.context -> quot_map Symtab.table
+ val get_quotients : Proof.context -> quotient Symtab.table
+ val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table
val setup: theory -> theory
end;
@@ -39,23 +39,62 @@
open Lifting_Util
-(** data containers **)
+(** data container **)
+
+type quot_map = {rel_quot_thm: thm}
+type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
+type quotient = {quot_thm: thm, pcr_info: pcr option}
+type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
+ pos_distr_rules: thm list, neg_distr_rules: thm list}
+
+structure Data = Generic_Data
+(
+ type T =
+ { quot_maps : quot_map Symtab.table,
+ quotients : quotient Symtab.table,
+ reflexivity_rules : thm Item_Net.T,
+ relator_distr_data : relator_distr_data Symtab.table
+ }
+ val empty =
+ { quot_maps = Symtab.empty,
+ quotients = Symtab.empty,
+ reflexivity_rules = Thm.full_rules,
+ relator_distr_data = Symtab.empty
+ }
+ val extend = I
+ fun merge
+ ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
+ { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
+ { quot_maps = Symtab.merge (K true) (qm1, qm2),
+ quotients = Symtab.merge (K true) (q1, q2),
+ reflexivity_rules = Item_Net.merge (rr1, rr2),
+ relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
+)
+
+fun map_data f1 f2 f3 f4
+ { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
+ { quot_maps = f1 quot_maps,
+ quotients = f2 quotients,
+ reflexivity_rules = f3 reflexivity_rules,
+ relator_distr_data = f4 relator_distr_data }
+
+fun map_quot_maps f = map_data f I I I
+fun map_quotients f = map_data I f I I
+fun map_reflexivity_rules f = map_data I I f I
+fun map_relator_distr_data f = map_data I I I f
+
+val get_quot_maps' = #quot_maps o Data.get
+val get_quotients' = #quotients o Data.get
+val get_reflexivity_rules' = #reflexivity_rules o Data.get
+val get_relator_distr_data' = #relator_distr_data o Data.get
+
+fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt)
+fun get_quotients ctxt = get_quotients' (Context.Proof ctxt)
+fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
(* info about Quotient map theorems *)
-type quotmaps = {rel_quot_thm: thm}
-structure Quotmaps = Generic_Data
-(
- type T = quotmaps Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data
-)
-
-val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
-
-(* FIXME export proper internal update operation!? *)
+val lookup_quot_maps = Symtab.lookup o get_quot_maps
fun quot_map_thm_sanity_check rel_quot_thm ctxt =
let
@@ -102,14 +141,14 @@
val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
val minfo = {rel_quot_thm = rel_quot_thm}
in
- Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
+ Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt
end
val quot_map_attribute_setup =
Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
"declaration of the Quotient map theorem"
-fun print_quotmaps ctxt =
+fun print_quot_maps ctxt =
let
fun prt_map (ty_name, {rel_quot_thm}) =
Pretty.block (separate (Pretty.brk 2)
@@ -118,67 +157,49 @@
Pretty.str "quot. theorem:",
Syntax.pretty_term ctxt (prop_of rel_quot_thm)])
in
- map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
+ map prt_map (Symtab.dest (get_quot_maps ctxt))
|> Pretty.big_list "maps for type constructors:"
|> Pretty.writeln
end
(* info about quotient types *)
-type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
-type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
-
-structure Quotients = Generic_Data
-(
- type T = quotients Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data
-)
-
-fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
+fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
{pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
-fun transform_quotients phi {quot_thm, pcrel_info} =
- {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
+fun transform_quotient phi {quot_thm, pcr_info} =
+ {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
-val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
-val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
+fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
-fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
+fun update_quotients type_name qinfo ctxt =
+ Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
fun delete_quotients quot_thm ctxt =
let
val (_, qtyp) = quot_thm_rty_qty quot_thm
val qty_full_name = (fst o dest_Type) qtyp
- val symtab = Quotients.get ctxt
- val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
+ val symtab = get_quotients' ctxt
+ fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
in
- case opt_stored_quot_thm of
- SOME data =>
- if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
- Quotients.map (Symtab.delete qty_full_name) ctxt
- else
- ctxt
- | NONE => ctxt
+ if Symtab.member compare_data symtab (qty_full_name, quot_thm)
+ then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
+ else ctxt
end
-fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *)
- map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
-
fun print_quotients ctxt =
let
- fun prt_quot (qty_name, {quot_thm, pcrel_info}: quotients) =
+ fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
Pretty.block (separate (Pretty.brk 2)
[Pretty.str "type:",
Pretty.str qty_name,
Pretty.str "quot. thm:",
Syntax.pretty_term ctxt (prop_of quot_thm),
Pretty.str "pcrel_def thm:",
- option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
+ option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info,
Pretty.str "pcr_cr_eq thm:",
- option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
+ option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info])
in
- map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
+ map prt_quot (Symtab.dest (get_quotients ctxt))
|> Pretty.big_list "quotients:"
|> Pretty.writeln
end
@@ -187,6 +208,8 @@
Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
"deletes the Quotient theorem"
+(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
+
structure Invariant_Commute = Named_Thms
(
val name = @{binding invariant_commute}
@@ -197,16 +220,8 @@
(* info about reflexivity rules *)
-structure Reflexivity_Rule = Generic_Data
-(
- type T = thm Item_Net.T
- val empty = Thm.full_rules
- val extend = I
- val merge = Item_Net.merge
-)
-
-fun get_reflexivity_rules ctxt = ctxt
- |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof)
+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 =
@@ -219,7 +234,7 @@
else_conv
Conv.all_conv) ct
-fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm)
+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 #>
@@ -230,40 +245,30 @@
val relfexivity_rule_setup =
let
val name = @{binding reflexivity_rule}
- fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm)
+ 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)
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 Reflexivity_Rule.get
+ val content = Item_Net.content o get_reflexivity_rules'
in
Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
#> Global_Theory.add_thms_dynamic (name, content)
end
(* info about relator distributivity theorems *)
-type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
- pos_distr_rules: thm list, neg_distr_rules: thm list}
-fun map_relator_distr_data f1 f2 f3 f4
+fun map_relator_distr_data' f1 f2 f3 f4
{pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
{pos_mono_rule = f1 pos_mono_rule,
neg_mono_rule = f2 neg_mono_rule,
pos_distr_rules = f3 pos_distr_rules,
neg_distr_rules = f4 neg_distr_rules}
-fun map_pos_mono_rule f = map_relator_distr_data f I I I
-fun map_neg_mono_rule f = map_relator_distr_data I f I I
-fun map_pos_distr_rules f = map_relator_distr_data I I f I
-fun map_neg_distr_rules f = map_relator_distr_data I I I f
-
-structure Relator_Distr = Generic_Data
-(
- type T = relator_distr_data Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data
-);
+fun map_pos_mono_rule f = map_relator_distr_data' f I I I
+fun map_neg_mono_rule f = map_relator_distr_data' I f I I
+fun map_pos_distr_rules f = map_relator_distr_data' I I f I
+fun map_neg_distr_rules f = map_relator_distr_data' I I I f
fun introduce_polarities rule =
let
@@ -315,14 +320,14 @@
val 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
- val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name
+ 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,
pos_distr_rules = [], neg_distr_rules = []}
in
- Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
+ Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) ctxt
end;
local
@@ -331,8 +336,9 @@
val distr_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) distr_rule
in
- if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then
- Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
+ if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then
+ Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)))
+ ctxt
else error "The monoticity rule is not defined."
end
@@ -425,14 +431,13 @@
fun get_distr_rules_raw ctxt = Symtab.fold
(fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
- (Relator_Distr.get ctxt) []
+ (get_relator_distr_data' ctxt) []
fun get_mono_rules_raw ctxt = Symtab.fold
(fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
- (Relator_Distr.get ctxt) []
+ (get_relator_distr_data' ctxt) []
-val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
-val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
+val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
val relator_distr_attribute_setup =
Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
@@ -456,8 +461,8 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
- (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
+ Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
+ (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
val _ =
Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 28 23:48:45 2013 +0200
@@ -201,12 +201,12 @@
val (pcr_cr_eq, lthy) = case pcrel_def of
SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
| NONE => (NONE, lthy)
- val pcrel_info = case pcrel_def of
+ val pcr_info = case pcrel_def of
SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
| NONE => NONE
- val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
+ val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
val qty_full_name = (fst o dest_Type) qtyp
- fun quot_info phi = Lifting_Info.transform_quotients phi quotients
+ fun quot_info phi = Lifting_Info.transform_quotient phi quotients
val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
val lthy = case opt_reflp_thm of
SOME reflp_thm => lthy
@@ -376,7 +376,7 @@
reduced_assm RS thm
end
in
- fun parametrize_domain dom_thm (pcrel_info : Lifting_Info.pcrel_info) ctxt =
+ fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
let
fun reduce_first_assm ctxt rules thm =
let
@@ -386,9 +386,9 @@
reduced_assm RS thm
end
- val pcr_cr_met_eq = #pcr_cr_eq pcrel_info RS @{thm eq_reflection}
+ val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
- val pcrel_def = #pcrel_def pcrel_info
+ val pcrel_def = #pcrel_def pcr_info
val pcr_Domainp_par_left_total =
(dom_thm RS @{thm pcr_Domainp_par_left_total})
|> fold_Domainp_pcrel pcrel_def
@@ -422,7 +422,7 @@
end
fun get_pcrel_info ctxt qty_full_name =
- #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+ #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
fun get_Domainp_thm quot_thm =
the (get_first (try(curry op RS quot_thm)) [@{thm invariant_to_Domainp}, @{thm Quotient_to_Domainp}])
--- a/src/HOL/Tools/Lifting/lifting_term.ML Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed Aug 28 23:48:45 2013 +0200
@@ -75,8 +75,8 @@
end
fun get_pcrel_info ctxt s =
- case #pcrel_info (get_quot_data ctxt s) of
- SOME pcrel_info => pcrel_info
+ case #pcr_info (get_quot_data ctxt s) of
+ SOME pcr_info => pcr_info
| NONE => raise QUOT_THM_INTERNAL (Pretty.block
[Pretty.str ("No parametrized correspondce relation for " ^ quote s),
Pretty.brk 1,
@@ -100,7 +100,7 @@
let
val thy = Proof_Context.theory_of ctxt
in
- (case Lifting_Info.lookup_quotmaps ctxt s of
+ (case Lifting_Info.lookup_quot_maps ctxt s of
SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
| NONE => raise QUOT_THM_INTERNAL (Pretty.block
[Pretty.str ("No relator for the type " ^ quote s),
--- a/src/HOL/Topological_Spaces.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Aug 28 23:48:45 2013 +0200
@@ -567,7 +567,7 @@
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
unfolding eventually_at_top_linorder by auto
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
+lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
unfolding eventually_at_top_linorder
proof safe
fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
@@ -578,7 +578,7 @@
qed
lemma eventually_gt_at_top:
- "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
+ "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
unfolding eventually_at_top_dense by auto
definition at_bot :: "('a::order) filter"
@@ -600,7 +600,7 @@
unfolding eventually_at_bot_linorder by auto
lemma eventually_at_bot_dense:
- fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
+ fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
unfolding eventually_at_bot_linorder
proof safe
fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
@@ -611,7 +611,7 @@
qed
lemma eventually_gt_at_bot:
- "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
+ "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
unfolding eventually_at_bot_dense by auto
subsection {* Sequentially *}
@@ -794,11 +794,11 @@
qed
lemma trivial_limit_at_left_real [simp]:
- "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))"
+ "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
lemma trivial_limit_at_right_real [simp]:
- "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
+ "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
@@ -1047,7 +1047,7 @@
by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
lemma filterlim_at_top_dense:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
filterlim_at_top[of f F] filterlim_iff[of f at_top F])
@@ -1084,7 +1084,7 @@
qed
lemma filterlim_at_top_gt:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
@@ -1104,7 +1104,7 @@
qed simp
lemma filterlim_at_bot_lt:
- fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
+ fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
--- a/src/HOL/ex/Dedekind_Real.thy Wed Aug 28 23:41:21 2013 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Wed Aug 28 23:48:45 2013 +0200
@@ -24,7 +24,7 @@
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
lemma interval_empty_iff:
- "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+ "{y. (x::'a::unbounded_dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
by (auto dest: dense)