diff --git a/thys/Conditional_Transfer_Rule/UD/UD.ML b/thys/Conditional_Transfer_Rule/UD/UD.ML --- a/thys/Conditional_Transfer_Rule/UD/UD.ML +++ b/thys/Conditional_Transfer_Rule/UD/UD.ML @@ -1,360 +1,360 @@ (* Title: UD/UD.ML Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins The following file provides an implementation of the command ud. The algorithm associated with the command ud draws inspiration and builds upon the ideas associated with/expressed in - The function Unoverload_Def.unoverload_def that was written by Fabian Immler and is available in the file HOL-Types_To_Sets/unoverload_def.ML in Isabelle2020. - The conference proceedings article titled "A Mechanized Translation from Higher-Order Logic to Set Theory" written by Alexander Krauss and Andreas Schropp [1]. [1] Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann M, Paulson LC, editors. Interactive Theorem Proving. Berlin: Springer; 2010. p. 323–38. (Lecture Notes in Computer Science; vol. 6172). *) signature UD = sig datatype ud_thm_out_type = trivial of thm | nontrivial of thm * thm val axioms_of_ci : theory -> Defs.T -> string * typ -> (string option * string) list val das_of_ci : theory -> Defs.T -> string * typ -> thm list val unoverload_definition : binding * mixfix -> string * typ -> theory -> ud_thm_out_type * theory end; structure UD : UD = struct (**** Auxiliary ****) fun mk_msg_unoverload_definition msg = "ud: " ^ msg; (**** Data ****) datatype ud_thm_out_type = trivial of thm | nontrivial of thm * thm (**** Definitional Axioms ****) (*the implementation of axioms_of_ci and da_of_ci are based on elements of the code HOL/Types_To_Sets/unoverloading.ML*) local fun match_args (Ts, Us) = if Type.could_matches (Ts, Us) then Option.map Envir.subst_type ( SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE ) else NONE; in fun axioms_of_ci thy defs (c, T) = let val const_entry = Theory.const_dep thy (c, T); val Uss = Defs.specifications_of defs (fst const_entry); in Uss |> filter (fn spec => is_some (match_args (#lhs spec, snd const_entry))) |> map (fn Us => (#def Us, #description Us)) end; fun das_of_ci thy defs = axioms_of_ci thy defs #> map #1 #> filter is_some #> map (the #> try (Thm.axiom thy)) #> filter is_some #> map (the #> Drule.abs_def); end; (**** Main ****) local val msg_no_cids = mk_msg_unoverload_definition "no suitable constant-instance definitions"; val msg_ud_ex = mk_msg_unoverload_definition "unoverloaded constant already exists"; val msg_multiple_cids = mk_msg_unoverload_definition "multiple constant-instance definitions"; val msg_extra_type_variables = mk_msg_unoverload_definition "specification depends on extra type variables"; fun map_sorts ctxt map_sortsT thm = let val Ts = thm |> Thm.full_prop_of |> (fn t => Term.add_tvars t []) val instTs = Ts |> map TVar |> map (Term.map_atyps (map_sortsT (Proof_Context.theory_of ctxt))) |> map (Thm.ctyp_of ctxt) |> curry op~~ Ts in Drule.instantiate_normalize (TVars.make instTs, Vars.empty) thm end; fun trivial_ud thy b cid' = let val (with_thm, thy') = let val b' = Binding.qualify_name true b "with" val attr = single UD_With.UDWithData.add in Global_Theory.add_thm ((b', cid'), attr) thy end val _ = let val c = Thm.derivation_name with_thm in with_thm |> single |> CTR_Utilities.thm_printer (Proof_Context.init_global thy') true c end in (trivial with_thm, thy') end; fun nontrivial_ud thy defs (b, mixfix) cid T = let fun mk_with_thm thm_rhs_ct with_def_thm cid = let val with_def_thm_rhs_ct = with_def_thm |> Thm.cprop_of |> Thm.dest_equals_rhs val inst = Thm.match (with_def_thm_rhs_ct, thm_rhs_ct) val const_with_def = with_def_thm |> Drule.instantiate_normalize inst |> Thm.symmetric val with_thm = Thm.transitive cid const_with_def in with_thm end; val ctxt = Proof_Context.init_global thy val cid' = Thm.unvarify_global thy cid val cid_rhs_ct = cid' |> Thm.cprop_of |> Thm.dest_equals_rhs val (cid_rhs_t, ctxt') = cid_rhs_ct |> Thm.term_of |> Logic.unoverload_types_term thy |> Logic.unvarify_types_local_term ctxt val rhs_consts = let val sort_const_cs = Term.add_tvarsT T [] |> map #2 |> map (Sorts.params_of_sort thy) |> flat |> distinct op= |> map #1 val consts = Term.add_consts cid_rhs_t [] val consts_no_cids = consts |> map (fn const => (const, axioms_of_ci thy defs const)) |> filter (fn (_, cid_opt) => null cid_opt) |> map fst val consts_in_sort = consts |> filter (fn (_, T) => Term.has_tfreesT T) |> filter (fn (c, _) => member op= sort_const_cs c) val elim_consts = thy |> UD_Consts.get_keys |> map (UD_Consts.const_of_key thy #> the #> dest_Const) val consts_out = consts_no_cids @ consts_in_sort |> distinct op= |> filter_out (member (swap #> Term.could_match_const) elim_consts) in consts_out end val (cs, ctxt'') = ctxt' |> Variable.variant_fixes (map (#1 #> Long_Name.base_name) rhs_consts) val fv_of_const = (map Const rhs_consts ~~ map Free (cs ~~ map #2 rhs_consts)) |> AList.lookup op= |> mk_opt_id I val rhs_const_ts = map Const rhs_consts val arg_ts = map fv_of_const rhs_const_ts val cid_rhs_t' = map_aterms fv_of_const cid_rhs_t fun declare_const_with thy = let val T = map type_of arg_ts ---> type_of cid_rhs_t' val b' = Binding.qualify_name true b "with" in Sign.declare_const_global ((b', T), mixfix) thy end val (lhst, thy') = declare_const_with thy val lhst' = Term.list_comb (lhst, arg_ts) val (with_def_thm, thy'') = let val b' = Binding.qualify_name true b "with_def" val def_t = Logic.mk_equals (lhst', cid_rhs_t') in Global_Theory.add_defs false [((b', def_t), [])] thy' |>> the_single handle ERROR c => - let val msg_match = "Specification depends on extra type variables" + let val msg_match = "Extra type variables on rhs" in if String.isSubstring msg_match c then error msg_extra_type_variables else error c end end val _ = let val c = Thm.derivation_name with_def_thm in with_def_thm |> single |> CTR_Utilities.thm_printer (Proof_Context.init_global thy'') true c end val (with_thm, thy''') = let val b' = Binding.qualify_name true b "with" val with_thm = cid' |> mk_with_thm cid_rhs_ct with_def_thm |> singleton (Proof_Context.export ctxt'' ctxt) val attr = single UD_With.UDWithData.add in Global_Theory.add_thm ((b', with_thm), attr) thy'' end val _ = let val c = Thm.derivation_name with_thm in with_thm |> single |> CTR_Utilities.thm_printer (Proof_Context.init_global thy''') true c end in (nontrivial (with_def_thm, with_thm), thy''') end; in fun unoverload_definition (b, mixfix) (c, T) thy = let (*auxiliary*) fun get_ud_const lr ud_thms = let val get_ud_const_impl = Thm.cprop_of #> lr #> Thm.term_of #> strip_abs_body #> head_of #> dest_Const in map get_ud_const_impl ud_thms end (*main*) val ctxt = Proof_Context.init_global thy val defs = Theory.defs_of thy val ud_thms = ctxt |> UD_With.UDWithData.get |> map (Local_Defs.meta_rewrite_rule ctxt) val T' = T |> Type.default_sorts_of_empty_sorts thy |> Logic.varifyT_mixed_global val _ = let val ud_lhs_consts = get_ud_const Thm.dest_equals_lhs ud_thms val ex = member (swap #> Term.could_match_const) ud_lhs_consts (c, T') in not ex orelse error msg_ud_ex end val cids = das_of_ci thy defs (c, T') val cid = if null cids then error msg_no_cids else if length cids = 1 then the_single cids else error msg_multiple_cids val cid' = let val lhs_const = cid |> Thm.cprop_of |> Thm.dest_equals_lhs |> Thm.term_of |> head_of val insts = (lhs_const, Const (c, T')) |> apply2 (Thm.cterm_of ctxt) |> Thm.first_order_match in cid |> Drule.instantiate_normalize insts |> map_sorts ctxt Type.default_sorts_of_empty_sorts |> Local_Defs.unfold ctxt ud_thms end val cid_rhs_t = cid' |> Thm.cprop_of |> Thm.dest_equals_rhs |> Thm.term_of val trivial_flag = let val ud_rhs_consts = get_ud_const Thm.dest_equals_rhs ud_thms in Term.is_comb cid_rhs_t andalso cid_rhs_t |> head_of |> is_Const andalso cid_rhs_t |> head_of |> dest_Const |> member (swap #> Term.could_match_const) ud_rhs_consts end val (ud_thm_out, thy') = if trivial_flag then trivial_ud thy b cid' else nontrivial_ud thy defs (b, mixfix) cid' T' in (ud_thm_out, thy') end; end; (**** Interface ****) val msg_not_constant = mk_msg_unoverload_definition "the input term is not a constant"; fun process_ud ((b_opt, t), mixfix) thy = let val t' = Proof_Context.read_term_pattern (Proof_Context.init_global thy) t val (c, T) = dest_Const t' handle TERM _ => error msg_not_constant val b = case b_opt of SOME b => b | NONE => Binding.name (Long_Name.base_name c) in unoverload_definition (b, mixfix) (c, T) thy |> #2 end; val parse_ud = Scan.option Parse.binding -- Parse.const -- Parse.opt_mixfix'; val _ = Outer_Syntax.command \<^command_keyword>\ud\ "unoverloading of constant-instance definitions" (parse_ud >> (process_ud #> Toplevel.theory)); end; \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML b/thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML --- a/thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML +++ b/thys/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML @@ -1,1045 +1,1051 @@ (* Title: ETTS/ETTS_Algorithm.ML Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins Implementation of the ERA. *) signature ETTS_ALGORITHM = sig (*misc*) val mk_local_typedef_ex : (string * sort) * term -> term val dest_local_typedef_ex : term -> typ * term (*output type*) datatype etts_output_type = default | verbose | active val etts_output_type_of_string : string -> etts_output_type val string_of_etts_output_type : etts_output_type -> string val is_verbose : etts_output_type -> bool val is_active : etts_output_type -> bool val is_default : etts_output_type -> bool (*relativization*) val etts_algorithm : Proof.context -> etts_output_type -> int list -> (indexname * term) list -> (term * term) list -> (Facts.ref * Token.src list) option -> (Facts.ref * Token.src list) list -> (term list * (Proof.context -> tactic)) option -> Token.src list -> thm -> (thm * int list) * Proof.context val etts_fact : Proof.context -> etts_output_type -> int list -> (indexname * term) list -> (term * term) list -> (Facts.ref * Token.src list) option -> (Facts.ref * Token.src list) list -> (term list * (Proof.context -> tactic)) option -> Token.src list -> thm list -> (thm list * int list) * Proof.context end; structure ETTS_Algorithm : ETTS_ALGORITHM = struct (**** Prerequisites ****) open UD_With; open ETTS_Utilities; open ETTS_RI; open ETTS_Substitution; (**** Misc ****) fun mk_local_typedef_ex (rcd_spec, rissett) = let val T = TFree rcd_spec val risset_ftv = rissett |> type_of |> (fn T => Term.add_tfreesT T []) |> the_single |> TFree in HOLogic.mk_exists ( "rep", T --> risset_ftv, HOLogic.mk_exists ( "abs", risset_ftv --> T, HOLogic.mk_type_definition_pred T risset_ftv $ Bound 1 $ Bound 0 $ rissett ) ) end; fun dest_local_typedef_ex t = let val (_, T', t') = HOLogic.dest_exists t handle TERM ("dest_exists", _) => raise TERM ("dest_local_typedef_ex", single t) val (_, _, t'') = HOLogic.dest_exists t' handle TERM ("dest_exists", _) => raise TERM ("dest_local_typedef_ex", single t) val (T''', _) = dest_funT T' val t''' = t'' |> HOLogic.dest_type_definition |> #3 in (T''', t''') end; (**** Output type ****) datatype etts_output_type = default | verbose | active; fun etts_output_type_of_string "" = default | etts_output_type_of_string "!" = verbose | etts_output_type_of_string "?" = active | etts_output_type_of_string _ = error "etts_output_type_of_string: invalid input"; fun string_of_etts_output_type default = "default" | string_of_etts_output_type verbose = "verbose" | string_of_etts_output_type active = "active"; fun is_verbose verbose = true | is_verbose _ = false; fun is_active active = true | is_active _ = false; fun is_default default = true | is_default _ = false; (**** Auxiliary functions ****) (*** Standard output ***) fun verbose_writer_prem etts_output_type writer c = if is_verbose etts_output_type then ETTS_Writer.write_action c writer else writer fun verbose_writer_concl_thms etts_output_type ctxt thms = if is_verbose etts_output_type then map (Thm.string_of_thm ctxt #> writeln) thms else single (); fun verbose_writer_concl_types etts_output_type ctxt Ts = if is_verbose etts_output_type then map (Syntax.string_of_typ ctxt #> writeln) Ts else single (); (*** Types-To-Sets ***) (*multiple applications of the function cancel_type_definition*) fun cancel_type_definition_repeat n thm = let fun apply_cancel_type_definition 0 thm = thm | apply_cancel_type_definition n thm = thm |> Local_Typedef.cancel_type_definition |> rotate_prems 1 |> apply_cancel_type_definition (n - 1) in thm |> apply_cancel_type_definition n |> rotate_prems (~n) end; (**** Initialization of the relativization context ****) local (*** Auxiliary ***) (*theorems used for the relativization in conjunction with transfer*) val risset_tthms = [@{thm type_definition_Domainp}, @{thm type_definition_Domainp'}]; val sc_tthms = [ @{thm typedef_bi_unique}, @{thm typedef_right_total}, @{thm typedef_left_unique}, @{thm typedef_right_unique} ]; (*obtain the types associated with a relativization isomorphism*) fun get_riT rit = rit |> type_of |> (fn T => (T |> binder_types |> the_single, body_type T)); (*create the rhs of the specification of cr*) fun mk_cr_rhst rept = let val (isoT, domT) = get_riT rept val rhst = Abs ( "r", domT, Abs ( "a", isoT, Const (\<^const_name>\HOL.eq\, domT --> domT --> HOLogic.boolT) $ Bound 1 $ (rept $ Bound 0) ) ) in rhst end; (*initialization*) fun etts_rlt_ctxt_intialize rispec = length rispec; (*declare fresh ris*) fun etts_rlt_ctxt_mk_fresh_ris ctxt rispec = rispec |> map #2 |> map (fn t => Term.add_frees t []) |> flat |> dup ||> map #1 ||> Variable.fix_new_vars ctxt |>> map Free |-> fold_rev Variable.declare_term; (*create fresh risstv isomorphic to risset*) fun etts_rlt_ctxt_mk_fresh_risstv ctxt etts_output_type writer nds rispec = let val writer' = verbose_writer_prem etts_output_type writer "types associated with the RIs..." val (rispec', ctxt') = ctxt |> (\<^sort>\HOL.type\ |> replicate nds |> Variable.invent_types) |>> curry (swap #> op~~) rispec val _ = verbose_writer_concl_types etts_output_type ctxt' (map (#1 #> TFree) rispec') in ((writer', rispec'), ctxt') end; (*assumptions for the local typedef*) fun etts_rlt_ctxt_mk_ltd_assms ctxt etts_output_type writer rispec = let val writer' = verbose_writer_prem etts_output_type writer "assumptions for the local typedef..." val (ltd_assms, ctxt') = rispec |> ( apsnd #2 #> mk_local_typedef_ex #> HOLogic.mk_Trueprop #> Thm.cterm_of ctxt |> map ) |> (fn ltdts => Assumption.add_assumes ltdts ctxt) val _ = verbose_writer_concl_thms etts_output_type ctxt' ltd_assms in ((writer', ltd_assms), ctxt') end; (*** Transfer relations associated with relativization isomorphisms ***) local fun mk_ex_crt rept = let val (isoT, domainT) = get_riT rept val crT = domainT --> isoT --> HOLogic.boolT val rhst = mk_cr_rhst rept val t = HOLogic.mk_exists ( "cr", crT, Const (\<^const_name>\HOL.eq\, crT --> crT --> HOLogic.boolT) $ Bound 0 $ rhst ) in t end; in fun etts_rlt_ctxt_mk_crs ctxt etts_output_type writer nds ltd_assms = let val writer' = verbose_writer_prem etts_output_type writer "crs..." val ((ra_var_specs, ra_thms), ctxt') = ctxt |> Obtain.result (K (REPEAT (eresolve_tac ctxt (single @{thm exE}) 1))) ltd_assms val repts = ra_var_specs |> map (#2 #> Thm.term_of) |> chop nds |> #1 val ex_cr_thms = let val hol_ex_cr_tac = resolve_tac ctxt' (single @{thm ex_eq}) 1 fun hol_cr_prover thm = Goal.prove ctxt' [] [] thm (K (hol_ex_cr_tac)) in map (mk_ex_crt #> HOLogic.mk_Trueprop #> hol_cr_prover) repts end val ((crts, hol_cr_thms), ctxt'') = ctxt' |> Obtain.result (K (REPEAT (eresolve_tac ctxt' (single @{thm exE}) 1))) ex_cr_thms |>> (fn x => x |>> map #2 |>> map Thm.term_of) val pure_cr_thms = let val pure_crts = map Logic.mk_equals (crts ~~ (map mk_cr_rhst repts)) fun pure_cr_tac thm _ = Object_Logic.full_atomize_tac ctxt'' 1 THEN resolve_tac ctxt'' (single thm) 1 fun pure_cr_prover (goal, tac_thm) = Goal.prove ctxt'' [] [] goal (pure_cr_tac tac_thm) in map pure_cr_prover (pure_crts ~~ hol_cr_thms) end val _ = verbose_writer_concl_thms etts_output_type ctxt'' pure_cr_thms in ((writer', ra_thms, crts, pure_cr_thms), ctxt'') end; end; (*** Transfer rules for the relativization isomorphisms ***) fun etts_rlt_ctxt_mk_ri_tr ctxt etts_output_type writer ra_thms pure_cr_thms = let val writer' = verbose_writer_prem etts_output_type writer "main transfer rules..." val (risset_transfer_thms, sc_transfer_thms) = let val OFthms = map list_of_pair (ra_thms ~~ pure_cr_thms) val apply_OFthms = map (fn thm => map ((curry op OF) thm) OFthms) #> flat in (risset_tthms, sc_tthms) |>> apply_OFthms ||> apply_OFthms end val _ = verbose_writer_concl_thms etts_output_type ctxt (risset_transfer_thms @ sc_transfer_thms) in (writer', risset_transfer_thms, sc_transfer_thms) end; (*** Transfer rules for the set-based terms ***) local fun get_sc_ex_rissets risset_transfer_thms sc_transfer_thms = let val nds = (length risset_transfer_thms) div (length risset_tthms) in (risset_transfer_thms, sc_transfer_thms) |>> take nds ||> chop nds ||> (nds |> chop #> #1 |> apsnd) ||> op ~~ |> op ~~ end; in fun etts_rlt_ctxt_mk_sbt_tr ctxt etts_output_type writer risset_transfer_thms sc_transfer_thms rispec sbtspec = let val writer' = verbose_writer_prem etts_output_type writer "transfer rules for the sbts..." val ((sbtspec_specs, pp_thms), ctxt') = let val sc_ex_rissets = get_sc_ex_rissets risset_transfer_thms sc_transfer_thms val scthms_of_ftv = let val scthms_ftv = ( map (#1 #> #2 #> #2 #> type_of #> dest_rissetT) rispec ~~ map reroute_sp_triple sc_ex_rissets ) in AList.lookup op= scthms_ftv end fun thm_prem_ftvs thm = thm |> Thm.prems_of |> map (fn t => Term.add_tfrees t []) |> flat |> distinct op= fun get_sc_ftv_specs (thm_ftv_specs, rvt_ftv_specs) = rvt_ftv_specs |> subtract op= (rvt_ftv_specs |> subtract op= thm_ftv_specs) fun obtain_prs ctxt ex_pr_thms = case ex_pr_thms of [] => (([], []), ctxt) | _ => Obtain.result (K (REPEAT (eresolve_tac ctxt (single @{thm exE}) 1))) ex_pr_thms ctxt in sbtspec |> ( (Thm.cterm_of ctxt #> (sbt_data_of ctxt #> the) |> apdupl) #> swap |> apsnd #> reroute_sp_ps |> map ) |> map (reroute_ps_sp #> apsnd swap) |> ( (fn (thm, t) => (thm, (thm, t))) #> ( (apfst thm_prem_ftvs) #> (type_of #> (fn t => Term.add_tfreesT t []) |> apsnd) #> get_sc_ftv_specs #> ( Option.compose (list_of_triple, scthms_of_ftv) #> ( fn xs_opt => case xs_opt of SOME xs_opt => xs_opt | NONE => [] ) |> map #> flat ) |> apsnd ) #> op OF |> apsnd |> map ) |> split_list ||> obtain_prs ctxt |> reroute_sp_ps |>> reroute_sp_ps |>> apfst op~~ |>> (#2 |> apsnd |> map |> apfst) |>> apsnd Transfer.mk_transfer_rels end val _ = verbose_writer_concl_thms etts_output_type ctxt' pp_thms in ((writer', pp_thms, sbtspec_specs), ctxt') end; end; (*** Post-processing ***) (** Post-processing 1: transfer theorems **) fun etts_rlt_ctxt_mk_transfer risset_transfer_thms sc_transfer_thms pp_thms = risset_transfer_thms @ sc_transfer_thms @ pp_thms; (** Post-processing 2: rispec lookup **) fun etts_rlt_ctxt_mk_rispec rispec = map (#1 #> swap #> apfst #1) rispec; (** Post-processing 3: sbtspec lookup **) fun etts_rlt_ctxt_mk_sbtspec sbtspec_specs = let val sbtspec_var_specs = sbtspec_specs |> filter (apfst is_Var #> #1) |> map (apfst dest_Var) val sbtspec_const_specs = sbtspec_specs |> filter (apfst is_Const #> #1) |> map (apfst dest_Const) in (sbtspec_var_specs, sbtspec_const_specs) end; in (*** Main ***) fun init_rlt_ctxt ctxt etts_output_type writer rispec sbtspec = let val nds = etts_rlt_ctxt_intialize rispec val ctxt' = etts_rlt_ctxt_mk_fresh_ris ctxt rispec val ((writer', rispec'), ctxt'') = etts_rlt_ctxt_mk_fresh_risstv ctxt' etts_output_type writer nds rispec val ((writer'', ltd_assms), ctxt''') = etts_rlt_ctxt_mk_ltd_assms ctxt'' etts_output_type writer' rispec' val ((writer''', ra_thms, crts, pure_cr_thms), ctxt'''') = etts_rlt_ctxt_mk_crs ctxt''' etts_output_type writer'' nds ltd_assms val rispec'' = rispec' ~~ crts val (writer'''', risset_transfer_thms, sc_transfer_thms) = etts_rlt_ctxt_mk_ri_tr ctxt'''' etts_output_type writer''' ra_thms pure_cr_thms val ((writer''''', pp_thms, sbtspec_specs), ctxt''''') = etts_rlt_ctxt_mk_sbt_tr ctxt'''' etts_output_type writer'''' risset_transfer_thms sc_transfer_thms rispec'' sbtspec val transfer_thms = etts_rlt_ctxt_mk_transfer risset_transfer_thms sc_transfer_thms pp_thms val rispec''' = etts_rlt_ctxt_mk_rispec rispec'' val (sbtspec_var_specs, sbtspec_const_specs) = etts_rlt_ctxt_mk_sbtspec sbtspec_specs in ( ctxt, ctxt''''', writer''''', rispec''', sbtspec_var_specs, sbtspec_const_specs, transfer_thms ) end; end; (**** Kernel of the relativization algorithm ****) local (*** Naming conventions for schematic type variables ***) fun etts_algorithm_fresh_stv ctxt writer rispec sbtspec_var_specs sbtspec_const_specs thm = let val stvs = thm |> Thm.full_prop_of |> (fn t => Term.add_tvars t []) val rispec' = rispec |> filter (fn (v, _) => member op= (map fst stvs) v) |> map (apfst (apdupr ((AList.lookup op= stvs #> the)))) val thm_stvs = let val cs = rispec' |> map fst |> map fst |> map fst in stvs |> filter (fn (v, _) => fst v |> member op= cs |> not) end val cs = let fun folder c (cs, nctxt) = let val out = Name.variant c nctxt in (fst out::cs, snd out) end val cs = rispec' |> map snd |> map fst val nctxt = fold Name.declare cs (Variable.names_of ctxt) in fold folder (thm_stvs |> map fst |> map fst) ([], nctxt) |> fst end val rhsTs = cs ~~ map (reroute_ps_sp #> snd) thm_stvs |> map reroute_sp_ps |> map TVar val thm' = let val rhs_cT = map (Thm.ctyp_of ctxt) rhsTs - in Drule.instantiate_normalize (thm_stvs ~~ rhs_cT, []) thm end + in + Drule.instantiate_normalize + (TVars.make (thm_stvs ~~ rhs_cT), Vars.empty) thm + end fun thm_stvs_map (v, T) = case AList.lookup op= (thm_stvs ~~ rhsTs) (v, T) of SOME T => T | NONE => TVar (v, T) val sbtspec_var_specs = sbtspec_var_specs |> map (fn ((v, T), x) => ((v, map_type_tvar thm_stvs_map T), x)) val sbtspec_const_specs = sbtspec_const_specs |> map (fn ((c, T), x) => ((c, map_type_tvar thm_stvs_map T), x)) val thm_stvs = thm' |> Thm.full_prop_of |> (fn t => Term.add_tvars t []) val thm_stvs_map = map_type_tvar (fn (v, _) => TVar (v, (AList.lookup op= thm_stvs #> the) v)) val sbtspec_const_specs = sbtspec_const_specs |> map (fn ((c, T), x) => ((c, thm_stvs_map T), x)) in ((writer, rispec', sbtspec_var_specs, sbtspec_const_specs), thm') end; (*** Unfold ud_with ***) fun etts_algorithm_unfold_ud_with ctxt'' etts_output_type writer sbtspec_var_specs sbtspec_const_specs thm = let val writer' = verbose_writer_prem etts_output_type writer "unfold ud_with..." val ud_with_thms = ctxt'' |> UDWithData.get |> map (Local_Defs.meta_rewrite_rule ctxt'') val thm' = Local_Defs.unfold ctxt'' ud_with_thms thm val stvs = thm' |> Thm.full_prop_of |> (fn t => Term.add_vars t []) val consts = thm' |> Thm.full_prop_of |> (fn t => Term.add_consts t []) val sbtspec_var_specs = sbtspec_var_specs |> filter (fn ((v, T), _) => member op= stvs (v, T)) val sbtspec_const_specs = sbtspec_const_specs |> filter (fn (const, _) => member op= consts const) val sbtspec_specs = ( (map (apfst Var) sbtspec_var_specs) @ (map (apfst Const) sbtspec_const_specs) ) val _ = verbose_writer_concl_thms etts_output_type ctxt'' (single thm') in ((writer', sbtspec_specs), thm') end; (*** Unoverload types ***) fun etts_algorithm_unoverload_types ctxt' etts_output_type writer rispec sbtspec_specs thm = let val writer' = verbose_writer_prem etts_output_type writer "unoverload types..." val thm' = Unoverload_Type.unoverload_type (Context.Proof ctxt') (rispec |> map (#1 #> #1) |> rev) thm val t = Thm.full_prop_of thm val n = Logic.count_prems t val out_t = Thm.full_prop_of thm' val out_n = Logic.count_prems out_t val out_prem_ts = out_t |> Logic.strip_imp_prems |> drop (out_n - n) val out_t' = Logic.list_implies (out_prem_ts, Logic.strip_imp_concl out_t) - + + (*FIXME: scalable datastructures*) val (mapT, mapt) = (Thm.cterm_of ctxt' out_t', Thm.cprop_of thm) |> Thm.match + |>> TVars.map (K Thm.typ_of) + ||> Vars.map (K Thm.term_of) + |>> TVars.dest + ||> Vars.dest |>> map (apfst TVar) ||> map (apfst Var) - |>> map (apsnd Thm.typ_of) - ||> map (apsnd Thm.term_of) |>> map swap ||> map swap val rispec' = rispec |> map (apfst TVar) |> map (apfst (map_atyps (AList.lookup op= mapT #> the))) |> map (apfst dest_TVar) val sbtspec_specs' = sbtspec_specs |> map (apfst (map_aterms (AList.lookup op= mapt #> the))) |> map (apfst dest_Var) |> map (apfst (apsnd (map_atyps (AList.lookup op= mapT #> the)))) val _ = verbose_writer_concl_thms etts_output_type ctxt' (single thm') in ((writer', rispec', sbtspec_specs'), thm') end; (*** Substitution of type variables ***) fun etts_algorithm_subst_type ctxt' etts_output_type writer rispec thm = let val writer' = verbose_writer_prem etts_output_type writer "substitution of type variables..." - val thm' = - Drule.instantiate_normalize - ( - rispec - |> map (apsnd TFree) - |> map (apsnd (Thm.ctyp_of ctxt')), - [] - ) - thm + val thm' = Drule.instantiate_normalize + ( + rispec + |> map (apsnd TFree) + |> map (apsnd (Thm.ctyp_of ctxt')) + |> TVars.make, + Vars.empty + ) + thm val _ = verbose_writer_concl_thms etts_output_type ctxt' (single thm') in (writer', thm') end; (*** Substitution of variables ***) fun etts_algorithm_subst_var ctxt' etts_output_type writer sbtspec_specs thm = let val writer' = verbose_writer_prem etts_output_type writer "substitution of variables..." val thm' = sbtspec_specs |> (Var #> (ctxt' |> Thm.cterm_of) |> apfst |> map) |> map Thm.first_order_match |> fold Drule.instantiate_normalize |> curry op|> thm val _ = verbose_writer_concl_thms etts_output_type ctxt' (single thm') in (writer', thm') end; (*** Untransfer ***) fun etts_algorithm_untransfer ctxt' etts_output_type writer transfer_thms thm = let val writer' = verbose_writer_prem etts_output_type writer "untransfer..." val (thm', context) = Thm.apply_attribute (Transfer.untransferred_attribute transfer_thms) thm (Context.Proof ctxt') val _ = verbose_writer_concl_thms etts_output_type ctxt' (single thm') in (context, writer', thm') end; (*** Export ***) fun etts_algorithm_export context ctxt etts_output_type writer thm = let val writer' = verbose_writer_prem etts_output_type writer "export..." val thy' = Context.theory_of context val ctxt' = Context.proof_of context val ctxt'' = Proof_Context.transfer thy' ctxt val thm' = singleton (Proof_Context.export ctxt' ctxt'') thm val _ = verbose_writer_concl_thms etts_output_type ctxt'' (single thm') in ((writer', thm'), ctxt'') end; (*** Cancel type definition ***) fun etts_algorithm_ctd ctxt etts_output_type writer rispec thm = let val writer' = verbose_writer_prem etts_output_type writer "cancel type definition..." val thm' = (rispec |> length |> cancel_type_definition_repeat) thm val _ = verbose_writer_concl_thms etts_output_type ctxt (single thm') in ((writer', thm'), ctxt) end; in fun etts_kera ctxt ctxt' etts_output_type writer rispec sbtspec_var_specs sbtspec_const_specs transfer_thms thm = let val ((writer', rispec, sbtspec_var_specs, sbtspec_const_specs), thm') = etts_algorithm_fresh_stv ctxt' writer rispec sbtspec_var_specs sbtspec_const_specs thm val ((writer'', sbtspec_specs), thm'') = etts_algorithm_unfold_ud_with ctxt' etts_output_type writer' sbtspec_var_specs sbtspec_const_specs thm' val ((writer''', rispec, sbtspec_specs'), thm''') = etts_algorithm_unoverload_types ctxt' etts_output_type writer'' rispec sbtspec_specs thm'' val (writer'''', thm'''') = etts_algorithm_subst_type ctxt' etts_output_type writer''' rispec thm''' val (writer''''', thm''''') = etts_algorithm_subst_var ctxt' etts_output_type writer'''' sbtspec_specs' thm'''' val (context, writer'''''', thm'''''') = etts_algorithm_untransfer ctxt' etts_output_type writer''''' transfer_thms thm''''' val ((writer''''''', thm'''''''), ctxt'') = etts_algorithm_export context ctxt etts_output_type writer'''''' thm'''''' val ((writer'''''''', thm''''''''), ctxt''') = etts_algorithm_ctd ctxt'' etts_output_type writer''''''' rispec thm''''''' in ((thm'''''''', writer''''''''), ctxt''') end; end; (**** Post-processing ****) local (*** Post-processing 1: simplification ***) fun etts_algorithm_simplification ctxt etts_output_type writer sbrr_opt thm = let val writer = verbose_writer_prem etts_output_type writer "simplification..." val out_thm = More_Simplifier.rewrite_simp_opt' ctxt sbrr_opt thm val _ = verbose_writer_concl_thms etts_output_type ctxt (single out_thm) in (writer, out_thm) end; (*** Post-processing 2: substitution of known premises ***) local (*ad-hoc application specific term equivalence*) fun term_equiv_st (t, u) = let fun term_equiv_st ((Const (a, T)), (Const (b, U))) = a = b andalso Type.could_match (T, U) | term_equiv_st ((Free (_, T)), (Free (_, U))) = Type.could_match (T, U) | term_equiv_st ((Var (_, T)), (Var (_, U))) = Type.could_match (T, U) | term_equiv_st ((Free (_, T)), (Var (_, U))) = Type.could_match (T, U) | term_equiv_st ((Var (_, T)), (Free (_, U))) = Type.could_match (T, U) | term_equiv_st ((Const (_, T)), (Free (_, U))) = Type.could_match (T, U) | term_equiv_st ((Free (_, T)), (Const (_, U))) = Type.could_match (T, U) | term_equiv_st ((Const (_, T)), (Var (_, U))) = Type.could_match (T, U) | term_equiv_st ((Var (_, T)), (Const (_, U))) = Type.could_match (T, U) | term_equiv_st ((Bound n), (Bound m)) = (n = m) | term_equiv_st ((Abs (_, T, t)), (Abs (_, U, u))) = Type.could_match (T, U) andalso term_equiv_st (t, u) | term_equiv_st ((tl $ tr), (ul $ ur)) = term_equiv_st (tl, ul) andalso term_equiv_st (tr, ur) | term_equiv_st ((Var (_, T)), (ul $ ur)) = Type.could_match (T, type_of (ul $ ur)) | term_equiv_st ((Var (_, T)), (Abs (c, U, u))) = Type.could_match (T, type_of (Abs (c, U, u))) | term_equiv_st (_, _) = false; in if (Term.add_frees t [] |> null |> not) andalso (Term.add_frees u [] |> null |> not) then term_equiv_st (t, u) else false end; in fun etts_algorithm_subst_prems ctxt etts_output_type writer subst_thms thm = let val writer' = verbose_writer_prem etts_output_type writer "substitute known premises..." val thm' = let val subst_thms = Attrib.eval_thms ctxt subst_thms val subst_thmst = map Thm.full_prop_of subst_thms fun option_thm thm_opt = case thm_opt of SOME thm => thm | _ => @{thm _} fun mk_OFthms ts = ts |> ( (subst_thmst ~~ subst_thms) |> AList.lookup term_equiv_st |> map ) |> map option_thm fun subst_premises_repeat thm = let val premsts = thm |> Thm.full_prop_of |> Logic.strip_imp_prems val out_thm = thm OF (mk_OFthms premsts) in if Thm.nprems_of thm = Thm.nprems_of out_thm then out_thm else subst_premises_repeat out_thm end in subst_premises_repeat thm end val _ = verbose_writer_concl_thms etts_output_type ctxt (single thm') in (writer', thm') end; end; (*** Post-processing 3: elimination of premises ***) fun etts_algorithm_premred ctxt etts_output_type writer mpespc_opt thm = let val writer' = verbose_writer_prem etts_output_type writer "elimination of premises..." val thm' = case mpespc_opt of SOME m_spec => let val (out_thm, ctxt') = Thm.unvarify_local_thm ctxt thm val out_thm = out_thm |> ETTS_Tactics.prem_red ctxt' m_spec |> singleton (Proof_Context.export ctxt' ctxt) in out_thm end | NONE => thm val _ = verbose_writer_concl_thms etts_output_type ctxt (single thm') in (writer', thm') end; (*** Post-processing 4: application of the attributes ***) fun etts_algorithm_app_attrb ctxt etts_output_type writer attrbs thm = let val writer' = verbose_writer_prem etts_output_type writer "application of the attributes for the set-based theorem..." val (thm', ctxt') = let val attrbs = map (Attrib.check_src ctxt #> Attrib.attribute ctxt) attrbs in Thm.proof_attributes attrbs thm ctxt end val _ = verbose_writer_concl_thms etts_output_type ctxt' (single thm') in (writer', thm') end; in fun etts_algorithm_pp ctxt etts_output_type writer sbrr_opt subst_thms mpespc_opt attrbs thm = let val (writer', thm') = etts_algorithm_simplification ctxt etts_output_type writer sbrr_opt thm val (writer'', thm'') = etts_algorithm_subst_prems ctxt etts_output_type writer' subst_thms thm' val (writer''', thm''') = etts_algorithm_premred ctxt etts_output_type writer'' mpespc_opt thm'' val (writer'''', thm'''') = etts_algorithm_app_attrb ctxt etts_output_type writer''' attrbs thm''' in ((thm'''', writer''''), ctxt) end; end; (**** Extended relativization algorithm ****) local fun mk_msg_etts_algorithm msg = "tts_algorithm: " ^ msg; fun etts_algorithm_input rispec thm = let val msg_etts_context = mk_msg_etts_algorithm "ERA can only be invoked from an appropriately parameterized tts context" val msg_ftvs = mk_msg_etts_algorithm "fixed type variables must not occur in the type-based theorems" val msg_fvs = mk_msg_etts_algorithm "fixed variables must not occur in the type-based theorems" val msg_not_risstv_subset = mk_msg_etts_algorithm "risstv must be a subset of the schematic type " ^ "variables that occur in the type-based theorems" val _ = not (null rispec) orelse error msg_etts_context val t = Thm.full_prop_of thm val _ = t |> (fn t => Term.add_tfrees t []) |> null orelse error msg_ftvs val _ = t |> (fn t => Term.add_frees t []) |> null orelse error msg_fvs val stvs = t |> (fn t => Term.add_tvars t []) |> map #1 |> distinct op= val risstv = map #1 rispec val _ = subset op= (risstv, stvs) orelse error msg_not_risstv_subset in () end; in fun etts_algorithm ctxt etts_output_type writer rispec sbtspec sbrr_opt subst_thms mpespc_opt attrbs thm = let (*0. User input validation*) val _ = etts_algorithm_input rispec thm (*1. Initialization of the relativization context*) val ( ctxt, ctxt', writer, rispec, sbtspec_var_specs, sbtspec_const_specs, transfer_thms ) = init_rlt_ctxt ctxt etts_output_type writer rispec sbtspec (*2. Initialization of the relativization context*) val writer' = ETTS_Writer.increment_index 2 writer val ((thm', writer'), ctxt'') = etts_kera ctxt ctxt' etts_output_type writer' rispec sbtspec_var_specs sbtspec_const_specs transfer_thms thm (*3. Initialization of the relativization context*) val writer'' = ETTS_Writer.increment_index 2 writer' val ((thm'', writer'''), ctxt''') = etts_algorithm_pp ctxt'' etts_output_type writer'' sbrr_opt subst_thms mpespc_opt attrbs thm' in ((thm'', writer'''), ctxt''') end; end; fun etts_fact ctxt etts_output_type writer rispec sbtspec sbrr_opt subst_thms mpespc_opt attrbs thms = let fun folder thm ((thms, writer), ctxt) = etts_algorithm ctxt etts_output_type writer rispec sbtspec sbrr_opt subst_thms mpespc_opt attrbs thm |>> apsnd (ETTS_Writer.increment_index 1) |>> apfst (curry (swap #> op::) thms) in fold_rev folder thms (([], writer), ctxt) end; end; \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML --- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML +++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML @@ -1,392 +1,393 @@ (* Title: ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) signature ETTS_TEST_TTS_ALGORITHM = sig type tts_algorithm_in_type val execute_test_suite_tts_algorithm : Proof.context -> (tts_algorithm_in_type, (thm * int list) * Proof.context) UT_Test_Suite.test_results_suite end; structure etts_test_tts_algorithm : ETTS_TEST_TTS_ALGORITHM = struct (**** Auxiliary ****) fun mk_msg_tts_algorithm_error msg = "tts_algorithm: " ^ msg (*** Data ***) type tts_algorithm_in_type = Proof.context * ETTS_Algorithm.etts_output_type * int list * (indexname * term) list * (term * term) list * (Facts.ref * Token.src list) option * (Facts.ref * Token.src list) list * (term list * (Proof.context -> tactic)) option * Token.src list * thm; (*** String I/O ***) fun string_of_writer writer = writer |> ML_Syntax.print_list Int.toString |> curry op^ "writer: " (*** Relation for the outputs ***) fun rel_tts_algorithm_out ( act_out : (thm * int list) * Proof.context, exp_out : (thm * int list) * Proof.context ) = let val ((thm_act_out, writer_act_out), _) = act_out val ((thm_exp_out, writer_exp_out), _) = exp_out val t_act_out = Thm.full_prop_of thm_act_out val t_exp_out = Thm.full_prop_of thm_exp_out in t_act_out aconv t_exp_out andalso writer_act_out = writer_exp_out end; (**** Tests ****) (*** Valid inputs ***) fun test_eq_tts_algorithm (ctxt : Proof.context) = let (*input*) val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt val rispec = #rispec tts_ctxt_data val sbtspec = #sbtspec tts_ctxt_data val sbrr_opt = #sbrr_opt tts_ctxt_data val subst_thms = #subst_thms tts_ctxt_data val mpespc_opt = #mpespc_opt tts_ctxt_data val attrbs = #attrbs tts_ctxt_data val tts_output_type = ETTS_Algorithm.default val writer_in = [1, 1, 1, 1] val in_thm = @{thm tta_semigroup_hom.tta_left_ideal_closed} val tts_algorithm_in : tts_algorithm_in_type = ( ctxt, tts_output_type, writer_in, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, in_thm ) (*output*) val writer_out = [1, 3, 1, 1] val exp_tts_algorithm_out = ((@{thm tta_left_ideal_ow_closed}, writer_out), ctxt) in UT_Test_Suite.assert_brel "equality" rel_tts_algorithm_out exp_tts_algorithm_out tts_algorithm_in end; (*** Exceptions ***) fun test_exc_ftvs ctxt = let val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt val rispec = #rispec tts_ctxt_data val sbtspec = #sbtspec tts_ctxt_data val sbrr_opt = #sbrr_opt tts_ctxt_data val subst_thms = #subst_thms tts_ctxt_data val mpespc_opt = #mpespc_opt tts_ctxt_data val attrbs = #attrbs tts_ctxt_data val tts_output_type = ETTS_Algorithm.default val writer_in = [1, 1, 1, 1] val in_thm = @{thm exI'[where 'a='a]} val tts_algorithm_in : tts_algorithm_in_type = ( ctxt, tts_output_type, writer_in, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, in_thm ) val err_msg = mk_msg_tts_algorithm_error "fixed type variables must not occur in the type-based theorems" in UT_Test_Suite.assert_exception "fixed type variables" tts_algorithm_in (ERROR err_msg) end; fun test_exc_fvs ctxt = let val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt val rispec = #rispec tts_ctxt_data val sbtspec = #sbtspec tts_ctxt_data val sbrr_opt = #sbrr_opt tts_ctxt_data val subst_thms = #subst_thms tts_ctxt_data val mpespc_opt = #mpespc_opt tts_ctxt_data val attrbs = #attrbs tts_ctxt_data val tts_output_type = ETTS_Algorithm.default val writer_in = [1, 1, 1, 1] val aT = TVar (("'a", 0), \<^sort>\type\) val xv = ("x", 0) val xt = Free ("x", aT) |> Thm.cterm_of ctxt - val in_thm = Drule.instantiate_normalize ([], [((xv, aT), xt)]) @{thm exI'} + val in_thm = Drule.instantiate_normalize + (TVars.empty, Vars.make [((xv, aT), xt)]) @{thm exI'} val tts_algorithm_in : tts_algorithm_in_type = ( ctxt, tts_output_type, writer_in, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, in_thm ) val err_msg = mk_msg_tts_algorithm_error "fixed variables must not occur in the type-based theorems" in UT_Test_Suite.assert_exception "fixed variables" tts_algorithm_in (ERROR err_msg) end; fun test_exc_not_risstv_subset ctxt = let val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt val rispec = #rispec tts_ctxt_data val sbtspec = #sbtspec tts_ctxt_data val sbrr_opt = #sbrr_opt tts_ctxt_data val subst_thms = #subst_thms tts_ctxt_data val mpespc_opt = #mpespc_opt tts_ctxt_data val attrbs = #attrbs tts_ctxt_data val tts_output_type = ETTS_Algorithm.default val writer_in = [1, 1, 1, 1] val in_thm = @{thm tta_semigroup.tta_assoc} val tts_algorithm_in : tts_algorithm_in_type = ( ctxt, tts_output_type, writer_in, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, in_thm ) val err_msg = mk_msg_tts_algorithm_error "risstv must be a subset of the schematic type " ^ "variables that occur in the type-based theorems" in UT_Test_Suite.assert_exception "risstv is not a subset of the stvs of the type-based theorems" tts_algorithm_in (ERROR err_msg) end; fun test_not_tts_context thy = let val ctxt = Proof_Context.init_global thy val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt val rispec = #rispec tts_ctxt_data val sbtspec = #sbtspec tts_ctxt_data val sbrr_opt = #sbrr_opt tts_ctxt_data val subst_thms = #subst_thms tts_ctxt_data val mpespc_opt = #mpespc_opt tts_ctxt_data val attrbs = #attrbs tts_ctxt_data val tts_output_type = ETTS_Algorithm.default val writer_in = [1, 1, 1, 1] val in_thm = @{thm tta_semigroup_hom.tta_left_ideal_closed} val tts_algorithm_in : tts_algorithm_in_type = ( ctxt, tts_output_type, writer_in, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, in_thm ) val err_msg = mk_msg_tts_algorithm_error "ERA can only be invoked from an appropriately parameterized tts context" in UT_Test_Suite.assert_exception "not tts context" tts_algorithm_in (ERROR err_msg) end; (**** Test suite ****) local fun string_of_rispec ctxt = ML_Syntax.print_pair (Term.string_of_vname) (Syntax.string_of_term ctxt) |> ML_Syntax.print_list; fun string_of_sbtspec ctxt = let val string_of_term = Syntax.string_of_term ctxt in ML_Syntax.print_pair string_of_term string_of_term |> ML_Syntax.print_list end; fun tts_algorithm_string_of_input (tts_algorithm_in : tts_algorithm_in_type) = let val ( ctxt, tts_output_type, writer, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, thm ) = tts_algorithm_in val ctxt_c = "ctxt: unknown context" val tts_output_type_c = ETTS_Algorithm.string_of_etts_output_type tts_output_type val writer_c = string_of_writer writer val rispec_c = rispec |> string_of_rispec ctxt |> curry op^ "rispec: " val sbtspec_c = sbtspec |> string_of_sbtspec ctxt |> curry op^ "sbtspec: " val sbrr_opt_c = sbrr_opt |> ETTS_Context.string_of_sbrr_opt |> curry op^ "sbrr_opt: " val subst_thms_c = subst_thms |> ETTS_Context.string_of_subst_thms |> curry op^ "subst_thms: " val mpespc_opt_c = mpespc_opt |> ETTS_Context.string_of_mpespc_opt ctxt |> curry op^ "mpespc_opt: " val attrbs_c = attrbs |> string_of_token_src_list |> curry op^ "attrbs: " val thm_c = thm |> Thm.string_of_thm ctxt |> curry op^ "in_thm: " val out_c = [ ctxt_c, tts_output_type_c, writer_c, rispec_c, sbtspec_c, sbrr_opt_c, subst_thms_c, mpespc_opt_c, attrbs_c, thm_c ] |> String.concatWith "\n" in out_c end; fun tts_algorithm_string_of_output (((thm, writer), ctxt) : (thm * int list) * Proof.context) = let val ctxt_c = "ctxt: unknown context" val thm_c = Thm.string_of_thm ctxt thm val writer_c = ML_Syntax.print_list Int.toString writer val out_c = [ctxt_c, thm_c, writer_c] |> String.concatWith "\n" in out_c end; fun tts_algorithm (tts_algorithm_in : tts_algorithm_in_type) = let val ( ctxt, tts_output_type, writer, rispec, sbtspec, sbrr_opt, subst_thms, mpespc_opt, attrbs, thm ) = tts_algorithm_in val tts_algorithm_out = ETTS_Algorithm.etts_algorithm ctxt tts_output_type writer rispec sbtspec sbrr_opt subst_thms mpespc_opt attrbs thm in tts_algorithm_out end; in fun mk_test_suite_tts_algorithm ctxt = let val test_suite_tts_algorithm = UT_Test_Suite.init "tts_algorithm" tts_algorithm tts_algorithm_string_of_input tts_algorithm_string_of_output in test_suite_tts_algorithm |> test_eq_tts_algorithm ctxt |> test_exc_ftvs ctxt |> test_exc_fvs ctxt |> test_exc_not_risstv_subset ctxt |> test_not_tts_context (Proof_Context.theory_of ctxt) end; end; fun execute_test_suite_tts_algorithm ctxt = UT_Test_Suite.execute (mk_test_suite_tts_algorithm ctxt); end; \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/Examples/Introduction.thy b/thys/Types_To_Sets_Extension/Examples/Introduction.thy --- a/thys/Types_To_Sets_Extension/Examples/Introduction.thy +++ b/thys/Types_To_Sets_Extension/Examples/Introduction.thy @@ -1,185 +1,185 @@ (* Title: Examples/Introduction.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) chapter\ETTS Case Studies: Introduction\ theory Introduction - imports Types_To_Sets_Extension.ETTS_Auxiliary + imports "../ETTS/ETTS_Auxiliary" begin section\Background\ subsection\Purpose\ text\ The remainder of this document presents several examples of the application of the extension of the framework Types-To-Sets and provides the potential users of the extension with a plethora of design patterns to choose from for their own applied relativization needs. \ subsection\Related work\ text\ Since the publication of the framework Types-To-Sets in \cite{blanchette_types_2016}, there has been a growing interest in its use in applied formalization. Some of the examples of the application of the framework include \cite{divason_perron-frobenius_2016}, \cite{maletzky_hilberts_2019} and \cite{immler_smooth_2019}. However, this list is not exhaustive. Arguably, the most significant application example was developed in \cite{immler_smooth_2019}, where Fabian Immler and Bohua Zhan performed the relativization of over 200 theorems from the standard mathematics library of Isabelle/HOL. Nonetheless, it is likely that the work presented in this document is the first significant application of the ETTS: unsurprisingly, the content of this document was developed in parallel with the extension of the framework itself. Also, perhaps, it is the largest application of the framework Types-To-Sets at the time of writing: only one of the three libraries (SML Relativization) presented in the context of this work contains the relativization of over 800 theorems from the standard library of Isabelle/HOL. \ section\Examples: overview\ subsection\Background\ text\ The examples that are presented in this document were developed for the demonstration of the impact of various aspects of the relativization process on the outcome of the relativization. Three libraries of relativized results were developed in the context of this work: \begin{itemize} \item \textit{SML Relativization}: a relativization of elements of the standard mathematics library of Isabelle/HOL \item \textit{TTS Vector Spaces}: a renovation of the set-based library that was developed in \cite{immler_smooth_2019} using the ETTS instead of the existing interface for Types-To-Sets \item \textit{TTS Foundations}: a relativization of a miniature type-based library with every constant being parametric under the side conditions compatible with Types-To-Sets \end{itemize} \ subsection\SML Relativization\ text\ The standard library that is associated with the object logic Isabelle/HOL and provided as a part of the standard distribution of Isabelle \cite{noauthor_isabellehol_2020} contains a significant number of formalized results from a variety of fields of mathematics. However, the formalization is performed using a type-based approach: for example, the carrier sets associated with the algebraic structures and the underlying sets of the topological spaces consist of all terms of an arbitrary type. The ETTS was applied to the relativization of a certain number of results from the standard library. The results that are formalized in the library SML Relativization are taken from an array of topics that include order theory, group theory, ring theory and topology. However, only the results whose relativization could be nearly fully automated using the frameworks UD, CTR and ETTS with almost no additional proof effort are included. \ subsection\TTS Vector Spaces\ text\ The TTS Vector Spaces is a remake of the library of relativized results that was developed in \cite{immler_smooth_2019} using the ETTS. The theorems that are provided in the library TTS Vector Spaces are nearly identical to the results that are provided in \cite{immler_smooth_2019}. A detailed description of the original library has already been given in \cite{immler_smooth_2019} and will not be restated. The definitional frameworks that are used in \cite{immler_smooth_2019} and the TTS Vector Spaces are similar. While the unoverloading of most of the constants could be performed by using the command @{command ud}, the command @{command ctr} could not be used to establish that the unoverloaded constants are parametric under a suitable set of side conditions. Therefore, like in \cite{immler_smooth_2019}, the proofs of the transfer rules were performed manually. However, the advantages of using the ETTS become apparent during the relativization of theorems: the complex infrastructure that was needed for compiling out dependencies on overloaded constants, the manual invocation of the attributes related to the individual steps of the relativization algorithm, the repeated explicit references to the theorem as it undergoes the transformations associated with the individual steps of the relativization algorithm, the explicitly stated names of the set-based theorems were no longer needed. Furthermore, the theorems synthesized by the ETTS in TTS Vector Spaces appear in the formal proof documents in a format that is similar to the canonical format of the Isabelle/Isar declarations associated with the standard commands such as @{command lemma}. \ subsection\TTS Foundations\ text\ The most challenging aspect of the relativization process, perhaps, is related to the availability of the transfer rules for the constants in the type-based theorems. Nonetheless, even if the transfer rules are available, having to use the relativized constants in the set-based theorems that are different from the original constants that are used in the type-based theorems can be seen as unnatural and inconvenient. Unfortunately, the library SML Relativization suffers from both of the aforementioned problems. The library that was developed in \cite{immler_smooth_2019} (hence, also the library TTS Vector Spaces) suffers, primarily, from the former problem, but, arguably, due to the methodology that was chosen for the relativization, the library has a more restricted scope of applicability. The library TTS Foundations provides an example of a miniature type-based library such that all constants associated with the operations on mathematical structures (effectively, this excludes the constants associated with the locale predicates) in the library are parametric under the side conditions compatible with Types-To-Sets. The relativization is performed with respect to all possible type variables; in this case, the type classes are not used in the type-based library. Currently, the library includes the results from the areas of order theory and semigroups. However, it is hoped that it can be seen that the library can be extended to include most of the content that is available in the main library of Isabelle/HOL. The library TTS Foundations demonstrates that the development of a set-based library can be nearly fully automated using the existing infrastructure associated with the UD, CTR and ETTS, and requires almost no explicit proofs on behalf of the users of these frameworks. \ end \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy --- a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy +++ b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy @@ -1,1240 +1,1240 @@ (* Title: Examples/SML_Relativization/Lattices/SML_Complete_Lattices.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section\Relativization of the results about complete lattices\ theory SML_Complete_Lattices imports SML_Lattices begin subsection\Simple complete lattices\ subsubsection\Definitions and common properties\ locale Inf_ow = fixes U :: "'al set" and Inf (\\\<^sub>o\<^sub>w\) assumes Inf_closed[simp]: "\\<^sub>o\<^sub>w ` Pow U \ U" begin notation Inf (\\\<^sub>o\<^sub>w\) lemma Inf_closed'[simp]: "\x\U. \\<^sub>o\<^sub>w x \ U" using Inf_closed by blast end locale Inf_pair_ow = Inf\<^sub>1: Inf_ow U\<^sub>1 Inf\<^sub>1 + Inf\<^sub>2: Inf_ow U\<^sub>2 Inf\<^sub>2 for U\<^sub>1 :: "'al set" and Inf\<^sub>1 and U\<^sub>2 :: "'bl set" and Inf\<^sub>2 begin notation Inf\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation Inf\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale Sup_ow = fixes U :: "'al set" and Sup (\\\<^sub>o\<^sub>w\) assumes Sup_closed[simp]: "\\<^sub>o\<^sub>w ` Pow U \ U" begin notation Sup (\\\<^sub>o\<^sub>w\) lemma Sup_closed'[simp]: "\x\U. \\<^sub>o\<^sub>w x \ U" using Sup_closed by blast end locale Sup_pair_ow = Sup\<^sub>1: Sup_ow U\<^sub>1 Sup\<^sub>1 + Sup\<^sub>2: Sup_ow U\<^sub>2 Sup\<^sub>2 for U\<^sub>1 :: "'al set" and Sup\<^sub>1 and U\<^sub>2 :: "'bl set" and Sup\<^sub>2 begin notation Sup\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation Sup\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale complete_lattice_ow = lattice_ow U inf le ls sup + Inf_ow U Inf + Sup_ow U Sup + bot_ow U bot + top_ow U top for U :: "'al set" and Inf Sup inf le ls sup bot top + assumes Inf_lower: "\ A \ U; x \ A \ \ \\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w x" and Inf_greatest: "\ A \ U; z \ U; (\x. x \ A \ z \\<^sub>o\<^sub>w x) \ \ z \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" and Sup_upper: "\ x \ A; A \ U \ \ x \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" and Sup_least: "\ A \ U; z \ U; (\x. x \ A \ x \\<^sub>o\<^sub>w z) \ \ \\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w z" and Inf_empty[simp]: "\\<^sub>o\<^sub>w {} = \\<^sub>o\<^sub>w" and Sup_empty[simp]: "\\<^sub>o\<^sub>w {} = \\<^sub>o\<^sub>w" begin sublocale bounded_lattice_ow U \(\\<^sub>o\<^sub>w)\ \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ \(\\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ \\\<^sub>o\<^sub>w\ apply standard subgoal using Sup_least by force subgoal using Inf_greatest by fastforce done tts_register_sbts \\\<^sub>o\<^sub>w\ | U proof- assume ALA: "Domainp ALA = (\x. x \ U)" have "Domainp ALA \\<^sub>o\<^sub>w" unfolding ALA by simp then obtain bot' where "ALA \\<^sub>o\<^sub>w bot'" by blast then show "\bot'. ALA \\<^sub>o\<^sub>w bot'" by auto qed tts_register_sbts \\\<^sub>o\<^sub>w\ | U proof- assume ALA: "Domainp ALA = (\x. x \ U)" have "Domainp ALA \\<^sub>o\<^sub>w" unfolding ALA by simp then obtain top' where "ALA \\<^sub>o\<^sub>w top'" by blast then show "\top'. ALA \\<^sub>o\<^sub>w top'" by auto qed end locale complete_lattice_pair_ow = cl\<^sub>1: complete_lattice_ow U\<^sub>1 Inf\<^sub>1 Sup\<^sub>1 inf\<^sub>1 le\<^sub>1 ls\<^sub>1 sup\<^sub>1 bot\<^sub>1 top\<^sub>1 + cl\<^sub>2: complete_lattice_ow U\<^sub>2 Inf\<^sub>2 Sup\<^sub>2 inf\<^sub>2 le\<^sub>2 ls\<^sub>2 sup\<^sub>2 bot\<^sub>2 top\<^sub>2 for U\<^sub>1 :: "'al set" and Inf\<^sub>1 Sup\<^sub>1 inf\<^sub>1 le\<^sub>1 ls\<^sub>1 sup\<^sub>1 bot\<^sub>1 top\<^sub>1 and U\<^sub>2 :: "'bl set" and Inf\<^sub>2 Sup\<^sub>2 inf\<^sub>2 le\<^sub>2 ls\<^sub>2 sup\<^sub>2 bot\<^sub>2 top\<^sub>2 begin sublocale bounded_lattice_pair_ow .. sublocale Inf_pair_ow .. sublocale Sup_pair_ow .. end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma complete_lattice_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (rel_set A ===> A) ===> (rel_set A ===> A) ===> (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (A ===> A ===> A) ===> A ===> A ===> (=) ) (complete_lattice_ow (Collect (Domainp A))) class.complete_lattice" proof- let ?P = "( (rel_set A ===> A) ===> (rel_set A ===> A) ===> (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (A ===> A ===> A) ===> A ===> A ===> (=) )" let ?complete_lattice_ow = "(complete_lattice_ow (Collect (Domainp A)))" let ?Inf_Sup_UNIV = "(\F'::'b set \ 'b. (F' ` Pow UNIV \ UNIV))" have rrng: "((A2 \ A3 \ A4 \ A5 \ A1 \ A6 \ A7 \ A8 \ A9 \ A10 \ A11) = F') \ ((A1 \ A2 \ A3 \ A4 \ A5 \ A6 \ A7 \ A8 \ A9 \ A10 \ A11) = F')" for A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 F' by auto have "?P ?complete_lattice_ow ( \Inf Sup inf le ls sup bot top. ?Inf_Sup_UNIV Inf \ ?Inf_Sup_UNIV Sup \ bot \ UNIV \ top \ UNIV \ class.complete_lattice Inf Sup inf le ls sup bot top )" unfolding complete_lattice_ow_def class.complete_lattice_def complete_lattice_ow_axioms_def class.complete_lattice_axioms_def Inf_ow_def Sup_ow_def bot_ow_def top_ow_def apply transfer_prover_start apply transfer_step+ apply(simp, intro ext, rule rrng, intro arg_cong2[where f="(\)"]) subgoal unfolding Ball_Collect by simp subgoal unfolding Ball_Collect by simp subgoal by simp subgoal by simp subgoal by simp subgoal unfolding Ball_Collect[symmetric] by auto subgoal unfolding Ball_Collect[symmetric] by metis subgoal unfolding Ball_Collect[symmetric] by auto subgoal unfolding Ball_Collect[symmetric] by metis subgoal by simp subgoal by simp done then show ?thesis by simp qed end subsubsection\Relativization\ context complete_lattice_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating \?a \ ?A\ and \?A \ ?B\ through auto applying [OF Inf_closed' Sup_closed' inf_closed' sup_closed'] begin tts_lemma Inf_atLeast: assumes "x \ U" shows "\\<^sub>o\<^sub>w {x..\<^sub>o\<^sub>w} = x" is complete_lattice_class.Inf_atLeast. tts_lemma Inf_atMost: assumes "x \ U" shows "\\<^sub>o\<^sub>w {..\<^sub>o\<^sub>wx} = \\<^sub>o\<^sub>w" is complete_lattice_class.Inf_atMost. tts_lemma Sup_atLeast: assumes "x \ U" shows "\\<^sub>o\<^sub>w {x..\<^sub>o\<^sub>w} = \\<^sub>o\<^sub>w" is complete_lattice_class.Sup_atLeast. tts_lemma Sup_atMost: assumes "y \ U" shows "\\<^sub>o\<^sub>w {..\<^sub>o\<^sub>wy} = y" is complete_lattice_class.Sup_atMost. tts_lemma Inf_insert: assumes "a \ U" and "A \ U" shows "\\<^sub>o\<^sub>w (insert a A) = a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" is complete_lattice_class.Inf_insert. tts_lemma Sup_insert: assumes "a \ U" and "A \ U" shows "\\<^sub>o\<^sub>w (insert a A) = a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" is complete_lattice_class.Sup_insert. tts_lemma Inf_atMostLessThan: assumes "x \ U" and "\\<^sub>o\<^sub>w <\<^sub>o\<^sub>w x" shows "\\<^sub>o\<^sub>w {..<\<^sub>o\<^sub>wx} = \\<^sub>o\<^sub>w" is complete_lattice_class.Inf_atMostLessThan. tts_lemma Sup_greaterThanAtLeast: assumes "x \ U" and "x <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" shows "\\<^sub>o\<^sub>w {x<\<^sub>o\<^sub>w..} = \\<^sub>o\<^sub>w" is complete_lattice_class.Sup_greaterThanAtLeast. tts_lemma le_Inf_iff: assumes "b \ U" and "A \ U" shows "(b \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A) = Ball A ((\\<^sub>o\<^sub>w) b)" is complete_lattice_class.le_Inf_iff. tts_lemma Sup_le_iff: assumes "A \ U" and "b \ U" shows "(\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w b) = (\x\A. x \\<^sub>o\<^sub>w b)" is complete_lattice_class.Sup_le_iff. tts_lemma Inf_atLeastLessThan: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {x.. U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w {x<\<^sub>o\<^sub>w..y} = y" is complete_lattice_class.Sup_greaterThanAtMost. tts_lemma Inf_atLeastAtMost: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w {x..\<^sub>o\<^sub>wy} = x" is complete_lattice_class.Inf_atLeastAtMost. tts_lemma Sup_atLeastAtMost: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w {x..\<^sub>o\<^sub>wy} = y" is complete_lattice_class.Sup_atLeastAtMost. tts_lemma Inf_lower2: assumes "A \ U" and "v \ U" and "u \ A" and "u \\<^sub>o\<^sub>w v" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w v" is complete_lattice_class.Inf_lower2. tts_lemma Sup_upper2: assumes "A \ U" and "v \ U" and "u \ A" and "v \\<^sub>o\<^sub>w u" shows "v \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" is complete_lattice_class.Sup_upper2. tts_lemma Inf_less_eq: assumes "A \ U" and "u \ U" and "\v. v \ A \ v \\<^sub>o\<^sub>w u" and "A \ {}" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w u" given complete_lattice_class.Inf_less_eq by auto tts_lemma less_eq_Sup: assumes "A \ U" and "u \ U" and "\v. v \ A \ u \\<^sub>o\<^sub>w v" and "A \ {}" shows "u \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" given complete_lattice_class.less_eq_Sup by auto tts_lemma Sup_eqI: assumes "A \ U" and "x \ U" and "\y. y \ A \ y \\<^sub>o\<^sub>w x" and "\y. \y \ U; \z. z \ A \ z \\<^sub>o\<^sub>w y\ \ x \\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w A = x" given complete_lattice_class.Sup_eqI by (simp add: Sup_least Sup_upper order.antisym) tts_lemma Inf_eqI: assumes "A \ U" and "x \ U" and "\i. i \ A \ x \\<^sub>o\<^sub>w i" and "\y. \y \ U; \i. i \ A \ y \\<^sub>o\<^sub>w i\ \ y \\<^sub>o\<^sub>w x" shows "\\<^sub>o\<^sub>w A = x" given complete_lattice_class.Inf_eqI by (simp add: subset_eq) tts_lemma Inf_union_distrib: assumes "A \ U" and "B \ U" shows "\\<^sub>o\<^sub>w (A \ B) = \\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" is complete_lattice_class.Inf_union_distrib. tts_lemma Sup_union_distrib: assumes "A \ U" and "B \ U" shows "\\<^sub>o\<^sub>w (A \ B) = \\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" is complete_lattice_class.Sup_union_distrib. tts_lemma Sup_inter_less_eq: assumes "A \ U" and "B \ U" shows "\\<^sub>o\<^sub>w (A \ B) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" is complete_lattice_class.Sup_inter_less_eq. tts_lemma less_eq_Inf_inter: assumes "A \ U" and "B \ U" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (A \ B)" is complete_lattice_class.less_eq_Inf_inter. tts_lemma Sup_subset_mono: assumes "B \ U" and "A \ B" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" is complete_lattice_class.Sup_subset_mono. tts_lemma Inf_superset_mono: assumes "A \ U" and "B \ A" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" is complete_lattice_class.Inf_superset_mono. tts_lemma Sup_bot_conv: assumes "A \ U" shows "(\\<^sub>o\<^sub>w A = \\<^sub>o\<^sub>w) = (\x\A. x = \\<^sub>o\<^sub>w)" "(\\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w A) = (\x\A. x = \\<^sub>o\<^sub>w)" is complete_lattice_class.Sup_bot_conv. tts_lemma Inf_top_conv: assumes "A \ U" shows "(\\<^sub>o\<^sub>w A = \\<^sub>o\<^sub>w) = (\x\A. x = \\<^sub>o\<^sub>w)" "(\\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w A) = (\x\A. x = \\<^sub>o\<^sub>w)" is complete_lattice_class.Inf_top_conv. tts_lemma Inf_le_Sup: assumes "A \ U" and "A \ {}" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w A" is complete_lattice_class.Inf_le_Sup. tts_lemma INF_UNIV_bool_expand: assumes "range A \ U" shows "\\<^sub>o\<^sub>w (range A) = A True \\<^sub>o\<^sub>w A False" is complete_lattice_class.INF_UNIV_bool_expand. tts_lemma SUP_UNIV_bool_expand: assumes "range A \ U" shows "\\<^sub>o\<^sub>w (range A) = A True \\<^sub>o\<^sub>w A False" is complete_lattice_class.SUP_UNIV_bool_expand. tts_lemma Sup_mono: assumes "A \ U" and "B \ U" and "\a. a \ A \ Bex B ((\\<^sub>o\<^sub>w) a)" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" given complete_lattice_class.Sup_mono by simp tts_lemma Inf_mono: assumes "B \ U" and "A \ U" and "\b. b \ B \ \x\A. x \\<^sub>o\<^sub>w b" shows "\\<^sub>o\<^sub>w A \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w B" given complete_lattice_class.Inf_mono by simp tts_lemma Sup_Inf_le: assumes "A \ Pow U" shows "\\<^sub>o\<^sub>w ( \\<^sub>o\<^sub>w ` {x. x \ U \ (\f\{f. f ` Pow U \ U}. x = f ` A \ (\Y\A. f Y \ Y))} ) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (\\<^sub>o\<^sub>w ` A)" is complete_lattice_class.Sup_Inf_le. end tts_context tts: (?'a to U) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty applying [ OF Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed ] begin tts_lemma Inf_UNIV: "\\<^sub>o\<^sub>w U = \\<^sub>o\<^sub>w" is complete_lattice_class.Inf_UNIV. tts_lemma Sup_UNIV: "\\<^sub>o\<^sub>w U = \\<^sub>o\<^sub>w" is complete_lattice_class.Sup_UNIV. end context fixes U\<^sub>2 :: "'b set" begin lemmas [transfer_rule] = image_transfer[where ?'a='b] tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through (insert Sup_least, auto) begin tts_lemma SUP_upper2: assumes "A \ U\<^sub>2" and "u \ U" and "\x\U\<^sub>2. f x \ U" and "i \ A" and "u \\<^sub>o\<^sub>w f i" shows "u \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" is complete_lattice_class.SUP_upper2. tts_lemma INF_lower2: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "u \ U" and "i \ A" and "f i \\<^sub>o\<^sub>w u" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w u" is complete_lattice_class.INF_lower2. tts_lemma less_INF_D: assumes "y \ U" and "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" and "y <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" and "i \ A" shows "y <\<^sub>o\<^sub>w f i" is complete_lattice_class.less_INF_D. tts_lemma SUP_lessD: assumes "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" and "y \ U" and "\\<^sub>o\<^sub>w (f ` A) <\<^sub>o\<^sub>w y" and "i \ A" shows "f i <\<^sub>o\<^sub>w y" is complete_lattice_class.SUP_lessD. tts_lemma SUP_le_iff: assumes "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" and "u \ U" shows "(\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w u) = (\x\A. f x \\<^sub>o\<^sub>w u)" is complete_lattice_class.SUP_le_iff. end end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through (auto dest: top_le) begin tts_lemma INF_eqI: assumes "A \ U\<^sub>2" and "x \ U" and "\x\U\<^sub>2. f x \ U" and "\i. \i \ U\<^sub>2; i \ A\ \ x \\<^sub>o\<^sub>w f i" and "\y. \y \ U; \i. \i \ U\<^sub>2; i \ A\ \ y \\<^sub>o\<^sub>w f i\ \ y \\<^sub>o\<^sub>w x" shows "\\<^sub>o\<^sub>w (f ` A) = x" is complete_lattice_class.INF_eqI. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty - eliminating through (auto simp: sup_bot.eq_iff) + eliminating through (auto simp: order.eq_iff) begin tts_lemma SUP_eqI: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "x \ U" and "\i. \i \ U\<^sub>2; i \ A\ \ f i \\<^sub>o\<^sub>w x" and "\y. \y \ U; \i. \i \ U\<^sub>2; i \ A\ \ f i \\<^sub>o\<^sub>w y\ \ x \\<^sub>o\<^sub>w y" shows "\\<^sub>o\<^sub>w (f ` A) = x" is complete_lattice_class.SUP_eqI. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through simp begin tts_lemma INF_le_SUP: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "A \ {}" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" is complete_lattice_class.INF_le_SUP. tts_lemma INF_inf_const1: assumes "I \ U\<^sub>2" and "x \ U" and "\x\U\<^sub>2. f x \ U" and "I \ {}" shows "\\<^sub>o\<^sub>w ((\i. x \\<^sub>o\<^sub>w f i) ` I) = x \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` I)" is complete_lattice_class.INF_inf_const1. tts_lemma INF_inf_const2: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "x \ U" and "I \ {}" shows "\\<^sub>o\<^sub>w ((\i. f i \\<^sub>o\<^sub>w x) ` I) = \\<^sub>o\<^sub>w (f ` I) \\<^sub>o\<^sub>w x" is complete_lattice_class.INF_inf_const2. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through auto begin tts_lemma INF_eq_const: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "I \ {}" and "\i. i \ I \ f i = x" shows "\\<^sub>o\<^sub>w (f ` I) = x" given complete_lattice_class.INF_eq_const proof- assume "\I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; I \ {}; \i. \i \ U\<^sub>2; i \ I\ \ f i = x\ \ \\<^sub>o\<^sub>w (f ` I) = x" for I :: "'a set" and U\<^sub>2 f x then have "\I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; I \ {}; \i. i \ I \ f i = x\ \ \\<^sub>o\<^sub>w (f ` I) = x" by presburger then show "\\<^sub>o\<^sub>w (f ` I) = x" using assms by simp qed tts_lemma SUP_eq_const: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "I \ {}" and "\i. i \ I \ f i = x" shows "\\<^sub>o\<^sub>w (f ` I) = x" given complete_lattice_class.SUP_eq_const proof- assume "\I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; I \ {}; \i. \i \ U\<^sub>2; i \ I\ \ f i = x\ \ \\<^sub>o\<^sub>w (f ` I) = x" for I :: "'a set" and U\<^sub>2 f x then have "\I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; I \ {}; \i. i \ I \ f i = x\ \ \\<^sub>o\<^sub>w (f ` I) = x" by presburger then show "\\<^sub>o\<^sub>w (f ` I) = x" using assms by simp qed tts_lemma SUP_eq_iff: assumes "I \ U\<^sub>2" and "c \ U" and "\x\U\<^sub>2. f x \ U" and "I \ {}" and "\i. i \ I \ c \\<^sub>o\<^sub>w f i" shows "(\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" given complete_lattice_class.SUP_eq_iff proof- assume "\ I \ U\<^sub>2; c \ U; \x\U\<^sub>2. f x \ U; I \ {}; \i. \i \ U\<^sub>2; i \ I\ \ c \\<^sub>o\<^sub>w f i \ \ (\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" for I :: "'a set" and U\<^sub>2 c f then have "\ I \ U\<^sub>2; c \ U; \x\U\<^sub>2. f x \ U; I \ {}; \i. i \ I \ c \\<^sub>o\<^sub>w f i \ \ (\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" by presburger then show "(\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" using assms by auto qed tts_lemma INF_eq_iff: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "c \ U" and "I \ {}" and "\i. i \ I \ f i \\<^sub>o\<^sub>w c" shows "(\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" given complete_lattice_class.INF_eq_iff proof- assume "\ I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; c \ U; I \ {}; \i. \i \ U\<^sub>2; i \ I\ \ f i \\<^sub>o\<^sub>w c \ \ (\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" for I :: "'a set" and U\<^sub>2 f c then have "\ I \ U\<^sub>2; \x\U\<^sub>2. f x \ U; c \ U; I \ {}; \i. i \ I \ f i \\<^sub>o\<^sub>w c \ \ (\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" by presburger then show "(\\<^sub>o\<^sub>w (f ` I) = c) = (\x\I. f x = c)" using assms by auto qed end context fixes U\<^sub>2 :: "'b set" begin lemmas [transfer_rule] = image_transfer[where ?'a='b] tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through (auto simp: sup_bot.top_unique top_le intro: Sup_least) begin tts_lemma INF_insert: assumes "\x\U\<^sub>2. f x \ U" and "a \ U\<^sub>2" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` insert a A) = f a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" is complete_lattice_class.INF_insert. tts_lemma SUP_insert: assumes "\x\U\<^sub>2. f x \ U" and "a \ U\<^sub>2" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` insert a A) = f a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" is complete_lattice_class.SUP_insert. tts_lemma le_INF_iff: assumes "u \ U" and "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" shows "(u \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)) = (\x\A. u \\<^sub>o\<^sub>w f x)" is complete_lattice_class.le_INF_iff. tts_lemma INF_union: assumes "\x\U\<^sub>2. M x \ U" and "A \ U\<^sub>2" and "B \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (M ` (A \ B)) = \\<^sub>o\<^sub>w (M ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (M ` B)" is complete_lattice_class.INF_union. tts_lemma SUP_union: assumes "\x\U\<^sub>2. M x \ U" and "A \ U\<^sub>2" and "B \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (M ` (A \ B)) = \\<^sub>o\<^sub>w (M ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (M ` B)" is complete_lattice_class.SUP_union. tts_lemma SUP_bot_conv: assumes "\x\U\<^sub>2. B x \ U" and "A \ U\<^sub>2" shows "(\\<^sub>o\<^sub>w (B ` A) = \\<^sub>o\<^sub>w) = (\x\A. B x = \\<^sub>o\<^sub>w)" "(\\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w (B ` A)) = (\x\A. B x = \\<^sub>o\<^sub>w)" is complete_lattice_class.SUP_bot_conv. tts_lemma INF_top_conv: assumes "\x\U\<^sub>2. B x \ U" and "A \ U\<^sub>2" shows "(\\<^sub>o\<^sub>w (B ` A) = \\<^sub>o\<^sub>w) = (\x\A. B x = \\<^sub>o\<^sub>w)" "(\\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w (B ` A)) = (\x\A. B x = \\<^sub>o\<^sub>w)" is complete_lattice_class.INF_top_conv. tts_lemma SUP_upper: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "i \ A" shows "f i \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (f ` A)" is complete_lattice_class.SUP_upper. tts_lemma INF_lower: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "i \ A" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w f i" is complete_lattice_class.INF_lower. tts_lemma INF_inf_distrib: assumes "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" and "\x\U\<^sub>2. g x \ U" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` A) = \\<^sub>o\<^sub>w ((\a. f a \\<^sub>o\<^sub>w g a) ` A)" is complete_lattice_class.INF_inf_distrib. tts_lemma SUP_sup_distrib: assumes "\x\U\<^sub>2. f x \ U" and "A \ U\<^sub>2" and "\x\U\<^sub>2. g x \ U" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` A) = \\<^sub>o\<^sub>w ((\a. f a \\<^sub>o\<^sub>w g a) ` A)" is complete_lattice_class.SUP_sup_distrib. tts_lemma SUP_subset_mono: assumes "B \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "\x\U\<^sub>2. g x \ U" and "A \ B" and "\x. x \ A \ f x \\<^sub>o\<^sub>w g x" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" given complete_lattice_class.SUP_subset_mono proof- assume "\ B \ U\<^sub>2; \x\U\<^sub>2. f x \ U; \x\U\<^sub>2. g x \ U; A \ B; \x. \x \ U\<^sub>2; x \ A\ \ f x \\<^sub>o\<^sub>w g x \ \ \\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" for B :: "'b set" and f g A then have "\ B \ U\<^sub>2; \x\U\<^sub>2. f x \ U; \x\U\<^sub>2. g x \ U; A \ B; \x. x \ A \ f x \\<^sub>o\<^sub>w g x \ \ \\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" by auto then show "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" using assms by blast qed tts_lemma INF_superset_mono: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "\x\U\<^sub>2. g x \ U" and "B \ A" and "\x. \x \ U\<^sub>2; x \ B\ \ f x \\<^sub>o\<^sub>w g x" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" given complete_lattice_class.INF_superset_mono proof- assume "\ A \ U\<^sub>2; \x\U\<^sub>2. f x \ U; \x\U\<^sub>2. g x \ U; B \ A; \x. \x \ U\<^sub>2; x \ B\ \ f x \\<^sub>o\<^sub>w g x \ \ \\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" for A :: "'b set" and f g B then have "\ A \ U\<^sub>2; \x\U\<^sub>2. f x \ U; \x\U\<^sub>2. g x \ U; B \ A; \x. x \ B \ f x \\<^sub>o\<^sub>w g x \ \ \\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" by auto then show "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" using assms by blast qed tts_lemma INF_absorb: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. A x \ U" and "k \ I" shows "A k \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (A ` I) = \\<^sub>o\<^sub>w (A ` I)" is complete_lattice_class.INF_absorb. tts_lemma SUP_absorb: assumes "I \ U\<^sub>2" and "\x\U\<^sub>2. A x \ U" and "k \ I" shows "A k \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (A ` I) = \\<^sub>o\<^sub>w (A ` I)" is complete_lattice_class.SUP_absorb. end end context fixes f :: "'b \ 'al" and U\<^sub>2 :: "'b set" assumes f[transfer_rule]: "\x \ U\<^sub>2. f x = \\<^sub>o\<^sub>w" begin tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) sbterms: (\Orderings.bot::?'a::complete_lattice\ to \\\<^sub>o\<^sub>w\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through simp begin tts_lemma SUP_bot: assumes "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w" is complete_lattice_class.SUP_bot[folded const_fun_def]. end end context fixes f :: "'b \ 'al" and U\<^sub>2 :: "'b set" assumes f[transfer_rule]: "\x \ U\<^sub>2. f x = \\<^sub>o\<^sub>w" begin tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) sbterms: (\Orderings.top::?'a::complete_lattice\ to \\\<^sub>o\<^sub>w\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through simp begin tts_lemma INF_top: assumes "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w" is complete_lattice_class.INF_top[folded const_fun_def]. end end context fixes f :: "'b \ 'al" and c and F and U\<^sub>2 :: "'b set" assumes c_closed[transfer_rule]: "c \ U" assumes f[transfer_rule]: "\x \ U\<^sub>2. f x = c" begin tts_register_sbts \c\ | U proof- assume ALC: "Domainp ALC = (\x. x \ U)" have "Domainp ALC c" unfolding ALC by (simp add: c_closed) then obtain c' where "ALC c c'" by blast then show "\c'. ALC c c'" by auto qed tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) sbterms: (\?c::?'a::complete_lattice\ to \c\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through simp begin tts_lemma INF_constant: assumes "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` A) = (if A = {} then \\<^sub>o\<^sub>w else c)" is complete_lattice_class.INF_constant[folded const_fun_def]. tts_lemma SUP_constant: assumes "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w (f ` A) = (if A = {} then \\<^sub>o\<^sub>w else c)" is complete_lattice_class.SUP_constant[folded const_fun_def]. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) sbterms: (\?f::?'a::complete_lattice\ to \c\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating through simp begin tts_lemma INF_const: assumes "A \ U\<^sub>2" and "A \ {}" shows "\\<^sub>o\<^sub>w ((\i. c) ` A) = c" is complete_lattice_class.INF_const. tts_lemma SUP_const: assumes "A \ U\<^sub>2" and "A \ {}" shows "\\<^sub>o\<^sub>w ((\i. c) ` A) = c" is complete_lattice_class.SUP_const. end end end context complete_lattice_ow begin tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) and (?'c to \U\<^sub>3::'c set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty eliminating \?U \ {}\ through (force simp: subset_iff INF_top equals0D) applying [ OF Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed ] begin tts_lemma SUP_eq: assumes "A \ U\<^sub>2" and "B \ U\<^sub>3" and "\x\U\<^sub>2. f (x::'a) \ U" and "\x\U\<^sub>3. g x \ U" and "\i. i \ A \ \x\B. f i \\<^sub>o\<^sub>w g x" and "\j. j \ B \ \x\A. g j \\<^sub>o\<^sub>w f x" shows "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" given complete_lattice_class.SUP_eq proof- assume "\ A \ U\<^sub>2; B \ U\<^sub>3; \x\U\<^sub>2. f x \ U; \x\U\<^sub>3. g x \ U; \i. \i \ U\<^sub>2; i \ A\ \ \x\B. f i \\<^sub>o\<^sub>w g x; \j. \j \ U\<^sub>3; j \ B\ \ \x\A. g j \\<^sub>o\<^sub>w f x \ \ \\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" for A :: "'a set" and U\<^sub>2 and B :: "'b set" and U\<^sub>3 f g then have "\ A \ U\<^sub>2; B \ U\<^sub>3; \x\U\<^sub>2. f x \ U; \x\U\<^sub>3. g x \ U; \i. i \ A \ \x\B. f i \\<^sub>o\<^sub>w g x; \j. j \ B \ \x\A. g j \\<^sub>o\<^sub>w f x \ \ \\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" by simp then show "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" using assms by simp qed tts_lemma INF_eq: assumes "A \ U\<^sub>2" and "B \ U\<^sub>3" and "\x\U\<^sub>3. g x \ U" and "\x\U\<^sub>2. f (x::'a) \ U" and "\i. i \ A \ \x\B. g x \\<^sub>o\<^sub>w f i" and "\j. j \ B \ \x\A. f x \\<^sub>o\<^sub>w g j" shows "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" given complete_lattice_class.INF_eq proof- assume "\ A \ U\<^sub>2; B \ U\<^sub>3; \x\U\<^sub>3. g x \ U; \x\U\<^sub>2. f x \ U; \i. \i \ U\<^sub>2; i \ A\ \ \x\B. g x \\<^sub>o\<^sub>w f i; \j. \j \ U\<^sub>3; j \ B\ \ \x\A. f x \\<^sub>o\<^sub>w g j \ \ \\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" for A :: "'a set" and U\<^sub>2 and B :: "'b set" and U\<^sub>3 g f then have "\ A \ U\<^sub>2; B \ U\<^sub>3; \x\U\<^sub>3. g x \ U; \x\U\<^sub>2. f x \ U; \i. i \ A \ \x\B. g x \\<^sub>o\<^sub>w f i; \j. j \ B \ \x\A. f x \\<^sub>o\<^sub>w g j \ \ \\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" by simp then show "\\<^sub>o\<^sub>w (f ` A) = \\<^sub>o\<^sub>w (g ` B)" using assms by simp qed end end context complete_lattice_ow begin context fixes U\<^sub>2 :: "'b set" and U\<^sub>3 :: "'c set" begin lemmas [transfer_rule] = image_transfer[where ?'a='b] image_transfer[where ?'a='c] tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) and (?'c to \U\<^sub>3::'c set\) rewriting ctr_simps substituting complete_lattice_ow_axioms and sup_bot.sl_neut.not_empty applying [ OF _ _ Inf_closed' Sup_closed' inf_closed' sup_closed' bot_closed top_closed ] begin tts_lemma ne_INF_commute: assumes "U\<^sub>2 \ {}" and "U\<^sub>3 \ {}" and "\x\U\<^sub>2. \y\U\<^sub>3. f (x::'b) y \ U" and "B \ U\<^sub>3" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w ((\i. \\<^sub>o\<^sub>w (f i ` B)) ` A) = \\<^sub>o\<^sub>w ((\j. \\<^sub>o\<^sub>w ((\i. f i j) ` A)) ` B)" is complete_lattice_class.INF_commute. tts_lemma ne_SUP_commute: assumes "U\<^sub>2 \ {}" and "U\<^sub>3 \ {}" and "\x\U\<^sub>2. \y\U\<^sub>3. f (x::'b) y \ U" and "B \ U\<^sub>3" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w ((\i. \\<^sub>o\<^sub>w (f i ` B)) ` A) = \\<^sub>o\<^sub>w ((\j. \\<^sub>o\<^sub>w ((\i. f i j) ` A)) ` B)" is complete_lattice_class.SUP_commute. tts_lemma ne_SUP_mono: assumes "U\<^sub>2 \ {}" and "U\<^sub>3 \ {}" and "A \ U\<^sub>2" and "B \ U\<^sub>3" and "\x\U\<^sub>2. f (x::'b) \ U" and "\x\U\<^sub>3. g x \ U" and "\n. \n \ U\<^sub>2; n \ A\ \ \x\B. f n \\<^sub>o\<^sub>w g x" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" is complete_lattice_class.SUP_mono. tts_lemma ne_INF_mono: assumes "U\<^sub>2 \ {}" and "U\<^sub>3 \ {}" and "B \ U\<^sub>2" and "A \ U\<^sub>3" and "\x\U\<^sub>3. f x \ U" and "\x\U\<^sub>2. g (x::'b) \ U" and "\m. \m \ U\<^sub>2; m \ B\ \ \x\A. f x \\<^sub>o\<^sub>w g m" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" is complete_lattice_class.INF_mono. end end lemma INF_commute: assumes "\x\U\<^sub>2. \y\U\<^sub>3. f x y \ U" and "B \ U\<^sub>3" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w ((\x. \\<^sub>o\<^sub>w (f x ` B)) ` A) = \\<^sub>o\<^sub>w ((\j. \\<^sub>o\<^sub>w ((\i. f i j) ` A)) ` B)" proof(cases \U\<^sub>2 = {}\) case True then show ?thesis using assms by (simp add: inf_top.sl_neut.neutral_map Inf_top_conv(2)) next case ne_U\<^sub>2: False show ?thesis proof(cases \U\<^sub>3 = {}\) case True show ?thesis proof- from assms(2) have "B = {}" unfolding True by simp from assms(1) show ?thesis unfolding \B = {}\ by (force intro: INF_top) qed next case False from ne_U\<^sub>2 False assms show ?thesis by (rule ne_INF_commute) qed qed lemma SUP_commute: assumes "\x\U\<^sub>2. \y\U\<^sub>3. f x y \ U" and "B \ U\<^sub>3" and "A \ U\<^sub>2" shows "\\<^sub>o\<^sub>w ((\x. \\<^sub>o\<^sub>w (f x ` B)) ` A) = \\<^sub>o\<^sub>w ((\j. \\<^sub>o\<^sub>w ((\i. f i j) ` A)) ` B)" proof(cases \U\<^sub>2 = {}\) case True show ?thesis proof- from assms(3) have "A = {}" unfolding True by simp from assms(2) show ?thesis unfolding \A = {}\ by (simp add: sup_bot.sl_neut.neutral_map inf_absorb1 SUP_bot) qed next case ne_U\<^sub>2: False show ?thesis proof(cases \U\<^sub>3 = {}\) case True show ?thesis proof- from assms(2) have "B = {}" unfolding True by simp from assms(1) show ?thesis unfolding \B = {}\ by (simp add: sup_bot.sl_neut.neutral_map Sup_bot_conv(1)) qed next case False from ne_U\<^sub>2 False assms show ?thesis by (rule ne_SUP_commute) qed qed lemma SUP_mono: assumes "A \ U\<^sub>2" and "B \ U\<^sub>3" and "\x\U\<^sub>2. f x \ U" and "\x\U\<^sub>3. g x \ U" and "\n. n \ A \ \m\B. f n \\<^sub>o\<^sub>w g m" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" proof(cases \U\<^sub>2 = {}\) case True show ?thesis proof- from assms(1) have "A = {}" unfolding True by simp have "f ` A = {}" unfolding \A = {}\ by simp from assms(2,4) show ?thesis unfolding \f ` A = {}\ by (simp add: image_subset_iff in_mono) qed next case ne_U\<^sub>2: False show ?thesis proof(cases \U\<^sub>3 = {}\) case True show ?thesis proof- from assms(2) have "B = {}" unfolding True by simp have "g ` B = {}" unfolding \B = {}\ by simp from assms(1,3,5) show ?thesis unfolding \g ` B = {}\ \B = {}\ by (force simp: subset_iff) qed next case False from ne_U\<^sub>2 False assms show ?thesis by (rule ne_SUP_mono) qed qed lemma INF_mono: assumes "B \ U\<^sub>2" and "A \ U\<^sub>3" and "\x\U\<^sub>3. f x \ U" and "\x\U\<^sub>2. g x \ U" and "\m. m \ B \ \n\A. f n \\<^sub>o\<^sub>w g m" shows "\\<^sub>o\<^sub>w (f ` A) \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w (g ` B)" proof(cases \U\<^sub>2 = {}\) case True show ?thesis proof- from assms(1) have "B = {}" unfolding True by simp have "g ` B = {}" unfolding \B = {}\ by simp from assms(2,3) show ?thesis unfolding \g ` B = {}\ by (simp add: image_subset_iff in_mono) qed next case ne_U\<^sub>2: False show ?thesis proof(cases \U\<^sub>3 = {}\) case True show ?thesis proof- from assms(2) have "A = {}" unfolding True by simp have "f ` A = {}" unfolding \A = {}\ by simp from assms show ?thesis unfolding \f ` A = {}\ \A = {}\ by (auto simp: subset_iff) fastforce qed next case False from ne_U\<^sub>2 False assms show ?thesis by (rule ne_INF_mono) qed qed end context complete_lattice_pair_ow begin tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) rewriting ctr_simps substituting cl\<^sub>1.complete_lattice_ow_axioms and cl\<^sub>2.complete_lattice_ow_axioms and cl\<^sub>1.inf_top.sl_neut.not_empty and cl\<^sub>2.inf_top.sl_neut.not_empty applying [ OF cl\<^sub>1.Inf_closed' cl\<^sub>1.Sup_closed' cl\<^sub>1.inf_closed' cl\<^sub>1.sup_closed' cl\<^sub>1.bot_closed cl\<^sub>1.top_closed cl\<^sub>2.Inf_closed' cl\<^sub>2.Sup_closed' cl\<^sub>2.inf_closed' cl\<^sub>2.sup_closed' cl\<^sub>2.bot_closed cl\<^sub>2.top_closed ] begin tts_lemma mono_Inf: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" shows "f (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1 A) \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 (f ` A)" is complete_lattice_class.mono_Inf. tts_lemma mono_Sup: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" shows "\\<^sub>o\<^sub>w\<^sub>.\<^sub>2 (f ` A) \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1 A)" is complete_lattice_class.mono_Sup. end context fixes U\<^sub>3 :: "'c set" begin lemmas [transfer_rule] = image_transfer[where ?'a='c] tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) and (?'c to \U\<^sub>3::'c set\) rewriting ctr_simps substituting cl\<^sub>1.complete_lattice_ow_axioms and cl\<^sub>2.complete_lattice_ow_axioms and cl\<^sub>1.inf_top.sl_neut.not_empty and cl\<^sub>2.inf_top.sl_neut.not_empty eliminating through (simp add: image_subset_iff image_subset_iff') applying [ OF _ cl\<^sub>1.Inf_closed' cl\<^sub>1.Sup_closed' cl\<^sub>1.inf_closed' cl\<^sub>1.sup_closed' cl\<^sub>1.bot_closed cl\<^sub>1.top_closed cl\<^sub>2.Inf_closed' cl\<^sub>2.Sup_closed' cl\<^sub>2.inf_closed' cl\<^sub>2.sup_closed' cl\<^sub>2.bot_closed cl\<^sub>2.top_closed ] begin tts_lemma mono_SUP: assumes "U\<^sub>3 \ {}" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "\x\U\<^sub>3. A x \ U\<^sub>1" and "I \ U\<^sub>3" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" shows "\\<^sub>o\<^sub>w\<^sub>.\<^sub>2 ((\x. f (A x)) ` I) \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1 (A ` I))" is complete_lattice_class.mono_SUP. tts_lemma mono_INF: assumes "U\<^sub>3 \ {}" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "\x\U\<^sub>3. A x \ U\<^sub>1" and "I \ U\<^sub>3" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" shows "f (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1 (A ` I)) \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 ((\x. f (A x)) ` I)" is complete_lattice_class.mono_INF. end end end text\\newpage\ end \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy --- a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy +++ b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Lattices/SML_Semilattices.thy @@ -1,810 +1,810 @@ (* Title: Examples/SML_Relativization/Lattices/SML_Semilattices.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section\Relativization of the results about semilattices\ theory SML_Semilattices imports "../Simple_Orders/SML_Simple_Orders" "../Algebra/SML_Monoids" begin subsection\Commutative bands\ subsubsection\Definitions and common properties\ locale semilattice_ow = abel_semigroup_ow U f for U :: "'al set" and f + assumes idem[simp]: "x \ U \ x \<^bold>*\<^sub>o\<^sub>w x = x" locale semilattice_set_ow = semilattice_ow U f for U :: "'al set" and f (infixl \\<^bold>*\<^sub>o\<^sub>w\ 70) subsubsection\Transfer rules\ context includes lifting_syntax begin lemma semilattice_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> A) ===> (=)) (\f. semilattice_ow (Collect (Domainp A)) f) semilattice" unfolding semilattice_ow_def semilattice_def semilattice_ow_axioms_def semilattice_axioms_def apply transfer_prover_start apply transfer_step+ by simp lemma semilattice_set_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> A) ===> (=)) (\f. semilattice_set_ow (Collect (Domainp A)) f) semilattice_set" unfolding semilattice_set_ow_def semilattice_set_def by transfer_prover end subsubsection\Relativization\ context semilattice_ow begin tts_context tts: (?'a to U) substituting semilattice_ow_axioms eliminating through simp begin tts_lemma left_idem: assumes "a \ U" and "b \ U" shows "a \<^bold>*\<^sub>o\<^sub>w (a \<^bold>*\<^sub>o\<^sub>w b) = a \<^bold>*\<^sub>o\<^sub>w b" is semilattice.left_idem. tts_lemma right_idem: assumes "a \ U" and "b \ U" shows "a \<^bold>*\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w b = a \<^bold>*\<^sub>o\<^sub>w b" is semilattice.right_idem. end end subsection\Simple upper and lower semilattices\ subsubsection\Definitions and common properties\ locale semilattice_order_ow = semilattice_ow U f for U :: "'al set" and f + fixes le :: "['al, 'al] \ bool" (infix \\\<^sub>o\<^sub>w\ 50) and ls :: "['al, 'al] \ bool" (infix \<\<^sub>o\<^sub>w\ 50) assumes order_iff: "\ a \ U; b \ U \ \ a \\<^sub>o\<^sub>w b \ a = a \<^bold>*\<^sub>o\<^sub>w b" and strict_order_iff: "\ a \ U; b \ U \ \ a <\<^sub>o\<^sub>w b \ a = a \<^bold>*\<^sub>o\<^sub>w b \ a \ b" begin sublocale ordering_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ proof show "\a \ U; b \ U\ \ (a <\<^sub>o\<^sub>w b) = (a \\<^sub>o\<^sub>w b \ a \ b)" for a b apply standard subgoal by (auto simp: commute order_iff strict_order_iff) subgoal by (auto simp: order_iff strict_order_iff) done show "x \ U \ x \\<^sub>o\<^sub>w x" for x by (simp add: order_iff) show "\ x \ U; y \ U; z \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w z \ \ x \\<^sub>o\<^sub>w z" for x y z proof- assume "x \ U" and "y \ U" and "z \ U" and "x \\<^sub>o\<^sub>w y" and "y \\<^sub>o\<^sub>w z" note xy = order_iff[THEN iffD1, OF \x \ U\ \y \ U\ \x \\<^sub>o\<^sub>w y\] note yz = order_iff[THEN iffD1, OF \y \ U\ \z \ U\ \y \\<^sub>o\<^sub>w z\] note xz = assoc[OF \x \ U\ \y \ U\ \z \ U\, folded xy yz, symmetric] show ?thesis by (rule order_iff[THEN iffD2, OF \x \ U\ \z \ U\ xz]) qed show "\ x \ U; y \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w x \ \ x = y" for x y by (fastforce simp: commute order_iff) qed notation le (infix "\\<^sub>o\<^sub>w" 50) and ls (infix "<\<^sub>o\<^sub>w" 50) end locale semilattice_order_set_ow = semilattice_order_ow U f le ls + semilattice_set_ow U f for U :: "'al set" and f le ls locale inf_ow = fixes U :: "'al set" and inf (infixl \\\<^sub>o\<^sub>w\ 70) assumes inf_closed[simp]: "\ x \ U; y \ U \ \ x \\<^sub>o\<^sub>w y \ U" begin notation inf (infixl \\\<^sub>o\<^sub>w\ 70) lemma inf_closed'[simp]: "\x\U. \y\U. x \\<^sub>o\<^sub>w y \ U" by simp end locale inf_pair_ow = inf\<^sub>1: inf_ow U\<^sub>1 inf\<^sub>1 + inf\<^sub>2: inf_ow U\<^sub>2 inf\<^sub>2 for U\<^sub>1 :: "'al set" and inf\<^sub>1 and U\<^sub>2 :: "'bl set" and inf\<^sub>2 begin notation inf\<^sub>1 (infixl \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 70) notation inf\<^sub>2 (infixl \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 70) end locale semilattice_inf_ow = inf_ow U inf + order_ow U le ls for U :: "'al set" and inf le ls + assumes inf_le1[simp]: "\ x \ U; y \ U \ \ x \\<^sub>o\<^sub>w y \\<^sub>o\<^sub>w x" and inf_le2[simp]: "\ x \ U; y \ U \ \ x \\<^sub>o\<^sub>w y \\<^sub>o\<^sub>w y" and inf_greatest: "\ x \ U; y \ U; z \ U; x \\<^sub>o\<^sub>w y; x \\<^sub>o\<^sub>w z \ \ x \\<^sub>o\<^sub>w y \\<^sub>o\<^sub>w z" begin sublocale inf: semilattice_order_ow U \(\\<^sub>o\<^sub>w)\ \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ proof show *: "\ a \ U; b \ U \ \ a \\<^sub>o\<^sub>w b \ U" for a b by simp show **: "\ a \ U; b \ U; c \ U \ \ a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c = a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" for a b c proof - assume "a \ U" and "b \ U" and "c \ U" from \a \ U\ \b \ U\ \c \ U\ have ab_c: "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \ U" by simp from \a \ U\ \b \ U\ \c \ U\ have a_bc: "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \ U" by simp from \a \ U\ \b \ U\ \c \ U\ have "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w b" by (meson * inf_le1 inf_le2 order_trans) moreover from \a \ U\ \b \ U\ \c \ U\ have "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w c" by simp ultimately have abc_le_bc: "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" by (rule inf_greatest[OF ab_c \b \ U\ \c \ U\]) from \a \ U\ \b \ U\ \c \ U\ have abc_le_a: "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w a" by (meson inf_le1 order_trans inf_closed) note lhs = inf_greatest[OF ab_c \a \ U\ *[OF \b \ U\ \c \ U\] abc_le_a abc_le_bc] from \a \ U\ \b \ U\ \c \ U\ have "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \\<^sub>o\<^sub>w a" by (meson * inf_le1 order_trans) moreover from \a \ U\ \b \ U\ \c \ U\ have "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \\<^sub>o\<^sub>w b" by (meson * inf_le1 inf_le2 order_trans) ultimately have abc_le_bc: "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" by (rule inf_greatest[OF a_bc \a \ U\ \b \ U\]) from \a \ U\ \b \ U\ \c \ U\ have abc_le_a: "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \\<^sub>o\<^sub>w c" by (meson inf_le2 order_trans inf_closed) note rhs = inf_greatest[OF a_bc *[OF \a \ U\ \b \ U\] \c \ U\ abc_le_bc abc_le_a] show "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c = a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by (rule antisym[OF ab_c a_bc lhs rhs]) qed show ***: "\ a \ U; b \ U \ \ a \\<^sub>o\<^sub>w b = b \\<^sub>o\<^sub>w a" for a b - by (simp add: eq_iff inf_greatest) + by (simp add: inf_greatest xt1(5)) show ****: "x \ U \ x \\<^sub>o\<^sub>w x = x" for x proof- assume "x \ U" have "x \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w x" by (simp add: \x \ U\) moreover have "x \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w x" by (simp add: \x \ U\ inf_greatest) ultimately show "x \\<^sub>o\<^sub>w x = x" by (simp add: \x \ U\ antisym) qed show *****: "\ a \ U; b \ U \ \ (a \\<^sub>o\<^sub>w b) = (a = a \\<^sub>o\<^sub>w b)" for a b - by (metis * *** eq_iff inf_greatest inf_le1 inf_le2) - + by (metis * *** inf_greatest inf_le2 order.eq_iff) + show "\ a \ U; b \ U \ \ (a <\<^sub>o\<^sub>w b) = (a = a \\<^sub>o\<^sub>w b \ a \ b)" for a b by (simp add: ***** less_le) qed sublocale Inf_fin: semilattice_order_set_ow U \(\\<^sub>o\<^sub>w)\ \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ .. end locale semilattice_inf_pair_ow = sl_inf\<^sub>1: semilattice_inf_ow U\<^sub>1 inf\<^sub>1 le\<^sub>1 ls\<^sub>1 + sl_inf\<^sub>2: semilattice_inf_ow U\<^sub>2 inf\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'al set" and inf\<^sub>1 le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bl set" and inf\<^sub>2 le\<^sub>2 ls\<^sub>2 begin sublocale inf_pair_ow .. sublocale order_pair_ow .. end locale sup_ow = fixes U :: "'ao set" and sup :: "['ao, 'ao] \ 'ao" (infixl \\\<^sub>o\<^sub>w\ 70) assumes sup_closed[simp]: "\ x \ U; y \ U \ \ sup x y \ U" begin notation sup (infixl \\\<^sub>o\<^sub>w\ 70) lemma sup_closed'[simp]: "\x\U. \y\U. x \\<^sub>o\<^sub>w y \ U" by simp end locale sup_pair_ow = sup\<^sub>1: sup_ow U\<^sub>1 sup\<^sub>1 + sup\<^sub>2: sup_ow U\<^sub>2 sup\<^sub>2 for U\<^sub>1 :: "'al set" and sup\<^sub>1 and U\<^sub>2 :: "'bl set" and sup\<^sub>2 begin notation sup\<^sub>1 (infixl \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 70) notation sup\<^sub>2 (infixl \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 70) end locale semilattice_sup_ow = sup_ow U sup + order_ow U le ls for U :: "'al set" and sup le ls + assumes sup_ge1[simp]: "\ x \ U; y \ U \ \ x \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w y" and sup_ge2[simp]: "\ y \ U; x \ U \ \ y \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w y" and sup_least: "\ y \ U; x \ U; z \ U; y \\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w x \ \ y \\<^sub>o\<^sub>w z \\<^sub>o\<^sub>w x" begin sublocale sup: semilattice_order_ow U \(\\<^sub>o\<^sub>w)\ \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ proof show *: "\ a \ U; b \ U \ \ a \\<^sub>o\<^sub>w b \ U" for a b by simp show **: "\ a \ U; b \ U; c \ U \ \ a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c = a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" for a b c proof - assume "a \ U" and "b \ U" and "c \ U" from \a \ U\ \b \ U\ \c \ U\ have ab_c: "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \ U" by simp from \a \ U\ \b \ U\ \c \ U\ have a_bc: "a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c) \ U" by simp from \a \ U\ \b \ U\ \c \ U\ have "b \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" by (meson order_trans sup_ge1 sup_ge2 sup_closed') moreover from \a \ U\ \b \ U\ \c \ U\ have "c \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" by simp ultimately have ab_le_abc: "b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" by (rule sup_least[OF \b \ U\ ab_c \c \ U\]) from \a \ U\ \b \ U\ \c \ U\ have a_le_abc: "a \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" by (meson "*" order_trans sup_ge1) note rhs = sup_least[OF \a \ U\ ab_c *[OF \b \ U\ \c \ U\] a_le_abc ab_le_abc] from \a \ U\ \b \ U\ \c \ U\ have "a \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by simp moreover from \a \ U\ \b \ U\ \c \ U\ have "b \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by (meson order_trans sup_ge1 sup_ge2 sup_closed') ultimately have ab_le_abc: "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by (rule sup_least[OF \a \ U\ a_bc \b \ U\]) from \a \ U\ \b \ U\ \c \ U\ have c_le_abc: "c \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by (meson "*" order_trans sup_ge2) note lhs = sup_least[OF *[OF \a \ U\ \b \ U\] a_bc \c \ U\ ab_le_abc c_le_abc] show "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c = a \\<^sub>o\<^sub>w (b \\<^sub>o\<^sub>w c)" by (rule antisym[OF ab_c a_bc lhs rhs]) qed show ***: "\ a \ U; b \ U \ \ a \\<^sub>o\<^sub>w b = b \\<^sub>o\<^sub>w a" for a b - by (simp add: eq_iff sup_least) + by (simp add: antisym sup_least) show ****: "x \ U \ x \\<^sub>o\<^sub>w x = x" for x proof- assume "x \ U" have "x \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w x" by (simp add: \x \ U\) moreover have "x \\<^sub>o\<^sub>w x \\<^sub>o\<^sub>w x" by (simp add: \x \ U\ sup_least) ultimately show "x \\<^sub>o\<^sub>w x = x" by (simp add: \x \ U\ antisym) qed show *****: "\ a \ U; b \ U \ \ (a \\<^sub>o\<^sub>w b) = (a = a \\<^sub>o\<^sub>w b)" for a b - by (metis *** sup_ge2 sup_least eq_iff eq_refl sup_closed') + by (metis *** order.eq_iff sup_ge2 sup_least sup_closed) show "\ a \ U; b \ U \ \ (a >\<^sub>o\<^sub>w b) = (a = a \\<^sub>o\<^sub>w b \ a \ b)" for a b by (auto simp: ***** less_le) qed sublocale Sup_fin: semilattice_order_set_ow U sup "(\\<^sub>o\<^sub>w)" "(>\<^sub>o\<^sub>w)" .. end locale semilattice_sup_pair_ow = sl_sup\<^sub>1: semilattice_sup_ow U\<^sub>1 sup\<^sub>1 le\<^sub>1 ls\<^sub>1 + sl_sup\<^sub>2: semilattice_sup_ow U\<^sub>2 sup\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'al set" and sup\<^sub>1 le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bl set" and sup\<^sub>2 le\<^sub>2 ls\<^sub>2 begin sublocale sup_pair_ow .. sublocale order_pair_ow .. end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma semilattice_order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) ) (semilattice_order_ow (Collect (Domainp A))) semilattice_order" unfolding semilattice_order_ow_def semilattice_order_def semilattice_order_ow_axioms_def semilattice_order_axioms_def apply transfer_prover_start apply transfer_step+ by simp lemma semilattice_order_set_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) ) (semilattice_order_set_ow (Collect (Domainp A))) semilattice_order_set" unfolding semilattice_order_set_ow_def semilattice_order_set_def apply transfer_prover_start apply transfer_step+ by simp lemma semilattice_inf_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) ) (semilattice_inf_ow (Collect (Domainp A))) class.semilattice_inf" proof - let ?P = "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) )" let ?semilattice_ow = "semilattice_inf_ow (Collect (Domainp A))" let ?rf_UNIV = "(\inf::['b, 'b] \ 'b. (\x y. x \ UNIV \ y \ UNIV \ inf x y \ UNIV))" have "?P ?semilattice_ow (\inf le ls. ?rf_UNIV inf \ class.semilattice_inf inf le ls)" unfolding class.semilattice_inf_def semilattice_inf_ow_def class.semilattice_inf_axioms_def semilattice_inf_ow_axioms_def inf_ow_def apply transfer_prover_start apply transfer_step+ unfolding Ball_def by fastforce then show ?thesis by simp qed lemma semilattice_sup_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) ) (semilattice_sup_ow (Collect (Domainp A))) class.semilattice_sup" proof - let ?P = "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) )" let ?semilattice_ow = "semilattice_sup_ow (Collect (Domainp A))" let ?rf_UNIV = "(\sup::['b, 'b] \ 'b. (\x y. x \ UNIV \ y \ UNIV \ sup x y \ UNIV))" have "?P ?semilattice_ow (\sup le ls. ?rf_UNIV sup \ class.semilattice_sup sup le ls)" unfolding class.semilattice_sup_def semilattice_sup_ow_def class.semilattice_sup_axioms_def semilattice_sup_ow_axioms_def sup_ow_def apply transfer_prover_start apply transfer_step+ unfolding Ball_def by fastforce then show ?thesis by simp qed end subsubsection\Relativization\ context semilattice_order_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting semilattice_order_ow_axioms eliminating through simp begin tts_lemma cobounded1: assumes "a \ U" and "b \ U" shows "a \<^bold>*\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w a" is semilattice_order.cobounded1. tts_lemma cobounded2: assumes "a \ U" and "b \ U" shows "a \<^bold>*\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w b" is semilattice_order.cobounded2. tts_lemma absorb_iff1: assumes "a \ U" and "b \ U" shows "(a \\<^sub>o\<^sub>w b) = (a \<^bold>*\<^sub>o\<^sub>w b = a)" is semilattice_order.absorb_iff1. tts_lemma absorb_iff2: assumes "b \ U" and "a \ U" shows "(b \\<^sub>o\<^sub>w a) = (a \<^bold>*\<^sub>o\<^sub>w b = b)" is semilattice_order.absorb_iff2. tts_lemma strict_coboundedI1: assumes "a \ U" and "c \ U" and "b \ U" and "a <\<^sub>o\<^sub>w c" shows "a \<^bold>*\<^sub>o\<^sub>w b <\<^sub>o\<^sub>w c" is semilattice_order.strict_coboundedI1. tts_lemma strict_coboundedI2: assumes "b \ U" and "c \ U" and "a \ U" and "b <\<^sub>o\<^sub>w c" shows "a \<^bold>*\<^sub>o\<^sub>w b <\<^sub>o\<^sub>w c" is semilattice_order.strict_coboundedI2. tts_lemma absorb1: assumes "a \ U" and "b \ U" and "a \\<^sub>o\<^sub>w b" shows "a \<^bold>*\<^sub>o\<^sub>w b = a" is semilattice_order.absorb1. tts_lemma coboundedI1: assumes "a \ U" and "c \ U" and "b \ U" and "a \\<^sub>o\<^sub>w c" shows "a \<^bold>*\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" is semilattice_order.coboundedI1. tts_lemma absorb2: assumes "b \ U" and "a \ U" and "b \\<^sub>o\<^sub>w a" shows "a \<^bold>*\<^sub>o\<^sub>w b = b" is semilattice_order.absorb2. tts_lemma coboundedI2: assumes "b \ U" and "c \ U" and "a \ U" and "b \\<^sub>o\<^sub>w c" shows "a \<^bold>*\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c" is semilattice_order.coboundedI2. tts_lemma orderI: assumes "a \ U" and "b \ U" and "a = a \<^bold>*\<^sub>o\<^sub>w b" shows "a \\<^sub>o\<^sub>w b" is semilattice_order.orderI. tts_lemma bounded_iff: assumes "a \ U" and "b \ U" and "c \ U" shows "(a \\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c) = (a \\<^sub>o\<^sub>w b \ a \\<^sub>o\<^sub>w c)" is semilattice_order.bounded_iff. tts_lemma boundedI: assumes "a \ U" and "b \ U" and "c \ U" and "a \\<^sub>o\<^sub>w b" and "a \\<^sub>o\<^sub>w c" shows "a \\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c" is semilattice_order.boundedI. tts_lemma orderE: assumes "a \ U" and "b \ U" and "a \\<^sub>o\<^sub>w b" and "a = a \<^bold>*\<^sub>o\<^sub>w b \ thesis" shows thesis is semilattice_order.orderE. tts_lemma mono: assumes "a \ U" and "c \ U" and "b \ U" and "d \ U" and "a \\<^sub>o\<^sub>w c" and "b \\<^sub>o\<^sub>w d" shows "a \<^bold>*\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \<^bold>*\<^sub>o\<^sub>w d" is semilattice_order.mono. tts_lemma strict_boundedE: assumes "a \ U" and "b \ U" and "c \ U" and "a <\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c" obtains "a <\<^sub>o\<^sub>w b" and "a <\<^sub>o\<^sub>w c" given semilattice_order.strict_boundedE by auto tts_lemma boundedE: assumes "a \ U" and "b \ U" and "c \ U" and "a \\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c" obtains "a \\<^sub>o\<^sub>w b" and "a \\<^sub>o\<^sub>w c" given semilattice_order.boundedE by auto end end context semilattice_inf_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting semilattice_inf_ow_axioms eliminating through simp begin tts_lemma le_iff_inf: assumes "x \ U" and "y \ U" shows "(x \\<^sub>o\<^sub>w y) = (x \\<^sub>o\<^sub>w y = x)" is semilattice_inf_class.le_iff_inf. tts_lemma less_infI1: assumes "a \ U" and "x \ U" and "b \ U" and "a <\<^sub>o\<^sub>w x" shows "a \\<^sub>o\<^sub>w b <\<^sub>o\<^sub>w x" is semilattice_inf_class.less_infI1. tts_lemma less_infI2: assumes "b \ U" and "x \ U" and "a \ U" and "b <\<^sub>o\<^sub>w x" shows "a \\<^sub>o\<^sub>w b <\<^sub>o\<^sub>w x" is semilattice_inf_class.less_infI2. tts_lemma le_infI1: assumes "a \ U" and "x \ U" and "b \ U" and "a \\<^sub>o\<^sub>w x" shows "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w x" is semilattice_inf_class.le_infI1. tts_lemma le_infI2: assumes "b \ U" and "x \ U" and "a \ U" and "b \\<^sub>o\<^sub>w x" shows "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w x" is semilattice_inf_class.le_infI2. tts_lemma le_inf_iff: assumes "x \ U" and "y \ U" and "z \ U" shows "(x \\<^sub>o\<^sub>w y \\<^sub>o\<^sub>w z) = (x \\<^sub>o\<^sub>w y \ x \\<^sub>o\<^sub>w z)" is semilattice_inf_class.le_inf_iff. tts_lemma le_infI: assumes "x \ U" and "a \ U" and "b \ U" and "x \\<^sub>o\<^sub>w a" and "x \\<^sub>o\<^sub>w b" shows "x \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" is semilattice_inf_class.le_infI. tts_lemma le_infE: assumes "x \ U" and "a \ U" and "b \ U" and "x \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" and "\x \\<^sub>o\<^sub>w a; x \\<^sub>o\<^sub>w b\ \ P" shows P is semilattice_inf_class.le_infE. tts_lemma inf_mono: assumes "a \ U" and "c \ U" and "b \ U" and "d \ U" and "a \\<^sub>o\<^sub>w c" and "b \\<^sub>o\<^sub>w d" shows "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w d" is semilattice_inf_class.inf_mono. end end context semilattice_sup_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting semilattice_sup_ow_axioms eliminating through simp begin tts_lemma le_iff_sup: assumes "x \ U" and "y \ U" shows "(x \\<^sub>o\<^sub>w y) = (x \\<^sub>o\<^sub>w y = y)" is semilattice_sup_class.le_iff_sup. tts_lemma less_supI1: assumes "x \ U" and "a \ U" and "b \ U" and "x <\<^sub>o\<^sub>w a" shows "x <\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" is semilattice_sup_class.less_supI1. tts_lemma less_supI2: assumes "x \ U" and "b \ U" and "a \ U" and "x <\<^sub>o\<^sub>w b" shows "x <\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" is semilattice_sup_class.less_supI2. tts_lemma le_supI1: assumes "x \ U" and "a \ U" and "b \ U" and "x \\<^sub>o\<^sub>w a" shows "x \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" is semilattice_sup_class.le_supI1. tts_lemma le_supI2: assumes "x \ U" and "b \ U" and "a \ U" and "x \\<^sub>o\<^sub>w b" shows "x \\<^sub>o\<^sub>w a \\<^sub>o\<^sub>w b" is semilattice_sup_class.le_supI2. tts_lemma le_sup_iff: assumes "x \ U" and "y \ U" and "z \ U" shows "(x \\<^sub>o\<^sub>w y \\<^sub>o\<^sub>w z) = (x \\<^sub>o\<^sub>w z \ y \\<^sub>o\<^sub>w z)" is semilattice_sup_class.le_sup_iff. tts_lemma le_supI: assumes "a \ U" and "x \ U" and "b \ U" and "a \\<^sub>o\<^sub>w x" and "b \\<^sub>o\<^sub>w x" shows "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w x" is semilattice_sup_class.le_supI. tts_lemma le_supE: assumes "a \ U" and "b \ U" and "x \ U" and "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w x" and "\a \\<^sub>o\<^sub>w x; b \\<^sub>o\<^sub>w x\ \ P" shows P is semilattice_sup_class.le_supE. tts_lemma sup_unique: assumes "\x\U. \y\U. f x y \ U" and "x \ U" and "y \ U" and "\x y. \x \ U; y \ U\ \ x \\<^sub>o\<^sub>w f x y" and "\x y. \x \ U; y \ U\ \ y \\<^sub>o\<^sub>w f x y" and "\x y z. \x \ U; y \ U; z \ U; y \\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w x\ \ f y z \\<^sub>o\<^sub>w x" shows "x \\<^sub>o\<^sub>w y = f x y" is semilattice_sup_class.sup_unique. tts_lemma sup_mono: assumes "a \ U" and "c \ U" and "b \ U" and "d \ U" and "a \\<^sub>o\<^sub>w c" and "b \\<^sub>o\<^sub>w d" shows "a \\<^sub>o\<^sub>w b \\<^sub>o\<^sub>w c \\<^sub>o\<^sub>w d" is semilattice_sup_class.sup_mono. end end subsection\Bounded semilattices\ subsubsection\Definitions and common properties\ locale semilattice_neutral_ow = semilattice_ow U f + comm_monoid_ow U f z for U :: "'al set" and f z locale semilattice_neutral_order_ow = sl_neut: semilattice_neutral_ow U f z + sl_ord: semilattice_order_ow U f le ls for U :: "'al set" and f z le ls begin sublocale order_top_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ \\<^bold>1\<^sub>o\<^sub>w\ apply unfold_locales subgoal by (auto simp: antisym sl_ord.strict_iff_order sl_ord.antisym) subgoal by (auto simp: sl_ord.order_iff) subgoal by (auto intro: sl_ord.trans) subgoal by (auto simp: sl_ord.antisym) subgoal by auto subgoal by (simp add: sl_ord.absorb_iff1) done end locale bounded_semilattice_inf_top_ow = semilattice_inf_ow U inf le ls + order_top_ow U le ls top for U :: "'al set" and inf le ls top begin sublocale inf_top: semilattice_neutral_order_ow U \(\\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ apply unfold_locales subgoal by simp subgoal using top_greatest by (simp add: inf.order_iff) done end locale bounded_semilattice_sup_bot_ow = semilattice_sup_ow U sup le ls + order_bot_ow U bot le ls for U :: "'al set" and sup le ls bot begin sublocale sup_bot: semilattice_neutral_order_ow U \(\\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ by unfold_locales (simp_all add: sup.absorb1) end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma semilattice_neutral_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> A) ===> A ===> (=)) (semilattice_neutral_ow (Collect (Domainp A))) semilattice_neutr" unfolding semilattice_neutral_ow_def semilattice_neutr_def by transfer_prover lemma semilattice_neutr_order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=) ) (semilattice_neutral_order_ow (Collect (Domainp A))) semilattice_neutr_order" unfolding semilattice_neutral_order_ow_def semilattice_neutr_order_def by transfer_prover lemma bounded_semilattice_inf_top_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=) ) (bounded_semilattice_inf_top_ow (Collect (Domainp A))) class.bounded_semilattice_inf_top" unfolding bounded_semilattice_inf_top_ow_def class.bounded_semilattice_inf_top_def by transfer_prover lemma bounded_semilattice_sup_bot_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "( (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=) ) (bounded_semilattice_sup_bot_ow (Collect (Domainp A))) class.bounded_semilattice_sup_bot" unfolding bounded_semilattice_sup_bot_ow_def class.bounded_semilattice_sup_bot_def by transfer_prover end text\\newpage\ end \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy --- a/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy +++ b/thys/Types_To_Sets_Extension/Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy @@ -1,1943 +1,1985 @@ (* Title: Examples/SML_Relativization/Simple_Orders/SML_Simple_Orders.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section\Relativization of the results about orders\ theory SML_Simple_Orders imports "../../Introduction" "../Foundations/SML_Relations" Complex_Main begin subsection\Class \<^class>\ord\\ subsubsection\Definitions and common properties\ locale ord_ow = fixes U :: "'ao set" and le :: "['ao, 'ao] \ bool" (infix \\\<^sub>o\<^sub>w\ 50) and ls :: "['ao, 'ao] \ bool" (infix \<\<^sub>o\<^sub>w\ 50) begin notation le (\'(\\<^sub>o\<^sub>w')\) and le (infix \\\<^sub>o\<^sub>w\ 50) and ls (\'(<\<^sub>o\<^sub>w')\) and ls (infix \<\<^sub>o\<^sub>w\ 50) abbreviation (input) ge (infix \\\<^sub>o\<^sub>w\ 50) where "x \\<^sub>o\<^sub>w y \ y \\<^sub>o\<^sub>w x" abbreviation (input) gt (infix \>\<^sub>o\<^sub>w\ 50) where "x >\<^sub>o\<^sub>w y \ y <\<^sub>o\<^sub>w x" notation ge (\'(\\<^sub>o\<^sub>w')\) and ge (infix \\\<^sub>o\<^sub>w\ 50) and gt (\'(>\<^sub>o\<^sub>w')\) and gt (infix \>\<^sub>o\<^sub>w\ 50) tts_register_sbts \(\\<^sub>o\<^sub>w)\ | U proof- assume "Domainp AOA = (\x. x \ U)" "bi_unique AOA" "right_total AOA" from tts_AA_eq_transfer[OF this] show ?thesis by auto qed tts_register_sbts \(<\<^sub>o\<^sub>w)\ | U proof- assume "Domainp AOA = (\x. x \ U)" "bi_unique AOA" "right_total AOA" from tts_AA_eq_transfer[OF this] show ?thesis by auto qed end locale ord_pair_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: ord_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 begin notation le\<^sub>1 (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and le\<^sub>1 (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ls\<^sub>1 (\'(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ls\<^sub>1 (infix \<\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and le\<^sub>2 (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and le\<^sub>2 (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) and ls\<^sub>2 (\'(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ls\<^sub>2 (infix \<\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) notation ord\<^sub>1.ge (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ord\<^sub>1.ge (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ord\<^sub>1.gt (\'(>\<^sub>o\<^sub>w\<^sub>.\<^sub>1')\) and ord\<^sub>1.gt (infix \>\<^sub>o\<^sub>w\<^sub>.\<^sub>1\ 50) and ord\<^sub>2.ge (\'(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ord\<^sub>2.ge (infix \\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) and ord\<^sub>2.gt (\'(>\<^sub>o\<^sub>w\<^sub>.\<^sub>2')\) and ord\<^sub>2.gt (infix \>\<^sub>o\<^sub>w\<^sub>.\<^sub>2\ 50) end ud \ord.lessThan\ (\(with _ : ({..<_}))\ [1000] 10) ud lessThan' \lessThan\ ud \ord.atMost\ (\(with _ : ({.._}))\ [1000] 10) ud atMost' \atMost\ ud \ord.greaterThan\ (\(with _ : ({_<..}))\ [1000] 10) ud greaterThan' \greaterThan\ ud \ord.atLeast\ (\(with _ : ({_..}))\ [1000] 10) ud atLeast' \atLeast\ ud \ord.greaterThanLessThan\ (\(with _ : ({_<..<_}))\ [1000, 999, 1000] 10) ud greaterThanLessThan' \greaterThanLessThan\ ud \ord.atLeastLessThan\ (\(with _ _ : ({_..<_}))\ [1000, 999, 1000, 1000] 10) ud atLeastLessThan' \atLeastLessThan\ ud \ord.greaterThanAtMost\ (\(with _ _ : ({_<.._}))\ [1000, 999, 1000, 999] 10) ud greaterThanAtMost' \greaterThanAtMost\ ud \ord.atLeastAtMost\ (\(with _ : ({_.._}))\ [1000, 1000, 1000] 10) ud atLeastAtMost' \atLeastAtMost\ ud \ord.min\ (\(with _ : \min\ _ _)\ [1000, 1000, 999] 10) ud min' \min\ ud \ord.max\ (\(with _ : \max\ _ _)\ [1000, 1000, 999] 10) ud max' \max\ ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" and [transfer_rule]: "right_total A" trp (?'a A) in lessThan_ow: lessThan.with_def (\(on _ with _ : ({..<_}))\ [1000, 1000, 1000] 10) and atMost_ow: atMost.with_def (\(on _ with _ : ({.._}))\ [1000, 1000, 1000] 10) and greaterThan_ow: greaterThan.with_def (\(on _ with _: ({_<..}))\ [1000, 1000, 1000] 10) and atLeast_ow: atLeast.with_def (\(on _ with _ : ({_..}))\ [1000, 1000, 1000] 10) ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" and [transfer_rule]: "bi_unique A" "right_total A" trp (?'a A) in greaterThanLessThan_ow: greaterThanLessThan.with_def (\(on _ with _ : ({_<..<_}))\ [1000, 1000, 1000, 1000] 10) and atLeastLessThan_ow: atLeastLessThan.with_def (\(on _ with _ _ : ({_..<_}))\ [1000, 1000, 999, 1000, 1000] 10) and greaterThanAtMost_ow: greaterThanAtMost.with_def (\(on _ with _ _ : ({_<.._}))\ [1000, 1000, 999, 1000, 1000] 10) and atLeastAtMost_ow: atLeastAtMost.with_def (\(on _ with _ : ({_.._}))\ [1000, 1000, 1000, 1000] 10) ctr parametricity in min_ow: min.with_def and max_ow: max.with_def context ord_ow begin abbreviation lessThan :: "'ao \ 'ao set" ("(1{..<\<^sub>o\<^sub>w_})") where "{..<\<^sub>o\<^sub>w u} \ on U with (<\<^sub>o\<^sub>w) : {.. 'ao set" ("(1{..\<^sub>o\<^sub>w_})") where "{..\<^sub>o\<^sub>w u} \ on U with (\\<^sub>o\<^sub>w) : {..u}" abbreviation greaterThan :: "'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w..})") where "{l<\<^sub>o\<^sub>w..} \ on U with (<\<^sub>o\<^sub>w) : {l<..}" abbreviation atLeast :: "'ao \ 'ao set" ("(1{_..\<^sub>o\<^sub>w})") where "atLeast l \ on U with (\\<^sub>o\<^sub>w) : {l..}" abbreviation greaterThanLessThan :: "'ao \ 'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>w_})") where "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} \ on U with (<\<^sub>o\<^sub>w) : {l<.. 'ao \ 'ao set" ("(1{_..<\<^sub>o\<^sub>w_})") where "{l..<\<^sub>o\<^sub>w u} \ on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l<..u}" abbreviation greaterThanAtMost :: "'ao \ 'ao \ 'ao set" ("(1{_<\<^sub>o\<^sub>w.._})") where "{l<\<^sub>o\<^sub>w..u} \ on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l<..u}" abbreviation atLeastAtMost :: "'ao \ 'ao \ 'ao set" ("(1{_..\<^sub>o\<^sub>w_})") where "{l..\<^sub>o\<^sub>wu} \ on U with (\\<^sub>o\<^sub>w) : {l..u}" abbreviation min :: "'ao \ 'ao \ 'ao" where "min \ min.with (\\<^sub>o\<^sub>w)" abbreviation max :: "'ao \ 'ao \ 'ao" where "max \ max.with (\\<^sub>o\<^sub>w)" end context ord_pair_ow begin notation ord\<^sub>1.lessThan ("(1{..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.atMost ("(1{..\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.greaterThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1..})") notation ord\<^sub>1.atLeast ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>1})") notation ord\<^sub>1.greaterThanLessThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.atLeastLessThan ("(1{_..<\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>1.greaterThanAtMost ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>1.._})") notation ord\<^sub>1.atLeastAtMost ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>1_})") notation ord\<^sub>2.lessThan ("(1{..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.atMost ("(1{..\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.greaterThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2..})") notation ord\<^sub>2.atLeast ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>2})") notation ord\<^sub>2.greaterThanLessThan ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.atLeastLessThan ("(1{_..<\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") notation ord\<^sub>2.greaterThanAtMost ("(1{_<\<^sub>o\<^sub>w\<^sub>.\<^sub>2.._})") notation ord\<^sub>2.atLeastAtMost ("(1{_..\<^sub>o\<^sub>w\<^sub>.\<^sub>2_})") end subsection\Preorders\ subsubsection\Definitions and common properties\ +locale partial_preordering_ow = + fixes U :: "'ao set" + and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + assumes refl: "a \ U \ a \<^bold>\\<^sub>o\<^sub>w a" + and trans: "\ a \ U; b \ U; c \ U; a \<^bold>\\<^sub>o\<^sub>w b; b \<^bold>\\<^sub>o\<^sub>w c \ \ a \<^bold>\\<^sub>o\<^sub>w c" +begin + +notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + +end + +locale preordering_ow = partial_preordering_ow U le + for U :: "'ao set" + and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + + fixes ls :: \'ao \ 'ao \ bool\ (infix "\<^bold><\<^sub>o\<^sub>w" 50) + assumes strict_iff_not: + "\ a \ U; b \ U \ \ a \<^bold><\<^sub>o\<^sub>w b \ a \<^bold>\\<^sub>o\<^sub>w b \ \ b \<^bold>\\<^sub>o\<^sub>w a" + locale preorder_ow = ord_ow U le ls for U :: "'ao set" and le ls + assumes less_le_not_le: "\ x \ U; y \ U \ \ x <\<^sub>o\<^sub>w y \ x \\<^sub>o\<^sub>w y \ \ (y \\<^sub>o\<^sub>w x)" and order_refl[iff]: "x \ U \ x \\<^sub>o\<^sub>w x" and order_trans: "\ x \ U; y \ U; z \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w z \ \ x \\<^sub>o\<^sub>w z" +begin + +sublocale + order: preordering_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ + + dual_order: preordering_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ + apply unfold_locales + subgoal by auto + subgoal by (meson order_trans) + subgoal using less_le_not_le by simp + subgoal by (meson order_trans) + subgoal by (metis less_le_not_le) + done + +end locale ord_preorder_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: preorder_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 begin sublocale ord_pair_ow . end locale preorder_pair_ow = ord\<^sub>1: preorder_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: preorder_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 and ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 and ls\<^sub>2 begin sublocale ord_preorder_ow .. end -ud \preorder.bdd_above\ (\(with _ : \bdd'_above\ _)\ [1000, 1000] 10) +ud \preordering_bdd.bdd\ +ud \preorder.bdd_above\ ud bdd_above' \bdd_above\ -ud \preorder.bdd_below\ (\(with _ : \bdd'_below\ _)\ [1000, 1000] 10) +ud \preorder.bdd_below\ ud bdd_below' \bdd_below\ ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (\x. x \ U)" - and [transfer_rule]: "right_total A" + and [transfer_rule]: "right_total A" "bi_unique A" trp (?'a A) - in bdd_above_ow: bdd_above.with_def + in bdd_ow: bdd.with_def + (\(on _ with _ : \bdd\ _)\ [1000, 1000, 1000] 10) + and bdd_above_ow: bdd_above.with_def (\(on _ with _ : \bdd'_above\ _)\ [1000, 1000, 1000] 10) and bdd_below_ow: bdd_below.with_def (\(on _ with _ : \bdd'_below\ _)\ [1000, 1000, 1000] 10) +declare bdd.with[ud_with del] + context preorder_ow begin abbreviation bdd_above :: "'ao set \ bool" where "bdd_above \ bdd_above_ow U (\\<^sub>o\<^sub>w)" abbreviation bdd_below :: "'ao set \ bool" where "bdd_below \ bdd_below_ow U (\\<^sub>o\<^sub>w)" end subsubsection\Transfer rules\ context includes lifting_syntax begin +lemma partial_preordering_transfer[transfer_rule]: + assumes [transfer_rule]: "right_total A" + shows + "((A ===> A ===> (=)) ===> (=)) + (partial_preordering_ow (Collect (Domainp A))) partial_preordering" + unfolding partial_preordering_ow_def partial_preordering_def + apply transfer_prover_start + apply transfer_step+ + by blast + +lemma preordering_transfer[transfer_rule]: + assumes [transfer_rule]: "right_total A" + shows + "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) + (preordering_ow (Collect (Domainp A))) preordering" + unfolding + preordering_ow_def preordering_ow_axioms_def + preordering_def preordering_axioms_def + apply transfer_prover_start + apply transfer_step+ + by blast + lemma preorder_transfer[transfer_rule]: assumes [transfer_rule]: "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (preorder_ow (Collect (Domainp A))) class.preorder" unfolding preorder_ow_def class.preorder_def apply transfer_prover_start apply transfer_step+ by blast end subsubsection\Relativization\ +context preordering_ow +begin + +tts_context + tts: (?'a to U) + rewriting ctr_simps + substituting preordering_ow_axioms + eliminating through auto +begin + +tts_lemma strict_implies_order: + assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" + shows "a \<^bold>\\<^sub>o\<^sub>w b" + is preordering.strict_implies_order. + +tts_lemma irrefl: + assumes "a \ U" + shows "\a \<^bold><\<^sub>o\<^sub>w a" + is preordering.irrefl. + +tts_lemma asym: + assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w a" + shows False + is preordering.asym. + +tts_lemma strict_trans1: + assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold>\\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" + shows "a \<^bold><\<^sub>o\<^sub>w c" + is preordering.strict_trans1. + +tts_lemma strict_trans2: + assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold>\\<^sub>o\<^sub>w c" + shows "a \<^bold><\<^sub>o\<^sub>w c" + is preordering.strict_trans2. + +tts_lemma strict_trans: + assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" + shows "a \<^bold><\<^sub>o\<^sub>w c" + is preordering.strict_trans. + +end + +end + context preorder_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting preorder_ow_axioms eliminating through auto begin tts_lemma less_irrefl: assumes "x \ U" shows "\ x <\<^sub>o\<^sub>w x" is preorder_class.less_irrefl. tts_lemma bdd_below_Ioc: assumes "a \ U" and "b \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..b}" is preorder_class.bdd_below_Ioc. tts_lemma bdd_above_Ioc: assumes "a \ U" and "b \ U" shows "bdd_above {a<\<^sub>o\<^sub>w..b}" is preorder_class.bdd_above_Ioc. tts_lemma bdd_above_Iic: assumes "b \ U" shows "bdd_above {..\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Iic. tts_lemma bdd_above_Iio: assumes "b \ U" shows "bdd_above {..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Iio. tts_lemma bdd_below_Ici: assumes "a \ U" shows "bdd_below {a..\<^sub>o\<^sub>w}" is preorder_class.bdd_below_Ici. tts_lemma bdd_below_Ioi: assumes "a \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..}" is preorder_class.bdd_below_Ioi. tts_lemma bdd_above_Icc: assumes "a \ U" and "b \ U" shows "bdd_above {a..\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Icc. tts_lemma bdd_above_Ioo: assumes "a \ U" and "b \ U" shows "bdd_above {a<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_above_Ioo. tts_lemma bdd_below_Icc: assumes "a \ U" and "b \ U" shows "bdd_below {a..\<^sub>o\<^sub>wb}" is preorder_class.bdd_below_Icc. tts_lemma bdd_below_Ioo: assumes "a \ U" and "b \ U" shows "bdd_below {a<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wb}" is preorder_class.bdd_below_Ioo. tts_lemma bdd_above_Ico: assumes "a \ U" and "b \ U" shows "bdd_above (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" and "b \ U" shows "bdd_below (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" shows "{a<\<^sub>o\<^sub>w..} \ {a..\<^sub>o\<^sub>w}" is preorder_class.Ioi_le_Ico. tts_lemma eq_refl: assumes "y \ U" and "x = y" shows "x \\<^sub>o\<^sub>w y" is preorder_class.eq_refl. tts_lemma less_imp_le: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "x \\<^sub>o\<^sub>w y" is preorder_class.less_imp_le. tts_lemma less_not_sym: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\ y <\<^sub>o\<^sub>w x" is preorder_class.less_not_sym. tts_lemma less_imp_not_less: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(\ y <\<^sub>o\<^sub>w x) = True" is preorder_class.less_imp_not_less. tts_lemma less_asym': assumes "a \ U" and "b \ U" and "a <\<^sub>o\<^sub>w b" and "b <\<^sub>o\<^sub>w a" shows P is preorder_class.less_asym'. tts_lemma less_imp_triv: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(y <\<^sub>o\<^sub>w x \ P) = True" is preorder_class.less_imp_triv. tts_lemma less_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x <\<^sub>o\<^sub>w y" and "y <\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.less_trans. tts_lemma less_le_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x <\<^sub>o\<^sub>w y" and "y \\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.less_le_trans. tts_lemma le_less_trans: assumes "x \ U" and "y \ U" and "z \ U" and "x \\<^sub>o\<^sub>w y" and "y <\<^sub>o\<^sub>w z" shows "x <\<^sub>o\<^sub>w z" is preorder_class.le_less_trans. tts_lemma bdd_aboveI: assumes "A \ U" and "M \ U" and "\x. \x \ U; x \ A\ \ x \\<^sub>o\<^sub>w M" shows "bdd_above A" is preorder_class.bdd_aboveI. tts_lemma bdd_belowI: assumes "A \ U" and "m \ U" and "\x. \x \ U; x \ A\ \ m \\<^sub>o\<^sub>w x" shows "bdd_below A" is preorder_class.bdd_belowI. tts_lemma less_asym: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" and "\ P \ y <\<^sub>o\<^sub>w x" shows P is preorder_class.less_asym. tts_lemma transp_less: "transp_on U (<\<^sub>o\<^sub>w)" is preorder_class.transp_less. tts_lemma transp_le: "transp_on U (\\<^sub>o\<^sub>w)" is preorder_class.transp_le. tts_lemma transp_gr: "transp_on U (\x y. y <\<^sub>o\<^sub>w x)" is preorder_class.transp_gr. tts_lemma transp_ge: "transp_on U (\x y. y \\<^sub>o\<^sub>w x)" is preorder_class.transp_ge. tts_lemma bdd_above_Int1: assumes "A \ U" and "B \ U" and "bdd_above A" shows "bdd_above (A \ B)" is preorder_class.bdd_above_Int1. tts_lemma bdd_above_Int2: assumes "B \ U" and "A \ U" and "bdd_above B" shows "bdd_above (A \ B)" is preorder_class.bdd_above_Int2. tts_lemma bdd_below_Int1: assumes "A \ U" and "B \ U" and "bdd_below A" shows "bdd_below (A \ B)" is preorder_class.bdd_below_Int1. tts_lemma bdd_below_Int2: assumes "B \ U" and "A \ U" and "bdd_below B" shows "bdd_below (A \ B)" is preorder_class.bdd_below_Int2. tts_lemma bdd_above_mono: assumes "B \ U" and "bdd_above B" and "A \ B" shows "bdd_above A" is preorder_class.bdd_above_mono. tts_lemma bdd_below_mono: assumes "B \ U" and "bdd_below B" and "A \ B" shows "bdd_below A" is preorder_class.bdd_below_mono. tts_lemma atLeastAtMost_subseteq_atLeastLessThan_iff: - assumes "a \ U" - and "b \ U" - and "c \ U" - and "d \ U" + assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {c..\<^sub>o\<^sub>w b \ b <\<^sub>o\<^sub>w d \ c \\<^sub>o\<^sub>w a)" is preorder_class.atLeastAtMost_subseteq_atLeastLessThan_iff. tts_lemma atMost_subset_iff: assumes "x \ U" and "y \ U" shows "({..\<^sub>o\<^sub>wx} \ {..\<^sub>o\<^sub>wy}) = (x \\<^sub>o\<^sub>w y)" is Set_Interval.atMost_subset_iff. tts_lemma single_Diff_lessThan: assumes "k \ U" shows "{k} - {..<\<^sub>o\<^sub>wk} = {k}" is Set_Interval.single_Diff_lessThan. tts_lemma atLeast_subset_iff: assumes "x \ U" and "y \ U" shows "({x..\<^sub>o\<^sub>w} \ {y..\<^sub>o\<^sub>w}) = (y \\<^sub>o\<^sub>w x)" is Set_Interval.atLeast_subset_iff. tts_lemma atLeastatMost_psubset_iff: assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ {c..\<^sub>o\<^sub>wd}) = (c \\<^sub>o\<^sub>w d \ (\ a \\<^sub>o\<^sub>w b \ c \\<^sub>o\<^sub>w a \ b \\<^sub>o\<^sub>w d \ (c <\<^sub>o\<^sub>w a \ b <\<^sub>o\<^sub>w d)))" is preorder_class.atLeastatMost_psubset_iff. tts_lemma not_empty_eq_Iic_eq_empty: assumes "h \ U" shows "{} \ {..\<^sub>o\<^sub>wh}" is preorder_class.not_empty_eq_Iic_eq_empty. tts_lemma atLeastatMost_subset_iff: assumes "a \ U" and "b \ U" and "c \ U" and "d \ U" shows "({a..\<^sub>o\<^sub>wb} \ {c..\<^sub>o\<^sub>wd}) = (\ a \\<^sub>o\<^sub>w b \ b \\<^sub>o\<^sub>w d \ c \\<^sub>o\<^sub>w a)" is preorder_class.atLeastatMost_subset_iff. tts_lemma Icc_subset_Ici_iff: assumes "l \ U" and "h \ U" and "l' \ U" shows "({l..\<^sub>o\<^sub>wh} \ {l'..\<^sub>o\<^sub>w}) = (\ l \\<^sub>o\<^sub>w h \ l' \\<^sub>o\<^sub>w l)" is preorder_class.Icc_subset_Ici_iff. tts_lemma Icc_subset_Iic_iff: assumes "l \ U" and "h \ U" and "h' \ U" shows "({l..\<^sub>o\<^sub>wh} \ {..\<^sub>o\<^sub>wh'}) = (\ l \\<^sub>o\<^sub>w h \ h \\<^sub>o\<^sub>w h')" is preorder_class.Icc_subset_Iic_iff. tts_lemma not_empty_eq_Ici_eq_empty: assumes "l \ U" shows "{} \ {l..\<^sub>o\<^sub>w}" is preorder_class.not_empty_eq_Ici_eq_empty. tts_lemma not_Ici_eq_empty: assumes "l \ U" shows "{l..\<^sub>o\<^sub>w} \ {}" is preorder_class.not_Ici_eq_empty. tts_lemma not_Iic_eq_empty: assumes "h \ U" shows "{..\<^sub>o\<^sub>wh} \ {}" is preorder_class.not_Iic_eq_empty. tts_lemma atLeastatMost_empty_iff2: assumes "a \ U" and "b \ U" shows "({} = {a..\<^sub>o\<^sub>wb}) = (\ a \\<^sub>o\<^sub>w b)" is preorder_class.atLeastatMost_empty_iff2. tts_lemma atLeastLessThan_empty_iff2: assumes "a \ U" and "b \ U" shows "({} = (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. a <\<^sub>o\<^sub>w b)" is preorder_class.atLeastLessThan_empty_iff2. tts_lemma greaterThanAtMost_empty_iff2: assumes "k \ U" and "l \ U" shows "({} = {k<\<^sub>o\<^sub>w..l}) = (\ k <\<^sub>o\<^sub>w l)" is preorder_class.greaterThanAtMost_empty_iff2. tts_lemma atLeastatMost_empty_iff: assumes "a \ U" and "b \ U" shows "({a..\<^sub>o\<^sub>wb} = {}) = (\ a \\<^sub>o\<^sub>w b)" is preorder_class.atLeastatMost_empty_iff. tts_lemma atLeastLessThan_empty_iff: assumes "a \ U" and "b \ U" shows "((on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. a <\<^sub>o\<^sub>w b)" is preorder_class.atLeastLessThan_empty_iff. tts_lemma greaterThanAtMost_empty_iff: assumes "k \ U" and "l \ U" shows "({k<\<^sub>o\<^sub>w..l} = {}) = (\ k <\<^sub>o\<^sub>w l)" is preorder_class.greaterThanAtMost_empty_iff. end - tts_context tts: (?'a to U) substituting preorder_ow_axioms begin tts_lemma bdd_above_empty: assumes "U \ {}" shows "bdd_above {}" is preorder_class.bdd_above_empty. tts_lemma bdd_below_empty: assumes "U \ {}" shows "bdd_below {}" is preorder_class.bdd_below_empty. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'a set\) rewriting ctr_simps substituting preorder_ow_axioms eliminating through (auto intro: bdd_above_empty bdd_below_empty) begin tts_lemma bdd_belowI2: assumes "A \ U\<^sub>2" and "m \ U" and "\x\U\<^sub>2. f x \ U" and "\x. x \ A \ m \\<^sub>o\<^sub>w f x" shows "bdd_below (f ` A)" given preorder_class.bdd_belowI2 by blast tts_lemma bdd_aboveI2: assumes "A \ U\<^sub>2" and "\x\U\<^sub>2. f x \ U" and "M \ U" and "\x. x \ A \ f x \\<^sub>o\<^sub>w M" shows "bdd_above (f ` A)" given preorder_class.bdd_aboveI2 by blast end end subsection\Partial orders\ subsubsection\Definitions and common properties\ -locale ordering_ow = - fixes U :: "'ao set" - and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) - and ls :: "'ao \ 'ao \ bool" (infix "\<^bold><\<^sub>o\<^sub>w" 50) +locale ordering_ow = partial_preordering_ow U le + for U :: "'ao set" and le :: "'ao \ 'ao \ bool" (infix "\<^bold>\\<^sub>o\<^sub>w" 50) + + fixes ls :: "'ao \ 'ao \ bool" (infix "\<^bold><\<^sub>o\<^sub>w" 50) assumes strict_iff_order: "\ a \ U; b \ U \ \ a \<^bold><\<^sub>o\<^sub>w b \ a \<^bold>\\<^sub>o\<^sub>w b \ a \ b" - and refl: "a \ U \ a \<^bold>\\<^sub>o\<^sub>w a" and antisym: "\ a \ U; b \ U; a \<^bold>\\<^sub>o\<^sub>w b; b \<^bold>\\<^sub>o\<^sub>w a \ \ a = b" - and trans: "\ a \ U; b \ U; c \ U; a \<^bold>\\<^sub>o\<^sub>w b; b \<^bold>\\<^sub>o\<^sub>w c \ \ a \<^bold>\\<^sub>o\<^sub>w c" begin notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) +sublocale preordering_ow U \(\<^bold>\\<^sub>o\<^sub>w)\ \(\<^bold><\<^sub>o\<^sub>w)\ + using local.antisym strict_iff_order by unfold_locales blast + end locale order_ow = preorder_ow U le ls for U :: "'ao set" and le ls + assumes antisym: "\ x \ U; y \ U; x \\<^sub>o\<^sub>w y; y \\<^sub>o\<^sub>w x \ \ x = y" begin sublocale order: ordering_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ + dual_order: ordering_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ apply unfold_locales subgoal by (force simp: less_le_not_le antisym) - subgoal by simp subgoal by (simp add: antisym) - subgoal by (metis order_trans) subgoal by (force simp: less_le_not_le antisym) subgoal by (simp add: antisym) - subgoal by (metis order_trans) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) end locale ord_order_ow = ord\<^sub>1: ord_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale ord_order_ow \ ord_preorder_ow .. locale preorder_order_ow = ord\<^sub>1: preorder_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale preorder_order_ow \ preorder_pair_ow .. locale order_pair_ow = ord\<^sub>1: order_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 sublocale order_pair_ow \ preorder_order_ow .. ud \order.mono\ (\(with _ _ : \mono\ _)\ [1000, 999, 1000] 10) ud mono' \mono\ ud \order.strict_mono\ (\(with _ _ : \strict'_mono\ _)\ [1000, 999, 1000] 10) ud strict_mono' \strict_mono\ ud \order.antimono\ (\(with _ _ : \strict'_mono\ _)\ [1000, 999, 1000] 10) ud antimono' \antimono\ ud \monoseq\ (\(with _ : \monoseq\ _)\ [1000, 1000] 10) ctr relativization synthesis ctr_simps assumes [transfer_domain_rule, transfer_rule]: "Domainp (B::'c\'d\bool) = (\x. x \ U\<^sub>2)" and [transfer_rule]: "right_total B" trp (?'b \A::'a\'b\bool\) and (?'a B) in mono_ow: mono.with_def (\(on _ with _ _ : \mono\ _)\ [1000, 1000, 999, 1000] 10) and strict_mono_ow: strict_mono.with_def (\(on _ with _ _ : \strict'_mono\ _)\ [1000, 1000, 999, 1000] 10) and antimono_ow: antimono.with_def (\(on _ with _ _ : \antimono\ _)\ [1000, 1000, 999, 1000] 10) and monoseq_ow: monoseq.with_def subsubsection\Transfer rules\ context includes lifting_syntax begin lemma ordering_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (ordering_ow (Collect (Domainp A))) ordering" - unfolding ordering_ow_def ordering_def + unfolding ordering_ow_def ordering_ow_axioms_def ordering_def ordering_axioms_def apply transfer_prover_start apply transfer_step+ unfolding Ball_Collect[symmetric] by (intro ext HOL.arg_cong2[where f="(\)"]) auto lemma order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (order_ow (Collect (Domainp A))) class.order" unfolding order_ow_def class.order_def order_ow_axioms_def class.order_axioms_def apply transfer_prover_start apply transfer_step+ by simp end subsubsection\Relativization\ context ordering_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting ordering_ow_axioms eliminating through simp begin -tts_lemma irrefl: - assumes "a \ U" - shows "\ a \<^bold><\<^sub>o\<^sub>w a" - is ordering.irrefl. - -tts_lemma strict_implies_order: - assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" - shows "a \<^bold>\\<^sub>o\<^sub>w b" - is ordering.strict_implies_order. - tts_lemma strict_implies_not_eq: assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" shows "a \ b" is ordering.strict_implies_not_eq. tts_lemma order_iff_strict: assumes "a \ U" and "b \ U" shows "(a \<^bold>\\<^sub>o\<^sub>w b) = (a \<^bold><\<^sub>o\<^sub>w b \ a = b)" is ordering.order_iff_strict. - -tts_lemma asym: - assumes "a \ U" and "b \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w a" - shows False - is ordering.asym. - -tts_lemma strict_trans: - assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" - shows "a \<^bold><\<^sub>o\<^sub>w c" - is ordering.strict_trans. - -tts_lemma strict_trans2: - assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold><\<^sub>o\<^sub>w b" and "b \<^bold>\\<^sub>o\<^sub>w c" - shows "a \<^bold><\<^sub>o\<^sub>w c" - is ordering.strict_trans2. - -tts_lemma strict_trans1: - assumes "a \ U" and "b \ U" and "c \ U" and "a \<^bold>\\<^sub>o\<^sub>w b" and "b \<^bold><\<^sub>o\<^sub>w c" - shows "a \<^bold><\<^sub>o\<^sub>w c" - is ordering.strict_trans1. - + tts_lemma not_eq_order_implies_strict: assumes "a \ U" and "b \ U" and "a \ b" and "a \<^bold>\\<^sub>o\<^sub>w b" shows "a \<^bold><\<^sub>o\<^sub>w b" is ordering.not_eq_order_implies_strict. +tts_lemma eq_iff: + assumes "a \ U" and "b \ U" + shows "(a = b) = (a \<^bold>\\<^sub>o\<^sub>w b \ b \<^bold>\\<^sub>o\<^sub>w a)" + is ordering.eq_iff. + end end context order_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_ow_axioms eliminating through clarsimp begin tts_lemma atLeastAtMost_singleton: assumes "a \ U" shows "{a..\<^sub>o\<^sub>wa} = {a}" is order_class.atLeastAtMost_singleton. tts_lemma less_imp_neq: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "x \ y" is order_class.less_imp_neq. tts_lemma atLeastatMost_empty: assumes "b \ U" and "a \ U" and "b <\<^sub>o\<^sub>w a" shows "{a..\<^sub>o\<^sub>wb} = {}" is order_class.atLeastatMost_empty. tts_lemma less_imp_not_eq: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(x = y) = False" is order_class.less_imp_not_eq. tts_lemma less_imp_not_eq2: assumes "y \ U" and "x <\<^sub>o\<^sub>w y" shows "(y = x) = False" is order_class.less_imp_not_eq2. tts_lemma atLeastLessThan_empty: assumes "b \ U" and "a \ U" and "b \\<^sub>o\<^sub>w a" shows "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a.. U" and "k \ U" and "l \\<^sub>o\<^sub>w k" shows "{k<\<^sub>o\<^sub>w..l} = {}" is order_class.greaterThanAtMost_empty. tts_lemma antisym_conv1: assumes "x \ U" and "y \ U" and "\ x <\<^sub>o\<^sub>w y" shows "(x \\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv1. tts_lemma antisym_conv2: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "(\ x <\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv2. tts_lemma greaterThanLessThan_empty: assumes "l \ U" and "k \ U" and "l \\<^sub>o\<^sub>w k" shows "{k<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wl} = {}" is order_class.greaterThanLessThan_empty. tts_lemma atLeastLessThan_eq_atLeastAtMost_diff: assumes "a \ U" and "b \ U" shows "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {a..o\<^sub>wb} - {b}" is order_class.atLeastLessThan_eq_atLeastAtMost_diff. tts_lemma greaterThanAtMost_eq_atLeastAtMost_diff: assumes "a \ U" and "b \ U" shows "{a<\<^sub>o\<^sub>w..b} = {a..\<^sub>o\<^sub>wb} - {a}" is order_class.greaterThanAtMost_eq_atLeastAtMost_diff. tts_lemma less_separate: assumes "x \ U" and "y \ U" and "x <\<^sub>o\<^sub>w y" shows "\x'\U. \y'\U. x \ {..<\<^sub>o\<^sub>wx'} \ y \ {y'<\<^sub>o\<^sub>w..} \ {..<\<^sub>o\<^sub>wx'} \ {y'<\<^sub>o\<^sub>w..} = {}" is order_class.less_separate. -tts_lemma eq_iff: - assumes "x \ U" and "y \ U" - shows "(x = y) = (x \\<^sub>o\<^sub>w y \ y \\<^sub>o\<^sub>w x)" - is order_class.eq_iff. - tts_lemma order_iff_strict: assumes "a \ U" and "b \ U" shows "(a \\<^sub>o\<^sub>w b) = (a <\<^sub>o\<^sub>w b \ a = b)" is order_class.order.order_iff_strict. tts_lemma le_less: assumes "x \ U" and "y \ U" shows "(x \\<^sub>o\<^sub>w y) = (x <\<^sub>o\<^sub>w y \ x = y)" is order_class.le_less. - -tts_lemma asym: - assumes "a \ U" and "b \ U" and "a <\<^sub>o\<^sub>w b" and "b <\<^sub>o\<^sub>w a" - shows False - is order_class.order.asym. tts_lemma strict_iff_order: assumes "a \ U" and "b \ U" shows "(a <\<^sub>o\<^sub>w b) = (a \\<^sub>o\<^sub>w b \ a \ b)" is order_class.order.strict_iff_order. tts_lemma less_le: assumes "x \ U" and "y \ U" shows "(x <\<^sub>o\<^sub>w y) = (x \\<^sub>o\<^sub>w y \ x \ y)" is order_class.less_le. tts_lemma atLeastAtMost_singleton': assumes "b \ U" and "a = b" shows "{a..\<^sub>o\<^sub>wb} = {a}" is order_class.atLeastAtMost_singleton'. tts_lemma le_imp_less_or_eq: assumes "x \ U" and "y \ U" and "x \\<^sub>o\<^sub>w y" shows "x <\<^sub>o\<^sub>w y \ x = y" is order_class.le_imp_less_or_eq. tts_lemma antisym_conv: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "(x \\<^sub>o\<^sub>w y) = (x = y)" is order_class.antisym_conv. -tts_lemma strict_trans: - assumes "a \ U" and "b \ U" and "c \ U" and "a <\<^sub>o\<^sub>w b" and "b <\<^sub>o\<^sub>w c" - shows "a <\<^sub>o\<^sub>w c" - is order_class.order.strict_trans. - -tts_lemma strict_trans2: - assumes "a \ U" and "b \ U" and "c \ U" and "a <\<^sub>o\<^sub>w b" and "b \\<^sub>o\<^sub>w c" - shows "a <\<^sub>o\<^sub>w c" - is order_class.order.strict_trans2. - -tts_lemma strict_trans1: - assumes "a \ U" and "b \ U" and "c \ U" and "a \\<^sub>o\<^sub>w b" and "b <\<^sub>o\<^sub>w c" - shows "a <\<^sub>o\<^sub>w c" - is order_class.order.strict_trans1. - tts_lemma le_neq_trans: assumes "a \ U" and "b \ U" and "a \\<^sub>o\<^sub>w b" and "a \ b" shows "a <\<^sub>o\<^sub>w b" is order_class.le_neq_trans. tts_lemma neq_le_trans: assumes "a \ U" and "b \ U" and "a \ b" and "a \\<^sub>o\<^sub>w b" shows "a <\<^sub>o\<^sub>w b" is order_class.neq_le_trans. tts_lemma Iio_Int_singleton: assumes "k \ U" and "x \ U" shows "{..<\<^sub>o\<^sub>wk} \ {x} = (if x <\<^sub>o\<^sub>w k then {x} else {})" is order_class.Iio_Int_singleton. tts_lemma atLeastAtMost_singleton_iff: assumes "a \ U" and "b \ U" and "c \ U" shows "({a..\<^sub>o\<^sub>wb} = {c}) = (a = b \ b = c)" is order_class.atLeastAtMost_singleton_iff. tts_lemma Icc_eq_Icc: assumes "l \ U" and "h \ U" and "l' \ U" and "h' \ U" shows "({l..\<^sub>o\<^sub>wh} = {l'..\<^sub>o\<^sub>wh'}) = (h = h' \ l = l' \ \ l' \\<^sub>o\<^sub>w h' \ \ l \\<^sub>o\<^sub>w h)" is order_class.Icc_eq_Icc. tts_lemma lift_Suc_mono_less_iff: assumes "range f \ U" and "\n. f n <\<^sub>o\<^sub>w f (Suc n)" shows "(f n <\<^sub>o\<^sub>w f m) = (n < m)" is order_class.lift_Suc_mono_less_iff. tts_lemma lift_Suc_mono_less: assumes "range f \ U" and "\n. f n <\<^sub>o\<^sub>w f (Suc n)" and "n < n'" shows "f n <\<^sub>o\<^sub>w f n'" is order_class.lift_Suc_mono_less. tts_lemma lift_Suc_mono_le: assumes "range f \ U" and "\n. f n \\<^sub>o\<^sub>w f (Suc n)" and "n \ n'" shows "f n \\<^sub>o\<^sub>w f n'" is order_class.lift_Suc_mono_le. tts_lemma lift_Suc_antimono_le: assumes "range f \ U" and "\n. f (Suc n) \\<^sub>o\<^sub>w f n" and "n \ n'" shows "f n' \\<^sub>o\<^sub>w f n" is order_class.lift_Suc_antimono_le. tts_lemma ivl_disj_int_two: assumes "l \ U" and "m \ U" and "u \ U" shows "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wm} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {m..o\<^sub>w..m} \ {m<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {m..o\<^sub>wm} \ {m<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wm} \ {m..\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..m} \ {m<\<^sub>o\<^sub>w..u} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. {m..\<^sub>o\<^sub>wu} = {}" "{l..\<^sub>o\<^sub>wm} \ {m<\<^sub>o\<^sub>w..u} = {}" is Set_Interval.ivl_disj_int_two. tts_lemma ivl_disj_int_one: assumes "l \ U" and "u \ U" shows "{..\<^sub>o\<^sub>wl} \ {l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} = {}" "{..<\<^sub>o\<^sub>wl} \ (on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l..o\<^sub>wl} \ {l<\<^sub>o\<^sub>w..u} = {}" "{..<\<^sub>o\<^sub>wl} \ {l..\<^sub>o\<^sub>wu} = {}" "{l<\<^sub>o\<^sub>w..u} \ {u<\<^sub>o\<^sub>w..} = {}" "{l<\<^sub>o\<^sub>w..<\<^sub>o\<^sub>wu} \ {u..\<^sub>o\<^sub>w} = {}" "{l..\<^sub>o\<^sub>wu} \ {u<\<^sub>o\<^sub>w..} = {}" "(on U with (\\<^sub>o\<^sub>w) (<\<^sub>o\<^sub>w) : {l.. {u..\<^sub>o\<^sub>w} = {}" is Set_Interval.ivl_disj_int_one. tts_lemma min_absorb2: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "local.min x y = y" is Orderings.min_absorb2. tts_lemma max_absorb1: assumes "y \ U" and "x \ U" and "y \\<^sub>o\<^sub>w x" shows "local.max x y = x" is Orderings.max_absorb1. tts_lemma finite_mono_remains_stable_implies_strict_prefix: assumes "range f \ U" and "finite (range f)" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ f" and "\n. f n = f (Suc n) \ f (Suc n) = f (Suc (Suc n))" shows "\N. (\n\N. f N = f n) \ (\n\N. \m\N. m < n \ f m <\<^sub>o\<^sub>w f n)" is Hilbert_Choice.finite_mono_remains_stable_implies_strict_prefix. tts_lemma incseq_imp_monoseq: assumes "range X \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ X" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.incseq_imp_monoseq. tts_lemma decseq_imp_monoseq: assumes "range X \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ X" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.decseq_imp_monoseq. -tts_lemma irrefl: - assumes "a \ U" - shows "\ a <\<^sub>o\<^sub>w a" - is order_class.order.irrefl. - tts_lemma incseq_Suc_iff: assumes "range f \ U" shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ f) = (\x. f x \\<^sub>o\<^sub>w f (Suc x))" is Topological_Spaces.incseq_Suc_iff. tts_lemma decseq_Suc_iff: assumes "range f \ U" shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f) = (\x. f (Suc x) \\<^sub>o\<^sub>w f x)" is Topological_Spaces.decseq_Suc_iff. tts_lemma incseq_const: assumes "k \ U" shows "on (UNIV::nat set) with (\\<^sub>o\<^sub>w) (\) : \mono\ (\x. k)" is Topological_Spaces.incseq_const. tts_lemma decseq_const: assumes "k \ U" shows "on (UNIV::nat set) with (\\<^sub>o\<^sub>w) (\) : \antimono\ (\x. k)" is Topological_Spaces.decseq_const. tts_lemma atMost_Int_atLeast: assumes "n \ U" shows "{..\<^sub>o\<^sub>wn} \ {n..\<^sub>o\<^sub>w} = {n}" is Set_Interval.atMost_Int_atLeast. tts_lemma monoseq_iff: assumes "range X \ U" shows "(with (\\<^sub>o\<^sub>w) : \monoseq\ X) = ( (on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ X) \ (on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ X) )" is Topological_Spaces.monoseq_iff. tts_lemma monoseq_Suc: assumes "range X \ U" shows "(with (\\<^sub>o\<^sub>w) : \monoseq\ X) = ((\x. X x \\<^sub>o\<^sub>w X (Suc x)) \ (\x. X (Suc x) \\<^sub>o\<^sub>w X x))" is Topological_Spaces.monoseq_Suc. tts_lemma incseq_SucI: assumes "range X \ U" and "\n. X n \\<^sub>o\<^sub>w X (Suc n)" shows "on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ X" is Topological_Spaces.incseq_SucI. tts_lemma incseq_SucD: assumes "range A \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ A" shows "A i \\<^sub>o\<^sub>w A (Suc i)" is Topological_Spaces.incseq_SucD. tts_lemma decseq_SucI: assumes "range X \ U" and "\n. X (Suc n) \\<^sub>o\<^sub>w X n" shows "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ X" is Topological_Spaces.decseq_SucI. tts_lemma decseq_SucD: assumes "range A \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ A" shows "A (Suc i) \\<^sub>o\<^sub>w A i" is Topological_Spaces.decseq_SucD. tts_lemma mono_SucI2: assumes "range X \ U" and "\x. X (Suc x) \\<^sub>o\<^sub>w X x" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.mono_SucI2. tts_lemma mono_SucI1: assumes "range X \ U" and "\x. X x \\<^sub>o\<^sub>w X (Suc x)" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.mono_SucI1. tts_lemma incseqD: assumes "range f \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ f" and "(i::nat) \ j" shows "f i \\<^sub>o\<^sub>w f j" is Topological_Spaces.incseqD. tts_lemma decseqD: assumes "range f \ U" and "on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f" and "(i::nat) \ j" shows "f j \\<^sub>o\<^sub>w f i" is Topological_Spaces.decseqD. tts_lemma monoI2: assumes "range X \ U" and "\x y. x \ y \ X y \\<^sub>o\<^sub>w X x" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.monoI2. tts_lemma monoI1: assumes "range X \ U" and "\x y. x \ y \ X x \\<^sub>o\<^sub>w X y" shows "with (\\<^sub>o\<^sub>w) : \monoseq\ X" is Topological_Spaces.monoI1. tts_lemma antimono_iff_le_Suc: assumes "range f \ U" shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \antimono\ f) = (\x. f (Suc x) \\<^sub>o\<^sub>w f x)" is Nat.antimono_iff_le_Suc. tts_lemma mono_iff_le_Suc: assumes "range f \ U" shows "(on UNIV with (\\<^sub>o\<^sub>w) (\) : \mono\ f) = (\x. f x \\<^sub>o\<^sub>w f (Suc x))" is Nat.mono_iff_le_Suc. tts_lemma funpow_mono2: assumes "\x\U. f x \ U" and "x \ U" and "y \ U" and "on U with (\\<^sub>o\<^sub>w) (\\<^sub>o\<^sub>w) : \mono\ f" and "i \ j" and "x \\<^sub>o\<^sub>w y" and "x \\<^sub>o\<^sub>w f x" shows "(f ^^ i) x \\<^sub>o\<^sub>w (f ^^ j) y" is Nat.funpow_mono2. tts_lemma funpow_mono: assumes "\x\U. f x \ U" and "A \ U" and "B \ U" and "on U with (\\<^sub>o\<^sub>w) (\\<^sub>o\<^sub>w) : \mono\ f" and "A \\<^sub>o\<^sub>w B" shows "(f ^^ n) A \\<^sub>o\<^sub>w (f ^^ n) B" is Nat.funpow_mono. end tts_context tts: (?'a to U) rewriting ctr_simps substituting order_ow_axioms eliminating through clarsimp begin tts_lemma ex_min_if_finite: assumes "S \ U" and "finite S" and "S \ {}" shows "\x\S. \ (\y\S. y <\<^sub>o\<^sub>w x)" is Lattices_Big.ex_min_if_finite. end tts_context tts: (?'a to U) sbterms: (\(\)::['a::order, 'a::order] \ bool\ to \(\\<^sub>o\<^sub>w)\) and (\(<)::['a::order, 'a::order] \ bool\ to \(<\<^sub>o\<^sub>w)\) substituting order_ow_axioms eliminating through clarsimp begin tts_lemma xt1: shows "\a = b; c <\<^sub>o\<^sub>w b\ \ c <\<^sub>o\<^sub>w a" "\b <\<^sub>o\<^sub>w a; b = c\ \ c <\<^sub>o\<^sub>w a" "\a = b; c \\<^sub>o\<^sub>w b\ \ c \\<^sub>o\<^sub>w a" "\b \\<^sub>o\<^sub>w a; b = c\ \ c \\<^sub>o\<^sub>w a" "\y \ U; x \ U; y \\<^sub>o\<^sub>w x; x \\<^sub>o\<^sub>w y\ \ x = y" "\y \ U; x \ U; z \ U; y \\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w y\ \ z \\<^sub>o\<^sub>w x" "\y \ U; x \ U; z \ U; y <\<^sub>o\<^sub>w x; z \\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\y \ U; x \ U; z \ U; y \\<^sub>o\<^sub>w x; z <\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\b \ U; a \ U; b <\<^sub>o\<^sub>w a; a <\<^sub>o\<^sub>w b\ \ P" "\y \ U; x \ U; z \ U; y <\<^sub>o\<^sub>w x; z <\<^sub>o\<^sub>w y\ \ z <\<^sub>o\<^sub>w x" "\b \ U; a \ U; b \\<^sub>o\<^sub>w a; a \ b\ \ b <\<^sub>o\<^sub>w a" "\a \ U; b \ U; a \ b; b \\<^sub>o\<^sub>w a\ \ b <\<^sub>o\<^sub>w a" "\ b \ U; c \ U; a = f b; c <\<^sub>o\<^sub>w b; \x y. \x \ U; y \ U; y <\<^sub>o\<^sub>w x\ \ f y <\<^sub>o\<^sub>w f x \ \ f c <\<^sub>o\<^sub>w a" "\ b \ U; a \ U; b <\<^sub>o\<^sub>w a; f b = c; \x y. \x \ U; y \ U; y <\<^sub>o\<^sub>w x\ \ f y <\<^sub>o\<^sub>w f x \ \ c <\<^sub>o\<^sub>w f a" "\ b \ U; c \ U; a = f b; c \\<^sub>o\<^sub>w b; \x y. \x \ U; y \ U; y \\<^sub>o\<^sub>w x\ \ f y \\<^sub>o\<^sub>w f x \ \ f c \\<^sub>o\<^sub>w a" "\ b \ U; a \ U; b \\<^sub>o\<^sub>w a; f b = c; \x y. \x \ U; y \ U; y \\<^sub>o\<^sub>w x\ \ f y \\<^sub>o\<^sub>w f x \ \ c \\<^sub>o\<^sub>w f a" is Orderings.xt1. end tts_context tts: (?'a to U) and (?'b to \U\<^sub>2::'b set\) rewriting ctr_simps substituting order_ow_axioms eliminating through (simp add: mono_ow_def) begin tts_lemma coinduct3_mono_lemma: assumes "\x\U. f x \ U\<^sub>2" and "X \ U\<^sub>2" and "B \ U\<^sub>2" and "on U with (\) (\\<^sub>o\<^sub>w) : \mono\ f" shows "on U with (\) (\\<^sub>o\<^sub>w) : \mono\ (\x. f x \ (X \ B))" is Inductive.coinduct3_mono_lemma. end end context ord_order_ow begin tts_context tts: (?'a to U\<^sub>2) and (?'b to U\<^sub>1) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(\)::[?'b::ord, ?'b::ord] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'b::ord, ?'b::ord] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) rewriting ctr_simps substituting ord\<^sub>2.order_ow_axioms eliminating through clarsimp begin tts_lemma xt2: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \ U\<^sub>1" and "a \ U\<^sub>2" and "c \ U\<^sub>1" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "f c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" is Orderings.xt2. tts_lemma xt6: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \ U\<^sub>1" and "a \ U\<^sub>2" and "c \ U\<^sub>1" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 a" is Orderings.xt6. end end context order_pair_ow begin tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through ( unfold strict_mono_ow_def mono_ow_def antimono_ow_def bdd_above_ow_def - bdd_below_ow_def, + bdd_below_ow_def + bdd_ow_def, clarsimp ) begin tts_lemma antimonoD: assumes "x \ U\<^sub>1" and "y \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" shows "f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" is Orderings.antimonoD. tts_lemma monoD: assumes "x \ U\<^sub>1" and "y \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" shows "f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" is Orderings.monoD. tts_lemma strict_monoD: assumes "x \ U\<^sub>1" and "y \ U\<^sub>1" and "on U\<^sub>1 with (<\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \strict_mono\ f" and "x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" shows "f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" is Orderings.strict_monoD. tts_lemma strict_monoI: assumes "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "on U\<^sub>1 with (<\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \strict_mono\ f" is Orderings.strict_monoI. tts_lemma antimonoI: assumes "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" is Orderings.antimonoI. tts_lemma monoI: assumes "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" is Orderings.monoI. tts_lemma antimonoE: assumes "x \ U\<^sub>1" and "y \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" and "f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x \ thesis" shows thesis is Orderings.antimonoE. tts_lemma monoE: assumes "x \ U\<^sub>1" and "y \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" and "x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y" and "f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y \ thesis" shows thesis is Orderings.monoE. tts_lemma strict_mono_mono: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "on U\<^sub>1 with (<\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \strict_mono\ f" shows "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" is Orderings.strict_mono_mono. - + tts_lemma bdd_below_image_antimono: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" and "ord\<^sub>1.bdd_above A" shows "ord\<^sub>2.bdd_below (f ` A)" is Conditionally_Complete_Lattices.bdd_below_image_antimono. tts_lemma bdd_above_image_antimono: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \antimono\ f" and "ord\<^sub>1.bdd_below A" shows "ord\<^sub>2.bdd_above (f ` A)" is Conditionally_Complete_Lattices.bdd_above_image_antimono. tts_lemma bdd_below_image_mono: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" and "ord\<^sub>1.bdd_below A" shows "ord\<^sub>2.bdd_below (f ` A)" is Conditionally_Complete_Lattices.bdd_below_image_mono. tts_lemma bdd_above_image_mono: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "A \ U\<^sub>1" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" and "ord\<^sub>1.bdd_above A" shows "ord\<^sub>2.bdd_above (f ` A)" is Conditionally_Complete_Lattices.bdd_above_image_mono. tts_lemma strict_mono_leD: assumes "\x\U\<^sub>1. r x \ U\<^sub>2" and "m \ U\<^sub>1" and "n \ U\<^sub>1" and "on U\<^sub>1 with (<\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \strict_mono\ r" and "m \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 n" shows "r m \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 r n" is Topological_Spaces.strict_mono_leD. tts_lemma mono_image_least: assumes "\x\U\<^sub>1. f x \ U\<^sub>2" and "m \ U\<^sub>1" and "n \ U\<^sub>1" and "m' \ U\<^sub>2" and "n' \ U\<^sub>2" and "on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : \mono\ f" and "f ` (on U\<^sub>1 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>1) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>1) : {m..2 with (\\<^sub>o\<^sub>w\<^sub>.\<^sub>2) (<\<^sub>o\<^sub>w\<^sub>.\<^sub>2) : {m'..o\<^sub>w\<^sub>.\<^sub>1 n" shows "f m = m'" is Set_Interval.mono_image_least. end tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'b::order, ?'b::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'b::order, ?'b::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through clarsimp begin tts_lemma xt3: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt3. tts_lemma xt4: assumes "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 b" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" is Orderings.xt4. tts_lemma xt5: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt5. tts_lemma xt7: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt7. tts_lemma xt8: assumes "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 b" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f x" shows "f c <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" is Orderings.xt8. tts_lemma xt9: assumes "b \ U\<^sub>1" and "a \ U\<^sub>1" and "c \ U\<^sub>2" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 a" and "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f b" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; y <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 x\ \ f y <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f x" shows "c <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f a" is Orderings.xt9. end tts_context tts: (?'a to U\<^sub>1) and (?'b to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'b::order, ?'b::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'b::order, ?'b::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through simp begin tts_lemma order_less_subst1: assumes "a \ U\<^sub>1" and "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f b" and "b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f y" shows "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f c" is Orderings.order_less_subst1. tts_lemma order_subst1: assumes "a \ U\<^sub>1" and "\x\U\<^sub>2. f x \ U\<^sub>1" and "b \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f b" and "b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>2; y \ U\<^sub>2; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f y" shows "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 f c" is Orderings.order_subst1. end tts_context tts: (?'a to U\<^sub>1) and (?'c to U\<^sub>2) sbterms: (\(\)::[?'a::order, ?'a::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(<)::[?'a::order, ?'a::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>1)\) and (\(\)::[?'c::order, ?'c::order] \ bool\ to \(\\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) and (\(<)::[?'c::order, ?'c::order] \ bool\ to \(<\<^sub>o\<^sub>w\<^sub>.\<^sub>2)\) rewriting ctr_simps substituting ord\<^sub>1.order_ow_axioms and ord\<^sub>2.order_ow_axioms eliminating through simp begin tts_lemma order_less_le_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_less_le_subst2. tts_lemma order_le_less_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_le_less_subst2. tts_lemma order_less_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x <\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a <\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_less_subst2. tts_lemma order_subst2: assumes "a \ U\<^sub>1" and "b \ U\<^sub>1" and "\x\U\<^sub>1. f x \ U\<^sub>2" and "c \ U\<^sub>2" and "a \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 b" and "f b \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" and "\x y. \x \ U\<^sub>1; y \ U\<^sub>1; x \\<^sub>o\<^sub>w\<^sub>.\<^sub>1 y\ \ f x \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 f y" shows "f a \\<^sub>o\<^sub>w\<^sub>.\<^sub>2 c" is Orderings.order_subst2. end end subsection\Dense orders\ subsubsection\Definitions and common properties\ locale dense_order_ow = order_ow U le ls for U :: "'ao set" and le ls + assumes dense: "\ x \ U; y \ U; x <\<^sub>o\<^sub>w y \ \ (\z\U. x <\<^sub>o\<^sub>w z \ z <\<^sub>o\<^sub>w y)" subsubsection\Transfer rules\ context includes lifting_syntax begin lemma dense_order_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (dense_order_ow (Collect (Domainp A))) class.dense_order" unfolding dense_order_ow_def class.dense_order_def dense_order_ow_axioms_def class.dense_order_axioms_def apply transfer_prover_start apply transfer_step+ by simp end subsection\ Partial orders with the greatest element and partial orders with the least elements \ subsubsection\Definitions and common properties\ locale ordering_top_ow = ordering_ow U le ls for U :: "'ao set" and le ls + fixes top :: "'ao" ("\<^bold>\\<^sub>o\<^sub>w") assumes top_closed[simp]: "\<^bold>\\<^sub>o\<^sub>w \ U" assumes extremum[simp]: "a \ U \ a \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" begin notation top ("\<^bold>\\<^sub>o\<^sub>w") end locale bot_ow = fixes U :: "'ao set" and bot (\\\<^sub>o\<^sub>w\) assumes bot_closed[simp]: "\\<^sub>o\<^sub>w \ U" begin notation bot (\\\<^sub>o\<^sub>w\) end locale bot_pair_ow = ord\<^sub>1: bot_ow U\<^sub>1 bot\<^sub>1 + ord\<^sub>2: bot_ow U\<^sub>2 bot\<^sub>2 for U\<^sub>1 :: "'ao set" and bot\<^sub>1 and U\<^sub>2 :: "'bo set" and bot\<^sub>2 begin notation bot\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation bot\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale order_bot_ow = order_ow U le ls + bot_ow U bot for U :: "'ao set" and bot le ls + assumes bot_least: "a \ U \ \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a" begin sublocale bot: ordering_top_ow U \(\\<^sub>o\<^sub>w)\ \(>\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ apply unfold_locales subgoal by simp subgoal by (simp add: bot_least) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) and top ("\<^bold>\\<^sub>o\<^sub>w") end locale order_bot_pair_ow = ord\<^sub>1: order_bot_ow U\<^sub>1 bot\<^sub>1 le\<^sub>1 ls\<^sub>1 + ord\<^sub>2: order_bot_ow U\<^sub>2 bot\<^sub>2 le\<^sub>2 ls\<^sub>2 for U\<^sub>1 :: "'ao set" and bot\<^sub>1 le\<^sub>1 ls\<^sub>1 and U\<^sub>2 :: "'bo set" and bot\<^sub>2 le\<^sub>2 ls\<^sub>2 begin sublocale bot_pair_ow .. sublocale order_pair_ow .. end locale top_ow = fixes U :: "'ao set" and top (\\\<^sub>o\<^sub>w\) assumes top_closed[simp]: "\\<^sub>o\<^sub>w \ U" begin notation top (\\\<^sub>o\<^sub>w\) end locale top_pair_ow = ord\<^sub>1: top_ow U\<^sub>1 top\<^sub>1 + ord\<^sub>2: top_ow U\<^sub>2 top\<^sub>2 for U\<^sub>1 :: "'ao set" and top\<^sub>1 and U\<^sub>2 :: "'bo set" and top\<^sub>2 begin notation top\<^sub>1 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>1\) notation top\<^sub>2 (\\\<^sub>o\<^sub>w\<^sub>.\<^sub>2\) end locale order_top_ow = order_ow U le ls + top_ow U top for U :: "'ao set" and le ls top + assumes top_greatest: "a \ U \ a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" begin sublocale top: ordering_top_ow U \(\\<^sub>o\<^sub>w)\ \(<\<^sub>o\<^sub>w)\ \\\<^sub>o\<^sub>w\ apply unfold_locales subgoal by simp subgoal by (simp add: top_greatest) done no_notation le (infix "\<^bold>\\<^sub>o\<^sub>w" 50) and ls (infix "\<^bold><\<^sub>o\<^sub>w" 50) and top ("\<^bold>\\<^sub>o\<^sub>w") end locale order_top_pair_ow = ord\<^sub>1: order_top_ow U\<^sub>1 le\<^sub>1 ls\<^sub>1 top\<^sub>1 + ord\<^sub>2: order_top_ow U\<^sub>2 le\<^sub>2 ls\<^sub>2 top\<^sub>2 for U\<^sub>1 :: "'ao set" and le\<^sub>1 ls\<^sub>1 top\<^sub>1 and U\<^sub>2 :: "'bo set" and le\<^sub>2 ls\<^sub>2 top\<^sub>2 begin sublocale top_pair_ow .. sublocale order_pair_ow .. end subsubsection\Transfer rules\ context includes lifting_syntax begin lemma ordering_top_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (ordering_top_ow (Collect (Domainp A))) ordering_top" proof- let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))" let ?ordering_top_ow = "ordering_top_ow (Collect (Domainp A))" have "?P ?ordering_top_ow (\le ls ext. ext \ UNIV \ ordering_top le ls ext)" unfolding ordering_top_ow_def ordering_top_def ordering_top_ow_axioms_def ordering_top_axioms_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed lemma order_bot_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) (order_bot_ow (Collect (Domainp A))) class.order_bot" proof- let ?P = "(A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))" let ?order_bot_ow = "order_bot_ow (Collect (Domainp A))" have "?P ?order_bot_ow (\bot le ls. bot \ UNIV \ class.order_bot bot le ls)" unfolding class.order_bot_def order_bot_ow_def class.order_bot_axioms_def order_bot_ow_axioms_def bot_ow_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed lemma order_top_transfer[transfer_rule]: assumes [transfer_rule]: "bi_unique A" "right_total A" shows "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=)) (order_top_ow (Collect (Domainp A))) class.order_top" proof- let ?P = "((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> A ===> (=))" let ?order_top_ow = "order_top_ow (Collect (Domainp A))" have "?P ?order_top_ow (\le ls top. top \ UNIV \ class.order_top le ls top)" unfolding class.order_top_def order_top_ow_def class.order_top_axioms_def order_top_ow_axioms_def top_ow_def apply transfer_prover_start apply transfer_step+ by blast thus ?thesis by simp qed end subsubsection\Relativization\ context ordering_top_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting ordering_top_ow_axioms eliminating through simp applying [OF top_closed] begin tts_lemma extremum_uniqueI: assumes "\<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" shows "\<^bold>\\<^sub>o\<^sub>w = \<^bold>\\<^sub>o\<^sub>w" is ordering_top.extremum_uniqueI. tts_lemma extremum_unique: shows "(\<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w) = (\<^bold>\\<^sub>o\<^sub>w = \<^bold>\\<^sub>o\<^sub>w)" is ordering_top.extremum_unique. tts_lemma extremum_strict: shows "\ \<^bold>\\<^sub>o\<^sub>w \<^bold><\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w" is ordering_top.extremum_strict. tts_lemma not_eq_extremum: shows "(\<^bold>\\<^sub>o\<^sub>w \ \<^bold>\\<^sub>o\<^sub>w) = (\<^bold>\\<^sub>o\<^sub>w \<^bold><\<^sub>o\<^sub>w \<^bold>\\<^sub>o\<^sub>w)" is ordering_top.not_eq_extremum. end end context order_bot_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_bot_ow_axioms eliminating through simp begin tts_lemma bdd_above_bot: assumes "A \ U" shows "bdd_below A" - is order_bot_class.bdd_above_bot. + is order_bot_class.bdd_below_bot. tts_lemma not_less_bot: assumes "a \ U" shows "\ a <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" is order_bot_class.not_less_bot. tts_lemma max_bot: assumes "x \ U" shows "max \\<^sub>o\<^sub>w x = x" is order_bot_class.max_bot. tts_lemma max_bot2: assumes "x \ U" shows "max x \\<^sub>o\<^sub>w = x" is order_bot_class.max_bot2. tts_lemma min_bot: assumes "x \ U" shows "min \\<^sub>o\<^sub>w x = \\<^sub>o\<^sub>w" is order_bot_class.min_bot. tts_lemma min_bot2: assumes "x \ U" shows "min x \\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w" is order_bot_class.min_bot2. tts_lemma bot_unique: assumes "a \ U" shows "(a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w) = (a = \\<^sub>o\<^sub>w)" is order_bot_class.bot_unique. tts_lemma bot_less: assumes "a \ U" shows "(a \ \\<^sub>o\<^sub>w) = (\\<^sub>o\<^sub>w <\<^sub>o\<^sub>w a)" is order_bot_class.bot_less. tts_lemma atLeast_eq_UNIV_iff: assumes "x \ U" shows "({x..\<^sub>o\<^sub>w} = U) = (x = \\<^sub>o\<^sub>w)" is order_bot_class.atLeast_eq_UNIV_iff. tts_lemma le_bot: assumes "a \ U" and "a \\<^sub>o\<^sub>w \\<^sub>o\<^sub>w" shows "a = \\<^sub>o\<^sub>w" is order_bot_class.le_bot. end end context order_top_ow begin tts_context tts: (?'a to U) rewriting ctr_simps substituting order_top_ow_axioms eliminating through simp begin tts_lemma bdd_above_top: assumes "A \ U" shows "bdd_above A" is order_top_class.bdd_above_top. tts_lemma not_top_less: assumes "a \ U" shows "\ \\<^sub>o\<^sub>w <\<^sub>o\<^sub>w a" is order_top_class.not_top_less. tts_lemma max_top: assumes "x \ U" shows "max \\<^sub>o\<^sub>w x = \\<^sub>o\<^sub>w" is order_top_class.max_top. tts_lemma max_top2: assumes "x \ U" shows "max x \\<^sub>o\<^sub>w = \\<^sub>o\<^sub>w" is order_top_class.max_top2. tts_lemma min_top: assumes "x \ U" shows "min \\<^sub>o\<^sub>w x = x" is order_top_class.min_top. tts_lemma min_top2: assumes "x \ U" shows "min x \\<^sub>o\<^sub>w = x" is order_top_class.min_top2. tts_lemma top_unique: assumes "a \ U" shows "(\\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a) = (a = \\<^sub>o\<^sub>w)" is order_top_class.top_unique. tts_lemma less_top: assumes "a \ U" shows "(a \ \\<^sub>o\<^sub>w) = (a <\<^sub>o\<^sub>w \\<^sub>o\<^sub>w)" is order_top_class.less_top. tts_lemma atMost_eq_UNIV_iff: assumes "x \ U" shows "({..\<^sub>o\<^sub>wx} = U) = (x = \\<^sub>o\<^sub>w)" is order_top_class.atMost_eq_UNIV_iff. tts_lemma top_le: assumes "a \ U" and "\\<^sub>o\<^sub>w \\<^sub>o\<^sub>w a" shows "a = \\<^sub>o\<^sub>w" is order_top_class.top_le. end end text\\newpage\ end \ No newline at end of file diff --git a/thys/Types_To_Sets_Extension/ROOT b/thys/Types_To_Sets_Extension/ROOT --- a/thys/Types_To_Sets_Extension/ROOT +++ b/thys/Types_To_Sets_Extension/ROOT @@ -1,44 +1,44 @@ chapter AFP session Types_To_Sets_Extension (AFP) = Conditional_Transfer_Rule + - options [timeout = 600] + options [timeout = 1200] sessions "HOL-Types_To_Sets" "HOL-Eisbach" "HOL-Analysis" directories "ETTS" "ETTS/ETTS_Tools" "ETTS/Manual" "ETTS/Tests" "Examples" "Examples/TTS_Foundations" "Examples/TTS_Foundations/Algebra" "Examples/TTS_Foundations/Foundations" "Examples/TTS_Foundations/Orders" "Examples/SML_Relativization" "Examples/SML_Relativization/Algebra" "Examples/SML_Relativization/Foundations" "Examples/SML_Relativization/Lattices" "Examples/SML_Relativization/Simple_Orders" "Examples/SML_Relativization/Topology" "Examples/Vector_Spaces" theories [document = false] "ETTS/ETTS_Tools/ETTS_Tools" "ETTS/ETTS" "ETTS/ETTS_Auxiliary" "ETTS/Manual/Manual_Prerequisites" "ETTS/Tests/ETTS_Tests" theories "ETTS/Manual/ETTS_CR" "Examples/Introduction" "Examples/SML_Relativization/SML_Conclusions" "Examples/Vector_Spaces/VS_Conclusions" "Examples/TTS_Foundations/FNDS_Conclusions" document_files "iman.sty" "extra.sty" "isar.sty" "style.sty" "root.tex" "root.bib" \ No newline at end of file