Theory Phi_Preliminary

chapter ‹Theoretical Foundations›

section ‹Preliminary›

theory Phi_Preliminary
  imports Main "Phi_Algebras.Algebras"
          Phi_Logic_Programming_Reasoner.Phi_Logic_Programming_Reasoner
          Phi_Logic_Programming_Reasoner.PLPR_error_msg
  keywords "optional_translations" :: thy_decl
       and "φadhoc_overloading" "φno_adhoc_overloading" :: thy_decl
begin

declare [ [ML_debugger, ML_exception_debugger]]

subsection ‹Named Theorems›

named_theorems φexpns ‹Semantics Expansions, used to expand assertions semantically.›

declare set_mult_expn[φexpns] Premise_def[φexpns]

ML ‹
structure Phi_Programming_Safe_Simp_SS = Simpset (
  val initial_ss = Simpset_Configure.Minimal_SS
  val binding = \<^binding>‹φprogramming_safe_simps›
  val comment = "Simplification rules used in low automation level, which is safer than usual"
)

structure Phi_Programming_Simp_SS = Simpset (
  val initial_ss = Simpset_Configure.Empty_SS
  val binding = \<^binding>‹φprogramming_simps›
  val comment = "Simplification rules used in the deductive programming"
)
›

lemmas [φprogramming_safe_simps] =
  mult_zero_right[where 'a=‹'a::sep_magma set›] mult_zero_left[where 'a=‹'a::sep_magma set›]
  mult_1_right[where 'a=‹'a::sep_magma_1 set›] mult_1_left[where 'a=‹'a::sep_magma_1 set›]
  add_0_right[where 'a=‹'a::sep_magma set›] add_0_left[where 'a=‹'a::sep_magma set›]
  zero_fun HOL.simp_thms

subsection ‹Error Mechanism›

ML_file ‹library/tools/error.ML›

subsection ‹Helper ML›

ML_file ‹library/tools/Phi_Help.ML›
ML_file ‹library/syntax/helps.ML›
ML_file ‹library/tools/Hook.ML›
ML_file ‹library/system/Phi_Envir0.ML›
ML_file ‹library/system/Phi_ID.ML›
ML_file ‹library/tools/cache_file.ML›

ML_file ‹library/tools/Hasher.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 Lemmas›

lemma imp_implication: "(P ⟶ Q ⟹ PROP R) ≡ ((P ⟹ Q) ⟹ PROP R)" by rule simp+

ML_file ‹library/tools/help_lemmas.ML›

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"


subsection ‹Helper Objects›

subsubsection ‹Big Number›

text ‹A tag to suppress unnecessary expanding of big numbers like ‹2^256  ››

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+

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 Antiquotations›

setup ‹
let
  val basic_entity = Document_Output.antiquotation_pretty_source_embedded
  fun pretty_term_style ctxt (style, t) = Document_Output.pretty_term ctxt (style t)

  fun typ  mode = Scan.peek (Args.named_typ  o Syntax.read_typ
                                             o Proof_Context.set_mode mode o Context.proof_of)
  fun term mode = Scan.peek (Args.named_term o Syntax.read_term
                                             o Proof_Context.set_mode mode o Context.proof_of)
  fun prop mode = Scan.peek (Args.named_term o Syntax.read_prop
                                             o Proof_Context.set_mode mode o Context.proof_of)

in
   ML_Antiquotation.inline_embedded \<^binding>‹pattern›
    (Args.term_pattern >> (ML_Syntax.atomic o ML_Syntax.print_term))
#> ML_Antiquotation.inline_embedded \<^binding>‹pattern_prop›
    (prop Proof_Context.mode_pattern >> (ML_Syntax.atomic o ML_Syntax.print_term))
#> ML_Antiquotation.value_embedded \<^binding>‹schematic_ctyp› (typ Proof_Context.mode_schematic
      >> (fn T => "Thm.ctyp_of ML_context"  ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))
#> ML_Antiquotation.value_embedded \<^binding>‹schematic_cterm› (term Proof_Context.mode_schematic
      >> (fn t => "Thm.cterm_of ML_context" ^ ML_Syntax.atomic (ML_Syntax.print_term t)))
#> ML_Antiquotation.value_embedded \<^binding>‹schematic_cprop› (prop Proof_Context.mode_schematic
      >> (fn t => "Thm.cterm_of ML_context" ^ ML_Syntax.atomic (ML_Syntax.print_term t)))
#> basic_entity \<^binding>‹schematic_term› (Term_Style.parse -- term Proof_Context.mode_schematic)
                                        pretty_term_style
#> basic_entity \<^binding>‹schematic_prop› (Term_Style.parse -- prop Proof_Context.mode_schematic)
                                        pretty_term_style
#> basic_entity \<^binding>‹pattern_term› (Term_Style.parse -- term Proof_Context.mode_pattern)
                                        pretty_term_style
#> basic_entity \<^binding>‹pattern_prop› (Term_Style.parse -- prop Proof_Context.mode_pattern)
                                        pretty_term_style
end›

subsection ‹Helper Methods›

ML_file ‹library/tools/where_tac.ML›

subsection ‹Helper Isar Commands›

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


subsection ‹The Friendly Character›

ML_file ‹library/tools/the_friendly_character.ML›

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

lemma Friendly_Help_I: ‹Friendly_Help ANY› unfolding Friendly_Help_def ..

φ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 ‹Some very Early Reasoning›

subsubsection ‹Extract Elimination Rule - Part I›

definition Extract_Elimination_Rule :: ‹prop ⇒ bool ⇒ bool ⇒ prop›
  where ‹Extract_Elimination_Rule IN OUT_L OUT_R ≡ (PROP IN ⟹ OUT_L ⟹ OUT_R)›

declare [[φreason_default_pattern ‹PROP Extract_Elimination_Rule ?I _ _›
                                ⇒ ‹PROP Extract_Elimination_Rule ?I _ _› (100) ]]

lemma Do_Extract_Elimination_Rule:
  ‹ PROP IN
⟹ PROP Extract_Elimination_Rule IN OUT_L OUT_R
⟹ 𝗋Success
⟹ OUT_L ⟹ (OUT_R ⟹ C) ⟹ C›
  unfolding Extract_Elimination_Rule_def
proof -
  assume IN: ‹PROP IN›
    and  RL: ‹PROP IN ⟹ OUT_L ⟹ OUT_R›
    and  OL: ‹OUT_L›
    and  OR: ‹OUT_R ⟹ C›
  from OR[OF RL[OF IN OL]] show ‹C› .
qed

ML_file ‹library/tools/elimination_rule.ML›

lemma [φreason 1000]:
  ‹ PROP Extract_Elimination_Rule (PROP P) OL OR
⟹ PROP Extract_Elimination_Rule (PROP P @action A) OL OR›
  unfolding Extract_Elimination_Rule_def Action_Tag_def .

lemma [φreason 1000]:
  ‹ PROP Q
⟹ PROP Extract_Elimination_Rule (PROP P) OL OR
⟹ PROP Extract_Elimination_Rule (PROP Q ⟹ PROP P) OL OR›
  unfolding Extract_Elimination_Rule_def Action_Tag_def
  subgoal premises P using P(2)[OF P(3)[OF P(1)] P(4)] . .

lemma [φreason 2000]:
  ‹ PROP Extract_Elimination_Rule (PROP P) OL OR
⟹ PROP Extract_Elimination_Rule (𝗋Success ⟹ PROP P) OL OR›
  unfolding Extract_Elimination_Rule_def Action_Tag_def 𝗋Success_def
  subgoal premises P using P(1)[OF P(2)[OF TrueI] P(3)] . .

subsubsection ‹Inhabitance Reasoning - Part I›

text ‹is by a set of General Elimination rules~\cite{elim_resolution} that extracts pure facts from
  an inhabited BI assertion, i.e., of a form like
  \[ ‹Inhabited X ⟹ (Pure1 ⟹ Pure2 ⟹ … ⟹ C) ⟹ … ⟹ C› \]
›

ML_file ‹library/tools/inhabited_rule.ML›

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!]:
  ‹Inhabited 1 ⟹ C ⟹ C› .

lemma Membership_E_Inhabitance:
  ‹x ∈ S ⟹ (Inhabited S ⟹ C) ⟹ C›
  unfolding Inhabited_def by blast


subsection ‹Very Early Mechanism›

subsubsection ‹Default Attributes in Programming›

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

ML_file ‹library/system/premise_attribute.ML›


subsection ‹Convention of Syntax Priority›


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


(*TODO: Move this*)
end