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 simp: those_eq_None 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. xxs. 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:
  "(xsset xss. xset xs. f x)  (xsset (product_lists xss). xset xs. f x)"
  by (induct xss, auto)

lemma bex_set_ball_set_distrib:
  "(xsset xss. xset xs. f x)  (xsset (product_lists xss). xset 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)

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)

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)

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

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

lemma hastype_in_Some[simp]: "x : σ in Some  x = σ" by (auto simp: hastype_def)

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)

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: "xdom 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

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

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_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_imageE:
  "b  dom (f `s A)  (a σ. a : σ in A  b = f a  thesis)  thesis"
  by (elim in_dom_hastypeE hastype_in_imageE)

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!: ext arg_cong[of _ _ safe_The] simp: 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