# HG changeset patch # User wenzelm # Date 1369775467 -7200 # Node ID afe61eefdc61cebf2c791ceca5a47c07579aa0c4 # Parent 8b2c3e548a2010dacb73239a617d0110ad8fc141# Parent 66bc827e37f88e1b6f79654780954ea3c9e6b0d1 merged diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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; diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/BNF/Tools/bnf_fp_util.ML --- 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) diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/BNF/Tools/bnf_gfp.ML --- 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; diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/BNF/Tools/bnf_lfp.ML --- 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; diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Cardinals/Constructions_on_Wellorders.thy --- 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 \ 'a rel \ 'a rel" (infix "Osum" 60) -where -"r Osum r' = r \ r' \ {(a,a'). a \ Field r \ a' \ Field r'}" - -abbreviation Osum2 :: "'a rel \ 'a rel \ 'a rel" (infix "\o" 60) -where "r \o r' \ r Osum r'" - -lemma Field_Osum: "Field(r Osum r') = Field r \ 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) \ r \o r'" and **: "(y, z) \ r \o r'" - show "(x, z) \ r \o r'" - proof- - {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - {assume Case11: "(y,z) \ r" - hence "(x,z) \ r" using Case1 TRANS trans_def[of r] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case12: "(y,z) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - {assume Case13: "z \ 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) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume Case21: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - {assume Case22: "(y,z) \ r'" - hence "(x,z) \ r'" using Case2 TRANS' trans_def[of r'] by blast - hence ?thesis unfolding Osum_def by auto - } - moreover - {assume Case23: "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume Case31: "(y,z) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,z) \ r'" - hence "z \ Field r'" unfolding Field_def by blast - hence ?thesis unfolding Osum_def using Case3 by auto - } - moreover - {assume Case33: "y \ 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: -"\Field r Int Field r' = {}; Preorder r; Preorder r'\ \ 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) \ r \o r'" and **: "(y, x) \ r \o r'" - show "x = y" - proof- - {assume Case1: "(x,y) \ r" - hence 1: "x \ Field r \ y \ Field r" unfolding Field_def by auto - have ?thesis - proof- - have "(y,x) \ r \ ?thesis" - using Case1 AN antisym_def[of r] by blast - moreover - {assume "(y,x) \ r'" - hence "y \ Field r'" unfolding Field_def by auto - hence False using FLD 1 by auto - } - moreover - have "x \ Field r' \ False" using FLD 1 by auto - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case2: "(x,y) \ r'" - hence 2: "x \ Field r' \ y \ Field r'" unfolding Field_def by auto - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD 2 by auto - } - moreover - have "(y,x) \ r' \ ?thesis" - using Case2 AN' antisym_def[of r'] by blast - moreover - {assume "y \ Field r" - hence False using FLD 2 by auto - } - ultimately show ?thesis using ** unfolding Osum_def by blast - qed - } - moreover - {assume Case3: "x \ Field r \ y \ Field r'" - have ?thesis - proof- - {assume "(y,x) \ r" - hence "y \ Field r" unfolding Field_def by auto - hence False using FLD Case3 by auto - } - moreover - {assume Case32: "(y,x) \ r'" - hence "x \ Field r'" unfolding Field_def by blast - hence False using FLD Case3 by auto - } - moreover - have "\ y \ 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: -"\Field r Int Field r' = {}; Partial_order r; Partial_order r'\ \ - 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: -"\Field r Int Field r' = {}; Linear_order r; Linear_order r'\ \ - 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 \ Field r \ Field r'" and **: "A \ {}" - obtain B where B_def: "B = A Int Field r" by blast - show "\a\A. \a'\A. (a', a) \ r \o r'" - proof(cases "B = {}") - assume Case1: "B \ {}" - hence "B \ {} \ B \ Field r" using B_def by auto - then obtain a where 1: "a \ B" and 2: "\a1 \ B. (a1,a) \ r" - using WF unfolding wf_eq_minimal2 by metis - hence 3: "a \ Field r \ a \ Field r'" using B_def FLD by auto - (* *) - have "\a1 \ A. (a1,a) \ r Osum r'" - proof(intro ballI) - fix a1 assume **: "a1 \ A" - {assume Case11: "a1 \ Field r" - hence "(a1,a) \ r" using B_def ** 2 by auto - moreover - have "(a1,a) \ r'" using 3 by (auto simp add: Field_def) - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto - } - moreover - {assume Case12: "a1 \ Field r" - hence "(a1,a) \ r" unfolding Field_def by auto - moreover - have "(a1,a) \ r'" using 3 unfolding Field_def by auto - ultimately have "(a1,a) \ r Osum r'" - using 3 unfolding Osum_def by auto - } - ultimately show "(a1,a) \ r Osum r'" by blast - qed - thus ?thesis using 1 B_def by auto - next - assume Case2: "B = {}" - hence 1: "A \ {} \ A \ Field r'" using * ** B_def by auto - then obtain a' where 2: "a' \ A" and 3: "\a1' \ A. (a1',a') \ r'" - using WF' unfolding wf_eq_minimal2 by metis - hence 4: "a' \ Field r' \ a' \ Field r" using 1 FLD by blast - (* *) - have "\a1' \ A. (a1',a') \ r Osum r'" - proof(unfold Osum_def, auto simp add: 3) - fix a1' assume "(a1', a') \ r" - thus False using 4 unfolding Field_def by blast - next - fix a1' assume "a1' \ A" and "a1' \ 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: "\ (r \ Id)" and NID': "\ (r' \ Id)" -shows "(r Osum r') - Id \ (r - Id) Osum (r' - Id)" -proof- - {fix a a' assume *: "(a,a') \ (r Osum r')" and **: "a \ a'" - have "(a,a') \ (r - Id) Osum (r' - Id)" - proof- - {assume "(a,a') \ r \ (a,a') \ r'" - with ** have ?thesis unfolding Osum_def by auto - } - moreover - {assume "a \ Field r \ a' \ Field r'" - hence "a \ Field(r - Id) \ a' \ 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 \ B)" -proof(unfold wf_def mem_Sigma_iff, intro impI allI) - fix P x - assume *: "\x. (\y. y \ A \ x \ B \ P y) \ P x" - moreover have "\y \ A. P y" using assms * by blast - ultimately show "P x" using * by (case_tac "x \ B") blast+ -qed - -lemma Osum_minus_Id1: -assumes "r \ Id" -shows "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" -proof- - let ?Left = "(r Osum r') - Id" - let ?Right = "(r' - Id) \ (Field r \ Field r')" - {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r'" - with * have "(a,b) \ r' - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?Right" - unfolding Osum_def by auto - } - thus ?thesis by auto -qed - -lemma Osum_minus_Id2: -assumes "r' \ Id" -shows "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" -proof- - let ?Left = "(r Osum r') - Id" - let ?Right = "(r - Id) \ (Field r \ Field r')" - {fix a::'a and b assume *: "(a,b) \ Id" - {assume "(a,b) \ r'" - with * have False using assms by auto - } - moreover - {assume "(a,b) \ r" - with * have "(a,b) \ r - Id" by auto - } - ultimately - have "(a,b) \ ?Left \ (a,b) \ ?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 \ Id \ r' \ Id") - assume Case1: "\(r \ Id \ r' \ 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) \o (r' - Id)" "(r Osum r') - Id"] by auto -next - have 1: "wf(Field r \ Field r')" - using FLD by (auto simp add: wf_Int_Times) - assume Case2: "r \ Id \ r' \ Id" - moreover - {assume Case21: "r \ Id" - hence "(r Osum r') - Id \ (r' - Id) \ (Field r \ Field r')" - using Osum_minus_Id1[of r r'] by simp - moreover - {have "Domain(Field r \ Field r') Int Range(r' - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r' - Id) \ (Field r \ Field r'))" - using 1 WF' wf_Un[of "Field r \ Field r'" "r' - Id"] - by (auto simp add: Un_commute) - } - ultimately have ?thesis by (auto simp add: wf_subset) - } - moreover - {assume Case22: "r' \ Id" - hence "(r Osum r') - Id \ (r - Id) \ (Field r \ Field r')" - using Osum_minus_Id2[of r' r] by simp - moreover - {have "Range(Field r \ Field r') Int Domain(r - Id) = {}" - using FLD unfolding Field_def by blast - hence "wf((r - Id) \ (Field r \ Field r'))" - using 1 WF wf_Un[of "r - Id" "Field r \ 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 \ 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 diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Library/Order_Union.thy --- 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 *} diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Library/Well_Order_Extension.thy --- 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 = (\x y. (x, y) \ r \ y \ A \ x \ A)" - -(* -text {*Connection to order filters of the @{theory Cardinals} theory.*} -lemma (in wo_rel) ofilter_downset_on_conv: - "ofilter A \ downset_on A r \ A \ Field r" - by (auto simp: downset_on_def ofilter_def under_def) -*) - -lemma downset_onI: - "(\x y. (x, y) \ r \ y \ A \ x \ A) \ downset_on A r" - by (auto simp: downset_on_def) - -lemma downset_onD: - "downset_on A r \ (x, y) \ r \ y \ A \ x \ 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 = (\x\A. \y\A. (x, y) \ s \ (x, y) \ r)" - -lemma extension_onI: - "(\x y. \x \ A; y \ A; (x, y) \ s\ \ (x, y) \ r) \ extension_on A r s" - by (auto simp: extension_on_def) - -lemma extension_onD: - "extension_on A r s \ x \ A \ y \ A \ (x, y) \ s \ (x, y) \ r" - by (auto simp: extension_on_def) - -lemma downset_on_Union: - assumes "\r. r \ R \ downset_on (Field r) p" - shows "downset_on (Field (\R)) p" - using assms by (auto intro: downset_onI dest: downset_onD) - -lemma chain_subset_extension_on_Union: - assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" - shows "extension_on (Field (\R)) (\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 "\w. p \ w \ Well_order w" -proof - - let ?K = "{r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p}" - def I \ "init_seg_of \ ?K \ ?K" - have I_init: "I \ init_seg_of" by (simp add: I_def) - then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" - by (auto simp: init_seg_of_def chain_subset_def Chains_def) - have Chains_wo: "\R r. R \ Chains I \ r \ R \ - Well_order r \ downset_on (Field r) p \ 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 \ Chains I" - then have Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast - have subch: "chain\<^sub>\ R" using `R \ Chains I` I_init - by (auto simp: init_seg_of_def chain_subset_def Chains_def) - have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r" and - "\r\R. Total r" and "\r\R. wf (r - Id)" and - "\r. r \ R \ downset_on (Field r) p" and - "\r. r \ R \ extension_on (Field r) r p" - using Chains_wo [OF `R \ Chains I`] by (simp_all add: order_on_defs) - have "Refl (\R)" using `\r\R. Refl r` by (auto simp: refl_on_def) - moreover have "trans (\R)" - by (rule chain_subset_trans_Union [OF subch `\r\R. trans r`]) - moreover have "antisym (\R)" - by (rule chain_subset_antisym_Union [OF subch `\r\R. antisym r`]) - moreover have "Total (\R)" - by (rule chain_subset_Total_Union [OF subch `\r\R. Total r`]) - moreover have "wf ((\R) - Id)" - proof - - have "(\R) - Id = \{r - Id | r. r \ R}" by blast - with `\r\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 (\R)" by (simp add: order_on_defs) - moreover have "\r\R. r initial_segment_of \R" using Ris - by (simp add: Chains_init_seg_of_Union) - moreover have "downset_on (Field (\R)) p" - by (rule downset_on_Union [OF `\r. r \ R \ downset_on (Field r) p`]) - moreover have "extension_on (Field (\R)) (\R) p" - by (rule chain_subset_extension_on_Union [OF subch `\r. r \ R \ extension_on (Field r) r p`]) - ultimately have "\R \ ?K \ (\r\R. (r,\R) \ I)" - using mono_Chains [OF I_init] and `R \ Chains I` - by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) - } - then have 1: "\R\Chains I. \u\Field I. \r\R. (r, u) \ 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 \ 'a) set" - where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and - max: "\r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p \ - (m, r) \ I \ r = m" - by (auto simp: FI) - have "Field p \ Field m" - proof (rule ccontr) - let ?Q = "Field p - Field m" - assume "\ (Field p \ Field m)" - with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] - obtain x where "x \ Field p" and "x \ Field m" and - min: "\y. (y, x) \ p \ y \ ?Q" by blast - txt {*Add @{term x} as topmost element to @{term m}.*} - let ?s = "{(y, x) | y. y \ Field m}" - let ?m = "insert (x, x) m \ ?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 \ Field m` - unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast - moreover have "antisym ?m" using `antisym m` `x \ 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 \ Field m` - by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis - thus ?thesis using `wf (m - Id)` `x \ 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) \ 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 \ 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 \ Field m` unfolding Field_def by blast - qed - have "p \ m" - using `Field p \ 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 "\w. p \ w \ Well_order w \ Field w = UNIV" -proof - - from well_order_extension [OF assms] obtain w - where "p \ 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 \ Field w' = {}" by simp - let ?w = "w \o w'" - have "p \ ?w" using `p \ 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 \ A" - shows "\w. p \ w \ well_order_on A w" -proof - - from total_well_order_extension [OF `wf p`] obtain r - where "p \ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast - let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" - from `p \ r` have "p \ ?r" using `Field p \ 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 \ ?r` show ?thesis by blast -qed - -end - diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Library/Zorn.thy --- 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 = (\x y. (x, y) \ r \ y \ A \ x \ A)" + +(* +text {*Connection to order filters of the @{theory Cardinals} theory.*} +lemma (in wo_rel) ofilter_downset_on_conv: + "ofilter A \ downset_on A r \ A \ Field r" + by (auto simp: downset_on_def ofilter_def under_def) +*) + +lemma downset_onI: + "(\x y. (x, y) \ r \ y \ A \ x \ A) \ downset_on A r" + by (auto simp: downset_on_def) + +lemma downset_onD: + "downset_on A r \ (x, y) \ r \ y \ A \ x \ 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 = (\x\A. \y\A. (x, y) \ s \ (x, y) \ r)" + +lemma extension_onI: + "(\x y. \x \ A; y \ A; (x, y) \ s\ \ (x, y) \ r) \ extension_on A r s" + by (auto simp: extension_on_def) + +lemma extension_onD: + "extension_on A r s \ x \ A \ y \ A \ (x, y) \ s \ (x, y) \ r" + by (auto simp: extension_on_def) + +lemma downset_on_Union: + assumes "\r. r \ R \ downset_on (Field r) p" + shows "downset_on (Field (\R)) p" + using assms by (auto intro: downset_onI dest: downset_onD) + +lemma chain_subset_extension_on_Union: + assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" + shows "extension_on (Field (\R)) (\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 "\w. p \ w \ Well_order w" +proof - + let ?K = "{r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p}" + def I \ "init_seg_of \ ?K \ ?K" + have I_init: "I \ init_seg_of" by (simp add: I_def) + then have subch: "\R. R \ Chains I \ chain\<^sub>\ R" + by (auto simp: init_seg_of_def chain_subset_def Chains_def) + have Chains_wo: "\R r. R \ Chains I \ r \ R \ + Well_order r \ downset_on (Field r) p \ 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 \ Chains I" + then have Ris: "R \ Chains init_seg_of" using mono_Chains [OF I_init] by blast + have subch: "chain\<^sub>\ R" using `R \ Chains I` I_init + by (auto simp: init_seg_of_def chain_subset_def Chains_def) + have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r" and + "\r\R. Total r" and "\r\R. wf (r - Id)" and + "\r. r \ R \ downset_on (Field r) p" and + "\r. r \ R \ extension_on (Field r) r p" + using Chains_wo [OF `R \ Chains I`] by (simp_all add: order_on_defs) + have "Refl (\R)" using `\r\R. Refl r` by (auto simp: refl_on_def) + moreover have "trans (\R)" + by (rule chain_subset_trans_Union [OF subch `\r\R. trans r`]) + moreover have "antisym (\R)" + by (rule chain_subset_antisym_Union [OF subch `\r\R. antisym r`]) + moreover have "Total (\R)" + by (rule chain_subset_Total_Union [OF subch `\r\R. Total r`]) + moreover have "wf ((\R) - Id)" + proof - + have "(\R) - Id = \{r - Id | r. r \ R}" by blast + with `\r\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 (\R)" by (simp add: order_on_defs) + moreover have "\r\R. r initial_segment_of \R" using Ris + by (simp add: Chains_init_seg_of_Union) + moreover have "downset_on (Field (\R)) p" + by (rule downset_on_Union [OF `\r. r \ R \ downset_on (Field r) p`]) + moreover have "extension_on (Field (\R)) (\R) p" + by (rule chain_subset_extension_on_Union [OF subch `\r. r \ R \ extension_on (Field r) r p`]) + ultimately have "\R \ ?K \ (\r\R. (r,\R) \ I)" + using mono_Chains [OF I_init] and `R \ Chains I` + by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) + } + then have 1: "\R\Chains I. \u\Field I. \r\R. (r, u) \ 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 \ 'a) set" + where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and + max: "\r. Well_order r \ downset_on (Field r) p \ extension_on (Field r) r p \ + (m, r) \ I \ r = m" + by (auto simp: FI) + have "Field p \ Field m" + proof (rule ccontr) + let ?Q = "Field p - Field m" + assume "\ (Field p \ Field m)" + with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] + obtain x where "x \ Field p" and "x \ Field m" and + min: "\y. (y, x) \ p \ y \ ?Q" by blast + txt {*Add @{term x} as topmost element to @{term m}.*} + let ?s = "{(y, x) | y. y \ Field m}" + let ?m = "insert (x, x) m \ ?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 \ Field m` + unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast + moreover have "antisym ?m" using `antisym m` `x \ 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 \ Field m` + by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis + thus ?thesis using `wf (m - Id)` `x \ 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) \ 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 \ 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 \ Field m` unfolding Field_def by blast + qed + have "p \ m" + using `Field p \ 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 "\w. p \ w \ Well_order w \ Field w = UNIV" +proof - + from well_order_extension [OF assms] obtain w + where "p \ 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 \ Field w' = {}" by simp + let ?w = "w \o w'" + have "p \ ?w" using `p \ 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 \ A" + shows "\w. p \ w \ well_order_on A w" +proof - + from total_well_order_extension [OF `wf p`] obtain r + where "p \ r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast + let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}" + from `p \ r` have "p \ ?r" using `Field p \ 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 \ ?r` show ?thesis by blast +qed + end diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Tools/Nitpick/nitpick.ML --- 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, diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 \ 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 diff -r 66bc827e37f8 -r afe61eefdc61 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 ()