Theory ValueSimilarity

theory ValueSimilarity
imports Value CValue Pointwise
begin

text {*
This theory formalizes Section 3 of \cite{functionspaces}. Their domain $D$ is our type @{typ Value},
their domain $E$ is our type @{typ CValue} and $A$ corresponds to @{typ "(C → CValue)"}.

In our case, the construction of the domains was taken care of by the HOLCF package
(\cite{holcf}), so where \cite{functionspaces} refers to elements of the domain approximations
$D_n$ resp. $E_n$, these are just elements of @{typ Value} resp. @{typ CValue} here. Therefore the
\emph{n-injection} $\phi_n^E \colon E_n \to E$ is the identity here.

The projections correspond to the take-functions generated by the HOLCF package:
\begin{alignstar}
\psi_n^E &\colon E \to E_n &\text{ corresponds to }&&@{term CValue_take}@{text "::"}&@{typeof "CValue_take :: nat ⇒ CValue → CValue" } \\
\psi_n^A &\colon A \to A_n &\text{ corresponds to }&&@{term C_to_CValue_take}@{text "::"}&@{typeof "C_to_CValue_take :: nat ⇒ (C → CValue) → (C → CValue)"} \\
\psi_n^D &\colon D \to D_n &\text{ corresponds to }&&@{term Value_take}@{text "::"}&@{typeof Value_take}.
\end{alignstar}

The syntactic overloading of $e(a)(c)$ to mean either $\mathrm{ |mathsf{Ap}}_{E_n}^|bot$ or $\mathrm{ |mathsf{AP}}_{E}^|bot$
turns into our non-overloaded @{text "_ ↓CFn _"}@{text "::"}@{typeof "op ↓CFn"}.
*}

text {*
To have our presentation closer to \cite{functionspaces}, we introduce some notation:
*}

notation Value_take ("ψ⇧D⇘_⇙")
notation C_to_CValue_take ("ψ⇧A⇘_⇙")
notation CValue_take ("ψ⇧E⇘_⇙")

subsubsection {* A note about section 2.3 *}

text {*
Section 2.3 of  \cite{functionspaces} contains equations (2) and (3) which do not hold in general.
We demonstrate that fact here using our corresponding definition, but the counter-example carries
over to the original formulation. Lemma (2) is a generalisation of (3) to the resourced semantics,
so the counter-example for (3) is the simpler and more educating:
*}

lemma counter_example:
  assumes "Equation (3)": "⋀ n d d'. ψ⇧D⇘n⇙⋅(d ↓Fn d') = ψ⇧D⇘Suc n⇙⋅d ↓Fn ψ⇧D⇘n⇙⋅d'"
  shows "False"
proof-
  def n == "1::nat"
  def d == "Fn⋅(Λ e. (e ↓Fn ⊥))"
  def d' == "Fn⋅(Λ _. Fn⋅(Λ _. ⊥))"
  have "Fn⋅(Λ _. ⊥) = ψ⇧D⇘n⇙⋅(d ↓Fn d')"
    by (simp add: d_def d'_def n_def cfun_map_def)
  also
  have "… = ψ⇧D⇘Suc n⇙⋅d ↓Fn ψ⇧D⇘n⇙⋅d'"
    using "Equation (3)".
  also have "… = ⊥"
    by (simp add: d_def d'_def n_def)
  finally show False by simp
qed

text {*
For completeness, and to avoid making false assertions, the counter-example to equation (2):
*}

lemma counter_example2:
  assumes "Equation (2)": "⋀ n e a c. ψ⇧E⇘n⇙⋅((e ↓CFn a)⋅c) = (ψ⇧E⇘Suc n⇙⋅e ↓CFn ψ⇧A⇘n⇙⋅a)⋅c"
  shows "False"
proof-
  def n == "1::nat"
  def e == "CFn⋅(Λ e r. (e⋅r ↓CFn ⊥)⋅r)"
  def a == "Λ _ . CFn⋅(Λ _ _. CFn⋅(Λ _ _. ⊥)) :: C → CValue"
  fix c :: C
  have "CFn⋅(Λ _ _. ⊥) = ψ⇧E⇘n⇙⋅((e ↓CFn a)⋅c)"
    by (simp add: e_def a_def n_def cfun_map_def)
  also
  have "… = (ψ⇧E⇘Suc n⇙⋅e ↓CFn ψ⇧A⇘n⇙⋅a)⋅c"
    using "Equation (2)".
  also have "… = ⊥"
    by (simp add: e_def a_def n_def)
  finally show False by simp
qed


text {* A suitable substitute for the lemma can be found in 4.3.5 (1) in \cite{fullabstraction},
which in our setting becomes the following (note the extra invocation of @{term "Value_take n"} on
the left hand side):
*}

lemma "Abramsky 4,3,5 (1)":
  "ψ⇧D⇘n⇙⋅(d ↓Fn ψ⇧D⇘n⇙⋅d') = ψ⇧D⇘Suc n⇙⋅d ↓Fn ψ⇧D⇘n⇙⋅d'"
  by (cases d) (auto simp add: Value.take_take)

text {*
The problematic equations are used in the proof of the only-if direction of proposition 9 in
\cite{functionspaces}. It can be fixed by applying take-induction, which inserts the
extra call to @{term "Value_take n"} in the right spot.
*}

subsubsection {* Working with @{typ Value} and @{typ CValue} *}

text {* Combined case distinguishing and induction rules. *}

lemma value_CValue_cases:
  obtains
  "x = ⊥" "y = ⊥" |
  f where "x = Fn⋅f" "y = ⊥" |
  g where "x = ⊥" "y = CFn⋅g" |
  f g where "x = Fn⋅f" "y = CFn ⋅ g" |
  b⇩1 where "x = B⋅(Discr b⇩1)" "y = ⊥" |
  b⇩1 g where "x = B⋅(Discr b⇩1)" "y = CFn⋅g" |
  b⇩1 b⇩2 where "x = B⋅(Discr b⇩1)" "y = CB⋅(Discr b⇩2)" |
  f b⇩2 where "x = Fn⋅f" "y = CB⋅(Discr b⇩2)" |
  b⇩2 where "x = ⊥" "y = CB⋅(Discr b⇩2)"
  by (metis CValue.exhaust Discr_undiscr Value.exhaust)

lemma Value_CValue_take_induct:
  assumes "adm (case_prod P)"
  assumes "⋀ n. P (ψ⇧D⇘n⇙⋅x) (ψ⇧A⇘n⇙⋅y)"
  shows "P x y"
proof-
  have "case_prod P (⨆n. (ψ⇧D⇘n⇙⋅x, ψ⇧A⇘n⇙⋅y))"
    by (rule admD[OF `adm (case_prod P)` ch2ch_Pair[OF ch2ch_Rep_cfunL[OF Value.chain_take] ch2ch_Rep_cfunL[OF C_to_CValue_chain_take]]])
       (simp add: assms(2))
  hence "case_prod P (x,y)"
    by (simp add: lub_Pair[OF ch2ch_Rep_cfunL[OF Value.chain_take] ch2ch_Rep_cfunL[OF C_to_CValue_chain_take]]
                  Value.reach C_to_CValue_reach)
  thus ?thesis by simp
qed

subsubsection {* Restricted similarity is defined recursively *}

text {* The base case *}

inductive similar'_base :: "Value ⇒ CValue ⇒ bool" where
  bot_similar'_base[simp,intro]: "similar'_base ⊥ ⊥"

inductive_cases [elim!]:
   "similar'_base x y"

text {* The inductive case *}

inductive similar'_step :: "(Value ⇒ CValue ⇒ bool) ⇒ Value ⇒ CValue ⇒ bool" for s where
  bot_similar'_step[intro!]: "similar'_step s ⊥ ⊥" |
  bool_similar'_step[intro]: "similar'_step s (B⋅b) (CB⋅b)" |
  Fun_similar'_step[intro]: "(⋀ x y . s x (y⋅C⇧∞) ⟹ s (f⋅x) (g⋅y⋅C⇧∞)) ⟹ similar'_step s (Fn⋅f) (CFn⋅g)"

inductive_cases [elim!]:
   "similar'_step s x ⊥"
   "similar'_step s ⊥ y"
   "similar'_step s (B⋅f) (CB⋅g)"
   "similar'_step s (Fn⋅f) (CFn⋅g)"

text {*
We now create the restricted similarity relation, by primitive recursion over @{term n}.

This cannot be done using an inductive definition, as it would not be monotone.
 *}

fun similar' where
 "similar' 0 = similar'_base" |
 "similar' (Suc n) = similar'_step (similar' n)"
declare similar'.simps[simp del]

abbreviation similar'_syn  ("_ ◃▹⇘_⇙ _" [50,50,50] 50)
  where "similar'_syn x n y ≡ similar' n x y"

lemma similar'_botI[intro!,simp]: "⊥ ◃▹⇘n⇙ ⊥"
  by (cases n) (auto simp add: similar'.simps)

lemma similar'_FnI[intro]:
  assumes "⋀x y.  x ◃▹⇘n⇙ y⋅C⇧∞ ⟹ f⋅x ◃▹⇘n⇙ g⋅y⋅C⇧∞"
  shows "Fn⋅f ◃▹⇘Suc n⇙ CFn⋅g"
using assms by (auto simp add: similar'.simps)

lemma similar'_FnE[elim!]:
  assumes "Fn⋅f ◃▹⇘Suc n⇙ CFn⋅g"
  assumes "(⋀x y.  x ◃▹⇘n⇙ y⋅C⇧∞ ⟹ f⋅x ◃▹⇘n⇙ g⋅y⋅C⇧∞) ⟹ P"
  shows P
using assms by (auto simp add: similar'.simps)

lemma bot_or_not_bot':
  "x ◃▹⇘n⇙ y ⟹ (x = ⊥ ⟷ y = ⊥)"
  by (cases n) (auto simp add: similar'.simps elim: similar'_base.cases similar'_step.cases)

lemma similar'_bot[elim_format, elim!]:
    "⊥ ◃▹⇘n⇙ x ⟹ x = ⊥"
    "y ◃▹⇘n⇙ ⊥ ⟹ y = ⊥"
by (metis bot_or_not_bot')+

lemma similar'_typed[simp]:
  "¬ B⋅b ◃▹⇘n⇙ CFn⋅g"
  "¬ Fn⋅f ◃▹⇘n⇙ CB⋅b"
  by (cases n, auto simp add: similar'.simps elim: similar'_base.cases similar'_step.cases)+

lemma similar'_bool[simp]:
  "B⋅b⇩1 ◃▹⇘Suc n⇙ CB⋅b⇩2 ⟷ b⇩1 = b⇩2"
  by (auto simp add: similar'.simps elim: similar'_base.cases similar'_step.cases)

subsubsection {* Moving up and down the similarity relations *}

text {*
These correspond to Lemma 7 in |cite{functionspaces}.
*}

lemma similar'_down: "d ◃▹⇘Suc n⇙ e ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅e"
  and similar'_up: "d ◃▹⇘n⇙ e ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘Suc n⇙ ψ⇧E⇘n⇙⋅e"
proof (induction n arbitrary: d e)
  case (Suc n) case 1 with  Suc
  show ?case
    by (cases d e rule:value_CValue_cases) auto
next
  case (Suc n) case 2 with Suc
  show ?case
    by (cases d e rule:value_CValue_cases) auto
qed auto

text {*
A generalisation of the above, doing multiple steps at once.
*}

lemma similar'_up_le: "n ≤ m ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅e ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘m⇙ ψ⇧E⇘n⇙⋅e"
  by (induction rule: dec_induct )
     (auto dest: similar'_up simp add: Value.take_take CValue.take_take min_absorb2)

lemma similar'_down_le: "n ≤ m ⟹ ψ⇧D⇘m⇙⋅d ◃▹⇘m⇙ ψ⇧E⇘m⇙⋅e ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅e"
  by (induction rule: inc_induct )
     (auto dest: similar'_down simp add: Value.take_take CValue.take_take min_absorb1)

lemma similar'_take: "d ◃▹⇘n⇙ e ⟹ ψ⇧D⇘n⇙⋅d ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅e"
  apply (drule similar'_up)
  apply (drule similar'_down)
  apply (simp add: Value.take_take CValue.take_take)
  done

subsubsection {* Admissibility *}

text {*
A technical prerequisite for induction is admissibility of the predicate, i.e.\ that the predicate
holds for the limit of a chain, given that it holds for all elements.
*}

lemma similar'_base_adm: "adm (λ x. similar'_base (fst x) (snd x))"
proof (rule admI, goal_cases)
  case (1 Y)
  then have "Y = (λ _ . ⊥)" by (metis prod.exhaust fst_eqD inst_prod_pcpo similar'_base.simps snd_eqD)
  thus ?case by auto
qed

lemma similar'_step_adm:
  assumes "adm (λ x. s (fst x) (snd x))"
  shows "adm (λ x. similar'_step s (fst x) (snd x))"
proof (rule admI, goal_cases)
  case prems: (1 Y)
  from `chain Y`
  have "chain (λ i. fst (Y i))" by (rule ch2ch_fst)
  thus ?case
  proof(cases rule: Value_chainE)
  case bot
    hence *: "⋀ i. fst (Y i) = ⊥" by metis
    with prems(2)[unfolded split_beta]
    have "⋀i. snd (Y i) = ⊥" by auto
    hence "Y = (λ i. (⊥, ⊥))" using * by (metis surjective_pairing)
    thus ?thesis by auto
  next
  case (B n b)
    hence "∀i. fst (Y (i + n)) = B⋅b" by (metis add.commute not_add_less1)
    with prems(2)
    have "∀i. Y (i + n) = (B⋅b, CB⋅b)"
      apply auto
      apply (erule_tac x = "i + n" in allE)
      apply (erule_tac x = "i" in allE)
      apply (erule similar'_step.cases)
      apply auto
      by (metis fst_conv old.prod.exhaust snd_conv)
    hence "similar'_step s (fst (⨆ i. Y (i + n))) (snd (⨆ i. Y (i + n)))" by auto
    thus ?thesis
      by (simp add: lub_range_shift[OF `chain Y`])
  next
    fix n
    fix Y'
    assume "chain Y'" and "(λi. fst (Y i)) = (λ m. (if m < n then ⊥ else Fn⋅(Y' (m-n))))"
    hence Y': "⋀ i. fst (Y (i+n)) = Fn⋅(Y' i)" by (metis add_diff_cancel_right' not_add_less2)
    with prems(2)[unfolded split_beta]
    have "⋀i. ∃ g'. snd (Y (i+n)) = CFn⋅g'"
      by -(erule_tac x = "i + n" in allE, auto elim!: similar'_step.cases)
    then obtain Y'' where Y'': "⋀ i. snd (Y (i+n)) = CFn⋅(Y'' i)" by metis
    from prems(1) have "⋀i. Y i ⊑ Y (Suc i)"
      by (simp add: po_class.chain_def)
    then have *: "⋀i. Y (i + n) ⊑ Y (Suc i + n)"
      by simp
    have "chain Y''"
      apply (rule chainI)
      apply (rule iffD1[OF CValue.inverts(1)])
      apply (subst (1 2) Y''[symmetric])
      apply (rule snd_monofun)
      apply (rule *)
      done

    have "similar'_step s (Fn⋅(⨆ i. (Y' i))) (CFn ⋅ (⨆ i. Y'' i))"
    proof (rule Fun_similar'_step)
      fix x y
      from prems(2) Y' Y''
      have "⋀i. similar'_step s (Fn⋅(Y' i)) (CFn⋅(Y'' i))" by metis
      moreover
      assume "s x (y⋅C⇧∞)"
      ultimately
      have "⋀i. s (Y' i⋅x) (Y'' i⋅y⋅C⇧∞)" by auto
      hence "case_prod s (⨆ i. ((Y' i)⋅x, (Y'' i)⋅y⋅C⇧∞))"
        apply -
        apply (rule admD[OF adm_case_prod[where P = "λ_ . s", OF assms]])
        apply (simp add:  `chain Y'`  `chain Y''`)
        apply simp
        done
      thus "s ((⨆ i. Y' i)⋅x) ((⨆ i. Y'' i)⋅y⋅C⇧∞)"
        by (simp add: lub_Pair  ch2ch_Rep_cfunL contlub_cfun_fun  `chain Y'`  `chain Y''`)
    qed
    hence "similar'_step s (fst (⨆ i. Y (i+n))) (snd (⨆ i. Y (i+n)))"
      by (simp add: Y' Y''
          cont2contlubE[OF cont_fst chain_shift[OF prems(1)]]  cont2contlubE[OF cont_snd chain_shift[OF prems(1)]]
           contlub_cfun_arg[OF `chain Y''`] contlub_cfun_arg[OF `chain Y'`])
    thus "similar'_step s (fst (⨆ i. Y i)) (snd (⨆ i. Y i))"
      by (simp add: lub_range_shift[OF `chain Y`])
  qed
qed


lemma similar'_adm: "adm (λx. fst x ◃▹⇘n⇙ snd x)"
  by (induct n) (auto simp add: similar'.simps intro: similar'_base_adm similar'_step_adm)

lemma similar'_admI: "cont f ⟹ cont g ⟹ adm (λx. f x ◃▹⇘n⇙ g x)"
  by (rule adm_subst[OF _ similar'_adm, where t = "λx. (f x, g x)", simplified]) auto

subsubsection {* The real similarity relation *}

text {*
This is the goal of the theory: A relation between @{typ Value} and @{typ CValue}.
*}

definition similar :: "Value ⇒ CValue ⇒ bool" (infix "◃▹" 50) where
  "x ◃▹ y ⟷ (∀n. ψ⇧D⇘n⇙⋅x ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅y)"

lemma similarI:
  "(⋀ n. ψ⇧D⇘n⇙⋅x ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅y) ⟹ x ◃▹ y"
  unfolding similar_def by blast

lemma similarE:
  "x ◃▹ y ⟹ ψ⇧D⇘n⇙⋅x ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅y"
  unfolding similar_def by blast

lemma similar_bot[simp]: "⊥ ◃▹ ⊥" by (auto intro: similarI)

lemma similar_bool[simp]: "B⋅b ◃▹ CB⋅b"
  by (rule similarI, case_tac n, auto)
 
lemma [elim_format, elim!]: "x ◃▹ ⊥ ⟹ x = ⊥"
  unfolding similar_def
  apply (cases x)
  apply auto
  apply (erule_tac x = "Suc 0" in allE, auto)+
  done

lemma [elim_format, elim!]: "x ◃▹ CB⋅b ⟹ x = B⋅b"
  unfolding similar_def
  apply (cases x)
  apply auto
  apply (erule_tac x = "Suc 0" in allE, auto)+
  done

lemma [elim_format, elim!]: "⊥ ◃▹ y ⟹ y = ⊥"
  unfolding similar_def
  apply (cases y)
  apply auto
  apply (erule_tac x = "Suc 0" in allE, auto)+
  done

lemma [elim_format, elim!]: "B⋅b ◃▹ y ⟹ y = CB⋅b"
  unfolding similar_def
  apply (cases y)
  apply auto
  apply (erule_tac x = "Suc 0" in allE, auto)+
  done

lemma take_similar'_similar:
  assumes "x ◃▹⇘n⇙ y"
  shows  "ψ⇧D⇘n⇙⋅x ◃▹ ψ⇧E⇘n⇙⋅y"
proof(rule similarI)
  fix m
  from assms
  have "ψ⇧D⇘n⇙⋅x ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅y" by (rule similar'_take)
  moreover
  have "n ≤ m ∨ m ≤ n" by auto
  ultimately
  show "ψ⇧D⇘m⇙⋅(ψ⇧D⇘n⇙⋅x) ◃▹⇘m⇙ ψ⇧E⇘m⇙⋅(ψ⇧E⇘n⇙⋅y)"
    by (auto elim: similar'_up_le similar'_down_le dest: similar'_take
        simp add: min_absorb2 min_absorb1 Value.take_take CValue.take_take)
qed

lemma bot_or_not_bot:
  "x ◃▹ y ⟹ (x = ⊥ ⟷ y = ⊥)"
  by (cases x y rule:value_CValue_cases) auto

lemma bool_or_not_bool:
  "x ◃▹ y ⟹ (x = B⋅b) ⟷ (y = CB⋅b)"
  by (cases x y rule:value_CValue_cases) auto

lemma slimilar_bot_cases[consumes 1, case_names bot bool Fn]:
  assumes "x ◃▹ y"
  obtains "x = ⊥" "y = ⊥" |
  b where "x = B⋅(Discr b)" "y = CB⋅(Discr b)" |
  f g where "x = Fn⋅f" "y = CFn ⋅ g"
using assms
by (metis CValue.exhaust Value.exhaust bool_or_not_bool bot_or_not_bot discr.exhaust)

lemma similar_adm: "adm (λx. fst x ◃▹ snd x)"
  unfolding similar_def
  by (intro adm_lemmas similar'_admI cont2cont)

lemma similar_admI: "cont f ⟹ cont g ⟹ adm (λx. f x ◃▹ g x)"
  by (rule adm_subst[OF _ similar_adm, where t = "λx. (f x, g x)", simplified]) auto

text {*
Having constructed the relation we can how show that it indeed is the desired relation,
relating $|bot$ with $|bot$ and functions with functions, if they take related arguments to related values.
This corresponds to Proposition 9 in |cite{functionspaces}.
*}

lemma similar_nice_def: "x ◃▹ y ⟷ (x = ⊥ ∧ y = ⊥ ∨ (∃ b. x = B⋅(Discr b) ∧ y = CB⋅(Discr b)) ∨ (∃ f g. x = Fn⋅f ∧ y = CFn⋅g ∧ (∀ a b. a ◃▹ b⋅C⇧∞ ⟶ f⋅a ◃▹ g⋅b⋅C⇧∞)))"
  (is "?L ⟷ ?R")
proof
  assume "?L"
  thus "?R"
  proof (cases x y rule:slimilar_bot_cases)
    case bot thus ?thesis by simp
  next
    case bool thus ?thesis by simp
  next 
    case (Fn f g)
    note `?L`[unfolded Fn]
    have "∀a b. a ◃▹ b⋅C⇧∞ ⟶ f⋅a ◃▹ g⋅b⋅C⇧∞"
    proof(intro impI allI)
      fix a b
      assume "a ◃▹ b⋅C⇧∞"

      show "f⋅a ◃▹ g⋅b⋅C⇧∞" 
      proof(rule similarI)
        fix n
        have "adm (λ(b, a). ψ⇧D⇘n⇙⋅(f⋅b) ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅(g⋅a⋅C⇧∞))"
          by (intro adm_case_prod similar'_admI cont2cont)
        thus "ψ⇧D⇘n⇙⋅(f⋅a) ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅(g⋅b⋅C⇧∞)"
        proof (induct a b rule: Value_CValue_take_induct[consumes 1])
          txt {* This take induction is required to avoid the wrong equation shown above. *}
          fix m

          from `a ◃▹ b⋅C⇧∞`
          have "ψ⇧D⇘m⇙⋅a ◃▹⇘m⇙ ψ⇧E⇘m⇙⋅(b⋅C⇧∞)" by (rule similarE)
          hence "ψ⇧D⇘m⇙⋅a ◃▹⇘max m n⇙ ψ⇧E⇘m⇙⋅(b⋅C⇧∞)" by (rule similar'_up_le[rotated]) auto
          moreover
          from `Fn⋅f ◃▹ CFn⋅g`
          have "ψ⇧D⇘Suc (max m n)⇙⋅(Fn⋅f) ◃▹⇘Suc (max m n)⇙ ψ⇧E⇘Suc (max m n)⇙⋅(CFn⋅g)" by (rule similarE)
          ultimately
          have "ψ⇧D⇘max m n⇙⋅(f⋅(ψ⇧D⇘max m n⇙⋅(ψ⇧D⇘m⇙⋅a))) ◃▹⇘max m n⇙ ψ⇧E⇘max m n⇙⋅(g⋅(ψ⇧A⇘max m n⇙⋅(ψ⇧A⇘m⇙⋅b))⋅C⇧∞)"
            by auto
          hence " ψ⇧D⇘max m n⇙⋅(f⋅(ψ⇧D⇘m⇙⋅a)) ◃▹⇘max m n⇙ ψ⇧E⇘max m n⇙⋅(g⋅(ψ⇧A⇘m⇙⋅b)⋅C⇧∞)"
            by (simp add: Value.take_take cfun_map_map CValue.take_take ID_def eta_cfun min_absorb2 min_absorb1)
          thus "ψ⇧D⇘n⇙⋅(f⋅(ψ⇧D⇘m⇙⋅a)) ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅(g⋅(ψ⇧A⇘m⇙⋅b)⋅C⇧∞)"
            by (rule similar'_down_le[rotated]) auto
        qed
      qed
    qed
    thus ?thesis unfolding Fn by simp
  qed
next
  assume "?R"
  thus "?L"
  proof(elim conjE disjE exE ssubst)
    show "⊥ ◃▹ ⊥" by simp
  next
    fix b
    show "B⋅(Discr b) ◃▹ CB⋅(Discr b)" by simp
  next
    fix f g
    assume imp: "∀a b. a ◃▹ b⋅C⇧∞ ⟶ f⋅a ◃▹ g⋅b⋅C⇧∞"
    show "Fn⋅f ◃▹ CFn⋅g"
    proof (rule similarI)
      fix n
      show "ψ⇧D⇘n⇙⋅(Fn⋅f) ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅(CFn⋅g)"
      proof(cases n)
        case 0 thus ?thesis by simp
      next
        case (Suc n)
        { fix x y
          assume "x ◃▹⇘n⇙ y⋅C⇧∞"
          hence "ψ⇧D⇘n⇙⋅x ◃▹ ψ⇧E⇘n⇙⋅(y⋅C⇧∞)" by (rule take_similar'_similar)
          hence "f⋅(ψ⇧D⇘n⇙⋅x) ◃▹ g⋅(ψ⇧A⇘n⇙⋅y)⋅C⇧∞" using imp by auto
          hence "ψ⇧D⇘n⇙⋅(f⋅(ψ⇧D⇘n⇙⋅x)) ◃▹⇘n⇙ ψ⇧E⇘n⇙⋅(g⋅(ψ⇧A⇘n⇙⋅y)⋅C⇧∞)"
            by (rule similarE)
        }
        with Suc
        show ?thesis by auto
      qed
    qed
  qed
qed

lemma similar_FnI[intro]:
  assumes "⋀x y.  x ◃▹ y⋅C⇧∞ ⟹ f⋅x ◃▹ g⋅y⋅C⇧∞"
  shows "Fn⋅f ◃▹ CFn⋅g"
by (metis assms similar_nice_def)

lemma similar_FnD[elim!]:
  assumes "Fn⋅f ◃▹ CFn⋅g"
  assumes "x ◃▹ y⋅C⇧∞"
  shows "f⋅x ◃▹ g⋅y⋅C⇧∞"
using assms 
by (subst (asm) similar_nice_def) auto

lemma similar_FnE[elim!]:
  assumes "Fn⋅f ◃▹ CFn⋅g"
  assumes "(⋀x y.  x ◃▹ y⋅C⇧∞ ⟹ f⋅x ◃▹ g⋅y⋅C⇧∞) ⟹ P"
  shows P
by (metis assms similar_FnD)

subsubsection {* The similarity relation lifted pointwise to functions. *}

abbreviation fun_similar :: "('a::type ⇒ Value) ⇒ ('a ⇒ (C → CValue)) ⇒ bool"  (infix "◃▹⇧*" 50) where
  "fun_similar ≡ pointwise (λx y. x ◃▹ y⋅C⇧∞)"

lemma fun_similar_fmap_bottom[simp]: "⊥ ◃▹⇧* ⊥"
  by auto

lemma fun_similarE[elim]:
  assumes "m ◃▹⇧* m'"
  assumes "(⋀x. (m  x) ◃▹ (m' x)⋅C⇧∞) ⟹ Q"
  shows Q
  using assms unfolding pointwise_def by blast

end