Session Intro_Dest_Elim

Theory IDE_Tools

(* Copyright 2021 (C) Mihails Milehins *)

sectionIDE_Tools›
theory IDE_Tools
  imports Main
begin

ML_file "IDE_Utilities.ML"

end

File ‹IDE_Utilities.ML›

(* Copyright 2021 (C) Mihails Milehins *)

signature IDE_UTILITIES =
sig

val thm_printer : Proof.context -> bool -> string -> thm list -> unit

end;

structure IDE_Utilities : IDE_UTILITIES =
struct

(* standard theorem printer *)
fun thm_printer ctxt print name thms = 
  Proof_Display.print_results 
    print 
    (Position.thread_data ()) 
    ctxt 
    ((Thm.theoremK, ""), single (name, thms));

end;

Theory IHOL_IDE

(* Copyright 2021 (C) Mihails Milehins *)

sectionIHOL_IDE›
theory IHOL_IDE
  imports "IDE_Tools/IDE_Tools"
  keywords "mk_ide" :: thy_defn
    and "rf"
    and "|intro" "|dest" "|elim" 
begin



subsection‹Miscellaneous results›
           
lemma PQ_P_Q: "P  Q  P  Q" by auto
    


subsection‹Import›

ML_file‹IDE.ML›

end

File ‹IDE.ML›

(* Copyright 2021 (C) Mihails Milehins *)

signature IDE =
sig

val mk_intro : Proof.context -> thm -> thm list
val mk_dest : Proof.context -> thm -> thm list
val mk_elim : Proof.context -> thm -> thm list

end;

structure IDE: IDE  =
struct



(*** Auxiliary ***)

fun is_conj (Const (const_name‹conj›, _) $ _ $ _) = true
  | is_conj _ = false;

fun is_equals (Const (const_name‹Pure.eq›, _) $ _ $ _) = true
  | is_equals _ = false;



(*** Introduction rule ***)

fun mk_intro ctxt thm =
  let 
    val thm' = thm RS @{thm verit_Pure_trans}
    val n = Thm.nprems_of thm'
  in 
    thm'
    |> rotate_prems (n - 1)
    |> Local_Defs.unfold ctxt (single @{thm conj_imp_eq_imp_imp}) 
    |> single 
  end;



(*** Destruction rule ***)

local 

fun is_conj_concl thm = thm
  |> Thm.concl_of
  |> HOLogic.dest_Trueprop
  |> is_conj

fun dest_conj_concl_impl [] = []
  | dest_conj_concl_impl (thm :: thms) = 
    if is_conj_concl thm 
    then 
      let
        val thm2 = thm RS conjunct2
        val thm1 = thm RS conjunct1
      in
        (if is_conj_concl thm2 then dest_conj_concl_impl [thm2] else [thm2]) @ 
        (if is_conj_concl thm1 then dest_conj_concl_impl [thm1] else [thm1]) @ 
        dest_conj_concl_impl thms
      end
    else thm :: dest_conj_concl_impl thms;

in

fun mk_dest ctxt thm =
  let 
    val thm' = Local_Defs.unfold ctxt (single @{thm conj_assoc}) thm
    val thm'' = thm' RS @{thm PQ_P_Q}
    val n = Thm.nprems_of thm''
    val thm''' = thm'' 
      |> rotate_prems (n - 1) 
      |> Local_Defs.unfold ctxt (single @{thm conj_imp_eq_imp_imp});
  in dest_conj_concl_impl [thm'''] |> rev end;

end;



(*** Elimination rule ***)

fun mk_elim ctxt thm = 
  let
    val thm' = (thm RS @{thm PQ_P_Q})
      |> Tactic.make_elim
      |> Local_Defs.unfold ctxt (single @{thm conj_imp_eq_imp_imp})
    val conclt = Thm.concl_of thm'
    val conclt' = conclt
      |> dest_Var
      ||> K typ‹bool›
      |> Var
      |> HOLogic.mk_Trueprop
    val insts = (conclt, conclt')
      |> apply2 (Thm.cterm_of ctxt)
      |> Thm.first_order_match 
  in thm' |> Drule.instantiate_normalize insts |> single end;



(*** Command ***)

val error_msg = "mk_ide: invalid arguments"

val mk_ide_parser = Scan.option keywordrf -- Parse.thm --
  (
    Scan.repeat
      (
        (keyword|intro -- Parse_Spec.opt_thm_name "|") ||
        (keyword|dest -- Parse_Spec.opt_thm_name "|") ||
        (keyword|elim -- Parse_Spec.opt_thm_name "|")
      )
  );

fun process_mk_rule mk_rule ((rf, b), thm) ctxt =
  let 
    val thms = thm
      |> mk_rule ctxt 
      |> 
        (
          fn thms => 
            if is_some rf 
            then map (Object_Logic.rulify ctxt) thms 
            else thms
        )
    val ((c, thms'), ctxt') = 
      Local_Theory.note (b ||> map (Attrib.check_src ctxt), thms) ctxt
    val _ = IDE_Utilities.thm_printer ctxt' true c thms'
  in ctxt' end;

fun folder_mk_rule (("|intro", b), (rf, thm)) ctxt =
      process_mk_rule mk_intro ((rf, b), thm) ctxt
  | folder_mk_rule (("|dest", b), (rf, thm)) ctxt =
      process_mk_rule mk_dest ((rf, b), thm) ctxt
  | folder_mk_rule (("|elim", b), (rf, thm)) ctxt = 
      process_mk_rule mk_elim ((rf, b), thm) ctxt
  | folder_mk_rule _ _ = error error_msg

fun process_mk_ide ((rf, thm), ins) ctxt =
  let
    val _ = ins |> map #1 |> has_duplicates op= |> not orelse error error_msg
    val thm' = thm
      |> singleton (Attrib.eval_thms ctxt) 
      |> Local_Defs.meta_rewrite_rule ctxt;
    val t = Thm.concl_of thm' 
    val _ = t |> is_equals orelse error error_msg
    val _ = (t |> Logic.dest_equals |> #1 |> type_of |> body_type) = typ‹bool› 
      orelse error error_msg
  in fold folder_mk_rule (map (fn x => (x, (rf, thm'))) ins) ctxt end;

val _ =
  Outer_Syntax.local_theory
    command_keywordmk_ide 
    "synthesis of the intro/dest/elim rules" 
    (mk_ide_parser >> process_mk_ide);

end;

Theory Reference_Prerequisites

(* Copyright 2021 (C) Mihails Milehins *)

section‹Reference prerequisites›
theory Reference_Prerequisites
  imports "HOL-Library.LaTeXsugar" 
begin

ML_file ‹~~/src/Doc/antiquote_setup.ML›


(* Copied from Transfer.thy in the main library. *)
notation rel_fun (infixr "===>" 55)
notation map_fun (infixr "--->" 55)

end

File ‹~~/src/Doc/antiquote_setup.ML›

(*  Title:      Doc/antiquote_setup.ML
    Author:     Makarius

Auxiliary antiquotations for the Isabelle manuals.
*)

structure Antiquote_Setup: sig end =
struct

(* misc utils *)

fun translate f = Symbol.explode #> map f #> implode;

val clean_string = translate
  (fn "_" => "\\_"
    | "#" => "\\#"
    | "$" => "\\$"
    | "%" => "\\%"
    | "<" => "$<$"
    | ">" => "$>$"
    | "{" => "\\{"
    | "|" => "$\\mid$"
    | "}" => "\\}"
    | "‐" => "-"
    | c => c);

fun clean_name "…" = "dots"
  | clean_name ".." = "ddot"
  | clean_name "." = "dot"
  | clean_name "_" = "underscore"
  | clean_name "{" = "braceleft"
  | clean_name "}" = "braceright"
  | clean_name s = s |> translate (fn "_" => "-" | "‐" => "-" | c => c);


(* ML text *)

local

fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
  | ml_val (toks1, toks2) =
      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";

fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
  | ml_op (toks1, toks2) =
      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";

fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
  | ml_type (toks1, toks2) =
      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
        toks2 @ ML_Lex.read ") option];";

fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
  | ml_exception (toks1, toks2) =
      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";

fun ml_structure (toks, _) =
  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";

fun ml_functor (Antiquote.Text tok :: _, _) =
      ML_Lex.read "ML_Env.check_functor " @
      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
  | ml_functor _ = raise Fail "Bad ML functor specification";

val is_name =
  ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);

fun ml_name txt =
  (case filter is_name (ML_Lex.tokenize txt) of
    toks as [_] => ML_Lex.flatten toks
  | _ => error ("Single ML name expected in input: " ^ quote txt));

fun prep_ml source =
  (#1 (Input.source_content source), ML_Lex.read_source source);

fun index_ml name kind ml = Thy_Output.antiquotation_raw name
  (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
  (fn ctxt => fn (source1, opt_source2) =>
    let
      val (txt1, toks1) = prep_ml source1;
      val (txt2, toks2) =
        (case opt_source2 of
          SOME source => prep_ml source
        | NONE => ("", []));

      val txt =
        if txt2 = "" then txt1
        else if kind = "type" then txt1 ^ " = " ^ txt2
        else if kind = "exception" then txt1 ^ " of " ^ txt2
        else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
        then txt1 ^ ": " ^ txt2
        else txt1 ^ " : " ^ txt2;
      val txt' = if kind = "" then txt else kind ^ " " ^ txt;

      val pos = Input.pos_of source1;
      val _ =
        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
          handle ERROR msg => error (msg ^ Position.here pos);
      val kind' = if kind = "" then "ML" else "ML " ^ kind;
    in
      Latex.block
       [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
        Thy_Output.verbatim ctxt txt']
    end);

in

val _ =
  Theory.setup
   (index_ml binding‹index_ML› "" ml_val #>
    index_ml binding‹index_ML_op› "infix" ml_op #>
    index_ml binding‹index_ML_type› "type" ml_type #>
    index_ml binding‹index_ML_exception› "exception" ml_exception #>
    index_ml binding‹index_ML_structure› "structure" ml_structure #>
    index_ml binding‹index_ML_functor› "functor" ml_functor);

end;


(* named theorems *)

val _ =
  Theory.setup (Thy_Output.antiquotation_raw binding‹named_thms›
    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
    (fn ctxt =>
      map (fn (thm, name) =>
        Output.output
          (Document_Antiquotation.format ctxt
            (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^
        enclose "\\rulename{" "}" (Output.output name))
      #> space_implode "\\par\\smallskip%\n"
      #> Latex.string #> single
      #> Thy_Output.isabelle ctxt));


(* Isabelle/Isar entities (with index) *)

local

fun no_check (_: Proof.context) (name, _: Position.T) = name;

fun check_keyword ctxt (name, pos) =
  if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
  else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);

fun check_system_option ctxt arg =
  (Completion.check_option (Options.default ()) ctxt arg; true)
    handle ERROR _ => false;

val arg = enclose "{" "}" o clean_string;

fun entity check markup binding index =
  Thy_Output.antiquotation_raw
    (binding |> Binding.map_name (fn name => name ^
      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position))
    (fn ctxt => fn (logic, (name, pos)) =>
      let
        val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
        val hyper_name =
          "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
        val hyper =
          enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
          index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
        val idx =
          (case index of
            NONE => ""
          | SOME is_def =>
              "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
        val _ =
          if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
        val latex =
          idx ^
          (Output.output name
            |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
            |> hyper o enclose "\\mbox{\\isa{" "}}");
      in Latex.string latex end);

fun entity_antiqs check markup kind =
  entity check markup kind NONE #>
  entity check markup kind (SOME true) #>
  entity check markup kind (SOME false);

in

val _ =
  Theory.setup
   (entity_antiqs no_check "" binding‹syntax› #>
    entity_antiqs Outer_Syntax.check_command "isacommand" binding‹command› #>
    entity_antiqs check_keyword "isakeyword" binding‹keyword› #>
    entity_antiqs check_keyword "isakeyword" binding‹element› #>
    entity_antiqs Method.check_name "" binding‹method› #>
    entity_antiqs Attrib.check_name "" binding‹attribute› #>
    entity_antiqs no_check "" binding‹fact› #>
    entity_antiqs no_check "" binding‹variable› #>
    entity_antiqs no_check "" binding‹case› #>
    entity_antiqs Document_Antiquotation.check "" binding‹antiquotation› #>
    entity_antiqs Document_Antiquotation.check_option "" binding‹antiquotation_option› #>
    entity_antiqs Document_Marker.check "" binding‹document_marker› #>
    entity_antiqs no_check "isasystem" binding‹setting› #>
    entity_antiqs check_system_option "isasystem" binding‹system_option› #>
    entity_antiqs no_check "" binding‹inference› #>
    entity_antiqs no_check "isasystem" binding‹executable› #>
    entity_antiqs Isabelle_Tool.check "isatool" binding‹tool› #>
    entity_antiqs ML_Context.check_antiquotation "" binding‹ML_antiquotation› #>
    entity_antiqs (K JEdit.check_action) "isasystem" binding‹action›);

end;

end;

Theory IDE_Reference

(* Copyright 2021 (C) Mihails Milehins *)

theory IDE_Reference
  imports
    IHOL_IDE
    Reference_Prerequisites
begin




section‹Introduction›



subsection‹Background›

text‹
This section presents a reference manual for the framework 
IDE. The framework IDE can be used for the automated synthesis of
the introduction, destruction and elimination rules from the definitions
of predicates stated in the object logic Isabelle/HOL 
(e.g., see \cite{yang_comprehending_2017}) 
of the proof assistant Isabelle \cite{paulson_natural_1986}.

The primary functionality of the framework is available via the Isar
command @{command mk_ide}.
Given a definition of a predicate in Isabelle/HOL, the
command can synthesise introduction, destruction and elimination rules
for this definition. The rules are stated
in a certain predetermined format that is meant to be both natural and
convenient for the end user and the tools for classical reasoning
available in Isabelle/HOL.
›



subsection‹Related and previous work›

text‹
The standard distribution of Isabelle2021 provides the attribute 
@{attribute elim_format} \cite{wenzel_isabelle/isar_2019-1} 
that can be used for the conversion of the
destruction rules to the elimination rules. The primary functionality of this
attribute is reused in the implementation of the command @{command mk_ide}.

Furthermore, Isabelle offers several definitional packages 
that provide similar rules automatically for the constants created
by these definitional packages \cite{wenzel_isabelle/isar_2019-1}. 
However, to the best knowledge of the author,
none of these packages can generate such rules for arbitrary predicates.
Perhaps, in the future, the approaches can be unified or integrated in
some manner. 
›

text‹\newpage›



section‹Syntax›

text‹
This subsection presents the syntactic categories that are associated with the 
command @{command mk_ide}. It is important to note that the presentation is 
only approximate.
›

text‹

\begin{matharray}{rcl}
  @{command_def "mk_ide"} & : & local_theory → local_theory›
\end{matharray}

  

  rail@@{command mk_ide} @{element "rf"}? thm ((intro | elim | dest)*)
    ;
    intro: @@{element "|intro"} (thmdef @'|')
    ;
    dest: @@{element "|dest"} (thmdef @'|')
    ;
    elim: @@{element "|elim"} (thmdef @'|')
  ›

   mk_ide (@{element "rf"}) def_thm› @{element "|intro"} 
name[attrbs]›@{element "|"} converts the
definition def_thm› into an introduction rule, followed by the application of 
the functionality associated with the optional keyword @{element "rf"} and
the attributes attrbs› to this rule. 
The result of the application of the attributes attrbs› 
is stored in the local context under the name name›. def_thm› is meant to be 
a fact that consists of exactly one theorem of the form
\begin{center}
A a1 … an ≃ f1 a1 … an ∧ … ∧ fm a1 … an,
\end{center}
where A› is a constant predicate in n› arguments, ≃› is either the meta-logic 
equality or the object logic equality, n› and m› are natural numbers,
a1 … an are schematic variables and f1 … fm are suitable predicates in n›
arguments (however, there are further implicit restrictions). The resulting
introduction rule is expected to be stated in the format 
\begin{center}
f1 a1 … an ⟹ … ⟹ fm a1 … an ⟹ A a1 … an
\end{center}
prior to the application of the functionality associated with the keyword 
@{element "rf"} and the attributes attrbs›. If the optional keyword
@{element "rf"} is passed to the command, then the output of the command 
(prior to the application of the attributes) is formatted using an algorithm
associated with the attribute @{attribute rule_format} 
\cite{wenzel_isabelle/isar_2019-1}. 
   mk_ide (@{element "rf"}) def_thm› @{element "|dest"} 
name[attrbs]›@{element "|"} converts the definition
def_thm› into one or more destruction rules, followed by the application of the
functionality associated with the optional keyword @{element "rf"} and the 
attributes attrbs› to each destruction rule. 
Given the theorem def_thm› in the format described above, 
the command provides m› destruction rules of the form
\begin{center}
A a1 … an ⟹ fi a1 … an
\end{center}
for each 1≤i≤m› prior to the application of the functionality associated with
the keyword @{element "rf"} and the attributes attrbs›.
   mk_ide (@{element "rf"}) def_thm› @{element "|elim"} 
name[attrbs]›@{element "|"} converts the definition
def_thm› into an elimination rule, followed by the application of the
functionality associated with the optional keyword @{element "rf"} and the 
attributes attrbs› to each destruction rule. 
Given the theorem def_thm› in the format
described above, the elimination rule has the format
\begin{center}
A a1 … an ⟹ (f1 a1 … an ⟹ … ⟹ fm a1 … an ⟹ P) ⟹ P›
\end{center}
prior to the application of the functionality associated with
the keyword @{element "rf"} and the attributes attrbs›.

It is also possible to combine the keywords @{element "|intro"},
@{element "|dest"} and @{element "|elim"} in a single invocation of the 
command.
›

text‹\newpage›



section‹Examples›

text‹
In this section, some of the capabilities of the framework IDE are demonstrated
by example. The example is based on the definition of the constant
const‹monoid› from the standard library of 
Isabelle/HOL \cite{noauthor_isabellehol_2020} and given by 
\begin{center}
@{thm monoid_def[unfolded monoid_axioms_def, no_vars]}
\end{center}
›
mk_ide rf monoid_def[unfolded monoid_axioms_def] 
  |intro monoidI|
  |dest monoidD|
  |elim monoidE|
  
text‹
The invocation of the command @{command mk_ide} provides the theorem
@{thm [source] monoidI} given by 
\begin{center}
@{thm monoidI[no_vars]},
\end{center}
the fact @{thm [source] monoidD} given by
\begin{center}
@{thm monoidD[no_vars]}
\end{center}
and the theorem
@{thm [source] monoidE} given by
\begin{center}
@{thm monoidE[no_vars]}.
\end{center}
›
     
end