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}‹::›&@{typeof "CValue_take :: nat ⇒ CValue → CValue" } \\
\psi_n^A &\colon A \to A_n &\text{ corresponds to }&&@{term C_to_CValue_take}‹::›&@{typeof "C_to_CValue_take :: nat ⇒ (C → CValue) → (C → CValue)"} \\
\psi_n^D &\colon D \to D_n &\text{ corresponds to }&&@{term Value_take}‹::›&@{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 ‹_ ↓CFn _›‹::›@{typeof "(↓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-
  define n :: nat where "n = 1"
  define d where "d = Fn⋅(Λ e. (e ↓Fn ⊥))"
  define d' where "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-
  define n :: nat where "n = 1"
  define e where "e = CFn⋅(Λ e r. (e⋅r ↓CFn ⊥)⋅r)"
  define a :: "C → CValue" where "a = (Λ _ . CFn⋅(Λ _ _. CFn⋅(Λ _ _. ⊥)))"
  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" |
  b1 where "x = B⋅(Discr b1)" "y = ⊥" |
  b1 g where "x = B⋅(Discr b1)" "y = CFn⋅g" |
  b1 b2 where "x = B⋅(Discr b1)" "y = CB⋅(Discr b2)" |
  f b2 where "x = Fn⋅f" "y = CB⋅(Discr b2)" |
  b2 where "x = ⊥" "y = CB⋅(Discr b2)"
  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⋅b1 ◃▹⇘Suc n⇙ CB⋅b2 ⟷ b1 = b2"
  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