--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 28 23:11:07 2013 +0200
@@ -9,7 +9,7 @@
sig
type fp_sugar =
{T: typ,
- lfp: bool,
+ fp: BNF_FP_Util.fp_kind,
index: int,
pre_bnfs: BNF_Def.bnf list,
fp_res: BNF_FP_Util.fp_result,
@@ -27,11 +27,11 @@
val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
val exists_subtype_in: typ list -> typ -> bool
- val mk_co_iter: theory -> bool -> typ -> typ list -> term -> term
+ val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
- val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> int list -> int list list ->
- term list -> term list -> Proof.context ->
+ val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
+ int list list -> term list -> term list -> Proof.context ->
(term list * term list * ((term list list * typ list list * term list list list)
* (term list list * typ list list * term list list list)) option
* (term list * term list list
@@ -71,14 +71,14 @@
* (thm list list * thm list list * Args.src list)
* (thm list list * thm list list * Args.src list)
- val co_datatypes: bool -> (mixfix list -> binding list -> binding list -> binding list list ->
- binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- local_theory -> BNF_FP_Util.fp_result * local_theory) ->
+ val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
+ binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
+ BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
(bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
((((binding * binding) * (binding * typ) list) * (binding * term) list) *
mixfix) list) list ->
local_theory -> local_theory
- val parse_co_datatype_cmd: bool -> (mixfix list -> binding list -> binding list ->
+ val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
(local_theory -> local_theory) parser
@@ -97,7 +97,7 @@
type fp_sugar =
{T: typ,
- lfp: bool,
+ fp: fp_kind,
index: int,
pre_bnfs: bnf list,
fp_res: fp_result,
@@ -110,14 +110,15 @@
un_fold_thmss: thm list list,
co_rec_thmss: thm list list};
-fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
- {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
- T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
+fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
+ {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
+ T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
-fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, co_recs,
- co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} =
- {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
- fp_res = morph_fp_result phi fp_res, ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
+fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds,
+ co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} =
+ {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi)
+ pre_bnfs, fp_res = morph_fp_result phi fp_res,
+ ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds,
co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct,
strong_co_induct = Morphism.thm phi strong_co_induct,
@@ -138,11 +139,11 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
-fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs
+fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs
co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
+ register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs,
co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss,
co_rec_thmss = co_rec_thmss} lthy)) Ts
@@ -220,22 +221,22 @@
val mk_ctor = mk_ctor_or_dtor range_type;
val mk_dtor = mk_ctor_or_dtor domain_type;
-fun mk_co_iter thy lfp fpT Cs t =
+fun mk_co_iter thy fp fpT Cs t =
let
val (bindings, body) = strip_type (fastype_of t);
val (f_Cs, prebody) = split_last bindings;
- val fpT0 = if lfp then prebody else body;
- val Cs0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Cs);
+ val fpT0 = if fp = Least_FP then prebody else body;
+ val Cs0 = distinct (op =) (map (if fp = Least_FP then body_type else domain_type) f_Cs);
val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
in
Term.subst_TVars rho t
end;
-fun mk_co_iters thy lfp fpTs Cs ts0 =
+fun mk_co_iters thy fp fpTs Cs ts0 =
let
val nn = length fpTs;
val (fpTs0, Cs0) =
- map ((not lfp ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0
+ map ((fp = Greatest_FP ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0
|> split_list;
val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs);
in
@@ -244,18 +245,21 @@
val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
-fun unzip_recT fpTs T =
+fun meta_unzip_rec getT proj1 proj2 fpTs y =
+ if exists_subtype_in fpTs (getT y) then ([proj1 y], [proj2 y]) else ([y], []);
+
+fun project_co_recT special_Tname fpTs proj =
let
- fun project_recT proj =
- let
- fun project (Type (s as @{type_name prod}, Ts as [T, U])) =
- if member (op =) fpTs T then proj (T, U) else Type (s, map project Ts)
- | project (Type (s, Ts)) = Type (s, map project Ts)
- | project T = T;
- in project end;
- in
- if exists_subtype_in fpTs T then ([project_recT fst T], [project_recT snd T]) else ([T], [])
- end;
+ fun project (Type (s, Ts as T :: Ts')) =
+ if s = special_Tname andalso member (op =) fpTs T then proj (hd Ts, hd Ts')
+ else Type (s, map project Ts)
+ | project T = T;
+ in project end;
+
+val project_recT = project_co_recT @{type_name prod};
+val project_corecT = project_co_recT @{type_name sum};
+
+fun unzip_recT fpTs = meta_unzip_rec I (project_recT fpTs fst) (project_recT fpTs snd) fpTs;
fun mk_fold_fun_typess y_Tsss Cs = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
val mk_rec_fun_typess = mk_fold_fun_typess oo map o map o flat_rec o unzip_recT;
@@ -292,16 +296,9 @@
fun repair_arity [0] = [1]
| repair_arity ms = ms;
- fun project_corecT proj =
- let
- fun project (Type (s as @{type_name sum}, Ts as [T, U])) =
- if member (op =) fpTs T then proj (T, U) else Type (s, map project Ts)
- | project (Type (s, Ts)) = Type (s, map project Ts)
- | project T = T;
- in project end;
-
fun unzip_corecT T =
- if exists_subtype_in fpTs T then [project_corecT fst T, project_corecT snd T] else [T];
+ if exists_subtype_in fpTs T then [project_corecT fpTs fst T, project_corecT fpTs snd T]
+ else [T];
val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
@@ -348,17 +345,17 @@
((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
end;
-fun mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
+fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
let
val thy = Proof_Context.theory_of lthy;
- val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy lfp fpTs Cs fp_folds0
+ val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy fp fpTs Cs fp_folds0
|> `(mk_fp_iter_fun_types o hd);
- val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy lfp fpTs Cs fp_recs0
+ val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy fp fpTs Cs fp_recs0
|> `(mk_fp_iter_fun_types o hd);
val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
- if lfp then
+ if fp = Least_FP then
mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy
|>> (rpair NONE o SOME)
else
@@ -443,20 +440,12 @@
fun mk_iter_body lthy fpTs ctor_iter fss xsss =
let
- fun build_prod_proj mk_proj = build_map lthy (mk_proj o fst);
+ fun build_proj sel sel_const (x as Free (_, T)) =
+ build_map lthy (sel_const o fst) (T, project_recT fpTs sel T) $ x;
(* TODO: Avoid these complications; cf. corec case *)
- fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
- if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
- | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
- | mk_U _ T = T;
-
- fun unzip_rec (x as Free (_, T)) =
- if exists_subtype_in fpTs T then
- ([build_prod_proj fst_const (T, mk_U fst T) $ x],
- [build_prod_proj snd_const (T, mk_U snd T) $ x])
- else
- ([x], []);
+ val unzip_rec = meta_unzip_rec (snd o dest_Free) (build_proj fst fst_const)
+ (build_proj snd snd_const) fpTs;
fun mk_iter_arg f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs);
in
@@ -513,11 +502,12 @@
val [fold_def, rec_def] = map (Morphism.thm phi) defs;
- val [foldx, recx] = map (mk_co_iter thy true fpT Cs o Morphism.term phi) csts;
+ val [foldx, recx] = map (mk_co_iter thy Least_FP fpT Cs o Morphism.term phi) csts;
in
((foldx, recx, fold_def, rec_def), lthy')
end;
+(* TODO: merge with above function? *)
fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold
dtor_corec lthy0 =
let
@@ -550,7 +540,7 @@
val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
- val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts;
+ val [unfold, corec] = map (mk_co_iter thy Greatest_FP fpT Cs o Morphism.term phi) csts;
in
((unfold, corec, unfold_def, corec_def), lthy')
end ;
@@ -681,14 +671,14 @@
val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
- fun unzip_iters fiters combine (x as Free (_, T)) =
- if exists_subtype_in fpTs T then
- combine (x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x)
- else
- ([x], []);
+ fun unzip_iters fiters =
+ meta_unzip_rec (snd o dest_Free) I
+ (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (K o nth fiters))
+ (T, mk_U T) $ x) fpTs;
- val gxsss = map (map (flat_rec (unzip_iters gfolds (fn (_, t) => ([t], []))))) xsss;
- val hxsss = map (map (flat_rec (unzip_iters hrecs (pairself single)))) xsss;
+ val gxsss = map (map (flat_rec ((fn (ts, ts') => ([hd (ts' @ ts)], [])) o
+ unzip_iters gfolds))) xsss;
+ val hxsss = map (map (flat_rec (unzip_iters hrecs))) xsss;
val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
@@ -984,13 +974,15 @@
(sel_unfold_thmss, sel_corec_thmss, simp_attrs))
end;
-fun define_co_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
+fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
(wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
- val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
- else ();
+ val _ = if fp = Greatest_FP andalso no_dests then
+ error "Cannot define destructor-less codatatypes"
+ else
+ ();
fun qualify mandatory fp_b_name =
Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
@@ -1134,7 +1126,7 @@
val mss = map (map length) ctr_Tsss;
val ((fp_folds, fp_recs, fold_rec_args_types, unfold_corec_args_types), lthy) =
- mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy;
+ mk_un_fold_co_rec_prelims fp fpTs Cs ns mss fp_folds0 fp_recs0 lthy;
fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
@@ -1244,7 +1236,7 @@
val nones = replicate live NONE;
val ctor_cong =
- if lfp then
+ if fp = Least_FP then
Drule.dummy_thm
else
let val ctor' = mk_ctor Bs ctor in
@@ -1252,7 +1244,7 @@
end;
fun mk_cIn ify =
- certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
+ certify lthy o (fp = Greatest_FP ? curry (op $) (map_types ify ctor)) oo
mk_InN_balanced (ify ctr_sum_prod_T) n;
val cxIns = map2 (mk_cIn I) tuple_xs ks;
@@ -1261,15 +1253,15 @@
fun mk_map_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
(unfold_thms lthy (pre_map_def ::
- (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
+ (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
(cterm_instantiate_pos (nones @ [SOME cxIn])
- (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
+ (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
fun mk_set_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
(unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
- (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
+ (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1283,7 +1275,7 @@
fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
fold_thms lthy ctr_defs'
(unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
- (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+ (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel)
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1326,7 +1318,7 @@
in
(wrap_ctrs
#> derive_maps_sets_rels
- ##>> (if lfp then define_fold_rec (the fold_rec_args_types)
+ ##>> (if fp = Least_FP then define_fold_rec (the fold_rec_args_types)
else define_unfold_corec (the unfold_corec_args_types)) mk_binding fpTs Cs fp_fold fp_rec
#> massage_res, lthy')
end;
@@ -1370,7 +1362,7 @@
in
lthy
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars true pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm
+ |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm
induct_thm fold_thmss rec_thmss
end;
@@ -1429,8 +1421,8 @@
in
lthy
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
- |> register_fp_sugars false pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs coinduct_thm
- strong_coinduct_thm unfold_thmss corec_thmss
+ |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs
+ coinduct_thm strong_coinduct_thm unfold_thmss corec_thmss
end;
val lthy' = lthy
@@ -1440,11 +1432,11 @@
mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
raw_sel_defaultsss)
|> wrap_types_etc
- |> (if lfp then derive_and_note_induct_fold_rec_thms_for_types
+ |> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types
else derive_and_note_coinduct_unfold_corec_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
- datatype_word lfp));
+ datatype_word fp));
in
timer; lthy'
end;
@@ -1496,6 +1488,6 @@
val parse_co_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
-fun parse_co_datatype_cmd lfp construct_fp = parse_co_datatype >> co_datatype_cmd lfp construct_fp;
+fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
end;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Tue May 28 23:11:07 2013 +0200
@@ -8,6 +8,8 @@
signature BNF_FP_UTIL =
sig
+ datatype fp_kind = Least_FP | Greatest_FP
+
type fp_result =
{Ts: typ list,
bnfs: BNF_Def.bnf list,
@@ -118,7 +120,7 @@
val mk_dtor_set_inductN: int -> string
val mk_set_inductN: int -> string
- val datatype_word: bool -> string
+ val datatype_word: fp_kind -> string
val base_name_of_typ: typ -> string
val mk_common_name: string list -> string
@@ -176,6 +178,8 @@
open BNF_Def
open BNF_Util
+datatype fp_kind = Least_FP | Greatest_FP;
+
type fp_result =
{Ts: typ list,
bnfs: BNF_Def.bnf list,
@@ -318,7 +322,7 @@
val sel_unfoldN = selN ^ "_" ^ unfoldN
val sel_corecN = selN ^ "_" ^ corecN
-fun datatype_word lfp = (if lfp then "" else "co") ^ "datatype";
+fun datatype_word fp = (if fp = Greatest_FP then "co" else "") ^ "datatype";
fun add_components_of_typ (Type (s, Ts)) =
fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 28 23:11:07 2013 +0200
@@ -3122,6 +3122,6 @@
val _ =
Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
- (parse_co_datatype_cmd false construct_gfp);
+ (parse_co_datatype_cmd Greatest_FP construct_gfp);
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 28 23:11:07 2013 +0200
@@ -1866,6 +1866,6 @@
val _ =
Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
- (parse_co_datatype_cmd true construct_lfp);
+ (parse_co_datatype_cmd Least_FP construct_lfp);
end;
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Tue May 28 23:11:07 2013 +0200
@@ -188,376 +188,7 @@
qed
qed
-
-subsection {* Ordinal-like sum of two (disjoint) well-orders *}
-
-text{* This is roughly obtained by ``concatenating" the two well-orders -- thus, all elements
-of the first will be smaller than all elements of the second. This construction
-only makes sense if the fields of the two well-order relations are disjoint. *}
-
-definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60)
-where
-"r Osum r' = r \<union> r' \<union> {(a,a'). a \<in> Field r \<and> a' \<in> Field r'}"
-
-abbreviation Osum2 :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "\<union>o" 60)
-where "r \<union>o r' \<equiv> r Osum r'"
-
-lemma Field_Osum: "Field(r Osum r') = Field r \<union> Field r'"
-unfolding Osum_def Field_def by blast
-
-lemma Osum_Refl:
-assumes FLD: "Field r Int Field r' = {}" and
- REFL: "Refl r" and REFL': "Refl r'"
-shows "Refl (r Osum r')"
-using assms (* Need first unfold Field_Osum, only then Osum_def *)
-unfolding refl_on_def Field_Osum unfolding Osum_def by blast
-
-lemma Osum_trans:
-assumes FLD: "Field r Int Field r' = {}" and
- TRANS: "trans r" and TRANS': "trans r'"
-shows "trans (r Osum r')"
-proof(unfold trans_def, auto)
- fix x y z assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, z) \<in> r \<union>o r'"
- show "(x, z) \<in> r \<union>o r'"
- proof-
- {assume Case1: "(x,y) \<in> r"
- hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume Case11: "(y,z) \<in> r"
- hence "(x,z) \<in> r" using Case1 TRANS trans_def[of r] by blast
- hence ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume Case12: "(y,z) \<in> r'"
- hence "y \<in> Field r'" unfolding Field_def by auto
- hence False using FLD 1 by auto
- }
- moreover
- {assume Case13: "z \<in> Field r'"
- hence ?thesis using 1 unfolding Osum_def by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case2: "(x,y) \<in> r'"
- hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume Case21: "(y,z) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD 2 by auto
- }
- moreover
- {assume Case22: "(y,z) \<in> r'"
- hence "(x,z) \<in> r'" using Case2 TRANS' trans_def[of r'] by blast
- hence ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume Case23: "y \<in> Field r"
- hence False using FLD 2 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
- have ?thesis
- proof-
- {assume Case31: "(y,z) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD Case3 by auto
- }
- moreover
- {assume Case32: "(y,z) \<in> r'"
- hence "z \<in> Field r'" unfolding Field_def by blast
- hence ?thesis unfolding Osum_def using Case3 by auto
- }
- moreover
- {assume Case33: "y \<in> Field r"
- hence False using FLD Case3 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- ultimately show ?thesis using * unfolding Osum_def by blast
- qed
-qed
-
-lemma Osum_Preorder:
-"\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
-unfolding preorder_on_def using Osum_Refl Osum_trans by blast
-
-lemma Osum_antisym:
-assumes FLD: "Field r Int Field r' = {}" and
- AN: "antisym r" and AN': "antisym r'"
-shows "antisym (r Osum r')"
-proof(unfold antisym_def, auto)
- fix x y assume *: "(x, y) \<in> r \<union>o r'" and **: "(y, x) \<in> r \<union>o r'"
- show "x = y"
- proof-
- {assume Case1: "(x,y) \<in> r"
- hence 1: "x \<in> Field r \<and> y \<in> Field r" unfolding Field_def by auto
- have ?thesis
- proof-
- have "(y,x) \<in> r \<Longrightarrow> ?thesis"
- using Case1 AN antisym_def[of r] by blast
- moreover
- {assume "(y,x) \<in> r'"
- hence "y \<in> Field r'" unfolding Field_def by auto
- hence False using FLD 1 by auto
- }
- moreover
- have "x \<in> Field r' \<Longrightarrow> False" using FLD 1 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case2: "(x,y) \<in> r'"
- hence 2: "x \<in> Field r' \<and> y \<in> Field r'" unfolding Field_def by auto
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD 2 by auto
- }
- moreover
- have "(y,x) \<in> r' \<Longrightarrow> ?thesis"
- using Case2 AN' antisym_def[of r'] by blast
- moreover
- {assume "y \<in> Field r"
- hence False using FLD 2 by auto
- }
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- moreover
- {assume Case3: "x \<in> Field r \<and> y \<in> Field r'"
- have ?thesis
- proof-
- {assume "(y,x) \<in> r"
- hence "y \<in> Field r" unfolding Field_def by auto
- hence False using FLD Case3 by auto
- }
- moreover
- {assume Case32: "(y,x) \<in> r'"
- hence "x \<in> Field r'" unfolding Field_def by blast
- hence False using FLD Case3 by auto
- }
- moreover
- have "\<not> y \<in> Field r" using FLD Case3 by auto
- ultimately show ?thesis using ** unfolding Osum_def by blast
- qed
- }
- ultimately show ?thesis using * unfolding Osum_def by blast
- qed
-qed
-
-lemma Osum_Partial_order:
-"\<lbrakk>Field r Int Field r' = {}; Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow>
- Partial_order (r Osum r')"
-unfolding partial_order_on_def using Osum_Preorder Osum_antisym by blast
-
-lemma Osum_Total:
-assumes FLD: "Field r Int Field r' = {}" and
- TOT: "Total r" and TOT': "Total r'"
-shows "Total (r Osum r')"
-using assms
-unfolding total_on_def Field_Osum unfolding Osum_def by blast
-
-lemma Osum_Linear_order:
-"\<lbrakk>Field r Int Field r' = {}; Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow>
- Linear_order (r Osum r')"
-unfolding linear_order_on_def using Osum_Partial_order Osum_Total by blast
-
-lemma Osum_wf:
-assumes FLD: "Field r Int Field r' = {}" and
- WF: "wf r" and WF': "wf r'"
-shows "wf (r Osum r')"
-unfolding wf_eq_minimal2 unfolding Field_Osum
-proof(intro allI impI, elim conjE)
- fix A assume *: "A \<subseteq> Field r \<union> Field r'" and **: "A \<noteq> {}"
- obtain B where B_def: "B = A Int Field r" by blast
- show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r \<union>o r'"
- proof(cases "B = {}")
- assume Case1: "B \<noteq> {}"
- hence "B \<noteq> {} \<and> B \<le> Field r" using B_def by auto
- then obtain a where 1: "a \<in> B" and 2: "\<forall>a1 \<in> B. (a1,a) \<notin> r"
- using WF unfolding wf_eq_minimal2 by metis
- hence 3: "a \<in> Field r \<and> a \<notin> Field r'" using B_def FLD by auto
- (* *)
- have "\<forall>a1 \<in> A. (a1,a) \<notin> r Osum r'"
- proof(intro ballI)
- fix a1 assume **: "a1 \<in> A"
- {assume Case11: "a1 \<in> Field r"
- hence "(a1,a) \<notin> r" using B_def ** 2 by auto
- moreover
- have "(a1,a) \<notin> r'" using 3 by (auto simp add: Field_def)
- ultimately have "(a1,a) \<notin> r Osum r'"
- using 3 unfolding Osum_def by auto
- }
- moreover
- {assume Case12: "a1 \<notin> Field r"
- hence "(a1,a) \<notin> r" unfolding Field_def by auto
- moreover
- have "(a1,a) \<notin> r'" using 3 unfolding Field_def by auto
- ultimately have "(a1,a) \<notin> r Osum r'"
- using 3 unfolding Osum_def by auto
- }
- ultimately show "(a1,a) \<notin> r Osum r'" by blast
- qed
- thus ?thesis using 1 B_def by auto
- next
- assume Case2: "B = {}"
- hence 1: "A \<noteq> {} \<and> A \<le> Field r'" using * ** B_def by auto
- then obtain a' where 2: "a' \<in> A" and 3: "\<forall>a1' \<in> A. (a1',a') \<notin> r'"
- using WF' unfolding wf_eq_minimal2 by metis
- hence 4: "a' \<in> Field r' \<and> a' \<notin> Field r" using 1 FLD by blast
- (* *)
- have "\<forall>a1' \<in> A. (a1',a') \<notin> r Osum r'"
- proof(unfold Osum_def, auto simp add: 3)
- fix a1' assume "(a1', a') \<in> r"
- thus False using 4 unfolding Field_def by blast
- next
- fix a1' assume "a1' \<in> A" and "a1' \<in> Field r"
- thus False using Case2 B_def by auto
- qed
- thus ?thesis using 2 by blast
- qed
-qed
-
-lemma Osum_minus_Id:
-assumes TOT: "Total r" and TOT': "Total r'" and
- NID: "\<not> (r \<le> Id)" and NID': "\<not> (r' \<le> Id)"
-shows "(r Osum r') - Id \<le> (r - Id) Osum (r' - Id)"
-proof-
- {fix a a' assume *: "(a,a') \<in> (r Osum r')" and **: "a \<noteq> a'"
- have "(a,a') \<in> (r - Id) Osum (r' - Id)"
- proof-
- {assume "(a,a') \<in> r \<or> (a,a') \<in> r'"
- with ** have ?thesis unfolding Osum_def by auto
- }
- moreover
- {assume "a \<in> Field r \<and> a' \<in> Field r'"
- hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
- using assms Total_Id_Field by blast
- hence ?thesis unfolding Osum_def by auto
- }
- ultimately show ?thesis using * unfolding Osum_def by blast
- qed
- }
- thus ?thesis by(auto simp add: Osum_def)
-qed
-
-lemma wf_Int_Times:
-assumes "A Int B = {}"
-shows "wf(A \<times> B)"
-proof(unfold wf_def mem_Sigma_iff, intro impI allI)
- fix P x
- assume *: "\<forall>x. (\<forall>y. y \<in> A \<and> x \<in> B \<longrightarrow> P y) \<longrightarrow> P x"
- moreover have "\<forall>y \<in> A. P y" using assms * by blast
- ultimately show "P x" using * by (case_tac "x \<in> B") blast+
-qed
-
-lemma Osum_minus_Id1:
-assumes "r \<le> Id"
-shows "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
-proof-
- let ?Left = "(r Osum r') - Id"
- let ?Right = "(r' - Id) \<union> (Field r \<times> Field r')"
- {fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r'"
- with * have "(a,b) \<in> r' - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
- }
- thus ?thesis by auto
-qed
-
-lemma Osum_minus_Id2:
-assumes "r' \<le> Id"
-shows "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
-proof-
- let ?Left = "(r Osum r') - Id"
- let ?Right = "(r - Id) \<union> (Field r \<times> Field r')"
- {fix a::'a and b assume *: "(a,b) \<notin> Id"
- {assume "(a,b) \<in> r'"
- with * have False using assms by auto
- }
- moreover
- {assume "(a,b) \<in> r"
- with * have "(a,b) \<in> r - Id" by auto
- }
- ultimately
- have "(a,b) \<in> ?Left \<Longrightarrow> (a,b) \<in> ?Right"
- unfolding Osum_def by auto
- }
- thus ?thesis by auto
-qed
-
-lemma Osum_wf_Id:
-assumes TOT: "Total r" and TOT': "Total r'" and
- FLD: "Field r Int Field r' = {}" and
- WF: "wf(r - Id)" and WF': "wf(r' - Id)"
-shows "wf ((r Osum r') - Id)"
-proof(cases "r \<le> Id \<or> r' \<le> Id")
- assume Case1: "\<not>(r \<le> Id \<or> r' \<le> Id)"
- have "Field(r - Id) Int Field(r' - Id) = {}"
- using FLD mono_Field[of "r - Id" r] mono_Field[of "r' - Id" r']
- Diff_subset[of r Id] Diff_subset[of r' Id] by blast
- thus ?thesis
- using Case1 Osum_minus_Id[of r r'] assms Osum_wf[of "r - Id" "r' - Id"]
- wf_subset[of "(r - Id) \<union>o (r' - Id)" "(r Osum r') - Id"] by auto
-next
- have 1: "wf(Field r \<times> Field r')"
- using FLD by (auto simp add: wf_Int_Times)
- assume Case2: "r \<le> Id \<or> r' \<le> Id"
- moreover
- {assume Case21: "r \<le> Id"
- hence "(r Osum r') - Id \<le> (r' - Id) \<union> (Field r \<times> Field r')"
- using Osum_minus_Id1[of r r'] by simp
- moreover
- {have "Domain(Field r \<times> Field r') Int Range(r' - Id) = {}"
- using FLD unfolding Field_def by blast
- hence "wf((r' - Id) \<union> (Field r \<times> Field r'))"
- using 1 WF' wf_Un[of "Field r \<times> Field r'" "r' - Id"]
- by (auto simp add: Un_commute)
- }
- ultimately have ?thesis by (auto simp add: wf_subset)
- }
- moreover
- {assume Case22: "r' \<le> Id"
- hence "(r Osum r') - Id \<le> (r - Id) \<union> (Field r \<times> Field r')"
- using Osum_minus_Id2[of r' r] by simp
- moreover
- {have "Range(Field r \<times> Field r') Int Domain(r - Id) = {}"
- using FLD unfolding Field_def by blast
- hence "wf((r - Id) \<union> (Field r \<times> Field r'))"
- using 1 WF wf_Un[of "r - Id" "Field r \<times> Field r'"]
- by (auto simp add: Un_commute)
- }
- ultimately have ?thesis by (auto simp add: wf_subset)
- }
- ultimately show ?thesis by blast
-qed
-
-lemma Osum_Well_order:
-assumes FLD: "Field r Int Field r' = {}" and
- WELL: "Well_order r" and WELL': "Well_order r'"
-shows "Well_order (r Osum r')"
-proof-
- have "Total r \<and> Total r'" using WELL WELL'
- by (auto simp add: order_on_defs)
- thus ?thesis using assms unfolding well_order_on_def
- using Osum_Linear_order Osum_wf_Id by blast
-qed
+(* More facts on ordinal sum: *)
lemma Osum_embed:
assumes FLD: "Field r Int Field r' = {}" and
--- a/src/HOL/Library/Order_Union.thy Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Library/Order_Union.thy Tue May 28 23:11:07 2013 +0200
@@ -1,8 +1,7 @@
(* Title: HOL/Library/Order_Union.thy
Author: Andrei Popescu, TU Muenchen
-Subset of Constructions_on_Wellorders that provides the ordinal sum but does
-not rely on the ~/HOL/Library/Zorn.thy.
+The ordinal-like sum of two orders with disjoint fields
*)
header {* Order Union *}
--- a/src/HOL/Library/Well_Order_Extension.thy Tue May 28 23:06:32 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-(* Title: HOL/Library/Well_Order_Extension.thy
- Author: Christian Sternagel, JAIST
-*)
-
-header {*Extending Well-founded Relations to Well-Orders.*}
-
-theory Well_Order_Extension
-imports Zorn Order_Union
-begin
-
-text {*A \emph{downset} (also lower set, decreasing set, initial segment, or
-downward closed set) is closed w.r.t.\ smaller elements.*}
-definition downset_on where
- "downset_on A r = (\<forall>x y. (x, y) \<in> r \<and> y \<in> A \<longrightarrow> x \<in> A)"
-
-(*
-text {*Connection to order filters of the @{theory Cardinals} theory.*}
-lemma (in wo_rel) ofilter_downset_on_conv:
- "ofilter A \<longleftrightarrow> downset_on A r \<and> A \<subseteq> Field r"
- by (auto simp: downset_on_def ofilter_def under_def)
-*)
-
-lemma downset_onI:
- "(\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> downset_on A r"
- by (auto simp: downset_on_def)
-
-lemma downset_onD:
- "downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A"
- by (auto simp: downset_on_def)
-
-text {*Extensions of relations w.r.t.\ a given set.*}
-definition extension_on where
- "extension_on A r s = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> s \<longrightarrow> (x, y) \<in> r)"
-
-lemma extension_onI:
- "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r) \<Longrightarrow> extension_on A r s"
- by (auto simp: extension_on_def)
-
-lemma extension_onD:
- "extension_on A r s \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> s \<Longrightarrow> (x, y) \<in> r"
- by (auto simp: extension_on_def)
-
-lemma downset_on_Union:
- assumes "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p"
- shows "downset_on (Field (\<Union>R)) p"
- using assms by (auto intro: downset_onI dest: downset_onD)
-
-lemma chain_subset_extension_on_Union:
- assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
- shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
- using assms
- by (simp add: chain_subset_def extension_on_def)
- (metis Field_def mono_Field set_mp)
-
-lemma downset_on_empty [simp]: "downset_on {} p"
- by (auto simp: downset_on_def)
-
-lemma extension_on_empty [simp]: "extension_on {} p q"
- by (auto simp: extension_on_def)
-
-text {*Every well-founded relation can be extended to a well-order.*}
-theorem well_order_extension:
- assumes "wf p"
- shows "\<exists>w. p \<subseteq> w \<and> Well_order w"
-proof -
- let ?K = "{r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p}"
- def I \<equiv> "init_seg_of \<inter> ?K \<times> ?K"
- have I_init: "I \<subseteq> init_seg_of" by (simp add: I_def)
- then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
- by (auto simp: init_seg_of_def chain_subset_def Chains_def)
- have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow>
- Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p"
- by (simp add: Chains_def I_def) blast
- have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def)
- then have 0: "Partial_order I"
- by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
- trans_def I_def elim: trans_init_seg_of)
- { fix R assume "R \<in> Chains I"
- then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
- have subch: "chain\<^sub>\<subseteq> R" using `R \<in> Chains I` I_init
- by (auto simp: init_seg_of_def chain_subset_def Chains_def)
- have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and
- "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" and
- "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and
- "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
- using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
- have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def)
- moreover have "trans (\<Union>R)"
- by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
- moreover have "antisym (\<Union>R)"
- by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`])
- moreover have "Total (\<Union>R)"
- by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`])
- moreover have "wf ((\<Union>R) - Id)"
- proof -
- have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
- with `\<forall>r\<in>R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
- show ?thesis by (simp (no_asm_simp)) blast
- qed
- ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs)
- moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris
- by (simp add: Chains_init_seg_of_Union)
- moreover have "downset_on (Field (\<Union>R)) p"
- by (rule downset_on_Union [OF `\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p`])
- moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p"
- by (rule chain_subset_extension_on_Union [OF subch `\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p`])
- ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)"
- using mono_Chains [OF I_init] and `R \<in> Chains I`
- by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
- }
- then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
- txt {*Zorn's Lemma yields a maximal well-order m.*}
- from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set"
- where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and
- max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and>
- (m, r) \<in> I \<longrightarrow> r = m"
- by (auto simp: FI)
- have "Field p \<subseteq> Field m"
- proof (rule ccontr)
- let ?Q = "Field p - Field m"
- assume "\<not> (Field p \<subseteq> Field m)"
- with assms [unfolded wf_eq_minimal, THEN spec, of ?Q]
- obtain x where "x \<in> Field p" and "x \<notin> Field m" and
- min: "\<forall>y. (y, x) \<in> p \<longrightarrow> y \<notin> ?Q" by blast
- txt {*Add @{term x} as topmost element to @{term m}.*}
- let ?s = "{(y, x) | y. y \<in> Field m}"
- let ?m = "insert (x, x) m \<union> ?s"
- have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def)
- have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
- using `Well_order m` by (simp_all add: order_on_defs)
- txt {*We show that the extension is a well-order.*}
- have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def)
- moreover have "trans ?m" using `trans m` `x \<notin> Field m`
- unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
- moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
- unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast
- moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def)
- moreover have "wf (?m - Id)"
- proof -
- have "wf ?s" using `x \<notin> Field m`
- by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
- thus ?thesis using `wf (m - Id)` `x \<notin> Field m`
- wf_subset [OF `wf ?s` Diff_subset]
- by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
- qed
- ultimately have "Well_order ?m" by (simp add: order_on_defs)
- moreover have "extension_on (Field ?m) ?m p"
- using `extension_on (Field m) m p` `downset_on (Field m) p`
- by (subst Fm) (auto simp: extension_on_def dest: downset_onD)
- moreover have "downset_on (Field ?m) p"
- using `downset_on (Field m) p` and min
- by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff)
- moreover have "(m, ?m) \<in> I"
- using `Well_order m` and `Well_order ?m` and
- `downset_on (Field m) p` and `downset_on (Field ?m) p` and
- `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and
- `Refl m` and `x \<notin> Field m`
- by (auto simp: I_def init_seg_of_def refl_on_def)
- ultimately
- --{*This contradicts maximality of m:*}
- show False using max and `x \<notin> Field m` unfolding Field_def by blast
- qed
- have "p \<subseteq> m"
- using `Field p \<subseteq> Field m` and `extension_on (Field m) m p`
- by (force simp: Field_def extension_on_def)
- with `Well_order m` show ?thesis by blast
-qed
-
-text {*Every well-founded relation can be extended to a total well-order.*}
-corollary total_well_order_extension:
- assumes "wf p"
- shows "\<exists>w. p \<subseteq> w \<and> Well_order w \<and> Field w = UNIV"
-proof -
- from well_order_extension [OF assms] obtain w
- where "p \<subseteq> w" and wo: "Well_order w" by blast
- let ?A = "UNIV - Field w"
- from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..
- have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp
- have *: "Field w \<inter> Field w' = {}" by simp
- let ?w = "w \<union>o w'"
- have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def)
- moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp
- moreover have "Field ?w = UNIV" by (simp add: Field_Osum)
- ultimately show ?thesis by blast
-qed
-
-corollary well_order_on_extension:
- assumes "wf p" and "Field p \<subseteq> A"
- shows "\<exists>w. p \<subseteq> w \<and> well_order_on A w"
-proof -
- from total_well_order_extension [OF `wf p`] obtain r
- where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast
- let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
- from `p \<subseteq> r` have "p \<subseteq> ?r" using `Field p \<subseteq> A` by (auto simp: Field_def)
- have 1: "Field ?r = A" using wo univ
- by (fastforce simp: Field_def order_on_defs refl_on_def)
- have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
- using `Well_order r` by (simp_all add: order_on_defs)
- have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ)
- moreover have "trans ?r" using `trans r`
- unfolding trans_def by blast
- moreover have "antisym ?r" using `antisym r`
- unfolding antisym_def by blast
- moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ)
- moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast
- ultimately have "well_order_on A ?r" by (simp add: order_on_defs)
- with `p \<subseteq> ?r` show ?thesis by blast
-qed
-
-end
-
--- a/src/HOL/Library/Zorn.thy Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Library/Zorn.thy Tue May 28 23:11:07 2013 +0200
@@ -5,12 +5,13 @@
Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
The well-ordering theorem.
+The extension of any well-founded relation to a well-order.
*)
header {* Zorn's Lemma *}
theory Zorn
-imports Order_Relation
+imports Order_Union
begin
subsection {* Zorn's Lemma for the Subset Relation *}
@@ -712,5 +713,206 @@
with 1 show ?thesis by metis
qed
+subsection {* Extending Well-founded Relations to Well-Orders *}
+
+text {*A \emph{downset} (also lower set, decreasing set, initial segment, or
+downward closed set) is closed w.r.t.\ smaller elements.*}
+definition downset_on where
+ "downset_on A r = (\<forall>x y. (x, y) \<in> r \<and> y \<in> A \<longrightarrow> x \<in> A)"
+
+(*
+text {*Connection to order filters of the @{theory Cardinals} theory.*}
+lemma (in wo_rel) ofilter_downset_on_conv:
+ "ofilter A \<longleftrightarrow> downset_on A r \<and> A \<subseteq> Field r"
+ by (auto simp: downset_on_def ofilter_def under_def)
+*)
+
+lemma downset_onI:
+ "(\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> downset_on A r"
+ by (auto simp: downset_on_def)
+
+lemma downset_onD:
+ "downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A"
+ by (auto simp: downset_on_def)
+
+text {*Extensions of relations w.r.t.\ a given set.*}
+definition extension_on where
+ "extension_on A r s = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> s \<longrightarrow> (x, y) \<in> r)"
+
+lemma extension_onI:
+ "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r) \<Longrightarrow> extension_on A r s"
+ by (auto simp: extension_on_def)
+
+lemma extension_onD:
+ "extension_on A r s \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> s \<Longrightarrow> (x, y) \<in> r"
+ by (auto simp: extension_on_def)
+
+lemma downset_on_Union:
+ assumes "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p"
+ shows "downset_on (Field (\<Union>R)) p"
+ using assms by (auto intro: downset_onI dest: downset_onD)
+
+lemma chain_subset_extension_on_Union:
+ assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
+ shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
+ using assms
+ by (simp add: chain_subset_def extension_on_def)
+ (metis Field_def mono_Field set_mp)
+
+lemma downset_on_empty [simp]: "downset_on {} p"
+ by (auto simp: downset_on_def)
+
+lemma extension_on_empty [simp]: "extension_on {} p q"
+ by (auto simp: extension_on_def)
+
+text {*Every well-founded relation can be extended to a well-order.*}
+theorem well_order_extension:
+ assumes "wf p"
+ shows "\<exists>w. p \<subseteq> w \<and> Well_order w"
+proof -
+ let ?K = "{r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p}"
+ def I \<equiv> "init_seg_of \<inter> ?K \<times> ?K"
+ have I_init: "I \<subseteq> init_seg_of" by (simp add: I_def)
+ then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
+ by (auto simp: init_seg_of_def chain_subset_def Chains_def)
+ have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow>
+ Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p"
+ by (simp add: Chains_def I_def) blast
+ have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def)
+ then have 0: "Partial_order I"
+ by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
+ trans_def I_def elim: trans_init_seg_of)
+ { fix R assume "R \<in> Chains I"
+ then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
+ have subch: "chain\<^sub>\<subseteq> R" using `R \<in> Chains I` I_init
+ by (auto simp: init_seg_of_def chain_subset_def Chains_def)
+ have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and
+ "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" and
+ "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and
+ "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
+ using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
+ have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def)
+ moreover have "trans (\<Union>R)"
+ by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
+ moreover have "antisym (\<Union>R)"
+ by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`])
+ moreover have "Total (\<Union>R)"
+ by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`])
+ moreover have "wf ((\<Union>R) - Id)"
+ proof -
+ have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
+ with `\<forall>r\<in>R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
+ show ?thesis by (simp (no_asm_simp)) blast
+ qed
+ ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs)
+ moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris
+ by (simp add: Chains_init_seg_of_Union)
+ moreover have "downset_on (Field (\<Union>R)) p"
+ by (rule downset_on_Union [OF `\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p`])
+ moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p"
+ by (rule chain_subset_extension_on_Union [OF subch `\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p`])
+ ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)"
+ using mono_Chains [OF I_init] and `R \<in> Chains I`
+ by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
+ }
+ then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
+ txt {*Zorn's Lemma yields a maximal well-order m.*}
+ from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set"
+ where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and
+ max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and>
+ (m, r) \<in> I \<longrightarrow> r = m"
+ by (auto simp: FI)
+ have "Field p \<subseteq> Field m"
+ proof (rule ccontr)
+ let ?Q = "Field p - Field m"
+ assume "\<not> (Field p \<subseteq> Field m)"
+ with assms [unfolded wf_eq_minimal, THEN spec, of ?Q]
+ obtain x where "x \<in> Field p" and "x \<notin> Field m" and
+ min: "\<forall>y. (y, x) \<in> p \<longrightarrow> y \<notin> ?Q" by blast
+ txt {*Add @{term x} as topmost element to @{term m}.*}
+ let ?s = "{(y, x) | y. y \<in> Field m}"
+ let ?m = "insert (x, x) m \<union> ?s"
+ have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def)
+ have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
+ using `Well_order m` by (simp_all add: order_on_defs)
+ txt {*We show that the extension is a well-order.*}
+ have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def)
+ moreover have "trans ?m" using `trans m` `x \<notin> Field m`
+ unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
+ moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
+ unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast
+ moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def)
+ moreover have "wf (?m - Id)"
+ proof -
+ have "wf ?s" using `x \<notin> Field m`
+ by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
+ thus ?thesis using `wf (m - Id)` `x \<notin> Field m`
+ wf_subset [OF `wf ?s` Diff_subset]
+ by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
+ qed
+ ultimately have "Well_order ?m" by (simp add: order_on_defs)
+ moreover have "extension_on (Field ?m) ?m p"
+ using `extension_on (Field m) m p` `downset_on (Field m) p`
+ by (subst Fm) (auto simp: extension_on_def dest: downset_onD)
+ moreover have "downset_on (Field ?m) p"
+ using `downset_on (Field m) p` and min
+ by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff)
+ moreover have "(m, ?m) \<in> I"
+ using `Well_order m` and `Well_order ?m` and
+ `downset_on (Field m) p` and `downset_on (Field ?m) p` and
+ `extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and
+ `Refl m` and `x \<notin> Field m`
+ by (auto simp: I_def init_seg_of_def refl_on_def)
+ ultimately
+ --{*This contradicts maximality of m:*}
+ show False using max and `x \<notin> Field m` unfolding Field_def by blast
+ qed
+ have "p \<subseteq> m"
+ using `Field p \<subseteq> Field m` and `extension_on (Field m) m p`
+ by (force simp: Field_def extension_on_def)
+ with `Well_order m` show ?thesis by blast
+qed
+
+text {*Every well-founded relation can be extended to a total well-order.*}
+corollary total_well_order_extension:
+ assumes "wf p"
+ shows "\<exists>w. p \<subseteq> w \<and> Well_order w \<and> Field w = UNIV"
+proof -
+ from well_order_extension [OF assms] obtain w
+ where "p \<subseteq> w" and wo: "Well_order w" by blast
+ let ?A = "UNIV - Field w"
+ from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..
+ have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp
+ have *: "Field w \<inter> Field w' = {}" by simp
+ let ?w = "w \<union>o w'"
+ have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def)
+ moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp
+ moreover have "Field ?w = UNIV" by (simp add: Field_Osum)
+ ultimately show ?thesis by blast
+qed
+
+corollary well_order_on_extension:
+ assumes "wf p" and "Field p \<subseteq> A"
+ shows "\<exists>w. p \<subseteq> w \<and> well_order_on A w"
+proof -
+ from total_well_order_extension [OF `wf p`] obtain r
+ where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast
+ let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
+ from `p \<subseteq> r` have "p \<subseteq> ?r" using `Field p \<subseteq> A` by (auto simp: Field_def)
+ have 1: "Field ?r = A" using wo univ
+ by (fastforce simp: Field_def order_on_defs refl_on_def)
+ have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
+ using `Well_order r` by (simp_all add: order_on_defs)
+ have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ)
+ moreover have "trans ?r" using `trans r`
+ unfolding trans_def by blast
+ moreover have "antisym ?r" using `antisym r`
+ unfolding antisym_def by blast
+ moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ)
+ moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast
+ ultimately have "well_order_on A ?r" by (simp add: order_on_defs)
+ with `p \<subseteq> ?r` show ?thesis by blast
+qed
+
end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue May 28 23:11:07 2013 +0200
@@ -544,8 +544,7 @@
val min_univ_card =
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
(univ_card nat_card int_card main_j0 [] KK.True)
- val _ = if debug then ()
- else check_arity guiltiest_party min_univ_card min_highest_arity
+ val _ = check_arity guiltiest_party min_univ_card min_highest_arity
val def_us =
def_us |> map (choose_reps_in_nut scope unsound rep_table true)
@@ -612,7 +611,7 @@
fold Integer.max (map (fst o fst) (maps fst bounds)) 0
val formula = fold_rev s_and axioms formula
val _ = if bits = 0 then () else check_bits bits formula
- val _ = if debug orelse formula = KK.False then ()
+ val _ = if formula = KK.False then ()
else check_arity "" univ_card highest_arity
in
SOME ({comment = comment, settings = settings, univ_card = univ_card,
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue May 28 23:11:07 2013 +0200
@@ -311,7 +311,6 @@
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
val sel_prefix = nitpick_prefix ^ "sel"
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
-val set_prefix = nitpick_prefix ^ "set" ^ name_sep
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
@@ -560,7 +559,8 @@
type typedef_info =
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option}
+ prop_of_Rep: thm, set_name: string option, Abs_inverse: thm option,
+ Rep_inverse: thm option}
fun typedef_info ctxt s =
if is_frac_type ctxt (Type (s, [])) then
@@ -569,8 +569,7 @@
Rep_name = @{const_name Nitpick.Rep_Frac},
prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
|> Logic.varify_global,
- set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE,
- Rep_inverse = NONE}
+ Abs_inverse = NONE, Rep_inverse = NONE}
else case Typedef.get_info ctxt s of
(* When several entries are returned, it shouldn't matter much which one
we take (according to Florian Haftmann). *)
@@ -582,8 +581,7 @@
SOME {abs_type = Logic.varifyT_global abs_type,
rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
Rep_name = Rep_name, prop_of_Rep = prop_of Rep,
- set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
- Rep_inverse = SOME Rep_inverse}
+ Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse}
| _ => NONE
val is_typedef = is_some oo typedef_info
@@ -1954,20 +1952,18 @@
if is_univ_typedef ctxt abs_T then
[]
else case typedef_info ctxt abs_s of
- SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
+ SOME {abs_type, rep_type, Rep_name, prop_of_Rep, ...} =>
let
val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type
val rep_t = Const (Rep_name, abs_T --> rep_T)
- val set_t = Const (set_name, HOLogic.mk_setT rep_T)
- val set_t' =
+ val set_t =
prop_of_Rep |> HOLogic.dest_Trueprop
|> specialize_type thy (dest_Const rep_t)
|> HOLogic.dest_mem |> snd
in
[HOLogic.all_const abs_T
- $ Abs (Name.uu, abs_T, HOLogic.mk_mem (rep_t $ Bound 0, set_t))]
- |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
- |> map HOLogic.mk_Trueprop
+ $ Abs (Name.uu, abs_T, HOLogic.mk_mem (rep_t $ Bound 0, set_t))
+ |> HOLogic.mk_Trueprop]
end
| NONE => []
end
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue May 28 23:06:32 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue May 28 23:11:07 2013 +0200
@@ -104,7 +104,7 @@
else
" of Kodkod relation associated with " ^
quote (original_name guilty_party)) ^
- " too large for universe of cardinality " ^
+ " too large for a universe of size " ^
string_of_int univ_card)
else
()