Theory Phi_BI.Phi_Preliminary

chapter ‹Theoretical Foundations›

section ‹Preliminary›

theory Phi_Preliminary
  imports Main "Phi_BI.Algebras" PhiTool_Symbol Phi_Aug
          Phi_Logic_Programming_Reasoner.PLPR
          Phi_Logic_Programming_Reasoner.PLPR_error_msg
          Phi_BI.Arrow_st
  keywords "optional_translations" :: thy_decl
       and "optional_translation_group" :: thy_decl
       and "φadhoc_overloading" "φno_adhoc_overloading" :: thy_decl
  abbrevs "<implies>" = "𝗂𝗆𝗉𝗅𝗂𝖾𝗌"
      and "<suffices>" = "𝗌𝗎𝖿𝖿𝗂𝖼𝖾𝗌"
begin

(* declare [[ML_debugger, ML_exception_debugger, ML_print_depth=100]] *)

subsection ‹Named Theorems›

ML ‹structure Phi_Expansions = Simpset (
  val initial_ss = Simpset_Configure.Empty_SS
  val binding = SOME \<^binding>‹φexpns›
  val comment = "Semantics Expansions, used to expand assertions semantically."
  val attribute = NONE
  val post_merging = I
)›

declare set_mult_expn[φexpns] Premise_def[φexpns]

ML ‹
structure Phi_Programming_Simp_SS = Simpset (
  val initial_ss = Simpset_Configure.Empty_SS
  val binding = SOME \<^binding>‹φprogramming_simps›
  val comment = "Simplification rules used in the deductive programming, including the φprogramming_base_simps."
  val attribute = NONE
  val post_merging = I
)
― ‹A trick: if a φprogramming_simp rule is also declared in the system simpset, just declare it
    by φprogramming_base_simps, and it can improve the performance.›

structure Phi_Programming_Base_Simp_SS = Simpset (
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = SOME \<^binding>‹φprogramming_base_simps›
  val comment = "Simplification rules used only in low level automation"
  val attribute = NONE
  val post_merging = I
)

structure Phi_Programming_Simp_Hook = Hooks (
  type arg = unit
  type state = Proof.context
)

fun equip_Phi_Programming_Simp lev ctxt =
  if lev >= 2
  then ctxt
    |> Context_Position.set_visible false
    |> Phi_Programming_Simp_SS.enhance
    |> Phi_Programming_Simp_Hook.invoke (Context.Proof ctxt) ()
    |> Context_Position.restore_visible ctxt
  else ctxt
    |> Context_Position.set_visible false
    |> Phi_Programming_Simp_SS.enhance o Phi_Programming_Base_Simp_SS.equip
    |> Phi_Programming_Simp_Hook.invoke (Context.Proof ctxt) ()
    |> Context_Position.restore_visible ctxt

signature PHI_TYPE_ALGEBRA_DERIVERS = sig
structure Expansion : SIMPSET (*The standard simpset for deriving*)
end

structure Phi_Type_Algebra_Derivers : PHI_TYPE_ALGEBRA_DERIVERS = struct
structure Expansion = Simpset (
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = SOME \<^binding>‹φderiver_simps›
  val comment = "Rules unfolding constraints and conditions in property deriving of φ-type algebra.\n\
                \Basically, simplification rules for object operators including mappers, relators, \
                \predicators of the abstract algebra of φ-types"
  val attribute = NONE
  val post_merging = I
)
end

›

setup ‹Context.theory_map (
     Phi_Programming_Base_Simp_SS.map (fn ctxt =>
       ctxt addsimprocs [\<^simproc>‹NO_MATCH›, \<^simproc>‹defined_All›, \<^simproc>‹defined_Ex›])
  #> Phi_Programming_Simp_Hook.add 1000 (fn _ => fn ctxt =>
       ctxt delsimps @{thms' One_nat_def}))›



subsection ‹Error Mechanism›

ML_file ‹library/tools/error.ML›


subsection ‹Helper ML›

ML_file ‹library/tools/Phi_Help.ML›
ML_file ‹library/tools/lift_type_sort.ML›
ML_file ‹library/syntax/helps.ML›
ML_file ‹library/system/Phi_Envir0.ML›
ML_file ‹library/system/Phi_ID.ML›
ML_file ‹library/tools/Hasher.ML›
ML_file ‹library/tools/cache_file.ML›
ML_file ‹library/tools/thy_hacks.ML›


(*
A JSON lib. Maybe one day in the cache file we will use JSON (or better some K-V data base)
instead of XML. I'm thinking of the performance of the XML, particularly we have a lot of
`<` and `>` symbols. Need some tests.

ML_file ‹contrib/sml-json/json.sig›
ML_file ‹contrib/sml-setmap/map/MONO_MAP.sig›
ML_file ‹contrib/sml-setmap/map/OrderMapImpl.sml›
ML_file ‹contrib/sml-setmap/map/OrderMap.sml›
ML_file ‹contrib/sml-setmap/map/StringMap.sml›
ML_file ‹contrib/sml-json/json.sml› *)

subsection ‹Helper Methods›

method_setup subgoal' = ‹
     Scan.lift (Scan.option (\<^keyword>‹premises› |-- Parse.binding))
  -- Scan.lift (Scan.option (\<^keyword>‹for› |-- Parse.and_list (Scan.repeat1 Parse.binding) >> flat))
  -- Scan.lift (Parse.token Parse.embedded) >>
 (fn ((prem_b, fixes), text_tok) => fn ctxt => fn rules =>
  let fun FOCUS tac ctxt i st =
        if Thm.nprems_of st < i then Seq.empty
        else let val (args as {context = ctxt', params, asms, prems, ...}, st') =
                    (if is_some prem_b then Subgoal.focus else Subgoal.focus_params_fixed) ctxt i fixes st
                 val ctxt' = case prem_b of SOME b =>
                                    Proof_Context.note_thms "" ((b,[]), map (fn th => ([th],[])) prems) ctxt'
                                      |> snd
                                | _ => ctxt'
              in Seq.lifts (Subgoal.retrofit ctxt' ctxt params asms i) (tac ctxt' st') st
             end
   in Context_Tactic.CONTEXT_TACTIC (HEADGOAL (FOCUS (fn ctxt =>
      let val (text, src) = Method.read_closure_input ctxt (Token.input_of text_tok)
       in Context_Tactic.NO_CONTEXT_TACTIC ctxt (Method.evaluate_runtime text ctxt rules)
      end) ctxt))
  end)
›

method_setup prefer_tac = ‹
    Scan.lift Parse.nat -- Scan.lift Parse.nat
  >> (fn (j,k) => fn ctxt => fn _ =>
  Context_Tactic.CONTEXT_TACTIC (fn th =>
    if Thm.nprems_of th = 0
    then Seq.empty
    else Seq.single (Thm.permute_prems j k th)))
›



subsection ‹Helper Lemmas›

(*TODO: IMPROVE ME!*)

(*declare Suc_le_eq[simp]*)
(*
lemma [simp]: ‹{ia. ia < Suc i } - {i} = {ia. ia < i}› for i :: nat
  by fastforce
*)
lemma proj_eq_pair_eq[simp]:
  ‹fst x = fst y ∧ snd x = snd y ⟷ x = y›
  using prod.expand by blast

lemma fst_snd_If_pair[simp]:
  ‹ fst (If C (a,b) (c,d)) = (If C a c) ›
  ‹ snd (If C (a,b) (c,d)) = (If C b d) ›
  by auto



(*
lemma [simp]:
  ‹list_all2 (λx y. snd x = snd y ∧ fst x = fst y) = (=)›
  by (auto simp: fun_eq_iff,
      smt (verit, ccfv_SIG) list.rel_eq list_all2_mono surjective_pairing,
      simp add: list.rel_refl)
*)
lemma imp_implication: "(P ⟶ Q ⟹ PROP R) ≡ ((P ⟹ Q) ⟹ PROP R)" by rule simp+

lemmas [φsafe_simp] = comb.K_app comb.K_comp comb.K_comp'

lemma case_sum_collapse[simp, φsafe_simp]:
  ‹case_sum Inl Inr = (λx. x)›
  unfolding fun_eq_iff
  by (clarsimp simp add: split_sum_all)

lemma snd_o_Pair_eq_id[simp, φsafe_simp]:
  ‹ snd ∘ Pair c = (λx. x) ›
  unfolding fun_eq_iff
  by simp

lemma apfst_id'[simp, φsafe_simp]:
  ‹apfst (λx. x) = (λx. x)›
  by (simp add: fun_eq_iff)

(*
lemma stupid_pair_eq_prj3[simp]:
  ‹snd (snd x) = snd (snd y) ∧ fst (snd x) = fst (snd y) ∧ fst x = fst y ⟷ x = y›
  by (meson prod.expand)
*)

ML_file ‹library/tools/help_lemmas.ML›

lemma nested_case_prod[no_atp, φprogramming_simps, φsafe_simp]:
  ‹ case_prod f⇩1 (case_prod f⇩2 x) = case_prod (λa b. case_prod f⇩1 (f⇩2 a b)) x›
  using prod.case_distrib .

lemmas [φprogramming_simps, φsafe_simp] =
  BNF_Fixpoint_Base.case_prod_app
  prod.case_distrib[where h=fst and f=‹λa b. (f⇩1 a b, f⇩2 a b)› for f⇩1 f⇩2, simplified]
  prod.case_distrib[where h=snd and f=‹λa b. (f⇩1 a b, f⇩2 a b)› for f⇩1 f⇩2, simplified]
  prod.case_distrib[where h=‹map_prod g⇩1 g⇩2› and f=‹λa b. (f⇩1 a b, f⇩2 a b)› for f⇩1 f⇩2 g⇩1 g⇩2, simplified]

lemmas [φprogramming_simps] =
  fst_def[symmetric] snd_def[symmetric]

setup ‹Context.theory_map (Phi_Safe_Simps.map (
  Simplifier.add_cong @{thm' mk_symbol_cong}
))›

(*simproc_setup case_prod_app (‹(case_prod f x) y›) = ‹fn _ => fn ctxt => fn ctm =>
  let val (Const(\<^const_name>‹case_prod›, _) $ f $ x $ y) = Thm.term_of ctm
   in SOME (Conv.rewr_conv @{thm' BNF_Fixpoint_Base.case_prod_app} ctm)
  end
›

lemma
  ‹ (case x of (a,b) ⇒ f a b) y = (case x of (a,b) ⇒ f a b y) ›
*)

subsubsection ‹Simple Boolean Conversions›

lemma boolean_conversions:
  ‹(C⇩R ∨ C⇩E) ∧ C⇩R ⟷ C⇩R›
  ‹(C⇩R ∨ C⇩E) ∧ C⇩E ⟷ C⇩E›
  ‹(C⇩W⇩1 ∨ C⇩W⇩2 ∨ C⇩E) ∧ C⇩W⇩2 ⟷ C⇩W⇩2›
  ‹(C⇩W⇩1 ∨ C⇩W⇩2 ∨ C⇩E) ∧ C⇩E ⟷ C⇩E›
  ‹(C⇩R⇩1 ∨ (C⇩R ∨ C⇩E) ∧ (C⇩W⇩2 ∨ C⇩E)) ⟷ (C⇩R⇩1 ∨ C⇩R ∨ C⇩E) ∧ (C⇩R⇩1 ∨ C⇩W⇩2 ∨ C⇩E)›
  ‹(C⇩R⇩1 ∨ C⇩R⇩2 ∨ C⇩E) ∧ (C⇩R⇩1 ∨ C⇩R⇩2) ⟷ C⇩R⇩1 ∨ C⇩R⇩2›
  by blast+


subsubsection ‹Setup Safe Simpset›

method_setup φsafe_simp = ‹
let val no_asmN = "no_asm";
    val no_asm_useN = "no_asm_use";
    val no_asm_simpN = "no_asm_simp";
    val asm_lrN = "asm_lr";

    fun conv_mode x =
      ((Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
        Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
        Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
        Scan.succeed asm_full_simp_tac) |> Scan.lift) x;
in conv_mode >> (fn simp => fn ctxt =>
    Method.METHOD (fn ths => Method.insert_tac ctxt ths 1 THEN simp (Phi_Safe_Simps.equip ctxt) 1 ))
end›


lemmas [φsafe_simp] =
    fmdom_fmupd fmdom_empty finsert_iff fempty_iff
    mk_symbol_inject[OF UNIV_I UNIV_I] fmadd_empty fmadd_idempotent
    fmadd_assoc fmadd_fmupd fmupd_idem

declare rel_fun_eq[iff]


subsection ‹Helper Attributes \& Tactics›

attribute_setup rotated = ‹Scan.lift (Scan.optional Parse.int 1 -- Scan.optional Parse.int 0) >>
  (fn (k,j) => Thm.rule_attribute [] (fn _ => Thm.permute_prems j k))›
  ‹Enhanced version of the Pure.rotated›

attribute_setup TRY_THEN = ‹(Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
      >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B) handle THM _ => A)))
    › "resolution with rule, and do nothing if fail"

ML ‹
val phi_system_ML_attribute_locker_do_not_override = Mutex.mutex ()
val phi_system_ML_attribute_sender_do_not_override : (morphism -> Thm.attribute) option Unsynchronized.ref =
      Unsynchronized.ref NONE
fun phi_system_read_ML_attribute generic src =
  let val _ = Mutex.lock phi_system_ML_attribute_locker_do_not_override
      val _ =   ML_Context.expression (Input.pos_of src)
              ( ML_Lex.read "phi_system_ML_attribute_sender_do_not_override := SOME (("
              @ ML_Lex.read_source src
              @ ML_Lex.read ") : morphism -> Thm.attribute)") generic
            handle err => (
              Mutex.unlock phi_system_ML_attribute_locker_do_not_override;
              raise err)
      val attr = the (@{print} (!phi_system_ML_attribute_sender_do_not_override))
      val _ = Mutex.unlock phi_system_ML_attribute_locker_do_not_override;
  in attr
  end
val phi_system_ML_attribute_parser = (
   Scan.lift Args.internal_attribute
|| Scan.peek (fn ctxt => Parse.token Parse.ML_source >>
    Token.evaluate Token.Attribute (fn tok => 
let val src = Token.input_of tok
in Morphism.entity (phi_system_read_ML_attribute ctxt src)
end )))
›

attribute_setup ML_attribute = ‹
  phi_system_ML_attribute_parser >> Morphism.form›
  ‹Use ML directly in an attribute without defining a new attribute if you just
  want to use it here specifically›


subsection ‹Helper Objects›

consts 𝒜infer :: action

subsubsection ‹Unspecified value›

consts unspec :: 'a
axiomatization ― ‹this axiomatization is definitional, where it defines the ‹unspec› on product type›
  where unspec_prod: ‹unspec = (unspec, unspec)›



subsubsection ‹Embedding Function into Relation›

definition embedded_func :: ‹('a ⇒ 'b) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool›
  where ‹embedded_func f P = (λx y. y = f x ∧ P x)›

lemma embedded_func_red[iff, φsafe_simp]:
  ‹ embedded_func f P x y ⟷ y = f x ∧ P x ›
  unfolding embedded_func_def
  by simp

subsubsection ‹Big Number›

text ‹A tag to suppress unnecessary expanding of big numbers like ‹2^256›
  (*deprecated! use ‹declare power_numeral[simp del]› instead!*)›

definition ‹Big x = x›

lemma [iff]:
  ‹(2::nat) ^ Big 8  = 256›
  ‹(2::nat) ^ Big 16 = 65536›
  ‹(2::nat) ^ Big 32 = 4294967296›
  by (simp add: Big_def)+

lemma [iff]:
  ‹ numeral x < (2::'a) ^ Big n ⟷ numeral x < (2::'a::{numeral,power,ord}) ^ n›
  ‹ 1 < (2::'a) ^ Big n ⟷ 1 < (2::'a::{numeral,power,ord}) ^ n›
  ‹ 0 < (2::'b) ^ Big n ⟷ 0 < (2::'b::{numeral,power,ord,zero}) ^ n›
  ‹ n < 16 ⟹ Big n = n ›
  unfolding Big_def by simp+



subsubsection ‹Product›


text ‹An algorithm of normalizing tuple operations.

Primitive operations:

▪ rotL : left rotation
▪ rotR : right rotation
▪ prod.swap
▪ fst, snd
▪ apfst, apsnd, map_prod

Composite operations are only combined from the primitive operations and functional composition.
‹case_prod› is not allowed (because it mixes operations together and cannot be separated any more,
cause certain operations that could be reduced e.g. ‹map (apfst f) o zip_list ≡ zip_list o apfst f›
cannot be reduced any more).

We apply the following normalization strategy to hope two equivalent sequences of the operations can
be normalized to an identical form.

▪ apfst, apsnd, map_prod are aggregated together, and split to each projection when need.
  They are swapped over prod.swap, rotations, down to the left most.
  The reason is, projectors (fst, snd) are always given at the left side, so we hope when the projectors
  meet the apfst, apsnd, map_prod first, their reduction can eliminate irrelevant mappings as early
  as possible.
▪ swap, rotation are reduced if possible, i.e. the following 6 rules
    (S for swap, L for L-rotate, R for R-rotate, A B for A o B, rewrites from LHS to RHS)
    L S L S = S R
    S L S L = R S
    S R S = L S L
    R S R = S L S
    L R = id, R L = id

Key facts why this normalization can work are,
1. Below, we only need to consider operations ‹h = apfst f | apsnd g›, and we split ‹map_prod f g›
   to ‹apfst f o apsnd g› and consider them separately.
   Note any ‹h› can swap over ‹S›.
2. any operation ‹h› that can swap over LHS in any of the equation above, can also swap over the RHS
   and result in an identical form.
3. S L S h L, if h can swap over the right L, h can also swap over the left ‹S L S›
   Similarly for the other rewrites.
4. L S h L, if h can swap over the right L to ‹h'›, ‹h'› can also swap over ‹S R S› from right,
   and results in the identical form with ‹h› swapping over ‹L S› from right
It means, swapping any ‹h› in any order towards the left end, doesn't break the normalization-ability.
The order doesn't matter.

So, any ‹apfst, apsnd, map_prod› can be swapped to the left most end, if it can.

Now, the sequence only remains ‹S, L, R›, ... the proof is to be completed

idk, maybe we lost some assumption, like, requiring the first projection of the tuple is always
single-element or a pair but no more nested level.

I am not sure if the normaliza is complete but is terminating.
›

named_theorems prod_opr_norm ‹normalizations of product operations›

notation map_prod (infixr "⊗⇩f" 56)

(*if C⇩R⇩1 then *)
setup ‹Sign.mandatory_path "prod"›

lemma map_beta[φsafe_simp]:
  ‹(f ⊗⇩f g) x = (f (fst x), g (snd x))›
  by (cases x; simp)

lemma map_pairewise_eq[φsafe_simp]:
  ‹ (f ⊗⇩f g) = (f' ⊗⇩f g') ⟷ f = f' ∧ g = g' ›
  unfolding fun_eq_iff
  by clarsimp

lemma map_unspec[φsafe_simp]:
  ‹ (λ_. unspec) ⊗⇩f (λ_. unspec) = (λ_. unspec) ›
  unfolding fun_eq_iff
  by (clarsimp simp: unspec_prod)

lemma map_unspec_eq[φsafe_simp]:
  ‹ f ⊗⇩f g = (λ_. unspec) ⟷ f = (λ_. unspec) ∧ g = (λ_. unspec) ›
  unfolding fun_eq_iff
  by (clarsimp simp: unspec_prod)

lemma case_prod_map_prod[simp, φsafe_simp]:
  ‹(case (f ⊗⇩f g) x of (a,b) ⇒ r a b) = (case x of (a,b) ⇒ let a' = f a ; b' = g b in r a' b')›
  unfolding Let_def
  using BNF_Fixpoint_Base.case_prod_map_prod .


definition rotL :: ‹'a × 'b × 'c ⇒ ('a × 'b) × 'c›
  where ‹rotL x = ((fst x, fst (snd x)), snd (snd x))›

definition rotR :: ‹('a × 'b) × 'c ⇒ 'a × 'b × 'c›
  where ‹rotR x = (fst (fst x), snd (fst x), snd x)›

abbreviation rpair :: ‹'a ⇒ 'b ⇒ 'b × 'a›
  where ‹rpair x ≡ prod.swap o Pair x›

lemma rot[simp, φsafe_simp]:
  ‹prod.rotL (a,b,c) = ((a,b),c)›
  ‹prod.rotR ((a,b),c) = (a,b,c)›
  unfolding prod.rotL_def prod.rotR_def
  by simp_all

lemma rot_rot_comp[simp, φsafe_simp]:
  ‹ prod.rotL o prod.rotR = id ›
  ‹ prod.rotR o prod.rotL = id ›
  unfolding fun_eq_iff
  by simp_all

lemmas rot_rot_comp'[simp, φsafe_simp] = prod.rot_rot_comp[THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]
lemmas rot_rot[simp, φsafe_simp] = prod.rot_rot_comp[unfolded fun_eq_iff comp_def id_def, THEN spec]
 
lemma
  ‹fst (prod.rotL x) = (fst x, fst (snd x))›
  ‹snd (prod.rotR y) = (snd (fst y), snd y)›
  by ((cases x; simp),
      (cases y; clarsimp))

lemma rot_prj_comp[simp, φsafe_simp]:
  ‹fst o prod.rotL = apsnd fst›
  ‹snd o prod.rotL = snd o snd›
  ‹fst o prod.rotR = fst o fst›
  ‹snd o prod.rotR = apfst snd›
  unfolding prod.rotL_def prod.rotR_def fun_eq_iff
  by simp_all

lemmas rot_prj[simp, φsafe_simp] = prod.rot_prj_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas rot_prj_comp'[simp, φsafe_simp] = prod.rot_prj_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma prj_Pair_comp[simp, φsafe_simp]:
  ‹fst o Pair x = comb.K x›
  ‹snd o Pair x = id›
  unfolding fun_eq_iff
  by simp_all

lemmas prj_Pair_comp' [simp, φsafe_simp] = prod.prj_Pair_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma ap_prj⇩0_rot_comp[simp, φsafe_simp]:
  ‹(f ⊗⇩f fst) o prod.rotR = apfst f o fst›
  ‹(f ⊗⇩f snd) o prod.rotR = apfst (f o fst)›
  ‹(snd ⊗⇩f g) o prod.rotL = apsnd g o snd›
  ‹(fst ⊗⇩f g) o prod.rotL = apsnd (g o snd)›
  ‹apsnd fst o prod.rotR = fst›
  ‹apsnd snd o prod.rotR = apfst fst›
  ‹apfst snd o prod.rotL = snd›
  ‹apfst fst o prod.rotL = apsnd snd›
  unfolding fun_eq_iff
  by simp_all

lemmas ap_prj⇩0_rot[simp, φsafe_simp] = prod.ap_prj⇩0_rot_comp[unfolded fun_eq_iff comp_def id_def, THEN spec]
lemmas ap_prj⇩0_rot_comp'[simp, φsafe_simp] = prod.ap_prj⇩0_rot_comp[THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma ap_prj_rot_comp[simp, φsafe_simp]:
  ‹(f ⊗⇩f (g o fst)) o prod.rotR = (f ⊗⇩f g) o fst›
  ‹(f ⊗⇩f (g o snd)) o prod.rotR = (f o fst) ⊗⇩f g›
  ‹((f o snd) ⊗⇩f g) o prod.rotL = (f ⊗⇩f g) o snd›
  ‹((f o fst) ⊗⇩f g) o prod.rotL = f ⊗⇩f (g o snd)›
  ‹apsnd (g o fst) o prod.rotR = apsnd g o fst›
  ‹apsnd (g o snd) o prod.rotR = fst ⊗⇩f g›
  ‹apfst (f o snd) o prod.rotL = apfst f o snd›
  ‹apfst (f o fst) o prod.rotL = f ⊗⇩f snd›
  unfolding fun_eq_iff
  by simp_all

lemmas ap_prj_rot[simp, φsafe_simp] = prod.ap_prj_rot_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas ap_prj_rot_comp'[simp, φsafe_simp] = prod.ap_prj_rot_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma ap_rotate_comp[no_atp, prod_opr_norm]:
  ‹prod.rotL o apfst f = apfst (apfst f) o prod.rotL›
  ‹prod.rotL o apsnd (apfst f) = apfst (apsnd f) o prod.rotL›
  ‹prod.rotL o apsnd (apsnd f) = apsnd f o prod.rotL›
  ‹prod.rotL o apsnd (f⇩1 ⊗⇩f f⇩2) = (apsnd f⇩1 ⊗⇩f f⇩2) o prod.rotL›
  ‹prod.rotR o apfst (apfst f o f'⇩1) = apfst f o prod.rotR o apfst f'⇩1›
  ‹prod.rotR o apsnd f = apsnd (apsnd f) o prod.rotR›
  ‹prod.rotR o apfst (apsnd f) = apsnd (apfst f) o prod.rotR›
  ‹prod.rotR o apfst (apsnd f o f') = apsnd (apfst f) o prod.rotR o apfst f'›
  ‹prod.rotR o apfst (f⇩1 ⊗⇩f f⇩2) = (f⇩1 ⊗⇩f apfst f⇩2) o prod.rotR›
  ‹prod.rotL o (g⇩1 ⊗⇩f g⇩2 ⊗⇩f g⇩3) = ((g⇩1 ⊗⇩f g⇩2) ⊗⇩f g⇩3) o prod.rotL›
  ‹prod.rotR o ((f⇩1 ⊗⇩f f⇩2) ⊗⇩f f⇩3) = (f⇩1 ⊗⇩f f⇩2 ⊗⇩f f⇩3) o prod.rotR›
  unfolding fun_eq_iff prod.rotR_def
  by (clarsimp)+

lemmas ap_rotate[no_atp, prod_opr_norm] = prod.ap_rotate_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas ap_rotate_comp'[no_atp, prod_opr_norm] = prod.ap_rotate_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]




lemma rotate_eq_simp[simp, φsafe_simp]:
  ‹((a,b),c) = prod.rotL x ⟷ (a,b,c) = x›
  ‹(a,b,c) = prod.rotR y ⟷ ((a,b),c) = y›
  unfolding prod.rotL_def prod.rotR_def
  by (clarsimp; rule; clarsimp)+

lemma rotate_eq_ap_simp[simp, φsafe_simp]:
  ‹(x, prod.rotL y) = apsnd prod.rotL z ⟷ (x, y) = z›
  by (cases z; cases y; clarsimp)

lemma swap_proj_comp[simp, φsafe_simp]:
  ‹fst o prod.swap = snd›
  ‹snd o prod.swap = fst›
  unfolding fun_eq_iff
  by simp_all

lemma swap_proj_comp'[simp, φsafe_simp]:
  ‹x o fst o prod.swap = x o snd›
  ‹y o snd o prod.swap = y o fst›
  unfolding fun_eq_iff
  by simp_all

lemma swap_ap_comp[no_atp, prod_opr_norm]:
  ‹prod.swap o apfst f = apsnd f o prod.swap›
  ‹prod.swap o apsnd g = apfst g o prod.swap›
  unfolding fun_eq_iff
  by clarsimp+

lemmas swap_ap[no_atp, prod_opr_norm] = prod.swap_ap_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas swap_ap_comp'[no_atp, prod_opr_norm] = prod.swap_ap_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]

lemma prj_rot_apS_rot_comp[no_atp, prod_opr_norm]:
  ‹fst ∘ prod.rotL ∘ apsnd prod.swap ∘ prod.rotR = apfst fst›
  ‹snd ∘ prod.rotR ∘ apfst prod.swap ∘ prod.rotL = apsnd snd›
  unfolding fun_eq_iff
  by simp_all

lemmas prj_rot_apS_rot[no_atp, prod_opr_norm] = prod.prj_rot_apS_rot_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas prj_rot_apS_rot_comp'[no_atp, prod_opr_norm] = prod.prj_rot_apS_rot_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma ap_ap_comp[no_atp, prod_opr_norm]:
  ‹apfst f o apfst g = apfst (f o g)›
  ‹apsnd f o apsnd g = apsnd (f o g)›
  unfolding fun_eq_iff
  by simp_all

lemmas ap_ap[no_atp, prod_opr_norm] = prod.ap_ap_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas ap_ap_comp'[no_atp, prod_opr_norm] = prod.ap_ap_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]


lemma prj_ap_comp'[simp, φsafe_simp]:
  ‹x⇩1 o fst o apfst f = x⇩1 o f o fst›
  ‹x⇩2 o snd o apfst f = x⇩2 o snd›
  ‹x⇩3 o snd o apsnd f = x⇩3 o f o snd›
  ‹x⇩4 o fst o apsnd f = x⇩4 o fst›
  unfolding fun_eq_iff
  by simp_all



lemma rot_apS_comp[no_atp, prod_opr_norm]:
  ‹prod.rotL o apsnd prod.swap = apfst prod.swap o prod.rotL o prod.swap o prod.rotL›
  ‹prod.rotR o apfst prod.swap = apsnd prod.swap o prod.rotR o prod.swap o prod.rotR›
  unfolding fun_eq_iff
  by simp_all

lemmas rot_apS[no_atp, prod_opr_norm] = prod.rot_apS_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas rot_apS_comp'[no_atp, prod_opr_norm] = prod.rot_apS_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]




(*reduction of 4 elements,
  strategy: eliminate ‹apsnd rot›*)
lemma rot_aprot_rot_comp[no_atp, prod_opr_norm]:
  ‹apsnd prod.rotR o prod.rotR = prod.rotR o prod.rotR o apfst prod.rotL›
  ‹apsnd prod.rotL o prod.rotR = prod.rotR o apfst prod.rotR o prod.rotL›
  ‹prod.rotL o apsnd prod.rotL = apfst prod.rotR o prod.rotL o prod.rotL›
  ‹prod.rotL o apsnd prod.rotR = prod.rotR o apfst prod.rotL o prod.rotL›
(*can be derived:
  ‹prod.rotL ∘ prod.rotL ∘ apsnd prod.rotR = apfst prod.rotL o prod.rotL›
  ‹prod.rotL o apsnd prod.rotL o prod.rotR = apfst prod.rotR o prod.rotL›
  ‹prod.rotL ∘ apsnd prod.rotR o prod.rotR = prod.rotR o apfst prod.rotL›
  ‹apsnd prod.rotL o prod.rotR o prod.rotR = prod.rotR o apfst prod.rotR›*)
  unfolding fun_eq_iff
  by clarsimp+

lemmas rot_aprot_rot[no_atp, prod_opr_norm] = prod.rot_aprot_rot_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas rot_aprot_rot_comp'[no_atp, prod_opr_norm] = prod.rot_aprot_rot_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]

lemma rot_aprot_rot_comp⇩f[no_atp, prod_opr_norm]:
  ‹apsnd (f⇩1 o prod.rotR) o prod.rotR = apsnd f⇩1 o prod.rotR o prod.rotR o apfst prod.rotL›
  ‹apsnd (f⇩2 o prod.rotL) o prod.rotR = apsnd f⇩2 o prod.rotR o apfst prod.rotR o prod.rotL›
  ‹prod.rotL o apsnd (prod.rotL o f⇩3) = apfst prod.rotR o prod.rotL o prod.rotL o apsnd f⇩3›
  ‹prod.rotL o apsnd (prod.rotR o f⇩4) = prod.rotR o apfst prod.rotL o prod.rotL o apsnd f⇩4›
  ‹prod.rotL o apsnd (prod.rotL o f⇩5 o g⇩5) = apfst prod.rotR o prod.rotL o prod.rotL o apsnd (f⇩5 o g⇩5)›
  ‹prod.rotL o apsnd (prod.rotR o f⇩6 o g⇩6) = prod.rotR o apfst prod.rotL o prod.rotL o apsnd (f⇩6 o g⇩6)›
  ‹prod.rotL o apsnd (prod.rotL o f⇩7 o g⇩7 o h⇩7) = apfst prod.rotR o prod.rotL o prod.rotL o apsnd (f⇩7 o g⇩7 o h⇩7)›
  ‹prod.rotL o apsnd (prod.rotR o f⇩8 o g⇩8 o h⇩8) = prod.rotR o apfst prod.rotL o prod.rotL o apsnd (f⇩8 o g⇩8 o h⇩8)›
  unfolding fun_eq_iff prod.ap_ap_comp[symmetric]
  by (clarsimp simp add: prod.rot_aprot_rot)+

lemmas rot_aprot_rot⇩f[no_atp, prod_opr_norm] = prod.rot_aprot_rot_comp⇩f [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas rot_aprot_rot_comp⇩f'[no_atp, prod_opr_norm] = prod.rot_aprot_rot_comp⇩f [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]







setup ‹Sign.parent_path›


lemma swap_map_prod[no_atp, prod_opr_norm]:
  ‹prod.swap ((f⇩1 ⊗⇩f f⇩2) x) = (f⇩2 ⊗⇩f f⇩1) (prod.swap x)›
  by (cases x; simp)+

lemma swap_map_prod_comp[no_atp, prod_opr_norm]:
  ‹prod.swap o (f⇩1 ⊗⇩f f⇩2) = (f⇩2 ⊗⇩f f⇩1) o prod.swap›
  unfolding fun_eq_iff
  by clarsimp

lemma swap_map_prod_comp'[no_atp, prod_opr_norm]:
  ‹g o prod.swap o (f⇩1 ⊗⇩f f⇩2) = g o (f⇩2 ⊗⇩f f⇩1) o prod.swap›
  unfolding fun_eq_iff
  by clarsimp


lemma map_prod_eq_apfst_apsnd:
  ‹map_prod f g = apfst f o apsnd g›
  unfolding fun_eq_iff
  by clarsimp

lemma map_prod_eq_apsnd_apfst:
  ‹map_prod f g = apsnd g o apfst f›
  unfolding fun_eq_iff
  by clarsimp




declare map_prod.compositionality[prod_opr_norm]
        map_prod.comp [prod_opr_norm]

lemma map_prod_comp'[no_atp, prod_opr_norm]:
  ‹x o f ⊗⇩f g ∘ h ⊗⇩f i = x o (f ∘ h) ⊗⇩f (g ∘ i)›
  unfolding fun_eq_iff
  by clarsimp

lemma map_prod_ap_simp_comp[simp, φsafe_simp]:
  ‹ (f ⊗⇩f g) o apsnd h = (f ⊗⇩f (g ∘ h)) ›
  ‹ apsnd h' o (f ⊗⇩f g) = f ⊗⇩f (h' ∘ g) ›
  ‹ (f ⊗⇩f g) o apfst l = (f ∘ l) ⊗⇩f g ›
  ‹ apfst l' o (f ⊗⇩f g) = (l' ∘ f) ⊗⇩f g ›
  by (simp_all add: fun_eq_iff)

lemmas map_prod_ap_simp[no_atp, prod_opr_norm] = map_prod_ap_simp_comp [simplified fun_eq_iff id_def comp_apply, THEN spec]
lemmas map_prod_ap_simp_comp'[no_atp, prod_opr_norm] = map_prod_ap_simp_comp [THEN fun_comp_intr_left, unfolded o_id, folded comp_assoc]

lemma swap_comp_swap'[simp, φsafe_simp]:
  ‹x o prod.swap ∘ prod.swap = x›
  unfolding fun_eq_iff
  by simp



(*
lemma apS_rot_apS_eq_rot_S_rot[no_atp, prod_opr_norm]:
  ‹apfst prod.swap (prod.rotL (apsnd prod.swap x)) = prod.rotL (prod.swap (prod.rotL x))›
  ‹apsnd prod.swap (prod.rotR (apfst prod.swap x)) = prod.rotR (prod.swap (prod.rotR x))›
  unfolding prod.rotL_def prod.rotR_def
  by simp_all

lemma apS_rot_apS_eq_rot_S_rot_comp[no_atp, prod_opr_norm]:
  ‹apfst prod.swap o prod.rotL o apsnd prod.swap = prod.rotL o prod.swap o prod.rotL›
  ‹apsnd prod.swap o prod.rotR o apfst prod.swap = prod.rotR o prod.swap o prod.rotR›
  unfolding fun_eq_iff
  by simp_all

lemma apS_rot_apS_eq_rot_S_rot_comp'[no_atp, prod_opr_norm]:
  ‹f o apfst prod.swap o prod.rotL o apsnd prod.swap = f o prod.rotL o prod.swap o prod.rotL›
  ‹g o apsnd prod.swap o prod.rotR o apfst prod.swap = g o prod.rotR o prod.swap o prod.rotR›
  unfolding fun_eq_iff
  by simp_all

term ‹apsnd prod.swap (prod.rotR (prod.swap x)) = prod.rotR (apfst prod.swap (prod.rotL x))›

lemma rot_apS_rot_eq_apS_rot_S[no_atp, prod_opr_norm]:
  ‹prod.rotL (apsnd prod.swap (prod.rotR x)) = apfst prod.swap (prod.rotL (prod.swap x))›
  ‹apsnd prod.swap (prod.rotR (prod.swap x)) = prod.rotR (apfst prod.swap (prod.rotL x))›
  unfolding prod.rotL_def prod.rotR_def
  by simp_all

lemma rot_apS_rot_eq_apS_rot_S_comp[no_atp, prod_opr_norm]:
  ‹prod.rotL ∘ apsnd prod.swap ∘ prod.rotR = apfst prod.swap o prod.rotL o prod.swap›
  ‹apsnd prod.swap o prod.rotR o prod.swap = prod.rotR ∘ apfst prod.swap ∘ prod.rotL› (*apsnd xx is a term has to be normalized, I guess*)
  unfolding fun_eq_iff
  by simp_all

lemma rot_apS_rot_eq_apS_rot_S_comp'[no_atp, prod_opr_norm]:
  ‹f o prod.rotL ∘ apsnd prod.swap ∘ prod.rotR = f o apfst prod.swap o prod.rotL o prod.swap›
  ‹g o apsnd prod.swap o prod.rotR o prod.swap = g o prod.rotR ∘ apfst prod.swap ∘ prod.rotL› (*apsnd xx is a term has to be normalized, I guess*)
  unfolding fun_eq_iff
  by simp_all
*)

subsection ‹Helper Conversion›

definition ‹PURE_TOP ≡ (⋀P::prop. PROP P ⟹ PROP P)›

lemma PURE_TOP_I[φreason 1000]: ‹PROP PURE_TOP› unfolding PURE_TOP_def .

lemma PURE_TOP_imp:
  ‹(PROP PURE_TOP ⟹ PROP P) ≡ PROP P› (is ‹PROP ?LHS ≡ PROP ?RHS›)
proof
  assume ‹PROP ?LHS›
  from this[OF PURE_TOP_I] show ‹PROP ?RHS› .
next
  assume ‹PROP ?RHS›
  then show ‹PROP ?LHS› .
qed

ML_file ‹library/syntax/helper_conv.ML›

subsection ‹Helper Simplification›

simproc_setup Funcomp_Lambda (‹f o g›) = ‹fn _ => fn ctxt => fn ctm =>
  case Thm.term_of ctm
    of Const(\<^const_name>‹Fun.comp›, _) $ Abs _ $ _ =>
        SOME (Conv.rewr_conv @{thm' comp_def[folded atomize_eq]} ctm)
     | Const(\<^const_name>‹Fun.comp›, _) $ _ $ Abs _ =>
        SOME (Conv.rewr_conv @{thm' comp_def[folded atomize_eq]} ctm)
     | _ => NONE
›

subsection ‹Helper Isar Commands›

(* declare [[ML_debugger=false, ML_exception_debugger=false]] *)

ML_file ‹library/tools/syntax_group.ML›
ML_file ‹library/tools/adhoc_overloading.ML›

(* declare [[ML_debugger, ML_exception_debugger]] *)

subsection ‹Syntax›

optional_translation_group do_notation
  ‹enables the do-notation for program monads›
  ‹fn flag => fn ctxt =>
      (print_mode := (if flag then insert else remove)
                        (op =) "do_notation" (!print_mode) ;
       ctxt)›

declare [[do_notation]]

subsection ‹The Friendly Character›

ML_file ‹library/tools/the_friendly_character.ML›

definition Friendly_Help :: ‹text ⇒ bool› where [iff, φsafe_simp]: ‹Friendly_Help _ ⟷ True›

lemma Friendly_Help_I[intro!]: ‹Friendly_Help ANY› unfolding Friendly_Help_def ..
lemma Friendly_Help_E[elim!]: ‹Friendly_Help ANY ⟹ C ⟹ C› .

(*TODO: move this to φlang_parser so that the help is displayed only when the IDECP ends at that*)

φreasoner_ML Friendly_Help 1000 (‹Friendly_Help _›) = ‹fn (_, (ctxt,sequent)) =>
 (if Config.get ctxt Phi_The_Friendly_Character.enable
  then let
        val _ $ (_ $ text) = Thm.major_prem_of sequent
        val pretty = Text_Encoding.decode_text_pretty ctxt text
       in Phi_The_Friendly_Character.info ctxt (fn _ => pretty) end
  else ();
  Seq.single (ctxt, @{thm Friendly_Help_I} RS sequent)
 )
›

subsection ‹General Reasoning Rules›

declare refl[φreason 1000]

subsubsection ‹pred_option›

lemma [φreason 1000]:
  ‹ P x
⟹ pred_option P (Some x)›
  by simp

lemma [φreason 1000]:
  ‹ pred_option P None›
  by simp

subsection ‹Some very Early Reasoning›



(*

declare (* disjE[φinhabitance_rule] *) (*I don't like divergence!*)
        conjE[φinhabitance_rule]
        set_mult_inhabited[φinhabitance_rule]
        set_plus_inhabited[φinhabitance_rule]

lemma [φinhabitance_rule, elim!]:
  ‹Satisfiable 1 ⟹ C ⟹ C› .*)

(*TODO:
lemma Membership_E_Inhabitance:
  ‹x ∈ S ⟹ (Satisfiable S ⟹ C) ⟹ C›
  unfolding Satisfiable_def by blast*)





subsection ‹Very Early Mechanism›

φreasoner_group local = (10000, [10000,10000])
  ‹local reasoning rules given from the hypothese of a programming context›

subsubsection ‹Default Attributes in Programming›

text ‹Registry of default attributes of antecedents in the deductive programming.›

ML_file ‹library/system/premise_attribute.ML›

φreasoner_group φattr_all = (100, [0,9999]) ‹collecting all φattribute groups›
                φattr_normalize = (3000, [3000, 3300]) in φattr_all ‹›
                φattr_EIF = (2500, [2500, 2500]) in φattr_all and < φattr_normalize
                      ‹extract facts implied inside›
                φattr_late_normalize = (2000, [2000,2300]) in φattr_all and < φattr_EIF ‹›
                φattr     = (1000, [1000, 1030]) in φattr_all and < φattr_late_normalize
                      ‹default group for specific forms of premises›

paragraph ‹Configuring Existing Antecedents›

(*attribute_setup forall_elim_vars =
  ‹Scan.succeed (Thm.rule_attribute [] (fn _ => fn th =>
      Thm.forall_elim_vars (Thm.maxidx_of th + 1) th))›
  "quantified schematic vars"*)
(*
named_theorems φattr_elim_tag_rules
  ‹Introduction rules that will be applied to eliminate tags for every premises›
attribute_setup φattr_elim_tags = ‹
  Scan.succeed (Thm.rule_attribute [] (fn ctxt => fn th =>
    let val rules = Named_Theorems.get (Context.proof_of ctxt) \<^named_theorems>‹φattr_elim_tag_rules›
        fun apply th =
          case get_first (fn rule => SOME (rule RS th) handle THM _ => NONE) rules
            of SOME ret => apply ret
             | NONE => th
        fun elim_vars th = Thm.forall_elim_vars (Thm.maxidx_of th + 1) th
     in th
     |> elim_vars
     |> apply
     |> elim_vars
    end))
›

φreasoner_group forall_elim_vars = (3550, [3550, 3550]) in φattr_normalize ‹› *)

declare [[
  φpremise_attribute once? [φdeclare]        for ‹PROP _›        (%φattr_EIF),
  φpremise_attribute once? [φreason? %local] for ‹Is_Literal _›  (%φattr),

  φpremise_attribute_ML ‹fn _ => Thm.declaration_attribute (fn thm => fn ctxt =>
    let val term_A = case Thm.prop_of thm
                       of _ $ (Const(\<^const_name>‹HOL.eq›, _) $ A $ _ ) => A
                        | _ $ (Const(\<^const_name>‹Simplify›, _) $ _ $ A $ _ ) => A
        val cterm_A = Context.cases Thm.global_cterm_of Thm.cterm_of ctxt term_A
        val rule = \<^instantiate>‹cterm_A and 'a=‹Thm.ctyp_of_cterm cterm_A› in
                                  lemma ‹Is_Literal (cterm_A::'a)› by (simp add: Is_Literal_def)›
     in Phi_Reasoner.add_rule Position.none Phi_Reasoner.NORMAL_LOCAL_CUT' (SOME @{reasoner_group %is_literal})
            ([(Thm.concl_of rule, NONE)], []) NONE [rule] ctxt
    end
    handle MATCH => ctxt
  )› for ‹Simplify mode_literal _ _› (%φattr)
]]


subsection ‹Convention of Syntax Priority›


text ‹
▪ 10: Labelled, Programming_CurrentConstruction, View_Shift_CurrentConstruction
      PendingConstruction, ToA_Construction, Argument tag
▪ 12: View_Shift, Transformation
▪ 13: Remains
▪ 14: ExBI
▪ 15: Comma, Subjection
▪ 16: Struct Tag, SYNTHESIS
▪ 18: Assertion_Matches
▪ 20: φ-type colon
›


(*TODO: Move this*)
end