Theory Phi_System.Phi_Fictions

theory Phi_Fictions
  imports Phi_Types
begin

lemma pairself_set_ex[simp]:
  ‹ pairself f ` { (a x, b x) |x. P x} = { (f (a x), f (b x)) |x. P x } ›
  unfolding set_eq_iff
  by (auto simp: image_iff)

lemma defined_set_ex[simp]:
  ‹ { f u' |u'. ∃u. u' = g u ∧ P u} = { f (g u) |u. P u } ›
  unfolding set_eq_iff
  by auto

definition refinement_projection :: ‹('abstract::sep_magma ⇒ 'concrete BI) ⇒ 'abstract set ⇒ 'concrete set›
  where ‹refinement_projection I D = Sup ((BI.dest o I) ` (D * top))›

lemma refinement_projection_mono:
  ‹ D ≤ D'
⟹ refinement_projection I D ≤ refinement_projection I D'›
  unfolding refinement_projection_def
  by (clarsimp simp add: less_eq_BI_iff set_mult_expn Bex_def; blast)

lemma set_top_times_idem:
  ‹top * top = (top :: 'a::sep_magma_1 set)›
  unfolding set_eq_iff
  by (clarsimp simp: set_mult_expn, metis mult_1_class.mult_1_right sep_magma_1_left)

lemma refinement_projection_UNIV_times_D[simp]:
  ‹ refinement_projection I (D * top) ≤ refinement_projection I D ›
  for D :: ‹'a::sep_monoid set›
  unfolding refinement_projection_def mult.assoc set_top_times_idem ..


subsection ‹Instances›

subsubsection ‹Itself›

lemma Itself_refinement_projection:
  ‹ S ≤ S'
⟹ refinement_projection Itself S ≤ S' * top›
  unfolding refinement_projection_def
  by (clarsimp simp add: set_mult_expn, blast)

lemma Itself_refinement:
  ‹{(u,v)} * Id_on top 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 {(u,v)} 𝗐.𝗋.𝗍 Itself 𝗂𝗇 {u}›
  for u :: ‹'a::{sep_cancel,sep_semigroup}›
  unfolding Fictional_Forward_Simulation_def
  by (clarsimp simp add: subset_iff set_mult_expn,
      metis sep_cancel sep_disj_multD1 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_assoc)


subsubsection ‹Composition›




lemma sep_refinement_stepwise:
  ‹ S1 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S2 𝗐.𝗋.𝗍 Ia 𝗂𝗇 D
⟹ S2 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S3 𝗐.𝗋.𝗍 Ib 𝗂𝗇 D'
⟹ refinement_projection Ib D' ≤ D
⟹ S1 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S3 𝗐.𝗋.𝗍 (Ia ⨾ Ib) 𝗂𝗇 D'›
  for Ia :: ‹('a::sep_magma_1, 'b::sep_magma_1) φ›
  unfolding Fictional_Forward_Simulation_def refinement_projection_def
  apply (auto simp add: subset_iff Image_def Bex_def less_eq_BI_iff set_mult_expn split_option_all)
  subgoal premises prems for x r R t u v xb
  proof -
    have ‹∃x. (∃u v. x = u * v ∧ u ⊨ Ia (xb * 1) ∧ v ⊨ R ∧ u ## v) ∧ xb ## 1 ∧ xb ∈ D ∧ (x, t) ∈ S1›
      using prems(10) prems(3) prems(4) prems(5) prems(6) prems(7) prems(8) prems(9) by fastforce
    note prems(1)[THEN spec[where x=xb],THEN spec[where x=1],THEN spec[where x=‹R›],THEN spec[where x=‹t›],
          THEN mp, OF this]
    then show ?thesis
      apply clarsimp
      subgoal premises prems2 for y u'' v''
      proof -
        have ‹∃xa. (∃u v. xa = u * v ∧ u ⊨ Ib (x * r) ∧ v ⊨ Itself 1 ∧ u ## v) ∧ x ## r ∧ x ∈ D' ∧ (xa, y) ∈ S2›
          by (simp, rule exI[where x=xb], simp add: prems2 prems)
        note prems(2)[THEN spec[where x=x],THEN spec[where x=r],THEN spec[where x=‹Itself 1›], THEN spec[where x=y],
                THEN mp, OF this]
        then show ?thesis
          apply clarsimp
          using prems2(3) prems2(4) prems2(5) by auto
      qed .
  qed .

lemma sep_refinement_stepwise':
  ‹ S1 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S2 𝗐.𝗋.𝗍 Ia 𝗂𝗇 D
⟹ S2' 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S3 𝗐.𝗋.𝗍 Ib 𝗂𝗇 D'
⟹ refinement_projection Ib D' ≤ D
⟹ S2 ≤ S2'
⟹ S1 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 S3 𝗐.𝗋.𝗍 (Ia ⨾ Ib) 𝗂𝗇 D'›
  for Ia :: ‹'b::sep_magma_1 ⇒ 'a::sep_magma_1 BI›
  using refinement_sub_fun sep_refinement_stepwise
  by metis

lemma refinement_projections_stepwise:
  ‹refinement_projection (Ia ⨾ Ib) D ≤ refinement_projection Ia (refinement_projection Ib D)›
  for Ia :: ‹('c::sep_magma_1, 'a::sep_monoid) φ›
  unfolding refinement_projection_def
  apply (clarsimp simp add: Bex_def less_eq_BI_iff set_mult_expn)
  subgoal for x x' u v
    by (metis mult_1_class.mult_1_right sep_magma_1_left) .

lemma refinement_projections_stepwise_UNIV_paired:
  ‹ refinement_projection Ia Da ≤ Dc * top
⟹ refinement_projection Ib Db ≤ Da * top
⟹ refinement_projection (Ia ⨾ Ib) Db ≤ Dc * top ›
  for Ia :: ‹('c::sep_magma_1, 'a::sep_monoid) φ›
  using refinement_projections_stepwise
  by (metis (no_types, opaque_lifting) order.trans refinement_projection_UNIV_times_D refinement_projection_mono)


subsubsection ‹Function, pointwise›

definition [simp]: "ℱ_finite_product I f = prod (λx. I x (f x)) (dom1 f)"

lemma ℱ_finite_product_split:
  " finite (dom1 f)
⟹ (⋀k. homo_one (I k))
⟹ ℱ_finite_product I f = I k (f k) * ℱ_finite_product I (f(k:=1))
   ∧ ℱ_finite_product I (f(k:=1)) ## I k (f k)"
  for I :: ‹'a ⇒ 'b::sep_algebra ⇒ 'c::sep_algebra BI›
  by (simp add: homo_one_def,
      smt (verit, best) dom1_upd fun_upd_triv mult.comm_neutral mult.commute prod.insert_remove)



(*
definition "ℱ_fun I = ℱ_fun' (λ_. I)"

lemma ℱ_fun_ℐ[simp]: "ℐ (ℱ_fun I) = (λf. prod (ℐ I o f) (dom1 f))"
  unfolding ℱ_fun_def by simp

lemma ℱ_fun_split:
  " finite (dom1 f)
⟹ ℐ (ℱ_fun I) f = ℐ (ℱ_fun I) (f(k:=1)) * ℐ I (f k)
  ∧ ℐ (ℱ_fun I) (f(k:=1)) ## ℐ I (f k)"
  for f :: "'a ⇒ 'b::sep_algebra"
  unfolding ℱ_fun_def using ℱ_fun'_split .

lemma ℱ_interp_fun_ℐ_1_fupdt[simp]: "ℐ (ℱ_fun I) (1(k:=v)) = ℐ I v" by simp
*)
(*
definition "ℱ_pointwise I = Interp (λf. {g. ∀x. g x ∈ ℐ I (f x) })"

lemma ℱ_pointwise_ℐ[simp]:
  "ℐ (ℱ_pointwise I) = (λf. {g. ∀x. g x ∈ ℐ I (f x) })"
  unfolding ℱ_pointwise_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def one_fun_def fun_eq_iff)

lemma ℱ_pointwise_Itself:
  ‹ℱ_pointwise Itself = Itself›
  by (rule interp_eq_I; simp add: fun_eq_iff set_eq_iff) *)

definition [simp]: "ℱ_pointwise I f = BI {g. ∀x. g x ⊨ (I x) (f x)}"

lemma ℱ_pointwise_homo_one[simp, locale_intro]:
  ‹ (⋀k. homo_one (I k))
⟹ homo_one (ℱ_pointwise I)›
  unfolding homo_one_def by (simp add: BI_eq_iff) fastforce

lemma ℱ_pointwise_Itself:
  ‹ℱ_pointwise (λ_. Itself) = Itself›
  by (simp add: fun_eq_iff BI_eq_iff)

lemma ℱ_pointwise_projection:
  ‹ refinement_projection (I k) D' ≤ D * top
⟹ refinement_projection (ℱ_pointwise I) (fun_upd 1 k ` D') ≤ fun_upd 1 k ` D * top›
  for D :: ‹'b::sep_monoid set›
  apply (clarsimp simp add: subset_iff Bex_def image_iff set_mult_expn times_fun
            refinement_projection_def)
  subgoal premises prems for t u xb
  proof -
    have t1: ‹xb ## u k›
      by (metis fun_upd_same prems(3) sep_disj_fun)
    have ‹∃x. (∃xa. (∃u v. xa = u * v ∧ u ∈ D' ∧ u ## v) ∧ x = BI.dest (I k xa)) ∧ t k ∈ x›
      by (metis Satisfaction_def prems(2) prems(4) t1)
    note prems(1)[THEN spec[where x=‹t k›], THEN mp, OF this]
    then show ?thesis
      apply clarsimp
      subgoal premises prems2 for u' v'
        by (rule exI[where x=‹1(k := u')›], rule exI[where x=‹t(k := v')›],
            simp add: fun_eq_iff prems2 sep_disj_fun_def times_fun) .
  qed .

lemma ℱ_pointwise_refinement:
  ‹ A * Id_on top 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 B 𝗐.𝗋.𝗍 I k 𝗂𝗇 D
⟹ pairself (fun_upd 1 k) ` A * Id_on top 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 pairself (fun_upd 1 k) ` B
    𝗐.𝗋.𝗍 ℱ_pointwise I 𝗂𝗇 fun_upd 1 k ` D›
  for I :: ‹'c ⇒ 'b::sep_magma_1 ⇒ 'a::sep_magma_1 BI›
  unfolding Fictional_Forward_Simulation_def
  apply (clarsimp simp add: set_mult_expn image_iff Image_def subset_iff Bex_def times_fun Id_on_iff)
  subgoal premises prems for r R u v xb xc a b
  proof -
thm prems
    have t1[simp]: ‹a ## xc k›
      by (metis fun_upd_same prems(8) sep_disj_fun)
    have t2[simp]: ‹b ## xc k›
      by (metis fun_upd_same prems(9) sep_disj_fun)
    have ‹∃x. (∃u va. x = u * va ∧ u ⊨ I k (xb * r k) ∧ va ⊨ Itself (v k) ∧ u ## va) ∧
     xb ## r k ∧ xb ∈ D ∧ (∃a ba aa. x = a * aa ∧ b * xc k = ba * aa ∧ (a, ba) ∈ A ∧ a ## aa ∧ ba ## aa)›
      by (auto simp add: prems,
          smt (verit, ccfv_threshold) fun_upd_same prems(10) prems(2) prems(3) prems(5) prems(7) sep_disj_fun_def t1 t2 times_fun_def)
    note prems(1)[THEN spec[where x=xb], THEN spec[where x=‹r k›], THEN spec[where x=‹Itself (v k)›], THEN spec[where x=‹b * xc k›],
          THEN mp, OF this]
    then show ?thesis
      apply clarsimp
      subgoal premises prems2 for y v'
      proof -
        have t4: ‹u(k := v') ## v›
          by (clarsimp simp add: sep_disj_fun_def prems2 prems(7)) (simp add: prems(7))
        have t3: ‹1(k := b) * xc = u(k := v') * v›
          by (clarsimp simp add: fun_eq_iff times_fun prems2,
              metis (mono_tags, opaque_lifting) fun_upd_apply mult_1_class.mult_1_left prems(5) times_fun)
        show ?thesis
          by (rule exI[where x=‹1(k := y)›]; simp add: prems prems2; rule,
              smt (verit, ccfv_SIG) fun_split_1 fun_upd_other fun_upd_same prems(3) prems(6) prems2(4) t3 t4 times_fun_def,
              metis fun_sep_disj_1_fupdt(2) fun_upd_triv prems2(1) prems2(2))
      qed .
  qed .

(* subsubsection ‹Pairwise›

definition "ℱ_pair I1 I2 = (λ(x,y). I1 x * I2 y) "

lemma ℱ_pair[simp]: "ℱ_pair I1 I2 (x,y) = I1 x * I2 y"
  for I1 :: "('a::one,'b::sep_monoid) interp"
  unfolding ℱ_pair_def by (simp add: one_prod_def)

notation ℱ_pair (infixl "∙⇩ℱ" 50)


subsubsection ‹Option›

definition "ℱ_option I = Interp (case_option 1 I)"

lemma ℱ_option_ℐ[simp]: "ℐ (ℱ_option I) = (case_option 1 I)"
  unfolding ℱ_option_def
  by (rule Interp_inverse) (simp add: Interpretation_def)


definition "ℱ_optionwise I = Interp (λx. case x of Some x' ⇒ Some ` I x' | _ ⇒ {None})"

lemma ℱ_optionwise_ℐ[simp]:
  "ℐ (ℱ_optionwise I) = (λx. case x of Some x' ⇒ Some ` I x' | _ ⇒ {None})"
  unfolding ℱ_optionwise_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def)
*)

(* subsubsection ‹Partiality›

definition "fine I = Interp (case_fine (ℐ I) {})"
lemma fine_ℐ[simp]: "ℐ (fine I) = case_fine (ℐ I) {}"
  unfolding fine_def by (rule Interp_inverse) (simp add: Interpretation_def one_fine_def)

definition "defined I = Interp (λx. Fine ` ℐ I x)"
lemma defined_ℐ[simp]: "ℐ (defined I) = (λx. Fine ` ℐ I x)"
  unfolding defined_def
  by (rule Interp_inverse) (auto simp add: Interpretation_def one_fine_def)

definition "partialwise I = ℱ_fine (defined I)"
lemma partialwise_ℐ[simp]: "ℐ (partialwise I) (Fine x) = { Fine y |y. y ∈ ℐ I x }"
  unfolding partialwise_def by auto
*)

subsubsection ‹Functional Fiction›

definition [simp]: ‹ℱ_functional ψ D x = BI {y. x = ψ y ∧ y ∈ D }›

(* lemma (in kernel_is_1) ℱ_functional_ℐ[simp]:
  ‹ℐ (ℱ_functional ψ) = (λx. {y. x = ψ y})›
  unfolding ℱ_functional_def
  by (rule Interp_inverse, simp add: Interpretation_def one_set_def set_eq_iff inj_at_1) *)

lemma ℱ_functional_homo_one[simp, locale_intro]:
  ‹ simple_homo_mul ψ D
⟹ homo_one (ℱ_functional ψ D)›
  unfolding homo_one_def ℱ_functional_def simple_homo_mul_def
  by (clarsimp simp add: BI_eq_iff Ball_def; blast)

(*TODO: move this or remove this*)
lemma map_option_inj_at_1[simp]:
  ‹simple_homo_mul (map_option f) top›
  unfolding one_option_def simple_homo_mul_def
  by (simp add: split_option_all)

lemma (in sep_orthogonal_monoid) ℱ_functional_projection:
  ‹ S ≤ D
⟹ refinement_projection (ℱ_functional ψ D) (ψ ` S) ≤ S * top›
  unfolding refinement_projection_def
  by (clarsimp simp add: subset_iff set_mult_expn eq_commute[where a=‹ψ _›] sep_orthogonal; blast)

lemma ℱ_functional_pointwise:
  ‹ℱ_functional ((∘) ψ) (pointwise_set D) = ℱ_pointwise (λ_. ℱ_functional ψ D)›
  by (auto simp add: fun_eq_iff set_eq_iff; simp add: pointwise_set_def)

lemma ℱ_functional_comp:
  ‹ g ` Dg ≤ Df
⟹ ℱ_functional (f o g) Dg = (ℱ_functional g Dg ⨾ ℱ_functional f Df)›
  by (auto simp add: fun_eq_iff BI_eq_iff)
  

(* definition "ℱ_share s = (case s of Share w v ⇒ if w = 1 then {v} else {})"

lemma ℱ_share_ℐ[simp]: "ℱ_share (Share w v) = (if w = 1 then {v} else {})"
  unfolding ℱ_share_def by simp *)

(* lemma In_ficion_fine [simp]:
  ‹x ∈ (case some_fine of Fine y ⇒ f y | Undef ⇒ {})
        ⟷ (∃y. some_fine = Fine y ∧ x ∈ f y)›
  by (cases some_fine; simp)
*)

subsubsection ‹Agreement›

(* TODO: check this!!!!
definition ‹ℱ_agree = (λx. case x of agree x' ⇒ {x'})› *)


subsection ‹Refinement of Algebraic Structures›

subsubsection ‹Cancellative Separation Insertion Homomorphism›

(*
lemma refinement_projection:
  ‹ kernel_is_1 ψ
⟹ Id_on UNIV * {(a, b)} 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 pairself ψ ` {(a,b)} 𝗐.𝗋.𝗍 ℱ_functional ψ 𝗂𝗇 ψ ` {a}›
  unfolding Fictional_Forward_Simulation_def
  apply (clarsimp simp add: set_mult_expn Subjection_expn_set)
subgoal for r R u v w *)

definition ℱ_functional_condition
  where ‹ℱ_functional_condition D ⟷ (∀r x y. x ## r ∧ y ## r ∧ r ∈ D ∧ x ∈ D ∧ x * r ∈ D ∧ y ∈ D ⟶ y * r ∈ D)›

lemma ℱ_functional_condition_UNIV[simp]:
  ‹ℱ_functional_condition top›
  unfolding ℱ_functional_condition_def by simp

definition frame_preserving_relation ― ‹TODO: UGLY?›
  where ‹frame_preserving_relation R
    ⟷ (∀a b c d r w. (a,b) ∈ R ∧ (c,d) ∈ R ∧ a * r = c * w ∧ a ## r ∧ b ## r ∧ c ## w
            ⟶ b * r = d * w ∧ d ## w)›

context cancl_sep_orthogonal_monoid begin

lemma ℱ_functional_refinement_complex:
  ‹ (∀a b. (a,b) ∈ R ⟶ a ∈ D ∧ b ∈ D)
⟹ frame_preserving_relation R
⟹ Sep_Closed D
⟹ R * Id_on UNIV 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 pairself ψ ` R 𝗐.𝗋.𝗍 ℱ_functional ψ D 𝗂𝗇 ψ ` (Domain R) ›
  unfolding Fictional_Forward_Simulation_def
  by (auto simp add: set_mult_expn sep_orthogonal Sep_Closed_def image_iff Bex_def,
      smt (z3) frame_preserving_relation_def homo_mult sep_disj_homo_semi sep_disj_multD1 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_assoc)

lemma ℱ_functional_refinement:
  ‹ a ∈ D ∧ b ∈ D
⟹ ℱ_functional_condition D
⟹ {(a, b)} * Id_on UNIV 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 pairself ψ ` {(a,b)} 𝗐.𝗋.𝗍 ℱ_functional ψ D 𝗂𝗇 ψ ` {a} ›
  unfolding Fictional_Forward_Simulation_def ℱ_functional_condition_def
  apply (auto simp add: set_mult_expn sep_orthogonal)
  apply (metis (no_types, lifting) homo_mult sep_cancel sep_disj_multD1 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_assoc)
  by (metis sep_cancel sep_disj_homo_semi sep_disj_multD1 sep_disj_multD2 sep_disj_multI2 sep_mult_assoc)

lemma ℱ_functional_refinement':
  ‹ a ∈ D ∧ B ⊆ D
⟹ ℱ_functional_condition D
⟹ {(a, b) |b. b∈B} * Id_on UNIV 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 pairself ψ ` {(a,b) |b. b∈B} 𝗐.𝗋.𝗍 ℱ_functional ψ D 𝗂𝗇 ψ ` {a} ›
  unfolding Fictional_Forward_Simulation_def ℱ_functional_condition_def
  by (auto simp add: set_mult_expn sep_orthogonal,
      smt (verit) homo_mult sep_cancel sep_disj_homo_semi sep_disj_multD1 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_assoc subsetD)


end

subsubsection ‹Cancellative Permission Insertion Homomorphism›


context cancl_share_orthogonal_homo begin

lemma refinement_projection_half_perm:
  ‹S ⊆ D ⟹ 0 < n ⟹ refinement_projection (ℱ_functional ψ D) ((share n o ψ) ` S) ⊆ S * UNIV›
  unfolding refinement_projection_def
  by (auto simp add: set_mult_expn sep_orthogonal share_orthogonal';
      cases ‹n ≤ 1›,
      ((insert share_orthogonal_homo.share_orthogonal' share_orthogonal_homo_axioms, blast)[1],
       metis in_mono leI sep_orthogonal share_bounded share_right_one))


end



end