Theory Naproche

section ‹Isabelle Prover IDE and logic support for NaProChe / ForTheL›

theory Naproche
  imports Main ZFC_Rudiments
  keywords "forthel" "forthel_tex" :: thy_decl
    and "forthel_file" :: thy_load
    and "naproche_problem" :: thy_goal
    and "naproche_problems" :: diag
begin


section ‹Logic›

text ‹See also 🗏‹$NAPROCHE_HOME/src/SAD/ForTheL/Base.hs››


axiomatization
  ― ‹primitive notions›
  Map :: ‹V ⇒ bool›  ― ‹maps› and
  Fun :: ‹V ⇒ bool›  ― ‹functions› and
  Set :: ‹V ⇒ bool›  ― ‹sets› and
  Class :: ‹V ⇒ bool›  ― ‹classes› and
  Elem :: ‹V ⇒ V ⇒ bool›  ― ‹set membership / elements of a set› and
  Obj :: ‹V ⇒ bool›  ― ‹mathematical objects› and

  ― ‹primitive predicates›
  Less :: ‹V ⇒ V ⇒ bool›  ― ‹relation for induction› and

  ― ‹primitive operations›
  Dom :: ‹V ⇒ V› and
  Pair :: ‹V ⇒ V ⇒ V› and
  App :: ‹V ⇒ V ⇒ V› and

  Thesis :: ‹bool› and
  This :: 'a

notation (output)
  Elem (infix ‹❙∈› 50) and
  Less (infix ‹≺› 50) and
  Pair (‹⟨_,/ _⟩› [0, 0] 1000) and
  App (infix ‹⋅› 90)

abbreviation Not_Elem :: ‹V ⇒ V ⇒ bool›
  where ‹Not_Elem x A ≡ ¬ Elem x A›

abbreviation All_Elem :: "V ⇒ (V ⇒ bool) ⇒ bool"
  where ‹All_Elem A B ≡ (∀x. Elem x A ⟶ B x)›

abbreviation Ex_Elem :: "V ⇒ (V ⇒ bool) ⇒ bool"
  where ‹Ex_Elem A B ≡ (∃x. Elem x A ∧ B x)›

syntax (output)
  "_All_Elem" :: ‹pttrn ⇒ V ⇒ bool ⇒ bool›  (‹(3∀(_/❙∈_)./ _)› [0, 0, 10] 10)
  "_Ex_Elem" :: ‹pttrn ⇒ V ⇒ bool ⇒ bool›  (‹(3∃(_/❙∈_)./ _)› [0, 0, 10] 10)
  "_Not_Ex_Elem" :: ‹pttrn ⇒ V ⇒ bool ⇒ bool›  (‹(3∄(_/❙∈_)./ _)› [0, 0, 10] 10)
translations
  "_All_Elem x A B" ⇌ "CONST All_Elem A (λx. B)"
  "_Ex_Elem x A B" ⇌ "CONST Ex_Elem A (λx. B)"
  "_Not_Ex_Elem x A B" ⇌ "CONST Not (CONST Ex_Elem A (λx. B))"


section ‹Isabelle/ML›

ML_file ‹naproche.ML›


section ‹Isabelle/Haskell›

generate_file "Isabelle/Naproche.hs" = ‹
{-
Authors: Makarius (2021)

Constants for Isabelle/Naproche.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Naproche (
  naproche_prove, naproche_check, naproche_skipfail,
  naproche_pos_id, naproche_pos_file, naproche_pos_shift,
  naproche_isabelle,

  cancel_program, forthel_program,

  threads_command, serials_command, cert_terms_command, print_terms_command,
  print_sequents_command, define_problems_command,

  output_state_command, output_writeln_command, output_information_command,
  output_tracing_command, output_warning_command, output_legacy_feature_command,
  output_error_command, output_report_command,

  iT, is_iT, mk_this, dest_this,

  map_const, fun_const, set_const, class_const, elem_const, obj_const,
  less_const, dom_const, pair_const, app_const, thesis_const
)
where

import Isabelle.Term
import Isabelle.Bytes (Bytes)


-- options

naproche_prove, naproche_check, naproche_skipfail :: Bytes
naproche_prove = ‹\<^system_option>‹naproche_prove››
naproche_check = ‹\<^system_option>‹naproche_check››
naproche_skipfail = ‹\<^system_option>‹naproche_skipfail››

naproche_pos_id, naproche_pos_file, naproche_pos_shift :: Bytes
naproche_pos_id = ‹\<^system_option>‹naproche_pos_id››
naproche_pos_file = ‹\<^system_option>‹naproche_pos_file››
naproche_pos_shift = ‹\<^system_option>‹naproche_pos_shift››

naproche_isabelle :: Bytes
naproche_isabelle = ‹\<^system_option>‹naproche_isabelle››


-- programs in Haskell
-- (see 🗏‹$NAPROCHE_HOME/src/SAD/Main.hs›)

cancel_program :: Bytes
cancel_program = ‹Naproche.cancel_program›

forthel_program :: Bytes
forthel_program = ‹Naproche.forthel_program›


-- commands in ML

threads_command, serials_command, cert_terms_command, print_terms_command,
  print_sequents_command, define_problems_command :: Bytes
threads_command = ‹\<^naproche_command>‹threads››
serials_command = ‹\<^naproche_command>‹serials››
cert_terms_command = ‹\<^naproche_command>‹cert_terms››
print_terms_command = ‹\<^naproche_command>‹print_terms››
print_sequents_command = ‹\<^naproche_command>‹print_sequents››
define_problems_command = ‹\<^naproche_command>‹define_problems››

output_state_command, output_writeln_command, output_information_command,
  output_tracing_command, output_warning_command, output_legacy_feature_command,
  output_error_command, output_report_command :: Bytes
output_state_command = ‹\<^naproche_command>‹output_state››
output_writeln_command = ‹\<^naproche_command>‹output_writeln››
output_information_command = ‹\<^naproche_command>‹output_information››
output_tracing_command = ‹\<^naproche_command>‹output_tracing››
output_warning_command = ‹\<^naproche_command>‹output_warning››
output_legacy_feature_command = ‹\<^naproche_command>‹output_legacy_feature››
output_error_command = ‹\<^naproche_command>‹output_error››
output_report_command = ‹\<^naproche_command>‹output_report››


-- logic

iT :: Typ; is_iT :: Typ -> Bool
(iT, is_iT) = type_op0 ‹\<^type_name>‹V››

mk_this :: Typ -> Term; dest_this :: Term -> Maybe Typ
(mk_this, dest_this) = typed_op0 ‹\<^const_name>‹This››

map_const, fun_const, set_const, class_const, elem_const, obj_const,
  less_const, dom_const, pair_const, app_const, thesis_const :: Bytes
map_const = ‹\<^const_name>‹Map››
fun_const = ‹\<^const_name>‹Fun››
set_const = ‹\<^const_name>‹Set››
class_const = ‹\<^const_name>‹Class››
elem_const = ‹\<^const_name>‹Elem››
obj_const = ‹\<^const_name>‹Obj››
less_const = ‹\<^const_name>‹Less››
dom_const = ‹\<^const_name>‹Dom››
pair_const = ‹\<^const_name>‹Pair››
app_const = ‹\<^const_name>‹App››
thesis_const = ‹\<^const_name>‹Thesis››
›

end