--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Jan 10 23:44:03 2014 +0100
@@ -15,7 +15,7 @@
val find_index_eq: ''a list -> ''a -> int
val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
- val drop_All: term -> term
+ val drop_all: term -> term
val mk_partial_compN: int -> typ -> term -> term
val mk_partial_comp: typ -> typ -> term -> term
@@ -38,7 +38,7 @@
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
-fun drop_All t =
+fun drop_all t =
subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
strip_qnt_body @{const_name all} t);
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 23:44:03 2014 +0100
@@ -158,10 +158,10 @@
(case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
(case dest_case ctxt s Ts t of
- NONE => apsnd (f conds t)
- | SOME (conds', branches) =>
- apfst (cons s) o fold_rev (uncurry fld)
- (map (append conds o conjuncts_s) conds' ~~ branches))
+ SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) =>
+ apfst (cons ctr_sugar) o fold_rev (uncurry fld)
+ (map (append conds o conjuncts_s) conds' ~~ branches)
+ | _ => apsnd (f conds t))
| _ => apsnd (f conds t))
else
apsnd (f conds t)
@@ -171,7 +171,10 @@
fld [] t o pair []
end;
-fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
+fun case_of ctxt s =
+ (case ctr_sugar_of ctxt s of
+ SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
+ | _ => NONE);
fun massage_let_if_case ctxt has_call massage_leaf =
let
@@ -319,8 +322,6 @@
if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
end;
-val fold_rev_corec_call = fold_rev_let_if_case;
-
fun expand_to_ctr_term ctxt s Ts t =
(case ctr_sugar_of ctxt s of
SOME {ctrs, casex, ...} =>
@@ -342,10 +343,7 @@
snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
fun case_thms_of_term ctxt bound_Ts t =
- let
- val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
- val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
- in
+ let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in
(maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
maps #sel_split_asms ctr_sugars)
end;
@@ -607,7 +605,7 @@
SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
| NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
- val user_eqn = drop_All eqn0;
+ val user_eqn = drop_all eqn0;
in
Sel {
fun_name = fun_name,
@@ -634,9 +632,11 @@
handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
val disc_concl = betapply (disc, lhs);
- val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1
- then (NONE, matchedsss)
- else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
+ val (eqn_data_disc_opt, matchedsss') =
+ if null (tl basic_ctr_specs) then
+ (NONE, matchedsss)
+ else
+ apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
(SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
val sel_concls = sels ~~ ctr_args
@@ -664,8 +664,7 @@
val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ =>
- if member ((op =) o apsnd #ctr) basic_ctr_specs ctr
- then cons (ctr, cs)
+ if member ((op =) o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)
else primcorec_error_eqn "not a constructor" ctr) [] rhs' []
|> AList.group (op =);
@@ -687,7 +686,7 @@
fun dissect_coeqn lthy has_call fun_names sequentials
(basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
let
- val eqn = drop_All eqn0
+ val eqn = drop_all eqn0
handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
val (prems, concl) = Logic.strip_horn eqn
|> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
@@ -714,7 +713,11 @@
else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
- (if null prems then SOME eqn0 else NONE) prems concl matchedsss
+ (if null prems then
+ SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
+ else
+ NONE)
+ prems concl matchedsss
else if null prems then
dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
|>> flat
@@ -865,7 +868,7 @@
auto_gen = true,
ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
- eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (*###*),
+ eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *),
user_eqn = undef_const};
in
chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
@@ -876,7 +879,7 @@
let
val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
|> find_index (curry (op =) sel) o #sels o the;
- fun find t = if has_call t then snd (fold_rev_corec_call ctxt (K cons) [] t []) else [];
+ fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else [];
in
find rhs_term
|> K |> nth_map sel_no |> AList.map_entry (op =) ctr
@@ -886,8 +889,7 @@
list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
fun is_trivial_implies thm =
- op aconv (Logic.dest_implies (Thm.prop_of thm))
- handle TERM _ => false;
+ uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
fun add_primcorec_ursive tac_opt opts fixes specs of_specs_opt lthy =
let
@@ -992,9 +994,14 @@
de_facto_exhaustives disc_eqnss
|> list_all_fun_args []
val nchotomy_taut_thmss =
- map3 (fn {disc_exhausts, ...} => fn false => K []
- | true => map_prove_with_tac (fn {context = ctxt, ...} =>
- mk_primcorec_nchotomy_tac ctxt disc_exhausts))
+ map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive =>
+ if syntactic_exhaustive then
+ map_prove_with_tac (fn {context = ctxt, ...} =>
+ mk_primcorec_nchotomy_tac ctxt disc_exhausts)
+ else
+ (case tac_opt of
+ SOME tac => map_prove_with_tac tac
+ | NONE => K []))
corec_specs syntactic_exhaustives nchotomy_goalss;
val goalss = goalss'
|> (if is_none tac_opt then
@@ -1007,9 +1014,11 @@
let
val def_thms = map (snd o snd) def_thms';
- val nchotomy_thmss = nchotomy_taut_thmss
- |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I);
- val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn;
+ val (nchotomy_thmss, exclude_thmss) =
+ if is_none tac_opt then
+ (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'')
+ else
+ (nchotomy_taut_thmss, thmss'');
val ps =
Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
@@ -1036,11 +1045,11 @@
val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
fun mk_excludesss excludes n =
- (excludes, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
- |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));
- val excludessss = (excludess' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
- |-> map2 (fn excludes => fn (_, {ctr_specs, ...}) =>
- mk_excludesss excludes (length ctr_specs));
+ fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])))
+ excludes (map (fn k => replicate k [asm_rl] @ replicate (n - k) []) (0 upto n - 1));
+ val excludessss =
+ map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
+ (map2 append excludess' taut_thmss) corec_specs;
fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
@@ -1165,7 +1174,8 @@
val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
val cond_ctrs =
fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
- val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
+ val ctr_thms =
+ map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
in SOME (false, rhs, raw_rhs, ctr_thms) end
| NONE =>
let
@@ -1214,13 +1224,13 @@
val (distincts, discIs, sel_splits, sel_split_asms) =
case_thms_of_term lthy bound_Ts raw_rhs;
- val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
- sel_splits sel_split_asms ms ctr_thms
+ val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
+ sel_split_asms ms ctr_thms
(if exhaustive_code then try the_single nchotomys else NONE)
|> K |> Goal.prove_sorry lthy [] [] raw_goal
|> Thm.close_derivation;
in
- mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
+ mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> single
@@ -1238,7 +1248,7 @@
fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
(({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
- if null disc_thms orelse null exhaust_thms then
+ if null exhaust_thms orelse null (tl ctr_specs) then
[]
else
let
@@ -1248,15 +1258,14 @@
mk_conjs prems)
|> curry Logic.list_all (map dest_Free fun_args);
in
- if prems = [@{term False}] then
- []
- else
- mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
- (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
- |> K |> Goal.prove_sorry lthy [] [] goal
- |> Thm.close_derivation
- |> pair eqn_pos
- |> single
+ mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
+ (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
+ |> K |> Goal.prove_sorry lthy [] [] goal
+ |> Thm.close_derivation
+ |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+ @{thms eqTrueE eq_False[THEN iffD1] notnotD}
+ |> pair eqn_pos
+ |> single
end;
val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
@@ -1271,7 +1280,9 @@
val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
ctr_specss;
- val simp_thmss = map2 append disc_thmss sel_thmss;
+ val disc_iff_or_disc_thmss =
+ map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;
+ val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
val common_name = mk_common_name fun_names;
@@ -1331,7 +1342,7 @@
val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
lthy
|> after_qed (map (fn [] => []
- | _ => primcorec_error "need exclusiveness proofs - use primcorecursive instead of primcorec")
+ | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
goalss)) ooo add_primcorec_ursive_cmd (SOME (auto_tac o #context));
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 23:44:03 2014 +0100
@@ -8,16 +8,16 @@
signature BNF_GFP_REC_SUGAR_TACTICS =
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
- val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
+ val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
- val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list ->
+ val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
thm list -> tactic
val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
- val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
- thm list -> int list -> thm list -> thm option -> tactic
+ val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
+ int list -> thm list -> thm option -> tactic
val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
end;
@@ -88,44 +88,48 @@
HEADGOAL (if m = 0 then rtac TrueI
else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
-fun different_case_tac ctxt m excl =
+fun different_case_tac ctxt m exclude =
HEADGOAL (if m = 0 then
mk_primcorec_assumption_tac ctxt []
else
- dtac excl THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
+ dtac exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
mk_primcorec_assumption_tac ctxt []);
-fun cases_tac ctxt k m exclsss =
- let val n = length exclsss in
+fun cases_tac ctxt k m excludesss =
+ let val n = length excludesss in
EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
- | [excl] => different_case_tac ctxt m excl)
- (take k (nth exclsss (k - 1))))
+ | [exclude] => different_case_tac ctxt m exclude)
+ (take k (nth excludesss (k - 1))))
end;
fun prelude_tac ctxt defs thm =
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
-fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
- prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
+fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss =
+ prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss;
-fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_disc fun_discss disc_excludes =
+fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
+ disc_excludes =
HEADGOAL (rtac iffI THEN'
rtac fun_exhaust THEN'
K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
EVERY' (map (fn [] => etac FalseE
- | [fun_disc'] =>
- if Thm.eq_thm (fun_disc', fun_disc) then
+ | fun_discs' as [fun_disc'] =>
+ if eq_list Thm.eq_thm (fun_discs', fun_discs) then
REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
else
- rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
+ rtac FalseE THEN'
+ (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
+ cut_tac fun_disc') THEN'
dresolve_tac disc_excludes THEN' etac notE THEN' atac)
fun_discss) THEN'
- rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
+ (etac FalseE ORELSE'
+ resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
- m exclsss =
+ m excludesss =
prelude_tac ctxt defs (fun_sel RS trans) THEN
- cases_tac ctxt k m exclsss THEN
+ cases_tac ctxt k m excludesss THEN
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
eresolve_tac falseEs ORELSE'
resolve_tac split_connectI ORELSE'
@@ -153,7 +157,7 @@
end
| _ => split);
-fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
+fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
let
val splits' =
map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
@@ -173,8 +177,7 @@
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
- nchotomy_opt =
+fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
let
val n = length ms;
val (ms', fun_ctrs') =
@@ -188,13 +191,12 @@
||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
|> op @));
in
- EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
- ms' fun_ctrs') THEN
+ EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
end;
-fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
+fun mk_primcorec_code_tac ctxt distincts splits raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
--- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Fri Jan 10 23:44:03 2014 +0100
@@ -237,7 +237,7 @@
fun dissect_eqn lthy fun_names eqn' =
let
- val eqn = drop_All eqn' |> HOLogic.dest_Trueprop
+ val eqn = drop_all eqn' |> HOLogic.dest_Trueprop
handle TERM _ =>
primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
val (lhs, rhs) = HOLogic.dest_eq eqn
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Fri Jan 10 23:44:03 2014 +0100
@@ -11,7 +11,6 @@
imports Cardinal_Arithmetic_FP Cardinal_Order_Relation
begin
-
subsection {* Binary sum *}
lemma csum_Cnotzero2:
@@ -33,12 +32,40 @@
lemma cone_ordLeq_ctwo: "cone \<le>o ctwo"
unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto
+lemma csum_czero1: "Card_order r \<Longrightarrow> r +c czero =o r"
+ unfolding czero_def csum_def Field_card_of
+ by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty1] card_of_Field_ordIso])
+
+lemma csum_czero2: "Card_order r \<Longrightarrow> czero +c r =o r"
+ unfolding czero_def csum_def Field_card_of
+ by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty2] card_of_Field_ordIso])
+
subsection {* Product *}
lemma Times_cprod: "|A \<times> B| =o |A| *c |B|"
by (simp only: cprod_def Field_card_of card_of_refl)
+lemma card_of_Times_singleton:
+fixes A :: "'a set"
+shows "|A \<times> {x}| =o |A|"
+proof -
+ def f \<equiv> "\<lambda>(a::'a,b::'b). (a)"
+ have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff)
+ hence "bij_betw f (A <*> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce
+ thus ?thesis using card_of_ordIso by blast
+qed
+
+lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t"
+ unfolding cprod_def Field_card_of by (rule card_of_Times_assoc)
+
+lemma cprod_czero: "r *c czero =o czero"
+ unfolding cprod_def czero_def Field_card_of by (simp add: card_of_empty_ordIso)
+
+lemma cprod_cone: "Card_order r \<Longrightarrow> r *c cone =o r"
+ unfolding cprod_def cone_def Field_card_of
+ by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
+
lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
by (simp only: cprod_def ordIso_Times_cong2)
@@ -48,6 +75,9 @@
lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
+lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
+ by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
+
subsection {* Exponentiation *}
@@ -112,7 +142,7 @@
qed
lemma cone_ordLeq_cexp: "cone \<le>o r1 \<Longrightarrow> cone \<le>o r1 ^c r2"
-by (simp add: cexp_def cone_def Func_non_emp card_of_singl_ordLeq cone_ordLeq_iff_Field)
+by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field)
lemma Card_order_czero: "Card_order czero"
by (simp only: card_of_Card_order czero_def)
@@ -177,7 +207,7 @@
shows "card_order (r1 ^c r2)"
proof -
have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto
- thus ?thesis unfolding cexp_def Func_def by (simp add: card_of_card_order_on)
+ thus ?thesis unfolding cexp_def Func_def by simp
qed
lemma Cinfinite_ordLess_cexp:
@@ -195,6 +225,58 @@
shows "r \<le>o r ^c r"
by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
+lemma czero_cexp: "Cnotzero r \<Longrightarrow> czero ^c r =o czero"
+ by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso)
+
+lemma Func_singleton:
+fixes x :: 'b and A :: "'a set"
+shows "|Func A {x}| =o |{x}|"
+proof (rule ordIso_symmetric)
+ def f \<equiv> "\<lambda>y a. if y = x \<and> a \<in> A then x else undefined"
+ have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
+ hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def
+ by (auto split: split_if_asm)
+ thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
+qed
+
+lemma cone_cexp: "cone ^c r =o cone"
+ unfolding cexp_def cone_def Field_card_of by (rule Func_singleton)
+
+lemma card_of_Func_squared:
+ fixes A :: "'a set"
+ shows "|Func (UNIV :: bool set) A| =o |A \<times> A|"
+proof (rule ordIso_symmetric)
+ def f \<equiv> "\<lambda>(x::'a,y) b. if A = {} then undefined else if b then x else y"
+ have "Func (UNIV :: bool set) A \<subseteq> f ` (A \<times> A)" unfolding f_def Func_def
+ by (auto simp: image_iff fun_eq_iff split: option.splits split_if_asm) blast
+ hence "bij_betw f (A \<times> A) (Func (UNIV :: bool set) A)"
+ unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff)
+ thus "|A \<times> A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast
+qed
+
+lemma cexp_ctwo: "r ^c ctwo =o r *c r"
+ unfolding cexp_def ctwo_def cprod_def Field_card_of by (rule card_of_Func_squared)
+
+lemma card_of_Func_Plus:
+ fixes A :: "'a set" and B :: "'b set" and C :: "'c set"
+ shows "|Func (A <+> B) C| =o |Func A C \<times> Func B C|"
+proof (rule ordIso_symmetric)
+ def f \<equiv> "\<lambda>(g :: 'a => 'c, h::'b \<Rightarrow> 'c) ab. case ab of Inl a \<Rightarrow> g a | Inr b \<Rightarrow> h b"
+ def f' \<equiv> "\<lambda>(f :: ('a + 'b) \<Rightarrow> 'c). (\<lambda>a. f (Inl a), \<lambda>b. f (Inr b))"
+ have "f ` (Func A C \<times> Func B C) \<subseteq> Func (A <+> B) C"
+ unfolding Func_def f_def by (force split: sum.splits)
+ moreover have "f' ` Func (A <+> B) C \<subseteq> Func A C \<times> Func B C" unfolding Func_def f'_def by force
+ moreover have "\<forall>a \<in> Func A C \<times> Func B C. f' (f a) = a" unfolding f'_def f_def Func_def by auto
+ moreover have "\<forall>a' \<in> Func (A <+> B) C. f (f' a') = a'" unfolding f'_def f_def Func_def
+ by (auto split: sum.splits)
+ ultimately have "bij_betw f (Func A C \<times> Func B C) (Func (A <+> B) C)"
+ by (intro bij_betw_byWitness[of _ f' f])
+ thus "|Func A C \<times> Func B C| =o |Func (A <+> B) C|" using card_of_ordIso by blast
+qed
+
+lemma cexp_csum: "r ^c (s +c t) =o r ^c s *c r ^c t"
+ unfolding cexp_def cprod_def csum_def Field_card_of by (rule card_of_Func_Plus)
+
subsection {* Powerset *}
@@ -218,4 +300,105 @@
lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r"
unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func)
+subsection {* Inverse image *}
+
+lemma vimage_ordLeq:
+assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
+shows "|vimage f A| \<le>o k"
+proof-
+ have "vimage f A = (\<Union> a \<in> A. vimage f {a})" by auto
+ also have "|\<Union> a \<in> A. vimage f {a}| \<le>o k"
+ using UNION_Cinfinite_bound[OF assms] .
+ finally show ?thesis .
+qed
+
+subsection {* Maximum *}
+
+definition cmax where
+ "cmax r s =
+ (if cinfinite r \<or> cinfinite s then czero +c r +c s
+ else natLeq_on (max (card (Field r)) (card (Field s))) +c czero)"
+
+lemma cmax_com: "cmax r s =o cmax s r"
+ unfolding cmax_def
+ by (auto simp: max.commute intro: csum_cong2[OF csum_com] csum_cong2[OF czero_ordIso])
+
+lemma cmax1:
+ assumes "Card_order r" "Card_order s" "s \<le>o r"
+ shows "cmax r s =o r"
+unfolding cmax_def proof (split if_splits, intro conjI impI)
+ assume "cinfinite r \<or> cinfinite s"
+ hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono)
+ have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum])
+ also have "r +c s =o r" by (rule csum_absorb1[OF Cinf assms(3)])
+ finally show "czero +c r +c s =o r" .
+next
+ assume "\<not> (cinfinite r \<or> cinfinite s)"
+ hence fin: "finite (Field r)" and "finite (Field s)" unfolding cinfinite_def by simp_all
+ moreover
+ { from assms(2) have "|Field s| =o s" by (rule card_of_Field_ordIso)
+ also from assms(3) have "s \<le>o r" .
+ also from assms(1) have "r =o |Field r|" by (rule ordIso_symmetric[OF card_of_Field_ordIso])
+ finally have "|Field s| \<le>o |Field r|" .
+ }
+ ultimately have "card (Field s) \<le> card (Field r)" by (subst sym[OF finite_card_of_iff_card2])
+ hence "max (card (Field r)) (card (Field s)) = card (Field r)" by (rule max_absorb1)
+ hence "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =
+ natLeq_on (card (Field r)) +c czero" by simp
+ also have "\<dots> =o natLeq_on (card (Field r))" by (rule csum_czero1[OF natLeq_on_Card_order])
+ also have "natLeq_on (card (Field r)) =o |Field r|"
+ by (rule ordIso_symmetric[OF finite_imp_card_of_natLeq_on[OF fin]])
+ also from assms(1) have "|Field r| =o r" by (rule card_of_Field_ordIso)
+ finally show "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =o r" .
+qed
+
+lemma cmax2:
+ assumes "Card_order r" "Card_order s" "r \<le>o s"
+ shows "cmax r s =o s"
+ by (metis assms cmax1 cmax_com ordIso_transitive)
+
+lemma csum_absorb2: "Cinfinite r2 \<Longrightarrow> r1 \<le>o r2 \<Longrightarrow> r1 +c r2 =o r2"
+ by (metis csum_absorb2')
+
+lemma cprod_infinite2': "\<lbrakk>Cnotzero r1; Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r1 *c r2 =o r2"
+ unfolding ordIso_iff_ordLeq
+ by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl)
+ (auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty)
+
+context
+ fixes r s
+ assumes r: "Cinfinite r"
+ and s: "Cinfinite s"
+begin
+
+lemma cmax_csum: "cmax r s =o r +c s"
+proof (cases "r \<le>o s")
+ case True
+ hence "cmax r s =o s" by (metis cmax2 r s)
+ also have "s =o r +c s" by (metis True csum_absorb2 ordIso_symmetric s)
+ finally show ?thesis .
+next
+ case False
+ hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def)
+ hence "cmax r s =o r" by (metis cmax1 r s)
+ also have "r =o r +c s" by (metis `s \<le>o r` csum_absorb1 ordIso_symmetric r)
+ finally show ?thesis .
+qed
+
+lemma cmax_cprod: "cmax r s =o r *c s"
+proof (cases "r \<le>o s")
+ case True
+ hence "cmax r s =o s" by (metis cmax2 r s)
+ also have "s =o r *c s" by (metis Cinfinite_Cnotzero True cprod_infinite2' ordIso_symmetric r s)
+ finally show ?thesis .
+next
+ case False
+ hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def)
+ hence "cmax r s =o r" by (metis cmax1 r s)
+ also have "r =o r *c s" by (metis Cinfinite_Cnotzero `s \<le>o r` cprod_infinite1' ordIso_symmetric r s)
+ finally show ?thesis .
+qed
+
end
+
+end
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jan 10 23:44:03 2014 +0100
@@ -67,8 +67,6 @@
cardSuc_finite[simp]
card_of_Plus_ordLeq_infinite_Field[simp]
curr_in[intro, simp]
- Func_empty[simp]
- Func_is_emp[simp]
subsection {* Cardinal of a set *}
@@ -418,8 +416,7 @@
proof-
have "\<forall>i \<in> I. |A(f i)| =o |B(f i)|"
using ISO BIJ unfolding bij_betw_def by blast
- hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|"
- using card_of_Sigma_cong1 by metis
+ hence "|SIGMA i : I. A (f i)| =o |SIGMA i : I. B (f i)|" by (rule card_of_Sigma_cong1)
moreover have "|SIGMA i : I. B (f i)| =o |SIGMA j : J. B j|"
using BIJ card_of_Sigma_cong2 by blast
ultimately show ?thesis using ordIso_transitive by blast
@@ -1173,9 +1170,8 @@
lemma natLeq_on_ordLeq_less:
"((natLeq_on m) <o (natLeq_on n)) = (m < n)"
-using not_ordLeq_iff_ordLess[of "natLeq_on m" "natLeq_on n"]
- natLeq_on_Well_order natLeq_on_ordLeq_less_eq
-by fastforce
+using not_ordLeq_iff_ordLess[OF natLeq_on_Well_order natLeq_on_Well_order, of n m]
+ natLeq_on_ordLeq_less_eq[of n m] by linarith
lemma ordLeq_natLeq_on_imp_finite:
assumes "|A| \<le>o natLeq_on n"
@@ -1298,7 +1294,7 @@
hence 4: "m \<le> n" using 2 by force
(* *)
have "bij_betw f (Field r') (f ` (Field r'))"
- using 1 WELL embed_inj_on unfolding bij_betw_def by force
+ using WELL embed_inj_on[OF _ 1] unfolding bij_betw_def by blast
moreover have "finite(f ` (Field r'))" using 3 finite_atLeastLessThan[of 0 m] by force
ultimately have 5: "finite (Field r') \<and> card(Field r') = card (f ` (Field r'))"
using bij_betw_same_card bij_betw_finite by metis
@@ -1547,8 +1543,6 @@
ultimately show ?thesis by (metis ordIso_ordLeq_trans)
qed
-lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
-
lemma empty_in_Func[simp]:
"B \<noteq> {} \<Longrightarrow> (\<lambda>x. undefined) \<in> Func {} B"
unfolding Func_def by auto
@@ -1583,4 +1577,333 @@
shows "\<not>finite (Func A B)"
using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
+section {* Infinite cardinals are limit ordinals *}
+
+lemma card_order_infinite_isLimOrd:
+assumes c: "Card_order r" and i: "\<not>finite (Field r)"
+shows "isLimOrd r"
+proof-
+ have 0: "wo_rel r" and 00: "Well_order r"
+ using c unfolding card_order_on_def wo_rel_def by auto
+ hence rr: "Refl r" by (metis wo_rel.REFL)
+ show ?thesis unfolding wo_rel.isLimOrd_def[OF 0] wo_rel.isSuccOrd_def[OF 0] proof safe
+ fix j assume j: "j \<in> Field r" and jm: "\<forall>i\<in>Field r. (i, j) \<in> r"
+ def p \<equiv> "Restr r (Field r - {j})"
+ have fp: "Field p = Field r - {j}"
+ unfolding p_def apply(rule Refl_Field_Restr2[OF rr]) by auto
+ have of: "ofilter r (Field p)" unfolding wo_rel.ofilter_def[OF 0] proof safe
+ fix a x assume a: "a \<in> Field p" and "x \<in> under r a"
+ hence x: "(x,a) \<in> r" "x \<in> Field r" unfolding rel.under_def Field_def by auto
+ moreover have a: "a \<noteq> j" "a \<in> Field r" "(a,j) \<in> r" using a jm unfolding fp by auto
+ ultimately have "x \<noteq> j" using j jm by (metis 0 wo_rel.max2_def wo_rel.max2_equals1)
+ thus "x \<in> Field p" using x unfolding fp by auto
+ qed(unfold p_def Field_def, auto)
+ have "p <o r" using j ofilter_ordLess[OF 00 of] unfolding fp p_def[symmetric] by auto
+ hence 2: "|Field p| <o r" using c by (metis Cardinal_Order_Relation_FP.ordLess_Field)
+ have "|Field p| =o |Field r|" unfolding fp using i by (metis infinite_card_of_diff_singl)
+ also have "|Field r| =o r"
+ using c by (metis card_of_unique ordIso_symmetric)
+ finally have "|Field p| =o r" .
+ with 2 show False by (metis not_ordLess_ordIso)
+ qed
+qed
+
+lemma insert_Chain:
+assumes "Refl r" "C \<in> Chains r" and "i \<in> Field r" and "\<And>j. j \<in> C \<Longrightarrow> (j,i) \<in> r \<or> (i,j) \<in> r"
+shows "insert i C \<in> Chains r"
+using assms unfolding Chains_def by (auto dest: refl_onD)
+
+lemma Collect_insert: "{R j |j. j \<in> insert j1 J} = insert (R j1) {R j |j. j \<in> J}"
+by auto
+
+lemma Field_init_seg_of[simp]:
+"Field init_seg_of = UNIV"
+unfolding Field_def init_seg_of_def by auto
+
+lemma refl_init_seg_of[intro, simp]: "refl init_seg_of"
+unfolding refl_on_def Field_def by auto
+
+lemma regular_all_ex:
+assumes r: "Card_order r" "regular r"
+and As: "\<And> i j b. b \<in> B \<Longrightarrow> (i,j) \<in> r \<Longrightarrow> P i b \<Longrightarrow> P j b"
+and Bsub: "\<forall> b \<in> B. \<exists> i \<in> Field r. P i b"
+and cardB: "|B| <o r"
+shows "\<exists> i \<in> Field r. \<forall> b \<in> B. P i b"
+proof-
+ let ?As = "\<lambda>i. {b \<in> B. P i b}"
+ have "EX i : Field r. B \<le> ?As i"
+ apply(rule regular_UNION) using assms unfolding relChain_def by auto
+ thus ?thesis by auto
+qed
+
+lemma relChain_stabilize:
+assumes rc: "relChain r As" and AsB: "(\<Union> i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
+and ir: "\<not>finite (Field r)" and cr: "Card_order r"
+shows "\<exists> i \<in> Field r. As (succ r i) = As i"
+proof(rule ccontr, auto)
+ have 0: "wo_rel r" and 00: "Well_order r"
+ unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
+ have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
+ have AsBs: "(\<Union> i \<in> Field r. As (succ r i)) \<subseteq> B"
+ using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
+ assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
+ have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
+ proof safe
+ fix i j assume 1: "(i, j) \<in> r" "i \<noteq> j" and Asij: "As i = As j"
+ hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
+ hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
+ moreover
+ {have "(i,succ r i) \<in> r" apply(rule wo_rel.succ_in[OF 0])
+ using 1 unfolding rel.aboveS_def by auto
+ hence "As i \<subset> As (succ r i)" using As_s rc rij unfolding relChain_def Field_def by auto
+ }
+ ultimately show False unfolding Asij by auto
+ qed (insert rc, unfold relChain_def, auto)
+ hence "\<forall> i \<in> Field r. \<exists> a. a \<in> As (succ r i) - As i"
+ using wo_rel.succ_in[OF 0] AsB
+ by(metis 0 card_order_infinite_isLimOrd cr ir psubset_imp_ex_mem
+ wo_rel.isLimOrd_aboveS wo_rel.succ_diff)
+ then obtain f where f: "\<forall> i \<in> Field r. f i \<in> As (succ r i) - As i" by metis
+ have "inj_on f (Field r)" unfolding inj_on_def proof safe
+ fix i j assume ij: "i \<in> Field r" "j \<in> Field r" and fij: "f i = f j"
+ show "i = j"
+ proof(cases rule: wo_rel.cases_Total3[OF 0], safe)
+ assume "(i, j) \<in> r" and ijd: "i \<noteq> j"
+ hence rij: "(succ r i, j) \<in> r" by (metis "0" wo_rel.succ_smallest)
+ hence "As (succ r i) \<subseteq> As j" using rc unfolding relChain_def by auto
+ thus "i = j" using ij ijd fij f by auto
+ next
+ assume "(j, i) \<in> r" and ijd: "i \<noteq> j"
+ hence rij: "(succ r j, i) \<in> r" by (metis "0" wo_rel.succ_smallest)
+ hence "As (succ r j) \<subseteq> As i" using rc unfolding relChain_def by auto
+ thus "j = i" using ij ijd fij f by fastforce
+ qed(insert ij, auto)
+ qed
+ moreover have "f ` (Field r) \<subseteq> B" using f AsBs by auto
+ moreover have "|B| <o |Field r|" using Br cr by (metis card_of_unique ordLess_ordIso_trans)
+ ultimately show False unfolding card_of_ordLess[symmetric] by auto
+qed
+
+section {* Regular vs. Stable Cardinals *}
+
+definition stable :: "'a rel \<Rightarrow> bool"
+where
+"stable r \<equiv> \<forall>(A::'a set) (F :: 'a \<Rightarrow> 'a set).
+ |A| <o r \<and> (\<forall>a \<in> A. |F a| <o r)
+ \<longrightarrow> |SIGMA a : A. F a| <o r"
+
+lemma regular_stable:
+assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and reg: "regular r"
+shows "stable r"
+unfolding stable_def proof safe
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set" assume A: "|A| <o r" and F: "\<forall>a\<in>A. |F a| <o r"
+ {assume "r \<le>o |Sigma A F|"
+ hence "|Field r| \<le>o |Sigma A F|" using card_of_Field_ordIso[OF cr]
+ by (metis Field_card_of card_of_cong ordLeq_iff_ordLess_or_ordIso ordLeq_ordLess_trans)
+ moreover have Fi: "Field r \<noteq> {}" using ir by auto
+ ultimately obtain f where f: "f ` Sigma A F = Field r" using card_of_ordLeq2 by metis
+ have r: "wo_rel r" using cr unfolding card_order_on_def wo_rel_def by auto
+ {fix a assume a: "a \<in> A"
+ def L \<equiv> "{(a,u) | u. u \<in> F a}"
+ have fL: "f ` L \<subseteq> Field r" using f a unfolding L_def by auto
+ have "|L| =o |F a|" unfolding L_def card_of_ordIso[symmetric]
+ apply(rule exI[of _ snd]) unfolding bij_betw_def inj_on_def by (auto simp: image_def)
+ hence "|L| <o r" using F a ordIso_ordLess_trans[of "|L|" "|F a|"] unfolding L_def by auto
+ hence "|f ` L| <o r" using ordLeq_ordLess_trans[OF card_of_image, of "L"] unfolding L_def by auto
+ hence "\<not> cofinal (f ` L) r" using reg fL unfolding regular_def by (metis not_ordLess_ordIso)
+ then obtain k where k: "k \<in> Field r" and "\<forall> l \<in> L. \<not> (f l \<noteq> k \<and> (k, f l) \<in> r)"
+ unfolding cofinal_def image_def by auto
+ hence "\<exists> k \<in> Field r. \<forall> l \<in> L. (f l, k) \<in> r" using r by (metis fL image_subset_iff wo_rel.in_notinI)
+ hence "\<exists> k \<in> Field r. \<forall> u \<in> F a. (f (a,u), k) \<in> r" unfolding L_def by auto
+ }
+ then obtain gg where gg: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u), gg a) \<in> r" by metis
+ obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
+ def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
+ have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
+ hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
+ using f[symmetric] unfolding rel.under_def image_def by auto
+ have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
+ moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
+ fix i assume "i \<in> Field r"
+ then obtain j where ij: "(i,j) \<in> r" "i \<noteq> j" using cr ir by (metis infinite_Card_order_limit)
+ hence "j \<in> Field r" by (metis card_order_on_def cr rel.well_order_on_domain)
+ then obtain a where a: "a \<in> A" and j: "(j, g a) \<in> r" using 1 unfolding rel.under_def by auto
+ hence "(i, g a) \<in> r" using ij wo_rel.TRANS[OF r] unfolding trans_def by blast
+ moreover have "i \<noteq> g a"
+ using ij j r unfolding wo_rel_def unfolding well_order_on_def linear_order_on_def
+ partial_order_on_def antisym_def by auto
+ ultimately show "\<exists>j\<in>g ` A. i \<noteq> j \<and> (i, j) \<in> r" using a by auto
+ qed
+ ultimately have "|g ` A| =o r" using reg unfolding regular_def by auto
+ moreover have "|g ` A| \<le>o |A|" by (metis card_of_image)
+ ultimately have False using A by (metis not_ordLess_ordIso ordLeq_ordLess_trans)
+ }
+ thus "|Sigma A F| <o r"
+ using cr not_ordLess_iff_ordLeq by (metis card_of_Well_order card_order_on_well_order_on)
+qed
+
+lemma stable_regular:
+assumes cr: "Card_order r" and ir: "\<not>finite (Field r)" and st: "stable r"
+shows "regular r"
+unfolding regular_def proof safe
+ fix K assume K: "K \<subseteq> Field r" and cof: "cofinal K r"
+ have "|K| \<le>o r" using K by (metis card_of_Field_ordIso card_of_mono1 cr ordLeq_ordIso_trans)
+ moreover
+ {assume Kr: "|K| <o r"
+ then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
+ using cof unfolding cofinal_def by metis
+ hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding rel.underS_def by auto
+ hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
+ by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
+ also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
+ also
+ {have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
+ hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
+ }
+ finally have "r <o r" .
+ hence False by (metis ordLess_irreflexive)
+ }
+ ultimately show "|K| =o r" by (metis ordLeq_iff_ordLess_or_ordIso)
+qed
+
+(* Note that below the types of A and F are now unconstrained: *)
+lemma stable_elim:
+assumes ST: "stable r" and A_LESS: "|A| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|SIGMA a : A. F a| <o r"
+proof-
+ obtain A' where 1: "A' < Field r \<and> |A'| <o r" and 2: " |A| =o |A'|"
+ using internalize_card_of_ordLess[of A r] A_LESS by blast
+ then obtain G where 3: "bij_betw G A' A"
+ using card_of_ordIso ordIso_symmetric by blast
+ (* *)
+ {fix a assume "a \<in> A"
+ hence "\<exists>B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"
+ using internalize_card_of_ordLess[of "F a" r] F_LESS by blast
+ }
+ then obtain F' where
+ temp: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F a| =o |F' a| \<and> |F' a| <o r"
+ using bchoice[of A "\<lambda> a B'. B' \<le> Field r \<and> |F a| =o |B'| \<and> |B'| <o r"] by blast
+ hence 4: "\<forall>a \<in> A. F' a \<le> Field r \<and> |F' a| <o r" by auto
+ have 5: "\<forall>a \<in> A. |F' a| =o |F a|" using temp ordIso_symmetric by auto
+ (* *)
+ have "\<forall>a' \<in> A'. F'(G a') \<le> Field r \<and> |F'(G a')| <o r"
+ using 3 4 bij_betw_ball[of G A' A] by auto
+ hence "|SIGMA a' : A'. F'(G a')| <o r"
+ using ST 1 unfolding stable_def by auto
+ moreover have "|SIGMA a' : A'. F'(G a')| =o |SIGMA a : A. F a|"
+ using card_of_Sigma_cong[of G A' A F' F] 5 3 by blast
+ ultimately show ?thesis using ordIso_symmetric ordIso_ordLess_trans by blast
+qed
+
+lemma stable_natLeq: "stable natLeq"
+proof(unfold stable_def, safe)
+ fix A :: "'a set" and F :: "'a \<Rightarrow> 'a set"
+ assume "|A| <o natLeq" and "\<forall>a\<in>A. |F a| <o natLeq"
+ hence "finite A \<and> (\<forall>a \<in> A. finite(F a))"
+ by (auto simp add: finite_iff_ordLess_natLeq)
+ hence "finite(Sigma A F)" by (simp only: finite_SigmaI[of A F])
+ thus "|Sigma A F | <o natLeq"
+ by (auto simp add: finite_iff_ordLess_natLeq)
+qed
+
+corollary regular_natLeq: "regular natLeq"
+using stable_regular[OF natLeq_Card_order _ stable_natLeq] Field_natLeq by simp
+
+lemma stable_cardSuc:
+assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
+shows "stable(cardSuc r)"
+using infinite_cardSuc_regular regular_stable
+by (metis CARD INF cardSuc_Card_order cardSuc_finite)
+
+lemma stable_UNION:
+assumes ST: "stable r" and A_LESS: "|A| <o r" and
+ F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
+shows "|\<Union> a \<in> A. F a| <o r"
+proof-
+ have "|\<Union> a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
+ using card_of_UNION_Sigma by blast
+ thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
+qed
+
+lemma stable_ordIso1:
+assumes ST: "stable r" and ISO: "r' =o r"
+shows "stable r'"
+proof(unfold stable_def, auto)
+ fix A::"'b set" and F::"'b \<Rightarrow> 'b set"
+ assume "|A| <o r'" and "\<forall>a \<in> A. |F a| <o r'"
+ hence "( |A| <o r) \<and> (\<forall>a \<in> A. |F a| <o r)"
+ using ISO ordLess_ordIso_trans by blast
+ hence "|SIGMA a : A. F a| <o r" using assms stable_elim by blast
+ thus "|SIGMA a : A. F a| <o r'"
+ using ISO ordIso_symmetric ordLess_ordIso_trans by blast
+qed
+
+lemma stable_ordIso2:
+assumes ST: "stable r" and ISO: "r =o r'"
+shows "stable r'"
+using assms stable_ordIso1 ordIso_symmetric by blast
+
+lemma stable_ordIso:
+assumes "r =o r'"
+shows "stable r = stable r'"
+using assms stable_ordIso1 stable_ordIso2 by blast
+
+lemma stable_nat: "stable |UNIV::nat set|"
+using stable_natLeq card_of_nat stable_ordIso by auto
+
+text{* Below, the type of "A" is not important -- we just had to choose an appropriate
+ type to make "A" possible. What is important is that arbitrarily large
+ \<not>finite sets of stable cardinality exist. *}
+
+lemma infinite_stable_exists:
+assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
+shows "\<exists>(A :: (nat + 'a set)set).
+ \<not>finite A \<and> stable |A| \<and> (\<forall>r \<in> R. r <o |A| )"
+proof-
+ have "\<exists>(A :: (nat + 'a set)set).
+ \<not>finite A \<and> stable |A| \<and> |UNIV::'a set| <o |A|"
+ proof(cases "finite (UNIV::'a set)")
+ assume Case1: "finite (UNIV::'a set)"
+ let ?B = "UNIV::nat set"
+ have "\<not>finite(?B <+> {})" using finite_Plus_iff by blast
+ moreover
+ have "stable |?B|" using stable_natLeq card_of_nat stable_ordIso1 by blast
+ hence "stable |?B <+> {}|" using stable_ordIso card_of_Plus_empty1 by blast
+ moreover
+ have "\<not>finite(Field |?B| ) \<and> finite(Field |UNIV::'a set| )" using Case1 by simp
+ hence "|UNIV::'a set| <o |?B|" by (simp add: finite_ordLess_infinite)
+ hence "|UNIV::'a set| <o |?B <+> {}|" using card_of_Plus_empty1 ordLess_ordIso_trans by blast
+ ultimately show ?thesis by blast
+ next
+ assume Case1: "\<not>finite (UNIV::'a set)"
+ hence *: "\<not>finite(Field |UNIV::'a set| )" by simp
+ let ?B = "Field(cardSuc |UNIV::'a set| )"
+ have 0: "|?B| =o |{} <+> ?B|" using card_of_Plus_empty2 by blast
+ have 1: "\<not>finite ?B" using Case1 card_of_cardSuc_finite by blast
+ hence 2: "\<not>finite({} <+> ?B)" using 0 card_of_ordIso_finite by blast
+ have "|?B| =o cardSuc |UNIV::'a set|"
+ using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
+ moreover have "stable(cardSuc |UNIV::'a set| )"
+ using stable_cardSuc * card_of_Card_order by blast
+ ultimately have "stable |?B|" using stable_ordIso by blast
+ hence 3: "stable |{} <+> ?B|" using stable_ordIso 0 by blast
+ have "|UNIV::'a set| <o cardSuc |UNIV::'a set|"
+ using card_of_Card_order cardSuc_greater by blast
+ moreover have "|?B| =o cardSuc |UNIV::'a set|"
+ using card_of_Card_order cardSuc_Card_order card_of_Field_ordIso by blast
+ ultimately have "|UNIV::'a set| <o |?B|"
+ using ordIso_symmetric ordLess_ordIso_trans by blast
+ hence "|UNIV::'a set| <o |{} <+> ?B|" using 0 ordLess_ordIso_trans by blast
+ thus ?thesis using 2 3 by blast
+ qed
+ thus ?thesis using CARD card_of_UNIV2 ordLeq_ordLess_trans by blast
+qed
+
+corollary infinite_regular_exists:
+assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"
+shows "\<exists>(A :: (nat + 'a set)set).
+ \<not>finite A \<and> regular |A| \<and> (\<forall>r \<in> R. r <o |A| )"
+using infinite_stable_exists[OF CARD] stable_regular by (metis Field_card_of card_of_card_order_on)
+
end
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Fri Jan 10 23:44:03 2014 +0100
@@ -1783,166 +1783,11 @@
subsection {* Others *}
-(* function space *)
-definition Func where
-"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
-
-lemma Func_empty:
-"Func {} B = {\<lambda>x. undefined}"
-unfolding Func_def by auto
-
-lemma Func_elim:
-assumes "g \<in> Func A B" and "a \<in> A"
-shows "\<exists> b. b \<in> B \<and> g a = b"
-using assms unfolding Func_def by (cases "g a = undefined") auto
-
-definition curr where
-"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
-
-lemma curr_in:
-assumes f: "f \<in> Func (A <*> B) C"
-shows "curr A f \<in> Func A (Func B C)"
-using assms unfolding curr_def Func_def by auto
-
-lemma curr_inj:
-assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
-shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
-proof safe
- assume c: "curr A f1 = curr A f2"
- show "f1 = f2"
- proof (rule ext, clarify)
- fix a b show "f1 (a, b) = f2 (a, b)"
- proof (cases "(a,b) \<in> A <*> B")
- case False
- thus ?thesis using assms unfolding Func_def by auto
- next
- case True hence a: "a \<in> A" and b: "b \<in> B" by auto
- thus ?thesis
- using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
- qed
- qed
-qed
-
-lemma curr_surj:
-assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
-proof
- let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
- show "curr A ?f = g"
- proof (rule ext)
- fix a show "curr A ?f a = g a"
- proof (cases "a \<in> A")
- case False
- hence "g a = undefined" using assms unfolding Func_def by auto
- thus ?thesis unfolding curr_def using False by simp
- next
- case True
- obtain g1 where "g1 \<in> Func B C" and "g a = g1"
- using assms using Func_elim[OF assms True] by blast
- thus ?thesis using True unfolding Func_def curr_def by auto
- qed
- qed
- show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
-qed
-
-lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
-unfolding bij_betw_def inj_on_def image_def
-apply (intro impI conjI ballI)
-apply (erule curr_inj[THEN iffD1], assumption+)
-apply auto
-apply (erule curr_in)
-using curr_surj by blast
-
lemma card_of_Func_Times:
"|Func (A <*> B) C| =o |Func A (Func B C)|"
unfolding card_of_ordIso[symmetric]
using bij_betw_curr by blast
-definition Func_map where
-"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
-
-lemma Func_map:
-assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
-shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
-using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
-
-lemma Func_non_emp:
-assumes "B \<noteq> {}"
-shows "Func A B \<noteq> {}"
-proof-
- obtain b where b: "b \<in> B" using assms by auto
- hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
- thus ?thesis by blast
-qed
-
-lemma Func_is_emp:
-"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
-proof
- assume L: ?L
- moreover {assume "A = {}" hence False using L Func_empty by auto}
- moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
- ultimately show ?R by blast
-next
- assume R: ?R
- moreover
- {fix f assume "f \<in> Func A B"
- moreover obtain a where "a \<in> A" using R by blast
- ultimately obtain b where "b \<in> B" unfolding Func_def by blast
- with R have False by blast
- }
- thus ?L by blast
-qed
-
-lemma Func_map_surj:
-assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
-and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
-shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
-proof(cases "B2 = {}")
- case True
- thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
-next
- case False note B2 = False
- show ?thesis
- proof safe
- fix h assume h: "h \<in> Func B2 B1"
- def j1 \<equiv> "inv_into A1 f1"
- have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
- then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
- {fix b2 assume b2: "b2 \<in> B2"
- hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
- moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
- ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
- } note kk = this
- obtain b22 where b22: "b22 \<in> B2" using B2 by auto
- def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
- have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
- have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
- using kk unfolding j2_def by auto
- def g \<equiv> "Func_map A2 j1 j2 h"
- have "Func_map B2 f1 f2 g = h"
- proof (rule ext)
- fix b2 show "Func_map B2 f1 f2 g b2 = h b2"
- proof(cases "b2 \<in> B2")
- case True
- show ?thesis
- proof (cases "h b2 = undefined")
- case True
- hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto
- show ?thesis using A2 f_inv_into_f[OF b1]
- unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto
- qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
- auto intro: f_inv_into_f)
- qed(insert h, unfold Func_def Func_map_def, auto)
- qed
- moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
- using inv_into_into j2A2 B1 A2 inv_into_into
- unfolding j1_def image_def by fast+
- ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
- unfolding Func_map_def[abs_def] unfolding image_def by auto
- qed(insert B1 Func_map[OF _ _ A2(2)], auto)
-qed
-
lemma card_of_Pow_Func:
"|Pow A| =o |Func A (UNIV::bool set)|"
proof-
--- a/src/HOL/Cardinals/Cardinals.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Cardinals.thy Fri Jan 10 23:44:03 2014 +0100
@@ -9,7 +9,7 @@
header {* Theory of Ordinals and Cardinals *}
theory Cardinals
-imports Cardinal_Order_Relation Cardinal_Arithmetic Wellorder_Extension
+imports Ordinal_Arithmetic Cardinal_Arithmetic Wellorder_Extension
begin
end
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy Fri Jan 10 23:44:03 2014 +0100
@@ -15,7 +15,10 @@
ordLeq_Well_order_simp[simp]
not_ordLeq_iff_ordLess[simp]
not_ordLess_iff_ordLeq[simp]
+ Func_empty[simp]
+ Func_is_emp[simp]
+lemma Func_emp2[simp]: "A \<noteq> {} \<Longrightarrow> Func A {} = {}" by auto
subsection {* Restriction to a set *}
@@ -430,4 +433,648 @@
using NE_P P omax_ordLess by blast
qed
+
+
+section {* Limit and Succesor Ordinals *}
+
+lemma embed_underS2:
+assumes r: "Well_order r" and s: "Well_order s" and g: "embed r s g" and a: "a \<in> Field r"
+shows "g ` underS r a = underS s (g a)"
+using embed_underS[OF assms] unfolding bij_betw_def by auto
+
+lemma bij_betw_insert:
+assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'"
+shows "bij_betw f (insert b A) (insert (f b) A')"
+using notIn_Un_bij_betw[OF assms] by auto
+
+context wo_rel
+begin
+
+lemma underS_induct:
+ assumes "\<And>a. (\<And> a1. a1 \<in> underS a \<Longrightarrow> P a1) \<Longrightarrow> P a"
+ shows "P a"
+ by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
+
+lemma suc_underS:
+assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
+shows "b \<in> underS (suc B)"
+using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
+
+lemma underS_supr:
+assumes bA: "b \<in> underS (supr A)" and A: "A \<subseteq> Field r"
+shows "\<exists> a \<in> A. b \<in> underS a"
+proof(rule ccontr, auto)
+ have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
+ assume "\<forall>a\<in>A. b \<notin> underS a"
+ hence 0: "\<forall>a \<in> A. (a,b) \<in> r" using A bA unfolding underS_def
+ by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
+ have "(supr A, b) \<in> r" apply(rule supr_least[OF A bb]) using 0 by auto
+ thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+qed
+
+lemma underS_suc:
+assumes bA: "b \<in> underS (suc A)" and A: "A \<subseteq> Field r"
+shows "\<exists> a \<in> A. b \<in> under a"
+proof(rule ccontr, auto)
+ have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
+ assume "\<forall>a\<in>A. b \<notin> under a"
+ hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
+ by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq rel.under_def set_rev_mp)
+ have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding rel.underS_def by auto
+ thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
+qed
+
+lemma (in rel) AboveS_underS:
+assumes "i \<in> Field r"
+shows "i \<in> AboveS (underS i)"
+using assms unfolding AboveS_def underS_def by auto
+
+lemma (in wo_rel) in_underS_supr:
+assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}"
+shows "j \<in> underS (supr A)"
+proof-
+ have "(i,supr A) \<in> r" using supr_greater[OF A AA i] .
+ thus ?thesis using j unfolding underS_def
+ by simp (metis REFL TRANS max2_def max2_equals1 rel.refl_on_domain transD)
+qed
+
+lemma inj_on_Field:
+assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b"
+shows "inj_on f A"
+unfolding inj_on_def proof safe
+ fix a b assume a: "a \<in> A" and b: "b \<in> A" and fab: "f a = f b"
+ {assume "a \<in> underS b"
+ hence False using f[OF a b] fab by auto
+ }
+ moreover
+ {assume "b \<in> underS a"
+ hence False using f[OF b a] fab by auto
+ }
+ ultimately show "a = b" using TOTALS A a b unfolding underS_def by auto
+qed
+
+lemma in_notinI:
+assumes "(j,i) \<notin> r \<or> j = i" and "i \<in> Field r" and "j \<in> Field r"
+shows "(i,j) \<in> r" by (metis assms max2_def max2_greater_among)
+
+lemma ofilter_init_seg_of:
+assumes "ofilter F"
+shows "Restr r F initial_segment_of r"
+using assms unfolding ofilter_def init_seg_of_def under_def by auto
+
+lemma underS_init_seg_of_Collect:
+assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
+shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of"
+unfolding Chains_def proof safe
+ fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i"
+ and init: "(R ja, R j) \<notin> init_seg_of"
+ hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
+ and jjai: "(j,i) \<in> r" "(ja,i) \<in> r"
+ and i: "i \<notin> {j,ja}" unfolding Field_def rel.underS_def by auto
+ have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
+ show "R j initial_segment_of R ja"
+ using jja init jjai i
+ by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: underS_def)
+qed
+
+lemma (in wo_rel) Field_init_seg_of_Collect:
+assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2"
+shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of"
+unfolding Chains_def proof safe
+ fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r"
+ and init: "(R ja, R j) \<notin> init_seg_of"
+ hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r"
+ unfolding Field_def rel.underS_def by auto
+ have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+
+ show "R j initial_segment_of R ja"
+ using jja init
+ by (elim cases_Total3 disjE) (auto elim: cases_Total3 intro!: assms simp: Field_def)
+qed
+
+subsection {* Successor and limit elements of an ordinal *}
+
+definition "succ i \<equiv> suc {i}"
+
+definition "isSucc i \<equiv> \<exists> j. aboveS j \<noteq> {} \<and> i = succ j"
+
+definition "zero = minim (Field r)"
+
+definition "isLim i \<equiv> \<not> isSucc i"
+
+lemma zero_smallest[simp]:
+assumes "j \<in> Field r" shows "(zero, j) \<in> r"
+unfolding zero_def
+by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS)
+
+lemma zero_in_Field: assumes "Field r \<noteq> {}" shows "zero \<in> Field r"
+using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)
+
+lemma leq_zero_imp[simp]:
+"(x, zero) \<in> r \<Longrightarrow> x = zero"
+by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest)
+
+lemma leq_zero[simp]:
+assumes "Field r \<noteq> {}" shows "(x, zero) \<in> r \<longleftrightarrow> x = zero"
+using zero_in_Field[OF assms] in_notinI[of x zero] by auto
+
+lemma under_zero[simp]:
+assumes "Field r \<noteq> {}" shows "under zero = {zero}"
+using assms unfolding under_def by auto
+
+lemma underS_zero[simp,intro]: "underS zero = {}"
+unfolding underS_def by auto
+
+lemma isSucc_succ: "aboveS i \<noteq> {} \<Longrightarrow> isSucc (succ i)"
+unfolding isSucc_def succ_def by auto
+
+lemma succ_in_diff:
+assumes "aboveS i \<noteq> {}" shows "(i,succ i) \<in> r \<and> succ i \<noteq> i"
+using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto
+
+lemmas succ_in[simp] = succ_in_diff[THEN conjunct1]
+lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2]
+
+lemma succ_in_Field[simp]:
+assumes "aboveS i \<noteq> {}" shows "succ i \<in> Field r"
+using succ_in[OF assms] unfolding Field_def by auto
+
+lemma succ_not_in:
+assumes "aboveS i \<noteq> {}" shows "(succ i, i) \<notin> r"
+proof
+ assume 1: "(succ i, i) \<in> r"
+ hence "succ i \<in> Field r \<and> i \<in> Field r" unfolding Field_def by auto
+ hence "(i, succ i) \<in> r \<and> succ i \<noteq> i" using assms by auto
+ thus False using 1 by (metis ANTISYM antisymD)
+qed
+
+lemma not_isSucc_zero: "\<not> isSucc zero"
+proof
+ assume "isSucc zero"
+ moreover
+ then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
+ unfolding isSucc_def zero_def by auto
+ hence "succ i \<in> Field r" by auto
+ ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain
+ subset_refl succ_in succ_not_in zero_def)
+qed
+
+lemma isLim_zero[simp]: "isLim zero"
+ by (metis isLim_def not_isSucc_zero)
+
+lemma succ_smallest:
+assumes "(i,j) \<in> r" and "i \<noteq> j"
+shows "(succ i, j) \<in> r"
+unfolding succ_def apply(rule suc_least)
+using assms unfolding Field_def by auto
+
+lemma isLim_supr:
+assumes f: "i \<in> Field r" and l: "isLim i"
+shows "i = supr (underS i)"
+proof(rule equals_supr)
+ fix j assume j: "j \<in> Field r" and 1: "\<And> j'. j' \<in> underS i \<Longrightarrow> (j',j) \<in> r"
+ show "(i,j) \<in> r" proof(intro in_notinI[OF _ f j], safe)
+ assume ji: "(j,i) \<in> r" "j \<noteq> i"
+ hence a: "aboveS j \<noteq> {}" unfolding aboveS_def by auto
+ hence "i \<noteq> succ j" using l unfolding isLim_def isSucc_def by auto
+ moreover have "(succ j, i) \<in> r" using succ_smallest[OF ji] by auto
+ ultimately have "succ j \<in> underS i" unfolding underS_def by auto
+ hence "(succ j, j) \<in> r" using 1 by auto
+ thus False using succ_not_in[OF a] by simp
+ qed
+qed(insert f, unfold underS_def Field_def, auto)
+
+definition "pred i \<equiv> SOME j. j \<in> Field r \<and> aboveS j \<noteq> {} \<and> succ j = i"
+
+lemma pred_Field_succ:
+assumes "isSucc i" shows "pred i \<in> Field r \<and> aboveS (pred i) \<noteq> {} \<and> succ (pred i) = i"
+proof-
+ obtain j where a: "aboveS j \<noteq> {}" and i: "i = succ j" using assms unfolding isSucc_def by auto
+ have 1: "j \<in> Field r" "j \<noteq> i" unfolding Field_def i
+ using succ_diff[OF a] a unfolding aboveS_def by auto
+ show ?thesis unfolding pred_def apply(rule someI_ex) using 1 i a by auto
+qed
+
+lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1]
+lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1]
+lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2]
+
+lemma isSucc_pred_in:
+assumes "isSucc i" shows "(pred i, i) \<in> r"
+proof-
+ def j \<equiv> "pred i"
+ have i: "i = succ j" using assms unfolding j_def by simp
+ have a: "aboveS j \<noteq> {}" unfolding j_def using assms by auto
+ show ?thesis unfolding j_def[symmetric] unfolding i using succ_in[OF a] .
+qed
+
+lemma isSucc_pred_diff:
+assumes "isSucc i" shows "pred i \<noteq> i"
+by (metis aboveS_pred assms succ_diff succ_pred)
+
+(* todo: pred maximal, pred injective? *)
+
+lemma succ_inj[simp]:
+assumes "aboveS i \<noteq> {}" and "aboveS j \<noteq> {}"
+shows "succ i = succ j \<longleftrightarrow> i = j"
+proof safe
+ assume s: "succ i = succ j"
+ {assume "i \<noteq> j" and "(i,j) \<in> r"
+ hence "(succ i, j) \<in> r" using assms by (metis succ_smallest)
+ hence False using s assms by (metis succ_not_in)
+ }
+ moreover
+ {assume "i \<noteq> j" and "(j,i) \<in> r"
+ hence "(succ j, i) \<in> r" using assms by (metis succ_smallest)
+ hence False using s assms by (metis succ_not_in)
+ }
+ ultimately show "i = j" by (metis TOTALS WELL assms(1) assms(2) succ_in_diff well_order_on_domain)
+qed
+
+lemma pred_succ[simp]:
+assumes "aboveS j \<noteq> {}" shows "pred (succ j) = j"
+unfolding pred_def apply(rule some_equality)
+using assms apply(force simp: Field_def aboveS_def)
+by (metis assms succ_inj)
+
+lemma less_succ[simp]:
+assumes "aboveS i \<noteq> {}"
+shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i"
+apply safe
+ apply (metis WELL assms in_notinI rel.well_order_on_domain suc_singl_pred succ_def succ_in_diff)
+ apply (metis (hide_lams, full_types) REFL TRANS assms max2_def max2_equals1 rel.refl_on_domain succ_in_Field succ_not_in transD)
+ apply (metis assms in_notinI succ_in_Field)
+done
+
+lemma underS_succ[simp]:
+assumes "aboveS i \<noteq> {}"
+shows "underS (succ i) = under i"
+unfolding underS_def under_def by (auto simp: assms succ_not_in)
+
+lemma succ_mono:
+assumes "aboveS j \<noteq> {}" and "(i,j) \<in> r"
+shows "(succ i, succ j) \<in> r"
+by (metis (full_types) assms less_succ succ_smallest)
+
+lemma under_succ[simp]:
+assumes "aboveS i \<noteq> {}"
+shows "under (succ i) = insert (succ i) (under i)"
+using less_succ[OF assms] unfolding under_def by auto
+
+definition mergeSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+"mergeSL S L f i \<equiv>
+ if isSucc i then S (pred i) (f (pred i))
+ else L f i"
+
+
+subsection {* Well-order recursion with (zero), succesor, and limit *}
+
+definition worecSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where "worecSL S L \<equiv> worec (mergeSL S L)"
+
+definition "adm_woL L \<equiv> \<forall>f g i. isLim i \<and> (\<forall>j\<in>underS i. f j = g j) \<longrightarrow> L f i = L g i"
+
+lemma mergeSL:
+assumes "adm_woL L" shows "adm_wo (mergeSL S L)"
+unfolding adm_wo_def proof safe
+ fix f g :: "'a => 'b" and i :: 'a
+ assume 1: "\<forall>j\<in>underS i. f j = g j"
+ show "mergeSL S L f i = mergeSL S L g i"
+ proof(cases "isSucc i")
+ case True
+ hence "pred i \<in> underS i" unfolding underS_def using isSucc_pred_in isSucc_pred_diff by auto
+ thus ?thesis using True 1 unfolding mergeSL_def by auto
+ next
+ case False hence "isLim i" unfolding isLim_def by auto
+ thus ?thesis using assms False 1 unfolding mergeSL_def adm_woL_def by auto
+ qed
+qed
+
+lemma worec_fixpoint1: "adm_wo H \<Longrightarrow> worec H i = H (worec H) i"
+by (metis worec_fixpoint)
+
+lemma worecSL_isSucc:
+assumes a: "adm_woL L" and i: "isSucc i"
+shows "worecSL S L i = S (pred i) (worecSL S L (pred i))"
+proof-
+ let ?H = "mergeSL S L"
+ have "worecSL S L i = ?H (worec ?H) i"
+ unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
+ also have "... = S (pred i) (worecSL S L (pred i))"
+ unfolding worecSL_def mergeSL_def using i by simp
+ finally show ?thesis .
+qed
+
+lemma worecSL_succ:
+assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
+shows "worecSL S L (succ j) = S j (worecSL S L j)"
+proof-
+ def i \<equiv> "succ j"
+ have i: "isSucc i" by (metis i i_def isSucc_succ)
+ have ij: "j = pred i" unfolding i_def using assms by simp
+ have 0: "succ (pred i) = i" using i by simp
+ show ?thesis unfolding ij using worecSL_isSucc[OF a i] unfolding 0 .
+qed
+
+lemma worecSL_isLim:
+assumes a: "adm_woL L" and i: "isLim i"
+shows "worecSL S L i = L (worecSL S L) i"
+proof-
+ let ?H = "mergeSL S L"
+ have "worecSL S L i = ?H (worec ?H) i"
+ unfolding worecSL_def using worec_fixpoint1[OF mergeSL[OF a]] .
+ also have "... = L (worecSL S L) i"
+ using i unfolding worecSL_def mergeSL_def isLim_def by simp
+ finally show ?thesis .
+qed
+
+definition worecZSL :: "'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where "worecZSL Z S L \<equiv> worecSL S (\<lambda> f a. if a = zero then Z else L f a)"
+
+lemma worecZSL_zero:
+assumes a: "adm_woL L"
+shows "worecZSL Z S L zero = Z"
+proof-
+ let ?L = "\<lambda> f a. if a = zero then Z else L f a"
+ have "worecZSL Z S L zero = ?L (worecZSL Z S L) zero"
+ unfolding worecZSL_def apply(rule worecSL_isLim)
+ using assms unfolding adm_woL_def by auto
+ also have "... = Z" by simp
+ finally show ?thesis .
+qed
+
+lemma worecZSL_succ:
+assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}"
+shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)"
+unfolding worecZSL_def apply(rule worecSL_succ)
+using assms unfolding adm_woL_def by auto
+
+lemma worecZSL_isLim:
+assumes a: "adm_woL L" and "isLim i" and "i \<noteq> zero"
+shows "worecZSL Z S L i = L (worecZSL Z S L) i"
+proof-
+ let ?L = "\<lambda> f a. if a = zero then Z else L f a"
+ have "worecZSL Z S L i = ?L (worecZSL Z S L) i"
+ unfolding worecZSL_def apply(rule worecSL_isLim)
+ using assms unfolding adm_woL_def by auto
+ also have "... = L (worecZSL Z S L) i" using assms by simp
+ finally show ?thesis .
+qed
+
+
+subsection {* Well-order succ-lim induction: *}
+
+lemma ord_cases:
+obtains j where "i = succ j" and "aboveS j \<noteq> {}" | "isLim i"
+by (metis isLim_def isSucc_def)
+
+lemma well_order_inductSL[case_names Suc Lim]:
+assumes SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
+LIM: "\<And>i. \<lbrakk>isLim i; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
+shows "P i"
+proof(induction rule: well_order_induct)
+ fix i assume 0: "\<forall>j. j \<noteq> i \<and> (j, i) \<in> r \<longrightarrow> P j"
+ show "P i" proof(cases i rule: ord_cases)
+ fix j assume i: "i = succ j" and j: "aboveS j \<noteq> {}"
+ hence "j \<noteq> i \<and> (j, i) \<in> r" by (metis succ_diff succ_in)
+ hence 1: "P j" using 0 by simp
+ show "P i" unfolding i apply(rule SUCC) using 1 j by auto
+ qed(insert 0 LIM, unfold underS_def, auto)
+qed
+
+lemma well_order_inductZSL[case_names Zero Suc Lim]:
+assumes ZERO: "P zero"
+and SUCC: "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and
+LIM: "\<And>i. \<lbrakk>isLim i; i \<noteq> zero; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i"
+shows "P i"
+apply(induction rule: well_order_inductSL) using assms by auto
+
+(* Succesor and limit ordinals *)
+definition "isSuccOrd \<equiv> \<exists> j \<in> Field r. \<forall> i \<in> Field r. (i,j) \<in> r"
+definition "isLimOrd \<equiv> \<not> isSuccOrd"
+
+lemma isLimOrd_succ:
+assumes isLimOrd and "i \<in> Field r"
+shows "succ i \<in> Field r"
+using assms unfolding isLimOrd_def isSuccOrd_def
+by (metis REFL in_notinI refl_on_domain succ_smallest)
+
+lemma isLimOrd_aboveS:
+assumes l: isLimOrd and i: "i \<in> Field r"
+shows "aboveS i \<noteq> {}"
+proof-
+ obtain j where "j \<in> Field r" and "(j,i) \<notin> r"
+ using assms unfolding isLimOrd_def isSuccOrd_def by auto
+ hence "(i,j) \<in> r \<and> j \<noteq> i" by (metis i max2_def max2_greater)
+ thus ?thesis unfolding aboveS_def by auto
+qed
+
+lemma succ_aboveS_isLimOrd:
+assumes "\<forall> i \<in> Field r. aboveS i \<noteq> {} \<and> succ i \<in> Field r"
+shows isLimOrd
+unfolding isLimOrd_def isSuccOrd_def proof safe
+ fix j assume j: "j \<in> Field r" "\<forall>i\<in>Field r. (i, j) \<in> r"
+ hence "(succ j, j) \<in> r" using assms by auto
+ moreover have "aboveS j \<noteq> {}" using assms j unfolding aboveS_def by auto
+ ultimately show False by (metis succ_not_in)
+qed
+
+lemma isLim_iff:
+assumes l: "isLim i" and j: "j \<in> underS i"
+shows "\<exists> k. k \<in> underS i \<and> j \<in> underS k"
+proof-
+ have a: "aboveS j \<noteq> {}" using j unfolding underS_def aboveS_def by auto
+ show ?thesis apply(rule exI[of _ "succ j"]) apply safe
+ using assms a unfolding underS_def isLim_def
+ apply (metis (lifting, full_types) isSucc_def mem_Collect_eq succ_smallest)
+ by (metis (lifting, full_types) a mem_Collect_eq succ_diff succ_in)
+qed
+
+
+end (* context wo_rel *)
+
+abbreviation "zero \<equiv> wo_rel.zero"
+abbreviation "succ \<equiv> wo_rel.succ"
+abbreviation "pred \<equiv> wo_rel.pred"
+abbreviation "isSucc \<equiv> wo_rel.isSucc"
+abbreviation "isLim \<equiv> wo_rel.isLim"
+abbreviation "isLimOrd \<equiv> wo_rel.isLimOrd"
+abbreviation "isSuccOrd \<equiv> wo_rel.isSuccOrd"
+abbreviation "adm_woL \<equiv> wo_rel.adm_woL"
+abbreviation "worecSL \<equiv> wo_rel.worecSL"
+abbreviation "worecZSL \<equiv> wo_rel.worecZSL"
+
+section {* Projections of Wellorders *}
+
+definition "oproj r s f \<equiv> Field s \<subseteq> f ` (Field r) \<and> compat r s f"
+
+lemma oproj_in:
+assumes "oproj r s f" and "(a,a') \<in> r"
+shows "(f a, f a') \<in> s"
+using assms unfolding oproj_def compat_def by auto
+
+lemma oproj_Field:
+assumes f: "oproj r s f" and a: "a \<in> Field r"
+shows "f a \<in> Field s"
+using oproj_in[OF f] a unfolding Field_def by auto
+
+lemma oproj_Field2:
+assumes f: "oproj r s f" and a: "b \<in> Field s"
+shows "\<exists> a \<in> Field r. f a = b"
+using assms unfolding oproj_def by auto
+
+lemma oproj_under:
+assumes f: "oproj r s f" and a: "a \<in> under r a'"
+shows "f a \<in> under s (f a')"
+using oproj_in[OF f] a unfolding rel.under_def by auto
+
+(* An ordinal is embedded in another whenever it is embedded as an order
+(not necessarily as initial segment):*)
+theorem embedI:
+assumes r: "Well_order r" and s: "Well_order s"
+and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
+shows "\<exists> g. embed r s g"
+proof-
+ interpret r!: wo_rel r by unfold_locales (rule r)
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ let ?G = "\<lambda> g a. suc s (g ` underS r a)"
+ def g \<equiv> "worec r ?G"
+ have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto
+ (* *)
+ {fix a assume "a \<in> Field r"
+ hence "bij_betw g (under r a) (under s (g a)) \<and>
+ g a \<in> under s (f a)"
+ proof(induction a rule: r.underS_induct)
+ case (1 a)
+ hence a: "a \<in> Field r"
+ and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)"
+ and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
+ and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
+ unfolding rel.underS_def Field_def bij_betw_def by auto
+ have fa: "f a \<in> Field s" using f[OF a] by auto
+ have g: "g a = suc s (g ` underS r a)"
+ using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
+ have A0: "g ` underS r a \<subseteq> Field s"
+ using IH1b by (metis IH2 image_subsetI in_mono rel.under_Field)
+ {fix a1 assume a1: "a1 \<in> underS r a"
+ from IH2[OF this] have "g a1 \<in> under s (f a1)" .
+ moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto
+ ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS rel.under_underS_trans)
+ }
+ hence "f a \<in> AboveS s (g ` underS r a)" unfolding rel.AboveS_def
+ using fa by simp (metis (lifting, full_types) mem_Collect_eq rel.underS_def)
+ hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto
+ have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)"
+ unfolding g apply(rule s.suc_underS[OF A0 A]) by auto
+ {fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2"
+ hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a
+ unfolding rel.underS_def rel.under_def refl_on_def Field_def by auto
+ hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto
+ hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12
+ unfolding rel.underS_def rel.under_def by auto
+ } note C = this
+ have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] .
+ have aa: "a \<in> under r a"
+ using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+ show ?case proof safe
+ show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe
+ show "inj_on g (under r a)" proof(rule r.inj_on_Field)
+ fix a1 a2 assume "a1 \<in> under r a" and a2: "a2 \<in> under r a" and a1: "a1 \<in> underS r a2"
+ hence a22: "a2 \<in> under r a2" and a12: "a1 \<in> under r a2" "a1 \<noteq> a2"
+ using a r.REFL unfolding rel.under_def rel.underS_def refl_on_def by auto
+ show "g a1 \<noteq> g a2"
+ proof(cases "a2 = a")
+ case False hence "a2 \<in> underS r a"
+ using a2 unfolding rel.underS_def rel.under_def by auto
+ from IH1a[OF this] show ?thesis using a12 a22 unfolding inj_on_def by auto
+ qed(insert B a1, unfold rel.underS_def, auto)
+ qed(unfold rel.under_def Field_def, auto)
+ next
+ fix a1 assume a1: "a1 \<in> under r a"
+ show "g a1 \<in> under s (g a)"
+ proof(cases "a1 = a")
+ case True thus ?thesis
+ using ga s.REFL unfolding refl_on_def rel.under_def by auto
+ next
+ case False
+ hence a1: "a1 \<in> underS r a" using a1 unfolding rel.underS_def rel.under_def by auto
+ thus ?thesis using B unfolding rel.underS_def rel.under_def by auto
+ qed
+ next
+ fix b1 assume b1: "b1 \<in> under s (g a)"
+ show "b1 \<in> g ` under r a"
+ proof(cases "b1 = g a")
+ case True thus ?thesis using aa by auto
+ next
+ case False
+ hence "b1 \<in> underS s (g a)" using b1 unfolding rel.underS_def rel.under_def by auto
+ from s.underS_suc[OF this[unfolded g] A0]
+ obtain a1 where a1: "a1 \<in> underS r a" and b1: "b1 \<in> under s (g a1)" by auto
+ obtain a2 where "a2 \<in> under r a1" and b1: "b1 = g a2" using IH1b[OF a1] b1 by auto
+ hence "a2 \<in> under r a" using a1
+ by (metis r.ANTISYM r.TRANS in_mono rel.underS_subset_under rel.under_underS_trans)
+ thus ?thesis using b1 by auto
+ qed
+ qed
+ next
+ have "(g a, f a) \<in> s" unfolding g proof(rule s.suc_least[OF A0])
+ fix b1 assume "b1 \<in> g ` underS r a"
+ then obtain a1 where a1: "b1 = g a1" and a1: "a1 \<in> underS r a" by auto
+ hence "b1 \<in> underS s (f a)"
+ using a by (metis `\<And>a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (f a)`)
+ thus "f a \<noteq> b1 \<and> (b1, f a) \<in> s" unfolding rel.underS_def by auto
+ qed(insert fa, auto)
+ thus "g a \<in> under s (f a)" unfolding rel.under_def by auto
+ qed
+ qed
+ }
+ thus ?thesis unfolding embed_def by auto
+qed
+
+corollary ordLeq_def2:
+ "r \<le>o s \<longleftrightarrow> Well_order r \<and> Well_order s \<and>
+ (\<exists> f. \<forall> a \<in> Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a))"
+using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s]
+unfolding ordLeq_def by fast
+
+lemma iso_oproj:
+ assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
+ shows "oproj r s f"
+using assms unfolding oproj_def
+by (subst (asm) iso_iff3) (auto simp: bij_betw_def)
+
+theorem oproj_embed:
+assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
+shows "\<exists> g. embed s r g"
+proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold rel.underS_def, safe)
+ fix b assume "b \<in> Field s"
+ thus "inv_into (Field r) f b \<in> Field r" using oproj_Field2[OF f] by (metis imageI inv_into_into)
+next
+ fix a b assume "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
+ "inv_into (Field r) f a = inv_into (Field r) f b"
+ with f show False by (auto dest!: inv_into_injective simp: Field_def oproj_def)
+next
+ fix a b assume *: "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s"
+ { assume "(inv_into (Field r) f a, inv_into (Field r) f b) \<notin> r"
+ moreover
+ from *(3) have "a \<in> Field s" unfolding Field_def by auto
+ with *(1,2) have
+ "inv_into (Field r) f a \<in> Field r" "inv_into (Field r) f b \<in> Field r"
+ "inv_into (Field r) f a \<noteq> inv_into (Field r) f b"
+ by (auto dest!: oproj_Field2[OF f] inv_into_injective intro!: inv_into_into)
+ ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r"
+ using r by (auto simp: well_order_on_def linear_order_on_def total_on_def)
+ with f[unfolded oproj_def compat_def] *(1) `a \<in> Field s`
+ f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"]
+ have "(b, a) \<in> s" by (metis in_mono)
+ with *(2,3) s have False
+ by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def)
+ } thus "(inv_into (Field r) f a, inv_into (Field r) f b) \<in> r" by blast
+qed
+
+corollary oproj_ordLeq:
+assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
+shows "s \<le>o r"
+using oproj_embed[OF assms] r s unfolding ordLeq_def by auto
+
end
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Fri Jan 10 23:44:03 2014 +0100
@@ -1617,5 +1617,158 @@
ultimately show ?thesis by blast
qed
+definition Func where
+"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"
+
+lemma Func_empty:
+"Func {} B = {\<lambda>x. undefined}"
+unfolding Func_def by auto
+
+lemma Func_elim:
+assumes "g \<in> Func A B" and "a \<in> A"
+shows "\<exists> b. b \<in> B \<and> g a = b"
+using assms unfolding Func_def by (cases "g a = undefined") auto
+
+definition curr where
+"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
+
+lemma curr_in:
+assumes f: "f \<in> Func (A <*> B) C"
+shows "curr A f \<in> Func A (Func B C)"
+using assms unfolding curr_def Func_def by auto
+
+lemma curr_inj:
+assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
+shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
+proof safe
+ assume c: "curr A f1 = curr A f2"
+ show "f1 = f2"
+ proof (rule ext, clarify)
+ fix a b show "f1 (a, b) = f2 (a, b)"
+ proof (cases "(a,b) \<in> A <*> B")
+ case False
+ thus ?thesis using assms unfolding Func_def by auto
+ next
+ case True hence a: "a \<in> A" and b: "b \<in> B" by auto
+ thus ?thesis
+ using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
+ qed
+ qed
+qed
+
+lemma curr_surj:
+assumes "g \<in> Func A (Func B C)"
+shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
+proof
+ let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
+ show "curr A ?f = g"
+ proof (rule ext)
+ fix a show "curr A ?f a = g a"
+ proof (cases "a \<in> A")
+ case False
+ hence "g a = undefined" using assms unfolding Func_def by auto
+ thus ?thesis unfolding curr_def using False by simp
+ next
+ case True
+ obtain g1 where "g1 \<in> Func B C" and "g a = g1"
+ using assms using Func_elim[OF assms True] by blast
+ thus ?thesis using True unfolding Func_def curr_def by auto
+ qed
+ qed
+ show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
+qed
+
+lemma bij_betw_curr:
+"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
+unfolding bij_betw_def inj_on_def image_def
+apply (intro impI conjI ballI)
+apply (erule curr_inj[THEN iffD1], assumption+)
+apply auto
+apply (erule curr_in)
+using curr_surj by blast
+
+definition Func_map where
+"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
+
+lemma Func_map:
+assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
+shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
+using assms unfolding Func_def Func_map_def mem_Collect_eq by auto
+
+lemma Func_non_emp:
+assumes "B \<noteq> {}"
+shows "Func A B \<noteq> {}"
+proof-
+ obtain b where b: "b \<in> B" using assms by auto
+ hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
+ thus ?thesis by blast
+qed
+
+lemma Func_is_emp:
+"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
+proof
+ assume L: ?L
+ moreover {assume "A = {}" hence False using L Func_empty by auto}
+ moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis}
+ ultimately show ?R by blast
+next
+ assume R: ?R
+ moreover
+ {fix f assume "f \<in> Func A B"
+ moreover obtain a where "a \<in> A" using R by blast
+ ultimately obtain b where "b \<in> B" unfolding Func_def by blast
+ with R have False by blast
+ }
+ thus ?L by blast
+qed
+
+lemma Func_map_surj:
+assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
+and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
+shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
+proof(cases "B2 = {}")
+ case True
+ thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
+next
+ case False note B2 = False
+ show ?thesis
+ proof safe
+ fix h assume h: "h \<in> Func B2 B1"
+ def j1 \<equiv> "inv_into A1 f1"
+ have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
+ then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis
+ {fix b2 assume b2: "b2 \<in> B2"
+ hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
+ moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
+ ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
+ } note kk = this
+ obtain b22 where b22: "b22 \<in> B2" using B2 by auto
+ def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
+ have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
+ have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
+ using kk unfolding j2_def by auto
+ def g \<equiv> "Func_map A2 j1 j2 h"
+ have "Func_map B2 f1 f2 g = h"
+ proof (rule ext)
+ fix b2 show "Func_map B2 f1 f2 g b2 = h b2"
+ proof(cases "b2 \<in> B2")
+ case True
+ show ?thesis
+ proof (cases "h b2 = undefined")
+ case True
+ hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto
+ show ?thesis using A2 f_inv_into_f[OF b1]
+ unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto
+ qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
+ auto intro: f_inv_into_f)
+ qed(insert h, unfold Func_def Func_map_def, auto)
+ qed
+ moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
+ using inv_into_into j2A2 B1 A2 inv_into_into
+ unfolding j1_def image_def by fast+
+ ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
+ unfolding Func_map_def[abs_def] unfolding image_def by auto
+ qed(insert B1 Func_map[OF _ _ A2(2)], auto)
+qed
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Jan 10 23:44:03 2014 +0100
@@ -0,0 +1,1728 @@
+(* Title: HOL/Cardinals/Ordinal_Arithmetic.thy
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2014
+
+Ordinal arithmetic.
+*)
+
+header {* Ordinal Arithmetic *}
+
+theory Ordinal_Arithmetic
+imports Constructions_on_Wellorders
+begin
+
+definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70)
+where
+ "r +o r' = map_pair Inl Inl ` r \<union> map_pair Inr Inr ` r' \<union>
+ {(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
+
+lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'"
+ unfolding osum_def Field_def by auto
+
+lemma osum_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r +o r')"
+ (*Need first unfold Field_osum, only then osum_def*)
+ unfolding refl_on_def Field_osum unfolding osum_def by blast
+
+lemma osum_trans:
+assumes TRANS: "trans r" and TRANS': "trans r'"
+shows "trans (r +o r')"
+proof(unfold trans_def, safe)
+ fix x y z assume *: "(x, y) \<in> r +o r'" "(y, z) \<in> r +o r'"
+ thus "(x, z) \<in> r +o r'"
+ proof (cases x y z rule: sum.exhaust[case_product sum.exhaust sum.exhaust])
+ case (Inl_Inl_Inl a b c)
+ with * have "(a,b) \<in> r" "(b,c) \<in> r" unfolding osum_def by auto
+ with TRANS have "(a,c) \<in> r" unfolding trans_def by blast
+ with Inl_Inl_Inl show ?thesis unfolding osum_def by auto
+ next
+ case (Inl_Inl_Inr a b c)
+ with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto
+ with Inl_Inl_Inr show ?thesis unfolding osum_def by auto
+ next
+ case (Inl_Inr_Inr a b c)
+ with * have "a \<in> Field r" "c \<in> Field r'" unfolding osum_def Field_def by auto
+ with Inl_Inr_Inr show ?thesis unfolding osum_def by auto
+ next
+ case (Inr_Inr_Inr a b c)
+ with * have "(a,b) \<in> r'" "(b,c) \<in> r'" unfolding osum_def by auto
+ with TRANS' have "(a,c) \<in> r'" unfolding trans_def by blast
+ with Inr_Inr_Inr show ?thesis unfolding osum_def by auto
+ qed (auto simp: osum_def)
+qed
+
+lemma osum_Preorder: "\<lbrakk>Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r +o r')"
+ unfolding preorder_on_def using osum_Refl osum_trans by blast
+
+lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r +o r')"
+ unfolding antisym_def osum_def by auto
+
+lemma osum_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r +o r')"
+ unfolding partial_order_on_def using osum_Preorder osum_antisym by blast
+
+lemma osum_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r +o r')"
+ unfolding total_on_def Field_osum unfolding osum_def by blast
+
+lemma osum_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r +o r')"
+ unfolding linear_order_on_def using osum_Partial_order osum_Total by blast
+
+lemma osum_wf:
+assumes WF: "wf r" and WF': "wf r'"
+shows "wf (r +o r')"
+unfolding wf_eq_minimal2 unfolding Field_osum
+proof(intro allI impI, elim conjE)
+ fix A assume *: "A \<subseteq> Inl ` Field r \<union> Inr ` Field r'" and **: "A \<noteq> {}"
+ obtain B where B_def: "B = A Int Inl ` Field r" by blast
+ show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r +o r'"
+ proof(cases "B = {}")
+ case False
+ hence "B \<noteq> {}" "B \<le> Inl ` Field r" using B_def by auto
+ hence "Inl -` B \<noteq> {}" "Inl -` B \<le> Field r" unfolding vimage_def by auto
+ then obtain a where 1: "a \<in> Inl -` B" and "\<forall>a1 \<in> Inl -` B. (a1, a) \<notin> r"
+ using WF unfolding wf_eq_minimal2 by metis
+ hence "\<forall>a1 \<in> A. (a1, Inl a) \<notin> r +o r'"
+ unfolding osum_def using B_def ** by (auto simp: vimage_def Field_def)
+ thus ?thesis using 1 unfolding B_def by auto
+ next
+ case True
+ hence 1: "A \<le> Inr ` Field r'" using * B_def by auto
+ with ** have "Inr -`A \<noteq> {}" "Inr -` A \<le> Field r'" unfolding vimage_def by auto
+ with ** obtain a' where 2: "a' \<in> Inr -` A" and "\<forall>a1' \<in> Inr -` A. (a1',a') \<notin> r'"
+ using WF' unfolding wf_eq_minimal2 by metis
+ hence "\<forall>a1' \<in> A. (a1', Inr a') \<notin> r +o r'"
+ unfolding osum_def using ** 1 by (auto simp: vimage_def Field_def)
+ thus ?thesis using 2 by blast
+ qed
+qed
+
+lemma osum_minus_Id:
+ assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)"
+ shows "(r +o r') - Id \<le> (r - Id) +o (r' - Id)"
+ unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto
+
+lemma osum_minus_Id1:
+ "r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_pair Inr Inr ` (r' - Id))"
+ unfolding osum_def by auto
+
+lemma osum_minus_Id2:
+ "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_pair Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
+ unfolding osum_def by auto
+
+lemma osum_wf_Id:
+ assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
+ shows "wf ((r +o r') - Id)"
+proof(cases "r \<le> Id \<or> r' \<le> Id")
+ case False
+ thus ?thesis
+ using osum_minus_Id[of r r'] assms osum_wf[of "r - Id" "r' - Id"]
+ wf_subset[of "(r - Id) +o (r' - Id)" "(r +o r') - Id"] by auto
+next
+ have 1: "wf (Inl ` Field r \<times> Inr ` Field r')" by (rule wf_Int_Times) auto
+ case True
+ thus ?thesis
+ proof (elim disjE)
+ assume "r \<subseteq> Id"
+ thus "wf ((r +o r') - Id)"
+ by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_pair_image[OF WF']]]) auto
+ next
+ assume "r' \<subseteq> Id"
+ thus "wf ((r +o r') - Id)"
+ by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_pair_image[OF WF] 1]]) auto
+ qed
+qed
+
+lemma osum_Well_order:
+assumes WELL: "Well_order r" and WELL': "Well_order r'"
+shows "Well_order (r +o 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
+
+lemma osum_embedL:
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "embed r (r +o r') Inl"
+proof -
+ have 1: "Well_order (r +o r')" using assms by (auto simp add: osum_Well_order)
+ moreover
+ have "compat r (r +o r') Inl" unfolding compat_def osum_def by auto
+ moreover
+ have "ofilter (r +o r') (Inl ` Field r)"
+ unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_osum rel.under_def
+ unfolding osum_def Field_def by auto
+ ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
+qed
+
+corollary osum_ordLeqL:
+ assumes WELL: "Well_order r" and WELL': "Well_order r'"
+ shows "r \<le>o r +o r'"
+ using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast
+
+lemma dir_image_alt: "dir_image r f = map_pair f f ` r"
+ unfolding dir_image_def map_pair_def by auto
+
+lemma map_pair_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_pair f f ` r =o r"
+ unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
+
+definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" (infixr "*o" 80)
+where "r *o r' = {((x1, y1), (x2, y2)).
+ (((y1, y2) \<in> r' - Id \<and> x1 \<in> Field r \<and> x2 \<in> Field r) \<or>
+ ((y1, y2) \<in> Restr Id (Field r') \<and> (x1, x2) \<in> r))}"
+
+lemma Field_oprod: "Field (r *o r') = Field r \<times> Field r'"
+ unfolding oprod_def Field_def by auto blast+
+
+lemma oprod_Refl:"\<lbrakk>Refl r; Refl r'\<rbrakk> \<Longrightarrow> Refl (r *o r')"
+ unfolding refl_on_def Field_oprod unfolding oprod_def by auto
+
+lemma oprod_trans:
+ assumes "trans r" "trans r'" "antisym r" "antisym r'"
+ shows "trans (r *o r')"
+proof(unfold trans_def, safe)
+ fix x y z assume *: "(x, y) \<in> r *o r'" "(y, z) \<in> r *o r'"
+ thus "(x, z) \<in> r *o r'"
+ unfolding oprod_def
+ apply safe
+ apply (metis assms(2) transE)
+ apply (metis assms(2) transE)
+ apply (metis assms(2) transE)
+ apply (metis assms(4) antisymD)
+ apply (metis assms(4) antisymD)
+ apply (metis assms(2) transE)
+ apply (metis assms(4) antisymD)
+ apply (metis Field_def Range_iff Un_iff)
+ apply (metis Field_def Range_iff Un_iff)
+ apply (metis Field_def Range_iff Un_iff)
+ apply (metis Field_def Domain_iff Un_iff)
+ apply (metis Field_def Domain_iff Un_iff)
+ apply (metis Field_def Domain_iff Un_iff)
+ apply (metis assms(1) transE)
+ apply (metis assms(1) transE)
+ apply (metis assms(1) transE)
+ apply (metis assms(1) transE)
+ done
+qed
+
+lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')"
+ unfolding preorder_on_def using oprod_Refl oprod_trans by blast
+
+lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r *o r')"
+ unfolding antisym_def oprod_def by auto
+
+lemma oprod_Partial_order: "\<lbrakk>Partial_order r; Partial_order r'\<rbrakk> \<Longrightarrow> Partial_order (r *o r')"
+ unfolding partial_order_on_def using oprod_Preorder oprod_antisym by blast
+
+lemma oprod_Total: "\<lbrakk>Total r; Total r'\<rbrakk> \<Longrightarrow> Total (r *o r')"
+ unfolding total_on_def Field_oprod unfolding oprod_def by auto
+
+lemma oprod_Linear_order: "\<lbrakk>Linear_order r; Linear_order r'\<rbrakk> \<Longrightarrow> Linear_order (r *o r')"
+ unfolding linear_order_on_def using oprod_Partial_order oprod_Total by blast
+
+lemma oprod_wf:
+assumes WF: "wf r" and WF': "wf r'"
+shows "wf (r *o r')"
+unfolding wf_eq_minimal2 unfolding Field_oprod
+proof(intro allI impI, elim conjE)
+ fix A assume *: "A \<subseteq> Field r \<times> Field r'" and **: "A \<noteq> {}"
+ then obtain y where y: "y \<in> snd ` A" "\<forall>y'\<in>snd ` A. (y', y) \<notin> r'"
+ using spec[OF WF'[unfolded wf_eq_minimal2], of "snd ` A"] by auto
+ let ?A = "fst ` A \<inter> {x. (x, y) \<in> A}"
+ from * y have "?A \<noteq> {}" "?A \<subseteq> Field r" by auto
+ then obtain x where x: "x \<in> ?A" and "\<forall>x'\<in> ?A. (x', x) \<notin> r"
+ using spec[OF WF[unfolded wf_eq_minimal2], of "?A"] by auto
+ with y have "\<forall>a'\<in>A. (a', (x, y)) \<notin> r *o r'"
+ unfolding oprod_def mem_Collect_eq split_beta fst_conv snd_conv Id_def by auto
+ moreover from x have "(x, y) \<in> A" by auto
+ ultimately show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r *o r'" by blast
+qed
+
+lemma oprod_minus_Id:
+ assumes r: "Total r" "\<not> (r \<le> Id)" and r': "Total r'" "\<not> (r' \<le> Id)"
+ shows "(r *o r') - Id \<le> (r - Id) *o (r' - Id)"
+ unfolding oprod_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto
+
+lemma oprod_minus_Id1:
+ "r \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x,y1), (x,y2)). x \<in> Field r \<and> (y1, y2) \<in> (r' - Id)}"
+ unfolding oprod_def by auto
+
+lemma wf_extend_oprod1:
+ assumes "wf r"
+ shows "wf {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}"
+proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
+ fix B
+ assume *: "B \<subseteq> Field {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" and "B \<noteq> {}"
+ from image_mono[OF *, of snd] have "snd ` B \<subseteq> Field r" unfolding Field_def by force
+ with `B \<noteq> {}` obtain x where x: "x \<in> snd ` B" "\<forall>x'\<in>snd ` B. (x', x) \<notin> r"
+ using spec[OF assms[unfolded wf_eq_minimal2], of "snd ` B"] by auto
+ then obtain a where "(a, x) \<in> B" by auto
+ moreover
+ from * x have "\<forall>a'\<in>B. (a', (a, x)) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by auto
+ ultimately show "\<exists>ax\<in>B. \<forall>a'\<in>B. (a', ax) \<notin> {((x,y1), (x,y2)) . x \<in> A \<and> (y1, y2) \<in> r}" by blast
+qed
+
+lemma oprod_minus_Id2:
+ "r' \<le> Id \<Longrightarrow> r *o r' - Id \<le> {((x1,y), (x2,y)). (x1, x2) \<in> (r - Id) \<and> y \<in> Field r'}"
+ unfolding oprod_def by auto
+
+lemma wf_extend_oprod2:
+ assumes "wf r"
+ shows "wf {((x1,y), (x2,y)) . (x1, x2) \<in> r \<and> y \<in> A}"
+proof (unfold wf_eq_minimal2, intro allI impI, elim conjE)
+ fix B
+ assume *: "B \<subseteq> Field {((x1, y), (x2, y)). (x1, x2) \<in> r \<and> y \<in> A}" and "B \<noteq> {}"
+ from image_mono[OF *, of fst] have "fst ` B \<subseteq> Field r" unfolding Field_def by force
+ with `B \<noteq> {}` obtain x where x: "x \<in> fst ` B" "\<forall>x'\<in>fst ` B. (x', x) \<notin> r"
+ using spec[OF assms[unfolded wf_eq_minimal2], of "fst ` B"] by auto
+ then obtain a where "(x, a) \<in> B" by auto
+ moreover
+ from * x have "\<forall>a'\<in>B. (a', (x, a)) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by auto
+ ultimately show "\<exists>xa\<in>B. \<forall>a'\<in>B. (a', xa) \<notin> {((x1, y), x2, y). (x1, x2) \<in> r \<and> y \<in> A}" by blast
+qed
+
+lemma oprod_wf_Id:
+ assumes TOT: "Total r" and TOT': "Total r'" and WF: "wf(r - Id)" and WF': "wf(r' - Id)"
+ shows "wf ((r *o r') - Id)"
+proof(cases "r \<le> Id \<or> r' \<le> Id")
+ case False
+ thus ?thesis
+ using oprod_minus_Id[of r r'] assms oprod_wf[of "r - Id" "r' - Id"]
+ wf_subset[of "(r - Id) *o (r' - Id)" "(r *o r') - Id"] by auto
+next
+ case True
+ thus ?thesis using wf_subset[OF wf_extend_oprod1[OF WF'] oprod_minus_Id1]
+ wf_subset[OF wf_extend_oprod2[OF WF] oprod_minus_Id2] by auto
+qed
+
+lemma oprod_Well_order:
+assumes WELL: "Well_order r" and WELL': "Well_order r'"
+shows "Well_order (r *o 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 oprod_Linear_order oprod_wf_Id by blast
+qed
+
+lemma oprod_embed:
+ assumes WELL: "Well_order r" and WELL': "Well_order r'" and "r' \<noteq> {}"
+ shows "embed r (r *o r') (\<lambda>x. (x, minim r' (Field r')))" (is "embed _ _ ?f")
+proof -
+ from assms(3) have r': "Field r' \<noteq> {}" unfolding Field_def by auto
+ have minim[simp]: "minim r' (Field r') \<in> Field r'"
+ using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
+ { fix b
+ assume "(b, minim r' (Field r')) \<in> r'"
+ moreover hence "b \<in> Field r'" unfolding Field_def by auto
+ hence "(minim r' (Field r'), b) \<in> r'"
+ using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
+ ultimately have "b = minim r' (Field r')"
+ by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
+ } note * = this
+ have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
+ moreover
+ from r' have "compat r (r *o r') ?f" unfolding compat_def oprod_def by auto
+ moreover
+ from * have "ofilter (r *o r') (?f ` Field r)"
+ unfolding wo_rel.ofilter_def[unfolded wo_rel_def, OF 1] Field_oprod rel.under_def
+ unfolding oprod_def by auto (auto simp: image_iff Field_def)
+ moreover have "inj_on ?f (Field r)" unfolding inj_on_def by auto
+ ultimately show ?thesis using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
+qed
+
+corollary oprod_ordLeq: "\<lbrakk>Well_order r; Well_order r'; r' \<noteq> {}\<rbrakk> \<Longrightarrow> r \<le>o r *o r'"
+ using oprod_embed oprod_Well_order unfolding ordLeq_def by blast
+
+definition "support z A f = {x \<in> A. f x \<noteq> z}"
+
+lemma support_Un[simp]: "support z (A \<union> B) f = support z A f \<union> support z B f"
+ unfolding support_def by auto
+
+lemma support_upd[simp]: "support z A (f(x := z)) = support z A f - {x}"
+ unfolding support_def by auto
+
+lemma support_upd_subset[simp]: "support z A (f(x := y)) \<subseteq> support z A f \<union> {x}"
+ unfolding support_def by auto
+
+lemma fun_unequal_in_support:
+ assumes "f \<noteq> g" "f \<in> Func A B" "g \<in> Func A C"
+ shows "(support z A f \<union> support z A g) \<inter> {a. f a \<noteq> g a} \<noteq> {}" (is "?L \<inter> ?R \<noteq> {}")
+proof -
+ from assms(1) obtain x where x: "f x \<noteq> g x" by blast
+ hence "x \<in> ?R" by simp
+ moreover from assms(2-3) x have "x \<in> A" unfolding Func_def by fastforce
+ with x have "x \<in> ?L" unfolding support_def by auto
+ ultimately show ?thesis by auto
+qed
+
+definition fin_support where
+ "fin_support z A = {f. finite (support z A f)}"
+
+lemma finite_support: "f \<in> fin_support z A \<Longrightarrow> finite (support z A f)"
+ unfolding support_def fin_support_def by auto
+
+lemma fin_support_Field_osum:
+ "f \<in> fin_support z (Inl ` A \<union> Inr ` B) \<longleftrightarrow>
+ (f o Inl) \<in> fin_support z A \<and> (f o Inr) \<in> fin_support z B" (is "?L \<longleftrightarrow> ?R1 \<and> ?R2")
+proof safe
+ assume ?L
+ from `?L` show ?R1 unfolding fin_support_def support_def
+ by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case id undefined"])
+ from `?L` show ?R2 unfolding fin_support_def support_def
+ by (fastforce simp: image_iff elim: finite_surj[of _ _ "sum_case undefined id"])
+next
+ assume ?R1 ?R2
+ thus ?L unfolding fin_support_def support_Un
+ by (auto simp: support_def elim: finite_surj[of _ _ Inl] finite_surj[of _ _ Inr])
+qed
+
+lemma Func_upd: "\<lbrakk>f \<in> Func A B; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> f(x := y) \<in> Func A B"
+ unfolding Func_def by auto
+
+context wo_rel
+begin
+
+definition isMaxim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
+where "isMaxim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (a,b) \<in> r)"
+
+definition maxim :: "'a set \<Rightarrow> 'a"
+where "maxim A \<equiv> THE b. isMaxim A b"
+
+lemma isMaxim_unique[intro]: "\<lbrakk>isMaxim A x; isMaxim A y\<rbrakk> \<Longrightarrow> x = y"
+ unfolding isMaxim_def using antisymD[OF ANTISYM, of x y] by auto
+
+lemma maxim_isMaxim: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> isMaxim A (maxim A)"
+unfolding maxim_def
+proof (rule theI', rule ex_ex1I[OF _ isMaxim_unique, rotated], assumption+,
+ induct A rule: finite_induct)
+ case (insert x A)
+ thus ?case
+ proof (cases "A = {}")
+ case True
+ moreover have "isMaxim {x} x" unfolding isMaxim_def using refl_onD[OF REFL] insert(5) by auto
+ ultimately show ?thesis by blast
+ next
+ case False
+ with insert(3,5) obtain y where "isMaxim A y" by blast
+ with insert(2,5) have "if (y, x) \<in> r then isMaxim (insert x A) x else isMaxim (insert x A) y"
+ unfolding isMaxim_def subset_eq by (metis insert_iff max2_def max2_equals1 max2_iff)
+ thus ?thesis by metis
+ qed
+qed simp
+
+lemma maxim_in: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> maxim A \<in> A"
+ using maxim_isMaxim unfolding isMaxim_def by auto
+
+lemma maxim_greatest: "\<lbrakk>finite A; x \<in> A; A \<subseteq> Field r\<rbrakk> \<Longrightarrow> (x, maxim A) \<in> r"
+ using maxim_isMaxim unfolding isMaxim_def by auto
+
+lemma isMaxim_zero: "isMaxim A zero \<Longrightarrow> A = {zero}"
+ unfolding isMaxim_def by auto
+
+lemma maxim_insert:
+ assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "x \<in> Field r"
+ shows "maxim (insert x A) = max2 x (maxim A)"
+proof -
+ from assms have *: "isMaxim (insert x A) (maxim (insert x A))" "isMaxim A (maxim A)"
+ using maxim_isMaxim by auto
+ show ?thesis
+ proof (cases "(x, maxim A) \<in> r")
+ case True
+ with *(2) have "isMaxim (insert x A) (maxim A)" unfolding isMaxim_def
+ using transD[OF TRANS, of _ x "maxim A"] by blast
+ with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
+ next
+ case False
+ hence "(maxim A, x) \<in> r" by (metis *(2) assms(3,4) in_mono in_notinI isMaxim_def)
+ with *(2) assms(4) have "isMaxim (insert x A) x" unfolding isMaxim_def
+ using transD[OF TRANS, of _ "maxim A" x] refl_onD[OF REFL, of x] by blast
+ with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
+ qed
+qed
+
+lemma maxim_Un:
+ assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r" "finite B" "B \<noteq> {}" "B \<subseteq> Field r"
+ shows "maxim (A \<union> B) = max2 (maxim A) (maxim B)"
+proof -
+ from assms have *: "isMaxim (A \<union> B) (maxim (A \<union> B))" "isMaxim A (maxim A)" "isMaxim B (maxim B)"
+ using maxim_isMaxim by auto
+ show ?thesis
+ proof (cases "(maxim A, maxim B) \<in> r")
+ case True
+ with *(2,3) have "isMaxim (A \<union> B) (maxim B)" unfolding isMaxim_def
+ using transD[OF TRANS, of _ "maxim A" "maxim B"] by blast
+ with *(1) True show ?thesis unfolding max2_def by (metis isMaxim_unique)
+ next
+ case False
+ hence "(maxim B, maxim A) \<in> r" by (metis *(2,3) assms(3,6) in_mono in_notinI isMaxim_def)
+ with *(2,3) have "isMaxim (A \<union> B) (maxim A)" unfolding isMaxim_def
+ using transD[OF TRANS, of _ "maxim B" "maxim A"] by blast
+ with *(1) False show ?thesis unfolding max2_def by (metis isMaxim_unique)
+ qed
+qed
+
+lemma maxim_insert_zero:
+ assumes "finite A" "A \<noteq> {}" "A \<subseteq> Field r"
+ shows "maxim (insert zero A) = maxim A"
+using assms zero_in_Field maxim_in[OF assms] by (subst maxim_insert[unfolded max2_def]) auto
+
+lemma maxim_equality: "isMaxim A x \<Longrightarrow> maxim A = x"
+ unfolding maxim_def by (rule the_equality) auto
+
+lemma maxim_singleton:
+ "x \<in> Field r \<Longrightarrow> maxim {x} = x"
+ using refl_onD[OF REFL] by (intro maxim_equality) (simp add: isMaxim_def)
+
+lemma maxim_Int: "\<lbrakk>finite A; A \<noteq> {}; A \<subseteq> Field r; maxim A \<in> B\<rbrakk> \<Longrightarrow> maxim (A \<inter> B) = maxim A"
+ by (rule maxim_equality) (auto simp: isMaxim_def intro: maxim_in maxim_greatest)
+
+lemma maxim_mono: "\<lbrakk>X \<subseteq> Y; finite Y; X \<noteq> {}; Y \<subseteq> Field r\<rbrakk> \<Longrightarrow> (maxim X, maxim Y) \<in> r"
+ using maxim_in[OF finite_subset, of X Y] by (auto intro: maxim_greatest)
+
+definition "max_fun_diff f g \<equiv> maxim ({a \<in> Field r. f a \<noteq> g a})"
+
+lemma max_fun_diff_commute: "max_fun_diff f g = max_fun_diff g f"
+ unfolding max_fun_diff_def by metis
+
+lemma zero_under: "x \<in> Field r \<Longrightarrow> zero \<in> under x"
+ unfolding under_def by (auto intro: zero_smallest)
+
+end
+
+definition "FinFunc r s = Func (Field s) (Field r) \<inter> fin_support (zero r) (Field s)"
+
+lemma FinFuncD: "\<lbrakk>f \<in> FinFunc r s; x \<in> Field s\<rbrakk> \<Longrightarrow> f x \<in> Field r"
+ unfolding FinFunc_def Func_def by (fastforce split: option.splits)
+
+locale wo_rel2 =
+ fixes r s
+ assumes rWELL: "Well_order r"
+ and sWELL: "Well_order s"
+begin
+
+interpretation r!: wo_rel r by unfold_locales (rule rWELL)
+interpretation s!: wo_rel s by unfold_locales (rule sWELL)
+
+abbreviation "SUPP \<equiv> support r.zero (Field s)"
+abbreviation "FINFUNC \<equiv> FinFunc r s"
+lemmas FINFUNCD = FinFuncD[of _ r s]
+
+lemma fun_diff_alt: "{a \<in> Field s. f a \<noteq> g a} = (SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a}"
+ by (auto simp: support_def)
+
+lemma max_fun_diff_alt:
+ "s.max_fun_diff f g = s.maxim ((SUPP f \<union> SUPP g) \<inter> {a. f a \<noteq> g a})"
+ unfolding s.max_fun_diff_def fun_diff_alt ..
+
+lemma isMaxim_max_fun_diff: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
+ s.isMaxim {a \<in> Field s. f a \<noteq> g a} (s.max_fun_diff f g)"
+ using fun_unequal_in_support[of f g] unfolding max_fun_diff_alt fun_diff_alt fun_eq_iff
+ by (intro s.maxim_isMaxim) (auto simp: FinFunc_def fin_support_def support_def)
+
+lemma max_fun_diff_in: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
+ s.max_fun_diff f g \<in> {a \<in> Field s. f a \<noteq> g a}"
+ using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast
+
+lemma max_fun_diff_max: "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<in> {a \<in> Field s. f a \<noteq> g a}\<rbrakk> \<Longrightarrow>
+ (x, s.max_fun_diff f g) \<in> s"
+ using isMaxim_max_fun_diff unfolding s.isMaxim_def by blast
+
+lemma max_fun_diff:
+ "\<lbrakk>f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC\<rbrakk> \<Longrightarrow>
+ (\<exists>a b. a \<noteq> b \<and> a \<in> Field r \<and> b \<in> Field r \<and>
+ f (s.max_fun_diff f g) = a \<and> g (s.max_fun_diff f g) = b)"
+ using isMaxim_max_fun_diff[of f g] unfolding s.isMaxim_def FinFunc_def Func_def by auto
+
+lemma max_fun_diff_le_eq:
+ "\<lbrakk>(s.max_fun_diff f g, x) \<in> s; f \<noteq> g; f \<in> FINFUNC; g \<in> FINFUNC; x \<noteq> s.max_fun_diff f g\<rbrakk> \<Longrightarrow>
+ f x = g x"
+ using max_fun_diff_max[of f g x] antisymD[OF s.ANTISYM, of "s.max_fun_diff f g" x]
+ by (auto simp: Field_def)
+
+lemma max_fun_diff_max2:
+ assumes ineq: "s.max_fun_diff f g = s.max_fun_diff g h \<longrightarrow>
+ f (s.max_fun_diff f g) \<noteq> h (s.max_fun_diff g h)" and
+ fg: "f \<noteq> g" and gh: "g \<noteq> h" and fh: "f \<noteq> h" and
+ f: "f \<in> FINFUNC" and g: "g \<in> FINFUNC" and h: "h \<in> FINFUNC"
+ shows "s.max_fun_diff f h = s.max2 (s.max_fun_diff f g) (s.max_fun_diff g h)"
+ (is "?fh = s.max2 ?fg ?gh")
+proof (cases "?fg = ?gh")
+ case True
+ with ineq have "f ?fg \<noteq> h ?fg" by simp
+ moreover
+ { fix x assume x: "x \<in> {a \<in> Field s. f a \<noteq> h a}"
+ hence "(x, ?fg) \<in> s"
+ proof (cases "x = ?fg")
+ case False show ?thesis
+ proof (rule ccontr)
+ assume "(x, ?fg) \<notin> s"
+ with max_fun_diff_in[OF fg f g] x False have *: "(?fg, x) \<in> s" by (blast intro: s.in_notinI)
+ hence "f x = g x" by (rule max_fun_diff_le_eq[OF _ fg f g False])
+ moreover have "g x = h x" using max_fun_diff_le_eq[OF _ gh g h] False True * by simp
+ ultimately show False using x by simp
+ qed
+ qed (simp add: refl_onD[OF s.REFL])
+ }
+ ultimately have "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg"
+ unfolding s.isMaxim_def using max_fun_diff_in[OF fg f g] by simp
+ hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
+ thus ?thesis unfolding True s.max2_def by simp
+next
+ case False note * = this
+ show ?thesis
+ proof (cases "(?fg, ?gh) \<in> s")
+ case True
+ hence *: "f ?gh = g ?gh" by (rule max_fun_diff_le_eq[OF _ fg f g *[symmetric]])
+ hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?gh" using isMaxim_max_fun_diff[OF gh g h]
+ isMaxim_max_fun_diff[OF fg f g] transD[OF s.TRANS _ True]
+ unfolding s.isMaxim_def by auto
+ hence "?fh = ?gh" using isMaxim_max_fun_diff[OF fh f h] by blast
+ thus ?thesis using True unfolding s.max2_def by simp
+ next
+ case False
+ with max_fun_diff_in[OF fg f g] max_fun_diff_in[OF gh g h] have True: "(?gh, ?fg) \<in> s"
+ by (blast intro: s.in_notinI)
+ hence *: "g ?fg = h ?fg" by (rule max_fun_diff_le_eq[OF _ gh g h *])
+ hence "s.isMaxim {a \<in> Field s. f a \<noteq> h a} ?fg" using isMaxim_max_fun_diff[OF gh g h]
+ isMaxim_max_fun_diff[OF fg f g] True transD[OF s.TRANS, of _ _ ?fg]
+ unfolding s.isMaxim_def by auto
+ hence "?fh = ?fg" using isMaxim_max_fun_diff[OF fh f h] by blast
+ thus ?thesis using False unfolding s.max2_def by simp
+ qed
+qed
+
+
+definition oexp where
+ "oexp = {(f, g) . f \<in> FINFUNC \<and> g \<in> FINFUNC \<and>
+ ((let m = s.max_fun_diff f g in (f m, g m) \<in> r) \<or> f = g)}"
+
+lemma Field_oexp: "Field oexp = FINFUNC"
+ unfolding oexp_def FinFunc_def by (auto simp: Let_def Field_def)
+
+lemma oexp_Refl: "Refl oexp"
+ unfolding refl_on_def Field_oexp unfolding oexp_def by (auto simp: Let_def)
+
+lemma oexp_trans: "trans oexp"
+proof (unfold trans_def, safe)
+ fix f g h :: "'b \<Rightarrow> 'a"
+ let ?fg = "s.max_fun_diff f g"
+ and ?gh = "s.max_fun_diff g h"
+ and ?fh = "s.max_fun_diff f h"
+ assume oexp: "(f, g) \<in> oexp" "(g, h) \<in> oexp"
+ thus "(f, h) \<in> oexp"
+ proof (cases "f = g \<or> g = h")
+ case False
+ with oexp have "f \<in> FINFUNC" "g \<in> FINFUNC" "h \<in> FINFUNC"
+ "(f ?fg, g ?fg) \<in> r" "(g ?gh, h ?gh) \<in> r" unfolding oexp_def Let_def by auto
+ note * = this False
+ show ?thesis
+ proof (cases "f \<noteq> h")
+ case True
+ show ?thesis
+ proof (cases "?fg = ?gh \<longrightarrow> f ?fg \<noteq> h ?gh")
+ case True
+ show ?thesis using max_fun_diff_max2[of f g h, OF True] * `f \<noteq> h` max_fun_diff_in
+ r.max2_iff[OF FINFUNCD FINFUNCD] r.max2_equals1[OF FINFUNCD FINFUNCD] max_fun_diff_le_eq
+ s.in_notinI[OF disjI1] unfolding oexp_def Let_def s.max2_def mem_Collect_eq by safe metis
+ next
+ case False with * show ?thesis unfolding oexp_def Let_def
+ using antisymD[OF r.ANTISYM, of "g ?gh" "h ?gh"] max_fun_diff_in[of g h] by auto
+ qed
+ qed (auto simp: oexp_def *(3))
+ qed auto
+qed
+
+lemma oexp_Preorder: "Preorder oexp"
+ unfolding preorder_on_def using oexp_Refl oexp_trans by blast
+
+lemma oexp_antisym: "antisym oexp"
+proof (unfold antisym_def, safe, rule ccontr)
+ fix f g assume "(f, g) \<in> oexp" "(g, f) \<in> oexp" "g \<noteq> f"
+ thus False using refl_onD[OF r.REFL FINFUNCD] max_fun_diff_in unfolding oexp_def Let_def
+ by (auto dest!: antisymD[OF r.ANTISYM] simp: s.max_fun_diff_commute)
+qed
+
+lemma oexp_Partial_order: "Partial_order oexp"
+ unfolding partial_order_on_def using oexp_Preorder oexp_antisym by blast
+
+lemma oexp_Total: "Total oexp"
+ unfolding total_on_def Field_oexp unfolding oexp_def using FINFUNCD max_fun_diff_in
+ by (auto simp: Let_def s.max_fun_diff_commute intro!: r.in_notinI)
+
+lemma oexp_Linear_order: "Linear_order oexp"
+ unfolding linear_order_on_def using oexp_Partial_order oexp_Total by blast
+
+definition "const = (\<lambda>x. if x \<in> Field s then r.zero else undefined)"
+
+lemma const_in[simp]: "x \<in> Field s \<Longrightarrow> const x = r.zero"
+ unfolding const_def by auto
+
+lemma const_notin[simp]: "x \<notin> Field s \<Longrightarrow> const x = undefined"
+ unfolding const_def by auto
+
+lemma const_Int_Field[simp]: "Field s \<inter> - {x. const x = r.zero} = {}"
+ by auto
+
+lemma const_FINFUNC[simp]: "Field r \<noteq> {} \<Longrightarrow> const \<in> FINFUNC"
+ unfolding FinFunc_def Func_def fin_support_def support_def const_def Int_iff mem_Collect_eq
+ using r.zero_in_Field by (metis (lifting) Collect_empty_eq finite.emptyI)
+
+lemma const_least:
+ assumes "Field r \<noteq> {}" "f \<in> FINFUNC"
+ shows "(const, f) \<in> oexp"
+proof (cases "f = const")
+ case True thus ?thesis using refl_onD[OF oexp_Refl] assms(2) unfolding Field_oexp by auto
+next
+ case False
+ with assms show ?thesis using max_fun_diff_in[of f const]
+ unfolding oexp_def Let_def by (auto intro: r.zero_smallest FinFuncD simp: s.max_fun_diff_commute)
+qed
+
+lemma support_not_const:
+ assumes "F \<subseteq> FINFUNC" and "const \<notin> F"
+ shows "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s"
+proof (intro ballI conjI)
+ fix f assume "f \<in> F"
+ thus "finite (SUPP f)" "SUPP f \<subseteq> Field s"
+ using assms(1) unfolding FinFunc_def fin_support_def support_def by auto
+ show "SUPP f \<noteq> {}"
+ proof (rule ccontr, unfold not_not)
+ assume "SUPP f = {}"
+ moreover from `f \<in> F` assms(1) have "f \<in> FINFUNC" by blast
+ ultimately have "f = const"
+ by (auto simp: fun_eq_iff support_def FinFunc_def Func_def const_def)
+ with assms(2) `f \<in> F` show False by blast
+ qed
+qed
+
+lemma maxim_isMaxim_support:
+ assumes f: "F \<subseteq> FINFUNC" and "const \<notin> F"
+ shows "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
+ using support_not_const[OF assms] by (auto intro!: s.maxim_isMaxim)
+
+lemma oexp_empty2: "Field s = {} \<Longrightarrow> oexp = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
+ unfolding oexp_def FinFunc_def fin_support_def support_def by auto
+
+lemma oexp_empty: "\<lbrakk>Field r = {}; Field s \<noteq> {}\<rbrakk> \<Longrightarrow> oexp = {}"
+ unfolding oexp_def FinFunc_def Let_def by auto
+
+lemma fun_upd_FINFUNC: "\<lbrakk>f \<in> FINFUNC; x \<in> Field s; y \<in> Field r\<rbrakk> \<Longrightarrow> f(x := y) \<in> FINFUNC"
+ unfolding FinFunc_def Func_def fin_support_def
+ by (auto intro: finite_subset[OF support_upd_subset])
+
+lemma fun_upd_same_oexp:
+ assumes "(f, g) \<in> oexp" "f x = g x" "x \<in> Field s" "y \<in> Field r"
+ shows "(f(x := y), g(x := y)) \<in> oexp"
+proof -
+ from assms(1) fun_upd_FINFUNC[OF _ assms(3,4)] have fg: "f(x := y) \<in> FINFUNC" "g(x := y) \<in> FINFUNC"
+ unfolding oexp_def by auto
+ moreover from assms(2) have "s.max_fun_diff (f(x := y)) (g(x := y)) = s.max_fun_diff f g"
+ unfolding s.max_fun_diff_def by auto metis
+ ultimately show ?thesis using assms refl_onD[OF r.REFL] unfolding oexp_def Let_def by auto
+qed
+
+lemma fun_upd_smaller_oexp:
+ assumes "f \<in> FINFUNC" "x \<in> Field s" "y \<in> Field r" "(y, f x) \<in> r"
+ shows "(f(x := y), f) \<in> oexp"
+ using assms fun_upd_FINFUNC[OF assms(1-3)] s.maxim_singleton[of "x"]
+ unfolding oexp_def FinFunc_def Let_def fin_support_def s.max_fun_diff_def by (auto simp: fun_eq_iff)
+
+lemma oexp_wf_Id: "wf (oexp - Id)"
+proof (cases "Field r = {} \<or> Field s = {}")
+ case True thus ?thesis using oexp_empty oexp_empty2 by fastforce
+next
+ case False
+ hence Fields: "Field s \<noteq> {}" "Field r \<noteq> {}" by simp_all
+ hence [simp]: "r.zero \<in> Field r" by (intro r.zero_in_Field)
+ have const[simp]: "\<And>F. \<lbrakk>const \<in> F; F \<subseteq> FINFUNC\<rbrakk> \<Longrightarrow> \<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
+ using const_least[OF Fields(2)] by auto
+ show ?thesis
+ unfolding Linear_order_wf_diff_Id[OF oexp_Linear_order] Field_oexp
+ proof (intro allI impI)
+ fix A assume A: "A \<subseteq> FINFUNC" "A \<noteq> {}"
+ { fix y F
+ have "F \<subseteq> FINFUNC \<and> (\<exists>f \<in> F. y = s.maxim (SUPP f)) \<longrightarrow>
+ (\<exists>f0 \<in> F. \<forall>f \<in> F. (f0, f) \<in> oexp)" (is "?P F y")
+ proof (induct y arbitrary: F rule: s.well_order_induct)
+ case (1 y)
+ show ?case
+ proof (intro impI, elim conjE bexE)
+ fix f assume F: "F \<subseteq> FINFUNC" "f \<in> F" "y = s.maxim (SUPP f)"
+ thus "\<exists>f0\<in>F. \<forall>f\<in>F. (f0, f) \<in> oexp"
+ proof (cases "const \<in> F")
+ case False
+ with F have maxF: "\<forall>f \<in> F. s.isMaxim (SUPP f) (s.maxim (SUPP f))"
+ and SUPPF: "\<forall>f \<in> F. finite (SUPP f) \<and> SUPP f \<noteq> {} \<and> SUPP f \<subseteq> Field s"
+ using maxim_isMaxim_support support_not_const by auto
+ def z \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> F}"
+ from F SUPPF maxF have zmin: "s.isMinim {s.maxim (SUPP f) | f. f \<in> F} z"
+ unfolding z_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
+ with F have zy: "(z, y) \<in> s" unfolding s.isMinim_def by auto
+ hence zField: "z \<in> Field s" unfolding Field_def by auto
+ def x0 \<equiv> "r.minim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)}"
+ from F(1,2) maxF(1) SUPPF zmin
+ have x0min: "r.isMinim {f z | f. f \<in> F \<and> z = s.maxim (SUPP f)} x0"
+ unfolding x0_def s.isMaxim_def s.isMinim_def
+ by (blast intro!: r.minim_isMinim FinFuncD[of _ r s])
+ with maxF(1) SUPPF F(1) have x0Field: "x0 \<in> Field r"
+ unfolding r.isMinim_def s.isMaxim_def by (auto intro!: FINFUNCD)
+ from x0min maxF(1) SUPPF F(1) have x0notzero: "x0 \<noteq> r.zero"
+ unfolding r.isMinim_def s.isMaxim_def FinFunc_def Func_def support_def
+ by fastforce
+ def G \<equiv> "{f(z := r.zero) | f. f \<in> F \<and> z = s.maxim (SUPP f) \<and> f z = x0}"
+ from zmin x0min have "G \<noteq> {}" unfolding G_def z_def s.isMinim_def r.isMinim_def by blast
+ have GF: "G \<subseteq> (\<lambda>f. f(z := r.zero)) ` F" unfolding G_def by auto
+ have "G \<subseteq> fin_support r.zero (Field s)"
+ unfolding FinFunc_def fin_support_def proof safe
+ fix g assume "g \<in> G"
+ with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto
+ moreover with SUPPF have "finite (SUPP f)" by blast
+ ultimately show "finite (SUPP g)"
+ by (elim finite_subset[rotated]) (auto simp: support_def)
+ qed
+ moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
+ using Func_upd[of _ "Field s" "Field r" z r.zero] unfolding FinFunc_def by auto
+ ultimately have G: "G \<subseteq> FINFUNC" unfolding FinFunc_def by blast
+ hence "\<exists>g0\<in>G. \<forall>g\<in>G. (g0, g) \<in> oexp"
+ proof (cases "const \<in> G")
+ case False
+ with G have maxG: "\<forall>g \<in> G. s.isMaxim (SUPP g) (s.maxim (SUPP g))"
+ and SUPPG: "\<forall>g \<in> G. finite (SUPP g) \<and> SUPP g \<noteq> {} \<and> SUPP g \<subseteq> Field s"
+ using maxim_isMaxim_support support_not_const by auto
+ def y' \<equiv> "s.minim {s.maxim (SUPP f) | f. f \<in> G}"
+ from G SUPPG maxG `G \<noteq> {}` have y'min: "s.isMinim {s.maxim (SUPP f) | f. f \<in> G} y'"
+ unfolding y'_def by (intro s.minim_isMinim) (auto simp: s.isMaxim_def)
+ moreover
+ have "\<forall>g \<in> G. z \<notin> SUPP g" unfolding support_def G_def by auto
+ moreover
+ { fix g assume g: "g \<in> G"
+ then obtain f where "f \<in> F" "g = f(z := r.zero)" and z: "z = s.maxim (SUPP f)"
+ unfolding G_def by auto
+ with SUPPF bspec[OF SUPPG g] have "(s.maxim (SUPP g), z) \<in> s"
+ unfolding z by (intro s.maxim_mono) auto
+ }
+ moreover from y'min have "\<And>g. g \<in> G \<Longrightarrow> (y', s.maxim (SUPP g)) \<in> s"
+ unfolding s.isMinim_def by auto
+ ultimately have "y' \<noteq> z" "(y', z) \<in> s" using maxG
+ unfolding s.isMinim_def s.isMaxim_def by auto
+ with zy have "y' \<noteq> y" "(y', y) \<in> s" using antisymD[OF s.ANTISYM] transD[OF s.TRANS]
+ by blast+
+ moreover from `G \<noteq> {}` have "\<exists>g \<in> G. y' = wo_rel.maxim s (SUPP g)" using y'min
+ by (auto simp: G_def s.isMinim_def)
+ ultimately show ?thesis using mp[OF spec[OF mp[OF spec[OF 1]]], of y' G] G by auto
+ qed simp
+ then obtain g0 where g0: "g0 \<in> G" "\<forall>g \<in> G. (g0, g) \<in> oexp" by blast
+ hence g0z: "g0 z = r.zero" unfolding G_def by auto
+ def f0 \<equiv> "g0(z := x0)"
+ with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
+ from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
+ have f0: "f0 \<in> F" using x0min g0(1)
+ Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
+ unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
+ from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
+ by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
+ show ?thesis
+ proof (intro bexI[OF _ f0] ballI)
+ fix f assume f: "f \<in> F"
+ show "(f0, f) \<in> oexp"
+ proof (cases "f0 = f")
+ case True thus ?thesis by (metis F(1) Field_oexp f0 in_mono oexp_Refl refl_onD)
+ next
+ case False
+ thus ?thesis
+ proof (cases "s.maxim (SUPP f) = z \<and> f z = x0")
+ case True
+ with f have "f(z := r.zero) \<in> G" unfolding G_def by blast
+ with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto
+ hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
+ by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
+ moreover
+ with f F(1) x0min True
+ have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
+ by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
+ ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
+ unfolding f0_def by auto
+ next
+ case False note notG = this
+ thus ?thesis
+ proof (cases "s.maxim (SUPP f) = z")
+ case True
+ with notG have "f0 z \<noteq> f z" unfolding f0_def by auto
+ hence "f0 z \<noteq> f z" by metis
+ with True maxf0 f0 f SUPPF have "s.max_fun_diff f0 f = z"
+ using s.maxim_Un[of "SUPP f0" "SUPP f", unfolded s.max2_def]
+ unfolding max_fun_diff_alt by (intro trans[OF s.maxim_Int]) auto
+ moreover
+ from x0min True f have "(x0, f z) \<in> r" unfolding r.isMinim_def by auto
+ ultimately show ?thesis using f f0 F(1) unfolding oexp_def f0_def by auto
+ next
+ case False
+ with notG have *: "(z, s.maxim (SUPP f)) \<in> s" "z \<noteq> s.maxim (SUPP f)"
+ using zmin f unfolding s.isMinim_def G_def by auto
+ have f0f: "f0 (s.maxim (SUPP f)) = r.zero"
+ proof (rule ccontr)
+ assume "f0 (s.maxim (SUPP f)) \<noteq> r.zero"
+ with f SUPPF maxF(1) have "s.maxim (SUPP f) \<in> SUPP f0"
+ unfolding support_def[of _ _ f0] s.isMaxim_def by auto
+ with SUPPF f0 have "(s.maxim (SUPP f), z) \<in> s" unfolding maxf0[symmetric]
+ by (auto intro: s.maxim_greatest)
+ with * antisymD[OF s.ANTISYM] show False by simp
+ qed
+ moreover
+ have "f (s.maxim (SUPP f)) \<noteq> r.zero"
+ using bspec[OF maxF(1) f, unfolded s.isMaxim_def] by (auto simp: support_def)
+ with f0f * f f0 maxf0 SUPPF
+ have "s.max_fun_diff f0 f = s.maxim (SUPP f0 \<union> SUPP f)"
+ unfolding max_fun_diff_alt using s.maxim_Un[of "SUPP f0" "SUPP f"]
+ by (intro s.maxim_Int) (auto simp: s.max2_def)
+ moreover have "s.maxim (SUPP f0 \<union> SUPP f) = s.maxim (SUPP f)"
+ using s.maxim_Un[of "SUPP f0" "SUPP f"] * maxf0 SUPPF f0 f
+ by (auto simp: s.max2_def)
+ ultimately show ?thesis using f f0 F(1) maxF(1) SUPPF unfolding oexp_def Let_def
+ by (fastforce simp: s.isMaxim_def intro!: r.zero_smallest FINFUNCD)
+ qed
+ qed
+ qed
+ qed
+ qed simp
+ qed
+ qed
+ } note * = mp[OF this]
+ from A(2) obtain f where f: "f \<in> A" by blast
+ with A(1) show "\<exists>a\<in>A. \<forall>a'\<in>A. (a, a') \<in> oexp"
+ proof (cases "f = const")
+ case False with f A(1) show ?thesis using maxim_isMaxim_support[of "{f}"]
+ by (intro *[of _ "s.maxim (SUPP f)"]) (auto simp: s.isMaxim_def support_def)
+ qed simp
+ qed
+qed
+
+lemma oexp_Well_order: "Well_order oexp"
+ unfolding well_order_on_def using oexp_Linear_order oexp_wf_Id by blast
+
+interpretation o: wo_rel oexp by unfold_locales (rule oexp_Well_order)
+
+lemma zero_oexp: "Field r \<noteq> {} \<Longrightarrow> o.zero = const"
+ by (rule sym[OF o.leq_zero_imp[OF const_least]])
+ (auto intro!: o.zero_in_Field[unfolded Field_oexp] dest!: const_FINFUNC)
+
+end
+
+notation wo_rel2.oexp (infixl "^o" 90)
+lemmas oexp_def = wo_rel2.oexp_def[unfolded wo_rel2_def, OF conjI]
+lemmas oexp_Well_order = wo_rel2.oexp_Well_order[unfolded wo_rel2_def, OF conjI]
+lemmas Field_oexp = wo_rel2.Field_oexp[unfolded wo_rel2_def, OF conjI]
+
+definition "ozero = {}"
+
+lemma ozero_Well_order[simp]: "Well_order ozero"
+ unfolding ozero_def by simp
+
+lemma ozero_ordIso[simp]: "ozero =o ozero"
+ unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def by auto
+
+lemma Field_ozero[simp]: "Field ozero = {}"
+ unfolding ozero_def by simp
+
+lemma iso_ozero_empty[simp]: "r =o ozero = (r = {})"
+ unfolding ozero_def ordIso_def iso_def[abs_def] embed_def bij_betw_def
+ by (auto dest: rel.well_order_on_domain)
+
+lemma ozero_ordLeq:
+assumes "Well_order r" shows "ozero \<le>o r"
+using assms unfolding ozero_def ordLeq_def embed_def[abs_def] rel.under_def by auto
+
+definition "oone = {((),())}"
+
+lemma oone_Well_order[simp]: "Well_order oone"
+ unfolding oone_def unfolding well_order_on_def linear_order_on_def partial_order_on_def
+ preorder_on_def total_on_def refl_on_def trans_def antisym_def by auto
+
+lemma Field_oone[simp]: "Field oone = {()}"
+ unfolding oone_def by simp
+
+lemma oone_ordIso: "oone =o {(x,x)}"
+ unfolding ordIso_def oone_def well_order_on_def linear_order_on_def partial_order_on_def
+ preorder_on_def total_on_def refl_on_def trans_def antisym_def
+ by (auto simp: iso_def embed_def bij_betw_def rel.under_def inj_on_def intro!: exI[of _ "\<lambda>_. x"])
+
+lemma osum_ordLeqR: "Well_order r \<Longrightarrow> Well_order s \<Longrightarrow> s \<le>o r +o s"
+ unfolding ordLeq_def2 rel.underS_def
+ by (auto intro!: exI[of _ Inr] osum_Well_order) (auto simp add: osum_def Field_def)
+
+lemma osum_congL:
+ assumes "r =o s" and t: "Well_order t"
+ shows "r +o t =o s +o t" (is "?L =o ?R")
+proof -
+ from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
+ unfolding ordIso_def by blast
+ let ?f = "sum_map f id"
+ from f have "inj_on ?f (Field ?L)"
+ unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
+ with f have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
+ moreover from f have "compat ?L ?R ?f"
+ unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
+ by (auto simp: map_pair_imageI)
+ ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
+ thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
+qed
+
+lemma osum_congR:
+ assumes "r =o s" and t: "Well_order t"
+ shows "t +o r =o t +o s" (is "?L =o ?R")
+proof -
+ from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
+ unfolding ordIso_def by blast
+ let ?f = "sum_map id f"
+ from f have "inj_on ?f (Field ?L)"
+ unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
+ with f have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
+ moreover from f have "compat ?L ?R ?f"
+ unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def
+ by (auto simp: map_pair_imageI)
+ ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
+ thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
+qed
+
+lemma osum_cong:
+ assumes "t =o u" and "r =o s"
+ shows "t +o r =o u +o s"
+using ordIso_transitive[OF osum_congL[OF assms(1)] osum_congR[OF assms(2)]]
+ assms[unfolded ordIso_def] by auto
+
+lemma Well_order_empty[simp]: "Well_order {}"
+ unfolding Field_empty by (rule well_order_on_empty)
+
+lemma well_order_on_singleton[simp]: "well_order_on {x} {(x, x)}"
+ unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def total_on_def
+ Field_def refl_on_def trans_def antisym_def by auto
+
+lemma oexp_empty[simp]:
+ assumes "Well_order r"
+ shows "r ^o {} = {(\<lambda>x. undefined, \<lambda>x. undefined)}"
+ unfolding oexp_def[OF assms Well_order_empty] FinFunc_def fin_support_def support_def by auto
+
+lemma oexp_empty2[simp]:
+ assumes "Well_order r" "r \<noteq> {}"
+ shows "{} ^o r = {}"
+proof -
+ from assms(2) have "Field r \<noteq> {}" unfolding Field_def by auto
+ thus ?thesis unfolding oexp_def[OF Well_order_empty assms(1)] FinFunc_def fin_support_def support_def
+ by auto
+qed
+
+lemma oprod_zero[simp]: "{} *o r = {}" "r *o {} = {}"
+ unfolding oprod_def by simp_all
+
+lemma oprod_congL:
+ assumes "r =o s" and t: "Well_order t"
+ shows "r *o t =o s *o t" (is "?L =o ?R")
+proof -
+ from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
+ unfolding ordIso_def by blast
+ let ?f = "map_pair f id"
+ from f have "inj_on ?f (Field ?L)"
+ unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
+ with f have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
+ moreover from f have "compat ?L ?R ?f"
+ unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
+ by (auto simp: map_pair_imageI)
+ ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
+ thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
+qed
+
+lemma oprod_congR:
+ assumes "r =o s" and t: "Well_order t"
+ shows "t *o r =o t *o s" (is "?L =o ?R")
+proof -
+ from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
+ unfolding ordIso_def by blast
+ let ?f = "map_pair id f"
+ from f have "inj_on ?f (Field ?L)"
+ unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
+ with f have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
+ moreover from f rel.well_order_on_domain[OF r] have "compat ?L ?R ?f"
+ unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
+ by (auto simp: map_pair_imageI dest: inj_onD)
+ ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
+ thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
+qed
+
+lemma oprod_cong:
+ assumes "t =o u" and "r =o s"
+ shows "t *o r =o u *o s"
+using ordIso_transitive[OF oprod_congL[OF assms(1)] oprod_congR[OF assms(2)]]
+ assms[unfolded ordIso_def] by auto
+
+lemma Field_singleton[simp]: "Field {(z,z)} = {z}"
+ by (metis rel.well_order_on_Field well_order_on_singleton)
+
+lemma zero_singleton[simp]: "zero {(z,z)} = z"
+ using wo_rel.zero_in_Field[unfolded wo_rel_def, of "{(z, z)}"] well_order_on_singleton[of z]
+ by auto
+
+lemma FinFunc_singleton: "FinFunc {(z,z)} s = {\<lambda>x. if x \<in> Field s then z else undefined}"
+ unfolding FinFunc_def Func_def fin_support_def support_def
+ by (auto simp: fun_eq_iff split: split_if_asm intro!: finite_subset[of _ "{}"])
+
+lemma oone_ordIso_oexp:
+ assumes "r =o oone" and s: "Well_order s"
+ shows "r ^o s =o oone" (is "?L =o ?R")
+proof -
+ from assms obtain f where *: "\<forall>x\<in>Field r. \<forall>y\<in>Field r. x = y" and "f ` Field r = {()}"
+ and r: "Well_order r"
+ unfolding ordIso_def oone_def by (auto simp: iso_def bij_betw_def inj_on_def)
+ then obtain x where "x \<in> Field r" by auto
+ with * have Fr: "Field r = {x}" by auto
+ interpret r: wo_rel r by unfold_locales (rule r)
+ from Fr r.well_order_on_domain[OF r] refl_onD[OF r.REFL, of x] have r_def: "r = {(x, x)}" by fast
+ interpret wo_rel2 r s by unfold_locales (rule r, rule s)
+ have "bij_betw (\<lambda>x. ()) (Field ?L) (Field ?R)"
+ unfolding bij_betw_def Field_oexp by (auto simp: r_def FinFunc_singleton)
+ moreover have "compat ?L ?R (\<lambda>x. ())" unfolding compat_def oone_def by auto
+ ultimately have "iso ?L ?R (\<lambda>x. ())" using s oone_Well_order
+ by (subst iso_iff3) (auto intro: oexp_Well_order)
+ thus ?thesis using s oone_Well_order unfolding ordIso_def by (auto intro: oexp_Well_order)
+qed
+
+(*Lemma 1.4.3 from Holz et al.*)
+context
+ fixes r s t
+ assumes r: "Well_order r"
+ assumes s: "Well_order s"
+ assumes t: "Well_order t"
+begin
+
+lemma osum_ozeroL: "ozero +o r =o r"
+ using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
+
+lemma osum_ozeroR: "r +o ozero =o r"
+ using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
+
+lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R")
+proof -
+ let ?f =
+ "\<lambda>rst. case rst of Inl (Inl r) \<Rightarrow> Inl r | Inl (Inr s) \<Rightarrow> Inr (Inl s) | Inr t \<Rightarrow> Inr (Inr t)"
+ have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_osum bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
+ moreover
+ have "compat ?L ?R ?f"
+ proof (unfold compat_def, safe)
+ fix a b
+ assume "(a, b) \<in> ?L"
+ thus "(?f a, ?f b) \<in> ?R"
+ unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum
+ unfolding osum_def Field_osum image_iff image_Un map_pair_def
+ by fastforce
+ qed
+ ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order)
+ thus ?thesis using r s t unfolding ordIso_def by (auto intro: osum_Well_order)
+qed
+
+lemma osum_monoR:
+ assumes "s <o t"
+ shows "r +o s <o r +o t" (is "?L <o ?R")
+proof -
+ from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
+ unfolding ordLess_def by blast
+ hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
+ using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
+ unfolding embedS_def by auto
+ let ?f = "sum_map id f"
+ from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
+ moreover
+ from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce
+ moreover
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
+ from *(3) have "ofilter ?R (?f ` Field ?L)"
+ unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image rel.under_def
+ by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
+ ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
+ by (auto intro: osum_Well_order r s t)
+ moreover
+ from *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_osum image_Un image_image by auto
+ ultimately have "embedS ?L ?R ?f" using embedS_iff[OF osum_Well_order[OF r s], of ?R ?f] by auto
+ thus ?thesis unfolding ordLess_def by (auto intro: osum_Well_order r s t)
+qed
+
+lemma osum_monoL:
+ assumes "r \<le>o s"
+ shows "r +o t \<le>o s +o t"
+proof -
+ from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
+ unfolding ordLeq_def2 by blast
+ let ?f = "sum_map f id"
+ from f have "\<forall>a\<in>Field (r +o t).
+ ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
+ unfolding Field_osum rel.underS_def by (fastforce simp: osum_def)
+ thus ?thesis unfolding ordLeq_def2 by (auto intro: osum_Well_order r s t)
+qed
+
+lemma oprod_ozeroL: "ozero *o r =o ozero"
+ using ozero_ordIso unfolding ozero_def by simp
+
+lemma oprod_ozeroR: "r *o ozero =o ozero"
+ using ozero_ordIso unfolding ozero_def by simp
+
+lemma oprod_ooneR: "r *o oone =o r" (is "?L =o ?R")
+proof -
+ have "bij_betw fst (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
+ moreover have "compat ?L ?R fst" unfolding compat_def oprod_def by auto
+ ultimately have "iso ?L ?R fst" using r oone_Well_order
+ by (subst iso_iff3) (auto intro: oprod_Well_order)
+ thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
+qed
+
+lemma oprod_ooneL: "oone *o r =o r" (is "?L =o ?R")
+proof -
+ have "bij_betw snd (Field ?L) (Field ?R)" unfolding Field_oprod bij_betw_def inj_on_def by simp
+ moreover have "Refl r" by (rule wo_rel.REFL[unfolded wo_rel_def, OF r])
+ hence "compat ?L ?R snd" unfolding compat_def oprod_def refl_on_def by auto
+ ultimately have "iso ?L ?R snd" using r oone_Well_order
+ by (subst iso_iff3) (auto intro: oprod_Well_order)
+ thus ?thesis using r oone_Well_order unfolding ordIso_def by (auto intro: oprod_Well_order)
+qed
+
+lemma oprod_monoR:
+ assumes "ozero <o r" "s <o t"
+ shows "r *o s <o r *o t" (is "?L <o ?R")
+proof -
+ from assms obtain f where s: "Well_order s" and t:" Well_order t" and "embedS s t f"
+ unfolding ordLess_def by blast
+ hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
+ using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
+ unfolding embedS_def by auto
+ let ?f = "map_pair id f"
+ from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
+ moreover
+ from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
+ by auto (metis rel.well_order_on_domain t, metis rel.well_order_on_domain s)
+ moreover
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
+ from *(3) have "ofilter ?R (?f ` Field ?L)"
+ unfolding t.ofilter_def rt.ofilter_def Field_oprod rel.under_def
+ by (auto simp: oprod_def image_iff) (fast | metis r rel.well_order_on_domain)+
+ ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
+ by (auto intro: oprod_Well_order r s t)
+ moreover
+ from not_ordLess_ordIso[OF assms(1)] have "r \<noteq> {}" by (metis ozero_def ozero_ordIso)
+ hence "Field r \<noteq> {}" unfolding Field_def by auto
+ with *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_oprod
+ by auto (metis SigmaD2 SigmaI map_pair_surj_on)
+ ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto
+ thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t)
+qed
+
+lemma oprod_monoL:
+ assumes "r \<le>o s"
+ shows "r *o t \<le>o s *o t"
+proof -
+ from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
+ unfolding ordLeq_def2 by blast
+ let ?f = "map_pair f id"
+ from f have "\<forall>a\<in>Field (r *o t).
+ ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
+ unfolding Field_oprod rel.underS_def unfolding map_pair_def oprod_def by auto
+ thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
+qed
+
+lemma oprod_assoc: "(r *o s) *o t =o r *o s *o t" (is "?L =o ?R")
+proof -
+ let ?f = "\<lambda>((a,b),c). (a,b,c)"
+ have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding Field_oprod bij_betw_def inj_on_def by (auto simp: image_Un image_iff)
+ moreover
+ have "compat ?L ?R ?f"
+ proof (unfold compat_def, safe)
+ fix a1 a2 a3 b1 b2 b3
+ assume "(((a1, a2), a3), ((b1, b2), b3)) \<in> ?L"
+ thus "((a1, a2, a3), (b1, b2, b3)) \<in> ?R"
+ unfolding oprod_def[of "r *o s" t] oprod_def[of r "s *o t"] Field_oprod
+ unfolding oprod_def Field_oprod image_iff image_Un by fast
+ qed
+ ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: oprod_Well_order)
+ thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order)
+qed
+
+lemma oprod_osum: "r *o (s +o t) =o r *o s +o r *o t" (is "?L =o ?R")
+proof -
+ let ?f = "\<lambda>(a,bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)"
+ have "bij_betw ?f (Field ?L) (Field ?R)" unfolding Field_oprod Field_osum bij_betw_def inj_on_def
+ by (fastforce simp: image_Un image_iff split: sum.splits)
+ moreover
+ have "compat ?L ?R ?f"
+ proof (unfold compat_def, intro allI impI)
+ fix a b
+ assume "(a, b) \<in> ?L"
+ thus "(?f a, ?f b) \<in> ?R"
+ unfolding oprod_def[of r "s +o t"] osum_def[of "r *o s" "r *o t"] Field_oprod Field_osum
+ unfolding oprod_def osum_def Field_oprod Field_osum image_iff image_Un by auto
+ qed
+ ultimately have "iso ?L ?R ?f" using r s t
+ by (subst iso_iff3) (auto intro: oprod_Well_order osum_Well_order)
+ thus ?thesis using r s t unfolding ordIso_def by (auto intro: oprod_Well_order osum_Well_order)
+qed
+
+lemma ozero_oexp: "\<not> (s =o ozero) \<Longrightarrow> ozero ^o s =o ozero"
+ unfolding oexp_def[OF ozero_Well_order s] FinFunc_def
+ by simp (metis Func_emp2 bot.extremum_uniqueI emptyE rel.well_order_on_domain s subrelI)
+
+lemma oone_oexp: "oone ^o s =o oone" (is "?L =o ?R")
+ by (rule oone_ordIso_oexp[OF ordIso_reflexive[OF oone_Well_order] s])
+
+lemma oexp_monoR:
+ assumes "oone <o r" "s <o t"
+ shows "r ^o s <o r ^o t" (is "?L <o ?R")
+proof -
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
+ interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
+ interpret r!: wo_rel r by unfold_locales (rule r)
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
+ moreover
+ { assume "Field r = {r.zero}"
+ hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto
+ hence "r =o oone" by (metis oone_ordIso ordIso_symmetric)
+ with not_ordLess_ordIso[OF assms(1)] have False by (metis ordIso_symmetric)
+ }
+ ultimately obtain x where x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
+ by (metis insert_iff r.zero_in_Field subsetI subset_singletonD)
+ moreover from assms(2) obtain f where "embedS s t f" unfolding ordLess_def by blast
+ hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
+ using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
+ unfolding embedS_def by auto
+ note invff = the_inv_into_f_f[OF *(1)] and injfD = inj_onD[OF *(1)]
+ def F \<equiv> "\<lambda>g z. if z \<in> f ` Field s then g (the_inv_into (Field s) f z) else
+ if z \<in> Field t then r.zero else undefined"
+ from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L \<subseteq> Field ?R"
+ unfolding rt.Field_oexp rs.Field_oexp FinFunc_def Func_def fin_support_def support_def F_def
+ by (fastforce split: option.splits split_if_asm elim!: finite_surj[of _ _ f])
+ have "inj_on F (Field ?L)" unfolding rs.Field_oexp inj_on_def fun_eq_iff
+ proof safe
+ fix g h x assume "g \<in> FinFunc r s" "h \<in> FinFunc r s" "\<forall>y. F g y = F h y"
+ with invff show "g x = h x" unfolding F_def fun_eq_iff FinFunc_def Func_def
+ by auto (metis image_eqI)
+ qed
+ moreover
+ have "compat ?L ?R F" unfolding compat_def rs.oexp_def rt.oexp_def
+ proof (safe elim!: bspec[OF iffD1[OF image_subset_iff FLR[unfolded rs.Field_oexp rt.Field_oexp]]])
+ fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r s" "F g \<noteq> F h"
+ "let m = s.max_fun_diff g h in (g m, h m) \<in> r"
+ hence "g \<noteq> h" by auto
+ note max_fun_diff_in = rs.max_fun_diff_in[OF `g \<noteq> h` gh(1,2)]
+ and max_fun_diff_max = rs.max_fun_diff_max[OF `g \<noteq> h` gh(1,2)]
+ with *(4) invff *(2) have "t.max_fun_diff (F g) (F h) = f (s.max_fun_diff g h)"
+ unfolding t.max_fun_diff_def compat_def
+ by (intro t.maxim_equality) (auto simp: t.isMaxim_def F_def dest: injfD)
+ with gh invff max_fun_diff_in
+ show "let m = t.max_fun_diff (F g) (F h) in (F g m, F h m) \<in> r"
+ unfolding F_def Let_def by (auto simp: dest: injfD)
+ qed
+ moreover
+ from FLR have "ofilter ?R (F ` Field ?L)"
+ unfolding rexpt.ofilter_def rel.under_def rs.Field_oexp rt.Field_oexp unfolding rt.oexp_def
+ proof (safe elim!: imageI)
+ fix g h assume gh: "g \<in> FinFunc r s" "h \<in> FinFunc r t" "F g \<in> FinFunc r t"
+ "let m = t.max_fun_diff h (F g) in (h m, F g m) \<in> r"
+ thus "h \<in> F ` FinFunc r s"
+ proof (cases "h = F g")
+ case False
+ hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}"
+ by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
+ { assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s"
+ with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
+ moreover
+ with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
+ ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
+ }
+ hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast
+ { fix z assume z: "z \<in> Field t - f ` Field s"
+ have "(t.max_fun_diff h (F g), z) \<in> t"
+ proof (rule ccontr)
+ assume "(t.max_fun_diff h (F g), z) \<notin> t"
+ hence "(z, t.max_fun_diff h (F g)) \<in> t" using t.in_notinI[of "t.max_fun_diff h (F g)" z]
+ z max_Field by auto
+ hence "z \<in> f ` Field s" using *(3) max_f_Field unfolding t.ofilter_def rel.under_def
+ by fastforce
+ with z show False by blast
+ qed
+ hence "h z = r.zero" using rt.max_fun_diff_le_eq[OF _ False gh(2,3), of z]
+ z max_f_Field unfolding F_def by auto
+ } note ** = this
+ with *(3) gh(2) have "h = F (\<lambda>x. if x \<in> Field s then h (f x) else undefined)" using invff
+ unfolding F_def fun_eq_iff FinFunc_def Func_def Let_def t.ofilter_def rel.under_def by auto
+ moreover from gh(2) *(1,3) have "(\<lambda>x. if x \<in> Field s then h (f x) else undefined) \<in> FinFunc r s"
+ unfolding FinFunc_def Func_def fin_support_def support_def t.ofilter_def rel.under_def
+ by (auto intro: subset_inj_on elim!: finite_imageD[OF finite_subset[rotated]])
+ ultimately show "?thesis" by (rule image_eqI)
+ qed simp
+ qed
+ ultimately have "embed ?L ?R F" using embed_iff_compat_inj_on_ofilter[of ?L ?R F]
+ by (auto intro: oexp_Well_order r s t)
+ moreover
+ from FLR have "F ` Field ?L \<subset> Field ?R"
+ proof (intro psubsetI)
+ from *(4) obtain z where z: "z \<in> Field t" "z \<notin> f ` Field s" by auto
+ def h \<equiv> "\<lambda>z'. if z' \<in> Field t then if z' = z then x else r.zero else undefined"
+ from z x(3) have "rt.SUPP h = {z}" unfolding support_def h_def by simp
+ with x have "h \<in> Field ?R" unfolding h_def rt.Field_oexp FinFunc_def Func_def fin_support_def
+ by auto
+ moreover
+ { fix g
+ from z have "F g z = r.zero" "h z = x" unfolding support_def h_def F_def by auto
+ with x(3) have "F g \<noteq> h" unfolding fun_eq_iff by fastforce
+ }
+ hence "h \<notin> F ` Field ?L" by blast
+ ultimately show "F ` Field ?L \<noteq> Field ?R" by blast
+ qed
+ ultimately have "embedS ?L ?R F" using embedS_iff[OF rs.oexp_Well_order, of ?R F] by auto
+ thus ?thesis unfolding ordLess_def using r s t by (auto intro: oexp_Well_order)
+qed
+
+lemma oexp_monoL:
+ assumes "r \<le>o s"
+ shows "r ^o t \<le>o s ^o t"
+proof -
+ interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
+ interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t)
+ interpret r!: wo_rel r by unfold_locales (rule r)
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ show ?thesis
+ proof (cases "t = {}")
+ case True thus ?thesis using r s unfolding ordLeq_def2 rel.underS_def by auto
+ next
+ case False thus ?thesis
+ proof (cases "r = {}")
+ case True thus ?thesis using t `t \<noteq> {}` st.oexp_Well_order ozero_ordLeq[unfolded ozero_def]
+ by auto
+ next
+ case False
+ from assms obtain f where f: "embed r s f" unfolding ordLeq_def by blast
+ hence f_underS: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
+ using embed_in_Field[OF rt.rWELL f] embed_underS2[OF rt.rWELL st.rWELL f] by auto
+ from f `t \<noteq> {}` False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
+ unfolding Field_def embed_def rel.under_def bij_betw_def by auto
+ with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
+ using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF r.under_Field] by blast
+ with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
+ unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
+ by (fastforce intro: s.leq_zero_imp)+
+ let ?f = "\<lambda>g x. if x \<in> Field t then f (g x) else undefined"
+ { fix g assume g: "g \<in> Field (r ^o t)"
+ with fz f_underS have Field_fg: "?f g \<in> Field (s ^o t)"
+ unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
+ by (auto elim!: finite_subset[rotated])
+ moreover
+ have "?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
+ proof safe
+ fix h
+ assume h_underS: "h \<in> underS (r ^o t) g"
+ hence "h \<in> Field (r ^o t)" unfolding rel.underS_def Field_def by auto
+ with fz f_underS have Field_fh: "?f h \<in> Field (s ^o t)"
+ unfolding st.Field_oexp rt.Field_oexp FinFunc_def Func_def fin_support_def support_def
+ by (auto elim!: finite_subset[rotated])
+ from h_underS have "h \<noteq> g" and hg: "(h, g) \<in> rt.oexp" unfolding rel.underS_def by auto
+ with f inj have neq: "?f h \<noteq> ?f g"
+ unfolding fun_eq_iff inj_on_def rt.oexp_def Option.map_def FinFunc_def Func_def Let_def
+ by simp metis
+ moreover
+ with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
+ using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`]
+ by (subst t.max_fun_diff_def, intro t.maxim_equality)
+ (auto simp: t.isMaxim_def intro: inj_onD[OF inj] intro!: rt.max_fun_diff_max)
+ with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
+ using rt.max_fun_diff[OF `h \<noteq> g`] rt.max_fun_diff_in[OF `h \<noteq> g`] unfolding st.Field_oexp
+ unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
+ ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding rel.underS_def by auto
+ qed
+ ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
+ by blast
+ }
+ thus ?thesis unfolding ordLeq_def2 by (fastforce intro: oexp_Well_order r s t)
+ qed
+ qed
+qed
+
+lemma ordLeq_oexp2:
+ assumes "oone <o r"
+ shows "s \<le>o r ^o s"
+proof -
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret r!: wo_rel r by unfold_locales (rule r)
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ from assms rel.well_order_on_domain[OF r] obtain x where
+ x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
+ unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def rel.under_def
+ by (auto simp: image_def)
+ (metis equals0D insert_not_empty r.under_def r.zero_in_Field rel.under_empty)
+ let ?f = "\<lambda>a b. if b \<in> Field s then if b = a then x else r.zero else undefined"
+ from x(3) have SUPP: "\<And>y. y \<in> Field s \<Longrightarrow> rs.SUPP (?f y) = {y}" unfolding support_def by auto
+ { fix y assume y: "y \<in> Field s"
+ with x(1,2) SUPP have "?f y \<in> Field (r ^o s)" unfolding rs.Field_oexp
+ by (auto simp: FinFunc_def Func_def fin_support_def)
+ moreover
+ have "?f ` underS s y \<subseteq> underS (r ^o s) (?f y)"
+ proof safe
+ fix z
+ assume "z \<in> underS s y"
+ hence z: "z \<noteq> y" "(z, y) \<in> s" "z \<in> Field s" unfolding rel.underS_def Field_def by auto
+ from x(3) y z(1,3) have "?f z \<noteq> ?f y" unfolding fun_eq_iff by auto
+ moreover
+ { from x(1,2) have "?f z \<in> FinFunc r s" "?f y \<in> FinFunc r s"
+ unfolding FinFunc_def Func_def fin_support_def by (auto simp: SUPP[OF z(3)] SUPP[OF y])
+ moreover
+ from x(3) y z(1,2) refl_onD[OF s.REFL] have "s.max_fun_diff (?f z) (?f y) = y"
+ unfolding rs.max_fun_diff_alt SUPP[OF z(3)] SUPP[OF y]
+ by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
+ ultimately have "(?f z, ?f y) \<in> rs.oexp" using y x(1)
+ unfolding rs.oexp_def Let_def by auto
+ }
+ ultimately show "?f z \<in> underS (r ^o s) (?f y)" unfolding rel.underS_def by blast
+ qed
+ ultimately have "?f y \<in> Field (r ^o s) \<and> ?f ` underS s y \<subseteq> underS (r ^o s) (?f y)" by blast
+ }
+ thus ?thesis unfolding ordLeq_def2 by (fast intro: oexp_Well_order r s)
+qed
+
+lemma FinFunc_osum:
+ "fg \<in> FinFunc r (s +o t) = (fg o Inl \<in> FinFunc r s \<and> fg o Inr \<in> FinFunc r t)"
+ (is "?L = (?R1 \<and> ?R2)")
+proof safe
+ assume ?L
+ from `?L` show ?R1 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
+ by (auto split: sum.splits)
+ from `?L` show ?R2 unfolding FinFunc_def Field_osum Func_def Int_iff fin_support_Field_osum o_def
+ by (auto split: sum.splits)
+next
+ assume ?R1 ?R2
+ thus "?L" unfolding FinFunc_def Field_osum Func_def
+ by (auto simp: fin_support_Field_osum o_def image_iff split: sum.splits) (metis sumE)
+qed
+
+lemma max_fun_diff_eq_Inl:
+ assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inl x"
+ "sum_case f1 g1 \<noteq> sum_case f2 g2"
+ "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
+ shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
+proof -
+ interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+ from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inl x)"
+ using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
+ hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
+ unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
+ thus ?P unfolding s.max_fun_diff_def by (rule s.maxim_equality)
+ from assms(3,4) have **: "g1 \<in> FinFunc r t" "g2 \<in> FinFunc r t" unfolding FinFunc_osum
+ by (auto simp: o_def)
+ show ?Q
+ proof
+ fix x
+ from * ** show "g1 x = g2 x" unfolding st.isMaxim_def Field_osum FinFunc_def Func_def fun_eq_iff
+ unfolding osum_def by (case_tac "x \<in> Field t") auto
+ qed
+qed
+
+lemma max_fun_diff_eq_Inr:
+ assumes "wo_rel.max_fun_diff (s +o t) (sum_case f1 g1) (sum_case f2 g2) = Inr x"
+ "sum_case f1 g1 \<noteq> sum_case f2 g2"
+ "sum_case f1 g1 \<in> FinFunc r (s +o t)" "sum_case f2 g2 \<in> FinFunc r (s +o t)"
+ shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
+proof -
+ interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+ from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). sum_case f1 g1 a \<noteq> sum_case f2 g2 a} (Inr x)"
+ using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
+ hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
+ unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
+ thus ?P ?Q unfolding t.max_fun_diff_def fun_eq_iff
+ by (auto intro: t.maxim_equality simp: t.isMaxim_def)
+qed
+
+lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
+proof (rule ordIso_symmetric)
+ interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
+ let ?f = "\<lambda>(f, g). sum_case f g"
+ have "bij_betw ?f (Field ?L) (Field ?R)"
+ unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
+ show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
+ by (auto simp: fun_eq_iff split: sum.splits)
+ show "?f ` (FinFunc r s \<times> FinFunc r t) = FinFunc r (s +o t)"
+ proof safe
+ fix fg assume "fg \<in> FinFunc r (s +o t)"
+ thus "fg \<in> ?f ` (FinFunc r s \<times> FinFunc r t)"
+ by (intro image_eqI[of _ _ "(fg o Inl, fg o Inr)"])
+ (auto simp: FinFunc_osum fun_eq_iff split: sum.splits)
+ qed (auto simp: FinFunc_osum o_def)
+ qed
+ moreover have "compat ?L ?R ?f"
+ unfolding compat_def rst.Field_oexp rs.Field_oexp rt.Field_oexp oprod_def
+ unfolding rst.oexp_def Let_def rs.oexp_def rt.oexp_def
+ by (fastforce simp: Field_osum FinFunc_osum o_def split: sum.splits
+ dest: max_fun_diff_eq_Inl max_fun_diff_eq_Inr)
+ ultimately have "iso ?L ?R ?f" using r s t
+ by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
+ thus "?L =o ?R" using r s t unfolding ordIso_def
+ by (auto intro: oexp_Well_order oprod_Well_order osum_Well_order)
+qed
+
+definition "rev_curr f b = (if b \<in> Field t then \<lambda>a. f (a, b) else undefined)"
+
+lemma rev_curr_FinFunc:
+ assumes Field: "Field r \<noteq> {}"
+ shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
+proof safe
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+ fix g assume g: "g \<in> FinFunc r (s *o t)"
+ hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))"
+ unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
+ rs.zero_oexp[OF Field] rev_curr_def by (auto simp: fun_eq_iff rs.const_def elim!: finite_surj)
+ with g show "rev_curr g \<in> FinFunc (r ^o s) t"
+ unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
+ by (auto simp: rev_curr_def fin_support_def)
+next
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+ fix fg assume *: "fg \<in> FinFunc (r ^o s) t"
+ let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined"
+ show "fg \<in> rev_curr ` FinFunc r (s *o t)"
+ proof (rule image_eqI[of _ _ ?g])
+ show "fg = rev_curr ?g"
+ proof
+ fix x
+ from * show "fg x = rev_curr ?g x"
+ unfolding FinFunc_def rs.Field_oexp Func_def rev_curr_def Field_oprod by auto
+ qed
+ next
+ have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) =
+ (\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
+ unfolding support_def by auto
+ from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
+ unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def these_def by force+
+ moreover hence "finite (fg ` Field t - {rs.const})" using *
+ unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
+ by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff these_def)
+ ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
+ by (subst **) (auto intro!: finite_cartesian_product)
+ with * show "?g \<in> FinFunc r (s *o t)"
+ unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def these_def
+ support_def rs.zero_oexp[OF Field] by (auto elim!: finite_subset[rotated])
+ qed
+qed
+
+lemma rev_curr_app_FinFunc[elim!]:
+ "\<lbrakk>f \<in> FinFunc r (s *o t); z \<in> Field t\<rbrakk> \<Longrightarrow> rev_curr f z \<in> FinFunc r s"
+ unfolding rev_curr_def FinFunc_def Func_def Field_oprod fin_support_def support_def
+ by (auto elim: finite_surj)
+
+lemma max_fun_diff_oprod:
+ assumes Field: "Field r \<noteq> {}" and "f \<noteq> g" "f \<in> FinFunc r (s *o t)" "g \<in> FinFunc r (s *o t)"
+ defines "m \<equiv> wo_rel.max_fun_diff t (rev_curr f) (rev_curr g)"
+ shows "wo_rel.max_fun_diff (s *o t) f g =
+ (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
+proof -
+ interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
+ interpret s!: wo_rel s by unfold_locales (rule s)
+ interpret t!: wo_rel t by unfold_locales (rule t)
+ interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+ from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
+ have diff1: "rev_curr f \<noteq> rev_curr g"
+ "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
+ unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
+ by auto fast
+ hence diff2: "rev_curr f m \<noteq> rev_curr g m" "rev_curr f m \<in> FinFunc r s" "rev_curr g m \<in> FinFunc r s"
+ using rst.max_fun_diff[OF diff1] assms(3,4) rst.max_fun_diff_in unfolding m_def by auto
+ show ?thesis unfolding st.max_fun_diff_def
+ proof (intro st.maxim_equality, unfold st.isMaxim_def Field_oprod, safe)
+ show "s.max_fun_diff (rev_curr f m) (rev_curr g m) \<in> Field s"
+ using rs.max_fun_diff_in[OF diff2] by auto
+ next
+ show "m \<in> Field t" using rst.max_fun_diff_in[OF diff1] unfolding m_def by auto
+ next
+ assume "f (s.max_fun_diff (rev_curr f m) (rev_curr g m), m) =
+ g (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)"
+ (is "f (?x, m) = g (?x, m)")
+ hence "rev_curr f m ?x = rev_curr g m ?x" unfolding rev_curr_def by auto
+ with rs.max_fun_diff[OF diff2] show False by auto
+ next
+ fix x y assume "f (x, y) \<noteq> g (x, y)" "x \<in> Field s" "y \<in> Field t"
+ thus "((x, y), (s.max_fun_diff (rev_curr f m) (rev_curr g m), m)) \<in> s *o t"
+ using rst.max_fun_diff_in[OF diff1] rs.max_fun_diff_in[OF diff2] diff1 diff2
+ rst.max_fun_diff_max[OF diff1, of y] rs.max_fun_diff_le_eq[OF _ diff2, of x]
+ unfolding oprod_def m_def rev_curr_def fun_eq_iff by auto (metis s.in_notinI)
+ qed
+qed
+
+lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
+proof (cases "r = {}")
+ case True
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+ show ?thesis
+ proof (cases "s = {} \<or> t = {}")
+ case True with `r = {}` show ?thesis
+ by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
+ intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]
+ ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
+ next
+ case False
+ moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
+ ultimately show ?thesis using `r = {}` ozero_ordIso
+ by (auto simp add: s t oprod_Well_order ozero_def)
+ qed
+next
+ case False
+ hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty)
+ show ?thesis
+ proof (rule ordIso_symmetric)
+ interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+ interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
+ interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+ have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
+ unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
+ show "inj_on rev_curr (FinFunc r (s *o t))"
+ unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
+ by (auto simp: fun_eq_iff) metis
+ show "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t" by (rule rev_curr_FinFunc[OF Field])
+ qed
+ moreover
+ have "compat ?L ?R rev_curr"
+ unfolding compat_def proof safe
+ fix fg1 fg2 assume fg: "(fg1, fg2) \<in> r ^o (s *o t)"
+ show "(rev_curr fg1, rev_curr fg2) \<in> r ^o s ^o t"
+ proof (cases "fg1 = fg2")
+ assume "fg1 \<noteq> fg2"
+ with fg show ?thesis
+ using rst.max_fun_diff_in[of "rev_curr fg1" "rev_curr fg2"]
+ max_fun_diff_oprod[OF Field, of fg1 fg2] rev_curr_FinFunc[OF Field, symmetric]
+ unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp unfolding r_st.oexp_def rst.oexp_def
+ by (auto simp: rs.oexp_def Let_def) (auto simp: rev_curr_def[abs_def])
+ next
+ assume "fg1 = fg2"
+ with fg bij show ?thesis unfolding r_st.Field_oexp rs.Field_oexp rst.Field_oexp bij_betw_def
+ by (auto simp: r_st.oexp_def rst.oexp_def)
+ qed
+ qed
+ ultimately have "iso ?L ?R rev_curr" using r s t
+ by (subst iso_iff3) (auto intro: oexp_Well_order oprod_Well_order)
+ thus "?L =o ?R" using r s t unfolding ordIso_def
+ by (auto intro: oexp_Well_order oprod_Well_order)
+ qed
+qed
+
+end (* context with 3 wellorders *)
+
+end
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Jan 10 23:42:18 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Jan 10 23:44:03 2014 +0100
@@ -52,7 +52,8 @@
val name_of_ctr: term -> string
val name_of_disc: term -> string
val dest_ctr: Proof.context -> string -> term -> term * term list
- val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
+ val dest_case: Proof.context -> string -> typ list -> term ->
+ (ctr_sugar * term list * term list) option
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
(((bool * (bool * bool)) * term list) * binding) *
@@ -266,7 +267,7 @@
(case Term.strip_comb t of
(Const (c, _), args as _ :: _) =>
(case ctr_sugar_of ctxt s of
- SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
+ SOME (ctr_sugar as {casex = Const (case_name, _), discs = discs0, selss = selss0, ...}) =>
if case_name = c then
let val n = length discs0 in
if n < length args then
@@ -278,7 +279,7 @@
val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
val branches' = map2 (curry Term.betapplys) branches branch_argss;
in
- SOME (conds, branches')
+ SOME (ctr_sugar, conds, branches')
end
else
NONE