Theory Sorted_Sets

theory Sorted_Sets
  imports 
    Main 
    "HOL-Library.FuncSet" 
    "HOL-Library.Monad_Syntax"
    Complete_Non_Orders.Binary_Relations
begin

section ‹Auxiliary Lemmas›

(* corr. all_set_conv_all_nth *)
lemma ex_set_conv_ex_nth:
  "(∃x ∈ set xs. P x) = (∃i. i < length xs ∧ P (xs ! i))"
  by (auto simp add: set_conv_nth)

lemma Ball_Pair_conv: "(∀(x,y)∈R. P x y) ⟷ (∀x y. (x,y) ∈ R ⟶ P x y)" by auto

lemma Some_eq_bind_conv: "(Some x = f ⤜ g) = (∃y. f = Some y ∧ g y = Some x)"
  by (fold bind_eq_Some_conv, auto)

lemma length_le_nth_append: "length xs ≤ n ⟹ (xs@ys)!n = ys!(n-length xs)"
  by (simp add: nth_append)

lemma list_all2_same_left:
 "∀a' ∈ set as. a' = a ⟹ list_all2 r as bs ⟷ length as = length bs ∧ (∀b ∈ set bs. r a b)"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_same_leftI:
 "∀a' ∈ set as. a' = a ⟹ length as = length bs ⟹ ∀b ∈ set bs. r a b ⟹ list_all2 r as bs"
  by (auto simp: list_all2_same_left)

lemma list_all2_same_right:
 "∀b' ∈ set bs. b' = b ⟹ list_all2 r as bs ⟷ length as = length bs ∧ (∀a ∈ set as. r a b)"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_same_rightI:
 "∀b' ∈ set bs. b' = b ⟹ length as = length bs ⟹ ∀a ∈ set as. r a b ⟹ list_all2 r as bs"
  by (auto simp: list_all2_same_right)

lemma list_all2_all_all:
 "∀a ∈ set as. ∀b ∈ set bs. r a b ⟹ list_all2 r as bs ⟷ length as = length bs"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_indep1:
  "list_all2 (λa b. P b) as bs ⟷ length as = length bs ∧ (∀b ∈ set bs. P b)"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_indep2:
  "list_all2 (λa b. P a) as bs ⟷ length as = length bs ∧ (∀a ∈ set as. P a)"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_replicate[simp]:
  "list_all2 r (replicate n x) ys ⟷ length ys = n ∧ (∀y ∈ set ys. r x y)"
  "list_all2 r xs (replicate n y) ⟷ length xs = n ∧ (∀x ∈ set xs. r x y)"
  by (auto simp: list_all2_conv_all_nth all_set_conv_all_nth)

lemma list_all2_choice_nth: assumes "∀i < length xs. ∃y. r (xs!i) y" shows "∃ys. list_all2 r xs ys"
proof-
  from assms have "∀i ∈ {0..<length xs}. ∃y. r (xs!i) y" by auto
  from finite_set_choice[OF _ this]
  obtain f where "∀i < length xs. r (xs ! i) (f i)" by (auto simp: Ball_def)
  then have "list_all2 r xs (map f [0..<length xs])" by (auto simp: list_all2_conv_all_nth)
  then show ?thesis by auto
qed

lemma list_all2_choice: "∀x ∈ set xs. ∃y. r x y ⟹ ∃ys. list_all2 r xs ys"
  using list_all2_choice_nth by (auto simp: all_set_conv_all_nth)

lemma list_all2_concat:
  "list_all2 (list_all2 r) ass bss ⟹ list_all2 r (concat ass) (concat bss)"
  by (induct rule:list_all2_induct, auto intro!: list_all2_appendI)

lemma those_eq_None[simp]: "those as = None ⟷ None ∈ set as" by (induct as, auto split:option.split)

lemma those_eq_Some[simp]: "those xos = Some xs ⟷ xos = map Some xs"
  by (induct xos arbitrary:xs, auto split:option.split_asm)

lemma those_map_Some[simp]: "those (map Some xs) = Some xs" by simp

lemma those_append:
  "those (as @ bs) = do {xs ← those as; ys ← those bs; Some (xs@ys)}"
  by (auto split: bind_split)

lemma those_Cons:
  "those (a#as) = do {x ← a; xs ← those as; Some (x # xs)}"
  by (auto split: option.split bind_split)

lemma map_singleton_o[simp]: "(λx. [x]) ∘ f = (λx. [f x])" by auto

lemmas list_3_cases = remdups_adj.cases

lemma in_set_updateD: "x ∈ set (xs[n := y]) ⟹ x ∈ set xs ∨ x = y"
  by (auto dest: subsetD[OF set_update_subset_insert])

lemma map_nth': "length xs = n ⟹ map (nth xs) [0..<n] = xs"
  using map_nth by auto

lemma product_lists_map_map: "product_lists (map (map f) xss) = map (map f) (product_lists xss)"
  by (induct xss, auto simp: Cons o_def map_concat)

lemma (in monoid_add) sum_list_concat: "sum_list (concat xs) = sum_list (map sum_list xs)" 
  by (induct xs, auto)

context semiring_1 begin

lemma prod_list_map_sum_list_distrib:
  shows "prod_list (map sum_list xss) = sum_list (map prod_list (product_lists xss))"
  by (induct xss, simp_all add: map_concat o_def sum_list_concat sum_list_const_mult sum_list_mult_const)

lemma prod_list_sum_list_distrib:
  "(∏xs ← xss. ∑x ← xs. f x) = (∑xs ← product_lists xss. ∏x←xs. f x)"
  using prod_list_map_sum_list_distrib[of "map (map f) xss"]
  by (simp add: o_def product_lists_map_map)

end

lemma ball_set_bex_set_distrib:
  "(∀xs∈set xss. ∃x∈set xs. f x) ⟷ (∃xs∈set (product_lists xss). ∀x∈set xs. f x)"
  by (induct xss, auto)

lemma bex_set_ball_set_distrib:
  "(∃xs∈set xss. ∀x∈set xs. f x) ⟷ (∀xs∈set (product_lists xss). ∃x∈set xs. f x)"
  by (induct xss, auto)

declare upt_Suc[simp del]

lemma map_nth_Cons: "map (nth (x#xs)) [0..<n] = (case n of 0 ⇒ [] | Suc n ⇒ x # map (nth xs) [0..<n])"
  by (auto simp:map_upt_Suc split: nat.split)

lemma upt_0_Suc_Cons: "[0..<Suc i] = 0 # map Suc [0..<i]"
  using map_upt_Suc[of id] by simp

lemma upt_map_add: "i ≤ j ⟹ [i..<j] = map (λk. k + i) [0..<j-i]"
  by (simp add: map_add_upt)

lemma map_nth_append:
  "map (nth (xs @ ys)) [0..<n] =
  (if n < length xs then map (nth xs) [0..<n] else xs @ map (nth ys) [0..<n-length xs])"
  by (induct xs arbitrary: n, auto simp: map_nth_Cons split: nat.split)

lemma all_dom: "(∀x ∈ dom f. P x) ⟷ (∀x y. f x = Some y ⟶ P x)" by auto

lemma trancl_Collect: "{(x,y). r x y}⇧+ = {(x,y). tranclp r x y}"
  by (simp add: tranclp_unfold)

lemma restrict_submap[intro!]: "A |` S ⊆⇩m A"
  by (auto simp: restrict_map_def map_le_def domIff)

lemma restrict_map_mono_left: "A ⊆⇩m A' ⟹ A |` S ⊆⇩m A' |` S"
  and restrict_map_mono_right: "S ⊆ S' ⟹ A |` S ⊆⇩m A |` S'"
  by (auto simp: map_le_def)


section ‹Sorted Sets and Maps›

declare domIff[iff del]

text ‹We view sorted sets just as partial maps from elements to their sorts.
We just introduce the following notation:›

definition hastype (‹((_) :/ (_) in/ (_))› [50,61,51]50)
  where "a : σ in A ≡ A a = Some σ"

abbreviation "all_hastype σ A P ≡ ∀a. a : σ in A ⟶ P a"
abbreviation "ex_hastype σ A P ≡ ∃a. a : σ in A ∧ P a"

syntax
  all_hastype :: "'pttrn ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹∀_ :/ _ in/ _./ _› [50,51,51,10]10)
  ex_hastype :: "'pttrn ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹∃_ :/ _ in/ _./ _› [50,51,51,10]10)

syntax_consts
  all_hastype ⇌ all_hastype and
  ex_hastype ⇌ ex_hastype

translations
  "∀a : σ in A. e" ⇌ "CONST all_hastype σ A (λa. e)"
  "∃a : σ in A. e" ⇌ "CONST ex_hastype σ A (λa. e)"

lemmas hastypeI = hastype_def[unfolded atomize_eq, THEN iffD2]
lemmas hastypeD[dest] = hastype_def[unfolded atomize_eq, THEN iffD1]
lemmas eq_Some_iff_hastype = hastype_def[symmetric]

lemma has_same_type: assumes "a : σ in A" shows "a : σ' in A ⟷ σ' = σ"
  using assms by (unfold hastype_def, auto)

lemma sset_eqI: assumes "(⋀a σ. a : σ in A ⟷ a : σ in B)" shows "A = B"
proof (intro ext)
  fix a show "A a = B a" using assms apply (cases "A a", auto simp: hastype_def)
    by (metis option.exhaust)
qed

lemma in_dom_iff_ex_type: "a ∈ dom A ⟷ (∃σ. a : σ in A)" by (auto simp: hastype_def domIff)

lemma in_dom_hastypeE: "a ∈ dom A ⟹ (⋀σ. a : σ in A ⟹ thesis) ⟹ thesis"
  by (auto simp: hastype_def domIff)

lemma hastype_imp_dom[simp]: "a : σ in A ⟹ a ∈ dom A" by (auto simp: domIff)

lemma untyped_imp_not_hastype: "A a = None ⟹ ¬ a : σ in A" by auto

lemma nex_hastype_iff: "(∄σ. a : σ in A) ⟷ A a = None" by (auto simp: hastype_def)

lemma all_dom_iff_all_hastype: "(∀x ∈ dom A. P x) ⟷ (∀x σ. x : σ in A ⟶ P x)"
  by (simp add: all_dom hastype_def)

text ‹Explicitly sorted sets:›

abbreviation "sort_annotated ≡ Some ∘ snd"

lemma hastype_in_Some[simp]: "a : σ in (λx. Some (f x)) ⟷ σ = f a"
  by (auto simp: hastype_def)

text ‹Listwise type judgement:›

abbreviation hastype_list (‹((_) :⇩l/ (_) in/ (_))› [50,61,51]50)
  where "as :⇩l σs in A ≡ list_all2 (λa σ. a : σ in A) as σs" 

lemma has_same_type_list:
  "as :⇩l σs in A ⟹ as :⇩l σs' in A ⟷ σs' = σs"
proof (induct as arbitrary: σs σs')
  case Nil
  then show ?case by auto
next
  case (Cons a as)
  then show ?case by (auto simp: has_same_type list_all2_Cons1)
qed

lemma hastype_list_iff_those: "as :⇩l σs in A ⟷ those (map A as) = Some σs"
proof (induct as arbitrary:σs)
  case Nil
  then show ?case by auto
next
  case IH: (Cons a as σσs)
  show ?case
  proof (cases σσs)
    case [simp]: Nil
    show ?thesis by (auto split:option.split)
  next
    case [simp]: (Cons σ σs)
    from IH show ?thesis by (auto intro!:hastypeI split: option.split)
  qed
qed

lemmas hastype_list_imp_those[simp] = hastype_list_iff_those[THEN iffD1]

lemma hastype_list_imp_lists_dom: "xs :⇩l σs in A ⟹ xs ∈ lists (dom A)"
  by (auto simp: list_all2_conv_all_nth in_set_conv_nth hastype_def)

lemma subsset: "A ⊆⇩m A' ⟷ (∀a σ. a : σ in A ⟶ a : σ in A')"
  by(auto simp: Ball_def map_le_def hastype_def domIff)

lemmas subssetI = subsset[THEN iffD2, rule_format]
lemmas subssetD = subsset[THEN iffD1, rule_format]

lemma subsset_hastype_listD: "A ⊆⇩m A' ⟹ as :⇩l σs in A ⟹ as :⇩l σs in A'"
  by (auto simp: list_all2_conv_all_nth subssetD)

lemma has_same_type_in_subsset:
  "a : σ in A' ⟹ A ⊆⇩m A' ⟹ a : σ' in A ⟹ σ' = σ"
  by (auto dest!: subssetD simp: has_same_type)

lemma has_same_type_in_dom_subsset:
  "a : σ in A' ⟹ A ⊆⇩m A' ⟹ a ∈ dom A ⟷ a : σ in A"
  by (auto simp: in_dom_iff_ex_type dest: has_same_type_in_subsset)

text ‹Restriction of partial map, also depending on the value.›

definition "restrict_sset A P a ≡
  do { σ ← A a; if P a σ then Some σ else None }"

syntax restrict_sset :: "'pttrn ⇒ 'pttrn ⇒ 'a ⇒ 'a ⇒ 'a"
  (‹{_ : _ in _./ _}› [50,51,50,0]1000)

translations "{a : σ in A. P}" ⇌ "CONST restrict_sset A (λa σ. P)"

lemma hastype_in_restrict_sset[simp]:
  "a : σ in {a : σ in A. P a σ} ⟷ a : σ in A ∧ P a σ"
  by (auto simp: restrict_sset_def hastype_def bind_eq_Some_conv)

lemma restrict_sset_cong:
  assumes "A = A'"
    and "⋀a σ. a : σ in A ⟹ P a σ ⟷ P' a σ"
  shows "{a : σ in A. P a σ} = {a : σ in A'. P' a σ}"
  by (auto intro!: sset_eqI simp: assms)

lemma restrict_sset_True[simp]: "{a : σ in A. True} = A"
  by (auto intro!: sset_eqI)

lemma dom_restrict_sset: "dom {a : σ in A. P a σ} = {a. ∃σ. a : σ in A ∧ P a σ}"
  by (auto elim!: in_dom_hastypeE)

lemma hastype_restrict: "a : σ in A |` S ⟷ a ∈ S ∧ a : σ in A"
  by (auto simp: restrict_map_def hastype_def)

lemma restrict_map_eq_restrict_sset: "A |` S = {x : σ in A. x ∈ S}"
  by (auto intro!: sset_eqI simp: hastype_restrict)

lemma hastype_the_simp[simp]: "a : σ in A ⟹ the (A a) = σ"
  by (auto)

lemma hastype_in_upd[simp]: "x : σ in A(y ↦ τ) ⟷ (if x = y then σ = τ else x : σ in A)"
  by (auto simp: hastype_def)

lemma all_set_hastype_iff_those: "∀a ∈ set as. a : σ in A ⟹
  those (map A as) = Some (replicate (length as) σ)"
  by (induct as, auto)

text ‹The partial version of list nth:›
primrec safe_nth where
    "safe_nth [] _ = None"
  | "safe_nth (a#as) n = (case n of 0 ⇒ Some a | Suc n ⇒ safe_nth as n)"

lemma safe_nth_simp[simp]: "i < length as ⟹ safe_nth as i = Some (as ! i)"
  by (induct as arbitrary:i, auto split:nat.split)

lemma safe_nth_None[simp]:
  "length as ≤ i ⟹ safe_nth as i = None"
  by (induct as arbitrary:i, auto split:nat.split)

lemma safe_nth: "safe_nth as i = (if i < length as then Some (as ! i) else None)"
  by auto

lemma safe_nth_eq_SomeE:
 "safe_nth as i = Some a ⟹ (i < length as ⟹ as ! i = a ⟹ thesis) ⟹ thesis"
  by (cases "i < length as", auto)

lemma dom_safe_nth[simp]: "dom (safe_nth as) = {0..<length as}"
  by (auto simp: domIff elim!: safe_nth_eq_SomeE)

lemma safe_nth_replicate[simp]:
  "safe_nth (replicate n a) i = (if i < n then Some a else None)"
  by auto

lemma safe_nth_append:
  "safe_nth (ls@rs) i = (if i < length ls then Some (ls!i) else safe_nth rs (i - length ls))"
  by (cases "i < length (ls@rs)", auto simp: nth_append)

lemma hastype_in_safe_nth[simp]: "i : σ in safe_nth σs ⟷ i < length σs ∧ σ = σs!i"
  by (auto simp: hastype_def safe_nth)

lemmas hastype_in_safe_nthE = safe_nth_eq_SomeE[folded hastype_def]

lemma hastype_in_o[simp]: "a : σ in A ∘ f ⟷ f a : σ in A" by (simp add: hastype_def)

definition o_sset (infix ‹∘s› 55) where
  "f ∘s A ≡ map_option f ∘ A"

lemma hastype_in_o_sset: "a : σ' in f ∘s A ⟷ (∃σ. a : σ in A ∧ σ' = f σ)"
  by (auto simp: o_sset_def hastype_def)

lemma hastype_in_o_ssetI: "a : σ in A ⟹ f σ = σ' ⟹ a : σ' in f ∘s A"
  by (auto simp: o_sset_def hastype_def)

lemma hastype_in_o_ssetD: "a : τ in f ∘s A ⟹ ∃σ. a : σ in A ∧ τ = f σ"
  by (auto simp: o_sset_def hastype_def)

lemma hastype_in_o_ssetE: "a : τ in f ∘s A ⟹ (⋀σ. a : σ in A ⟹ τ = f σ ⟹ thesis) ⟹ thesis"
  by (auto simp: o_sset_def hastype_def)

lemma o_sset_restrict_sset_assoc[simp]: "f ∘s (A |` X) = (f ∘s A) |` X"
  by (auto simp: o_sset_def restrict_map_def)

lemma id_o_sset[simp]: "id ∘s A = A"
  and identity_o_sset[simp]: "(λx. x) ∘s A = A"
  by (auto simp: o_sset_def map_option.id map_option.identity)

lemma o_ssetI: "A x = Some y ⟹ z = f y ⟹ (f ∘s A) x = Some z" by (auto simp: o_sset_def)

lemma o_ssetE: "(f ∘s A) x = Some z ⟹ (⋀y. A x = Some y ⟹ z = f y ⟹ thesis) ⟹ thesis"
  by (auto simp: o_sset_def)

lemma dom_o_sset[simp]: "dom (f ∘s A) = dom A"
  by (auto intro!: o_ssetI elim!: o_ssetE simp: domIff)

lemma safe_nth_map: "safe_nth (map f as) = f ∘s safe_nth as"
  by (auto simp: safe_nth o_sset_def)

notation Map.empty (‹∅›)
lemma safe_nth_Nil[simp]: "safe_nth [] = ∅" by auto

lemma o_sset_empty[simp]: "f ∘s ∅ = ∅" by (auto simp: o_sset_def)

lemma hastype_in_empty[simp]: "¬x : σ in ∅" by (auto simp: hastype_def)

subsection ‹Maps between Sorted Sets›

locale sort_preserving = fixes f :: "'a ⇒ 'b" and A :: "'a ⇀ 's"
  assumes same_value_imp_same_type: "a : σ in A ⟹ b : τ in A ⟹ f a = f b ⟹ σ = τ"
begin

lemma same_value_imp_in_dom_iff:
  assumes fafa': "f a = f a'" and a: "a : σ in A" shows a': "a' ∈ dom A ⟷ a' : σ in A"
  using same_value_imp_same_type[OF a _ fafa'] by (auto elim!: in_dom_hastypeE)

lemma sort_preserving_subsset:
  assumes "A' ⊆⇩m A"
  shows "sort_preserving f A'"
  using same_value_imp_same_type
  apply unfold_locales by (auto dest!: subssetD[OF assms])

end

lemma sort_preserving_cong:
  "A = A' ⟹ (⋀a σ. a : σ in A ⟹ f a = f' a) ⟹ sort_preserving f A ⟷ sort_preserving f' A'"
  by (auto simp: sort_preserving_def)

lemma inj_on_dom_imp_sort_preserving:
  assumes "inj_on f (dom A)" shows "sort_preserving f A"
proof unfold_locales
  fix a b σ τ
  assume a: "a : σ in A" and b: "b : τ in A" and eq: "f a = f b"
  with inj_onD[OF assms] have "a = b" by auto
  with a b show "σ = τ" by (auto simp: has_same_type)
qed

lemma inj_imp_sort_preserving:
  assumes "inj f" shows "sort_preserving f A"
  using assms by (auto intro!: inj_on_dom_imp_sort_preserving simp: inj_on_def)

locale sorted_map =
  fixes f :: "'a ⇒ 'b" and A :: "'a ⇀ 's" and B :: "'b ⇀ 's"
  assumes sorted_map: "⋀a σ. a : σ in A ⟹ f a : σ in B"
begin

lemma target_has_same_type: "a : σ in A ⟹ f a : τ in B ⟷ σ = τ"
  by (auto simp:has_same_type dest!: sorted_map)

lemma target_dom_iff_hastype:
  "a : σ in A ⟹ f a ∈ dom B ⟷ f a : σ in B"
  by (auto simp: in_dom_iff_ex_type target_has_same_type)

lemma source_dom_iff_hastype:
  "f a : σ in B ⟹ a ∈ dom A ⟷ a : σ in A"
  by (auto simp: in_dom_iff_ex_type target_has_same_type)

lemma elim:
  assumes a: "(⋀a σ. a : σ in A ⟹ f a : σ in B) ⟹ P"
  shows P
  using a by (auto simp: sorted_map)

sublocale sort_preserving
  apply unfold_locales
  by (auto simp add: sorted_map dest!: target_has_same_type)

lemma funcset_dom: "f : dom A → dom B"
  using sorted_map[unfolded hastype_def] by (auto simp: domIff)

lemma sorted_map_list: "as :⇩l σs in A ⟹ map f as :⇩l σs in B"
  by (auto simp: list_all2_conv_all_nth sorted_map)

lemma in_dom: "a ∈ dom A ⟹ f a ∈ dom B" by (auto elim!: in_dom_hastypeE dest!:sorted_map)

end

notation sorted_map (‹_ :⇩s(/ _ →/ _)› [50,51,51]50)

abbreviation "all_sorted_map A B P ≡ ∀f. f :⇩s A → B ⟶ P f"
abbreviation "ex_sorted_map A B P ≡ ∃f. f :⇩s A → B ∧ P f"

syntax
  all_sorted_map :: "'pttrn ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹∀_ :⇩s(/ _ →/ _)./ _› [50,51,51,10]10)
  ex_sorted_map :: "'pttrn ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹∃_ :⇩s(/ _ →/ _)./ _› [50,51,51,10]10)

translations
  "∀f :⇩s A → B. e" ⇌ "CONST all_sorted_map A B (λf. e)"
  "∃f :⇩s A → B. e" ⇌ "CONST ex_sorted_map A B (λf. e)"

lemmas sorted_mapI = sorted_map.intro

lemma sorted_mapD: "f :⇩s A → B ⟹ a : σ in A ⟹ f a : σ in B"
  using sorted_map.sorted_map.

lemmas sorted_mapE = sorted_map.elim

lemma assumes "f :⇩s A → B"
  shows sorted_map_o: "g :⇩s B → C ⟹ g ∘ f :⇩s A → C"
    and sorted_map_cmono: "A' ⊆⇩m A ⟹ f :⇩s A' → B"
    and sorted_map_mono: "B ⊆⇩m B' ⟹ f :⇩s A → B'"
  using assms by (auto intro!:sorted_mapI dest!:subssetD sorted_mapD)

lemma sorted_map_cong:
  "(⋀a σ. a : σ in A ⟹ f a = f' a) ⟹
   A = A' ⟹
   (⋀a σ. a : σ in A ⟹ f a : σ in B ⟷ f a : σ in B') ⟹
  f :⇩s A → B ⟷ f' :⇩s A' → B'"
  by (auto simp: sorted_map_def)

lemma sorted_choice:
  assumes "∀a σ. a : σ in A ⟶ (∃b : σ in B. P a b)"
  shows "∃f :⇩s A → B. (∀a ∈ dom A. P a (f a))"
proof-
  have "∀a ∈ dom A. ∃b. A a = B b ∧ P a b"
  proof
    fix a assume "a ∈ dom A"
    then obtain σ where a: "a : σ in A" by (auto elim!: in_dom_hastypeE)
    with assms obtain b where b: "b : σ in B" and P: "P a b" by auto
    with a have "A a = B b" by (auto simp: hastype_def)
    with P show "∃b. A a = B b ∧ P a b" by auto
  qed
  from bchoice[OF this] obtain f where f: "∀x∈dom A. A x = B (f x) ∧ P x (f x)" by auto
  have "f :⇩s A → B"
  proof
    fix a σ assume a: "a : σ in A"
    then have "a ∈ dom A" by auto
    with f have "A a = B (f a)" by auto
    with a show "f a : σ in B" by (auto simp: hastype_def)
  qed
  with f show ?thesis by auto
qed

lemma sorted_map_empty[simp]: "f :⇩s ∅ → A"
  by (auto simp: sorted_map_def)

lemma sorted_map_comp_nth:
  "α :⇩s (f ∘s safe_nth (a#as)) → A ⟷ α 0 : f a in A ∧ (α ∘ Suc :⇩s (f ∘s safe_nth as) → A)"
  (is "?l ⟷ ?r")
proof
  assume ?l
  from sorted_mapD(1)[OF this, of 0] sorted_mapD(1)[OF this, of "Suc _"]
  show ?r
    apply (intro conjI sorted_map.intro, unfold hastype_in_o_sset)
    by (auto simp: hastype_def)
next
  assume r: ?r
  then have 0: "α 0 : f a in A" and "α ∘ Suc :⇩s f ∘s safe_nth as → A" by auto
  then
  have *: "i' < length as ⟹ α (Suc i') : f (as!i') in A" for i'
    apply (elim sorted_mapE)
    apply (unfold hastype_in_o_sset)
    apply (auto simp:sorted_map_def hastype_def).
  with 0 show ?l
    by (intro sorted_map.intro, unfold hastype_in_o_sset, unfold hastype_def,auto split:nat.split_asm elim:safe_nth_eq_SomeE)
qed

subsubsection ‹Sorted bijection›

locale sorted_surjection = sorted_map +
  assumes surj: "f ` dom A = dom B"
begin

lemma hastype_in_target_iff: "b : σ in B ⟷ (∃a : σ in A. b = f a)"
proof safe
  assume b: "b : σ in B"
  then have "b ∈ f ` dom A" by (auto simp: surj)
  then obtain a where "a ∈ dom A" "b = f a" by auto
  with b show "∃a : σ in A. b = f a"
    by (auto intro!:exI[of _ a] simp: source_dom_iff_hastype)
qed (simp add: sorted_map)

lemma image_of_sort: "f ` {a. a : σ in A} = {b. b : σ in B}"
  by (auto simp: hastype_in_target_iff)

lemma all_in_target_iff: "(∀b : σ in B. P b) ⟷ (∀a : σ in A. P (f a))"
  by (auto simp: hastype_in_target_iff)

end

locale sorted_bijection = sorted_map +
  assumes bij: "bij_betw f (dom A) (dom B)"
begin

lemma inj: "inj_on f (dom A)"
  using bij by (auto simp: bij_betw_def)

sublocale sorted_surjection
proof
  show "f ` dom A = dom B" using bij by (auto simp: bij_betw_def)
qed

thm inj_on_subset[OF inj]

lemma bij_betw_sort: "bij_betw f {a. a : σ in A} {b. b : σ in B}"
  by (auto simp: bij_betw_def sorted_map hastype_in_target_iff intro: inj_on_subset[OF inj])

end

locale inhabited = fixes A
  assumes inhabited: "⋀σ. ∃a. a : σ in A"
begin

lemma some_hastype:
  "(SOME a. a : σ in A) : σ in A"
  using inhabited[of σ] by (auto intro: someI)

lemma ex_sorted_map: "∃α. α :⇩s V → A"
proof (unfold sorted_map_def, intro choice allI)
  fix v
  from inhabited
  obtain a where "∀σ. v : σ in V ⟶ a : σ in A"
    apply (cases "V v")
    apply (auto dest: untyped_imp_not_hastype)[1]
    apply force.
  then show "∃y. ∀σ. v : σ in V ⟶ y : σ in A"
    by (intro exI[of _ a], auto)
qed

end

subsection ‹Sorted Images›

text ‹The partial version of @{term The} operator.›

definition "safe_The P ≡ if ∃!x. P x then Some (The P) else None"

lemma safe_The_cong[cong]:
  assumes eq: "⋀x. P x ⟷ Q x"
  shows "safe_The P = safe_The Q"
  using ext[of P Q, OF eq] by simp

lemma safe_The_eq_Some: "safe_The P = Some x ⟷ P x ∧ (∀x'. P x' ⟶ x' = x)"
  apply (unfold safe_The_def)
  apply (cases "∃!x. P x")
   apply (metis option.sel the_equality)
  by auto

lemma safe_The_eq_None: "safe_The P = None ⟷ ¬(∃!x. P x)"
  by (auto simp: safe_The_def)

lemma safe_The_False[simp]: "safe_The (λx. False) = None"
  by (auto simp: safe_The_def)

definition sorted_image :: "('a ⇒ 'b) ⇒ ('a ⇀ 's) ⇒ 'b ⇀ 's" (infixr ‹`⇧s› 90) where
  "(f `⇧s A) b ≡ safe_The (λσ. ∃a : σ in A. f a = b)"

lemma hastype_in_imageE:
  assumes "fx : σ in f `⇧s X"
    and "⋀x. x : σ in X ⟹ fx = f x ⟹ thesis"
  shows thesis
  using assms by (auto simp: hastype_def sorted_image_def safe_The_eq_Some)

lemma in_dom_image_hastypeE:
  "b ∈ dom (f `⇧s A) ⟹ (⋀a σ. a : σ in A ⟹ b = f a ⟹ thesis) ⟹ thesis"
  by (elim in_dom_hastypeE hastype_in_imageE)

lemma in_dom_imageE:
  assumes x: "x ∈ dom (f `⇧s A)" and main: "⋀a. a ∈ dom A ⟹ x = f a ⟹ thesis"
  shows thesis
proof-
  from x obtain a σ where a: "a : σ in A" and xf: "x = f a" by (auto elim!: in_dom_image_hastypeE)
  from main[OF hastype_imp_dom[OF a] xf] show thesis.
qed

context sort_preserving begin

lemma hastype_in_imageI: "a : σ in A ⟹ b = f a ⟹ b : σ in f `⇧s A"
  by (auto simp: hastype_def sorted_image_def safe_The_eq_Some)
    (meson eq_Some_iff_hastype same_value_imp_same_type)

lemma hastype_in_imageI2: "a : σ in A ⟹ f a : σ in f `⇧s A"
  using hastype_in_imageI by simp

lemma hastype_in_image: "b : σ in f `⇧s A ⟷ (∃a : σ in A. f a = b)"
  by (auto elim!: hastype_in_imageE intro!: hastype_in_imageI)

lemma in_dom_imageI: "a ∈ dom A ⟹ b = f a ⟹ b ∈ dom (f `⇧s A)"
  by (auto intro!: hastype_imp_dom hastype_in_imageI elim!: in_dom_hastypeE)

lemma in_dom_imageI2: "a ∈ dom A ⟹ f a ∈ dom (f `⇧s A)"
  by (auto intro!: in_dom_imageI)

lemma hastype_list_in_image: "bs :⇩l σs in f `⇧s A ⟷ (∃as. as :⇩l σs in A ∧ map f as = bs)"
  by (auto simp: list_all2_conv_all_nth hastype_in_image Skolem_list_nth intro!:nth_equalityI)

lemma dom_image[simp]: "dom (f `⇧s A) = f ` dom A"
  by (auto intro!: map_le_implies_dom_le in_dom_imageI elim!: in_dom_imageE)

sublocale to_image: sorted_map f A "f `⇧s A"
  apply unfold_locales by (auto intro!: hastype_in_imageI)

lemma sorted_map_iff_image_subset:
  "f :⇩s A → B ⟷ f `⇧s A ⊆⇩m B"
  by (auto intro!: subssetI sorted_mapI hastype_in_imageI elim!: hastype_in_imageE sorted_mapE dest!:subssetD)

end

lemma sort_preserving_o:
  assumes f: "sort_preserving f A" and g: "sort_preserving g (f `⇧s A)"
  shows "sort_preserving (g ∘ f) A"
proof (intro sort_preserving.intro, unfold o_def)
  interpret f: sort_preserving using f.
  interpret g: sort_preserving g "f `⇧s A" using g.
  fix a b σ τ
  assume a: "a : σ in A" and b: "b : τ in A" and eq: "g (f a) = g (f b)"
  from a b have "g (f a) : σ in g `⇧s f `⇧s A" "g (f b) : τ in g `⇧s f `⇧s A"
    by (auto intro!: g.hastype_in_imageI f.hastype_in_imageI)
  with eq show "σ = τ" by (auto simp: has_same_type)
qed

lemma sorted_image_image:
  assumes f: "sort_preserving f A" and g: "sort_preserving g (f `⇧s A)"
  shows "g `⇧s f `⇧s A = (g ∘ f) `⇧s A"
proof-
  interpret f: sort_preserving using f.
  interpret g: sort_preserving g "f `⇧s A" using g.
  interpret gf: sort_preserving ‹g ∘ f› A using sort_preserving_o[OF f g].
  show ?thesis
    by (auto elim!: hastype_in_imageE
        intro!: sset_eqI gf.hastype_in_imageI g.hastype_in_imageI f.hastype_in_imageI)
qed

context sorted_map begin

lemma image_subsset[intro!]: "f `⇧s A ⊆⇩m B"
  by (auto intro!: subssetI sorted_map elim!: hastype_in_imageE)

lemma dom_image_subset[intro!]: "f ` dom A ⊆ dom B"
  using map_le_implies_dom_le[OF image_subsset] by simp

end

lemma sorted_image_cong: "(⋀a σ. a : σ in A ⟹ f a = f' a) ⟹ f `⇧s A = f' `⇧s A"
  by (auto 0 3 intro!: arg_cong[of _ _ safe_The] simp: fun_eq_iff sorted_image_def)

lemma inj_on_dom_imp_sort_preserving_inv_into:
  assumes inj: "inj_on f (dom A)" shows "sort_preserving (inv_into (dom A) f) (f `⇧s A)"
  by (unfold_locales, auto elim!: hastype_in_imageE simp: inv_into_f_f[OF inj] has_same_type)

lemma inj_imp_sort_preserving_inv:
  assumes inj: "inj f" shows "sort_preserving (inv f) (f `⇧s A)"
  by (unfold_locales, auto elim!: hastype_in_imageE simp: inv_into_f_f[OF inj] has_same_type)

lemma inj_on_dom_imp_inv_into_image_cancel:
  assumes inj: "inj_on f (dom A)"
  shows "inv_into (dom A) f `⇧s f `⇧s A = A"
proof-
  interpret f: sort_preserving f A using inj_on_dom_imp_sort_preserving[OF inj].
  interpret f': sort_preserving ‹inv_into (dom A) f› ‹f `⇧s A›
    using inj_on_dom_imp_sort_preserving_inv_into[OF inj].
  show ?thesis
    by (auto intro!: sset_eqI f'.hastype_in_imageI f.hastype_in_imageI elim!: hastype_in_imageE simp: inj)
qed

lemma inj_imp_inv_image_cancel:
  assumes inj: "inj f"
  shows "inv f `⇧s f `⇧s A = A"
proof-
  interpret f: sort_preserving f A using inj_imp_sort_preserving[OF inj].
  interpret f': sort_preserving ‹inv f› ‹f `⇧s A› using inj_imp_sort_preserving_inv[OF inj].
  show ?thesis
    by (auto intro!: sset_eqI f'.hastype_in_imageI f.hastype_in_imageI elim!: hastype_in_imageE simp: inj)
qed

definition sorted_Imagep (infixr ‹``⇧s› 90)
  where "((⊑) ``⇧s A) b ≡ safe_The (λσ. ∃a : σ in A. a ⊑ b)" for r (infix ‹⊑› 50)

lemma untyped_hastypeE: "A a = None ⟹ a : σ in A ⟹ thesis"
  by (auto simp: hastype_def)

end