src/Pure/Isar/local_defs.ML

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

(*  Title:      Pure/Isar/local_defs.ML
    Author:     Makarius

Local definitions.
*)

signature LOCAL_DEFS =
sig
  val cert_def: Proof.context -> term -> (string * typ) * term
  val abs_def: term -> (string * typ) * term
  val mk_def: Proof.context -> (string * term) list -> term list
  val expand: cterm list -> thm -> thm
  val def_export: Assumption.export
  val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
    (term * (string * thm)) list * Proof.context
  val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
  val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
    (term * term) * Proof.context
  val export: Proof.context -> Proof.context -> thm -> thm list * thm
  val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
  val trans_terms: Proof.context -> thm list -> thm
  val trans_props: Proof.context -> thm list -> thm
  val contract: Proof.context -> thm list -> cterm -> thm -> thm
  val print_rules: Proof.context -> unit
  val defn_add: attribute
  val defn_del: attribute
  val meta_rewrite_conv: Proof.context -> conv
  val meta_rewrite_rule: Proof.context -> thm -> thm
  val unfold: Proof.context -> thm list -> thm -> thm
  val unfold_goals: Proof.context -> thm list -> thm -> thm
  val unfold_tac: Proof.context -> thm list -> tactic
  val fold: Proof.context -> thm list -> thm -> thm
  val fold_tac: Proof.context -> thm list -> tactic
  val derived_def: Proof.context -> bool -> term ->
    ((string * typ) * term) * (Proof.context -> thm -> thm)
end;

structure Local_Defs: LOCAL_DEFS =
struct

(** primitive definitions **)

(* prepare defs *)

fun cert_def ctxt eq =
  let
    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
      quote (Syntax.string_of_term ctxt eq));
    val ((lhs, _), eq') = eq
      |> Sign.no_vars (Syntax.pp ctxt)
      |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
      handle TERM (msg, _) => err msg | ERROR msg => err msg;
  in (Term.dest_Free (Term.head_of lhs), eq') end;

val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free;

fun mk_def ctxt args =
  let
    val (xs, rhss) = split_list args;
    val (bind, _) = ProofContext.bind_fixes xs ctxt;
    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
  in map Logic.mk_equals (lhss ~~ rhss) end;


(* export defs *)

val head_of_def =
  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;


(*
  [x, x == a]
       :
      B x
  -----------
      B a
*)
fun expand defs =
  Drule.implies_intr_list defs
  #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
  #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);

val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);

fun def_export _ defs = (expand defs, expand_term defs);


(* add defs *)

fun add_defs defs ctxt =
  let
    val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
    val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    val xs = map Name.of_binding bvars;
    val names = map2 Thm.def_binding_optional bvars bfacts;
    val eqs = mk_def ctxt (xs ~~ rhss);
    val lhss = map (fst o Logic.dest_equals) eqs;
  in
    ctxt
    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
    |> fold Variable.declare_term eqs
    |> ProofContext.add_assms_i def_export
      (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
    |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
  end;

fun add_def (var, rhs) ctxt =
  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
  in ((lhs, th), ctxt') end;


(* fixed_abbrev *)

fun fixed_abbrev ((x, mx), rhs) ctxt =
  let
    val T = Term.fastype_of rhs;
    val ([x'], ctxt') = ctxt
      |> Variable.declare_term rhs
      |> ProofContext.add_fixes [(x, SOME T, mx)];
    val lhs = Free (x', T);
    val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
    fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
    val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
  in ((lhs, rhs), ctxt'') end;


(* specific export -- result based on educated guessing *)

(*
  [xs, xs == as]
        :
       B xs
  --------------
       B as
*)
fun export inner outer =    (*beware of closure sizes*)
  let
    val exp = Assumption.export false inner outer;
    val prems = Assumption.all_prems_of inner;
  in fn th =>
    let
      val th' = exp th;
      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
      val defs = prems |> filter_out (fn prem =>
        (case try (head_of_def o Thm.prop_of) prem of
          SOME x => member (op =) still_fixed x
        | NONE => true));
    in (map Drule.abs_def defs, th') end
  end;

(*
  [xs, xs == as]
        :
     TERM b xs
  --------------  and  --------------
     TERM b as          b xs == b as
*)
fun export_cterm inner outer ct =
  export inner outer (Drule.mk_term ct) ||> Drule.dest_term;


(* basic transitivity reasoning -- modulo beta-eta *)

local

val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;

fun trans_list _ _ [] = raise Empty
  | trans_list trans ctxt (th :: raw_eqs) =
      (case filter_out is_trivial raw_eqs of
        [] => th
      | eqs =>
          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
          in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);

in

val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm));
val trans_props = trans_list (fn eq => fn th => th COMP (eq COMP Drule.equal_elim_rule1));

end;

fun contract ctxt defs ct th =
  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];


(** defived definitions **)

(* transformation rules *)

structure Rules = Generic_Data
(
  type T = thm list;
  val empty = [];
  val extend = I;
  val merge = Thm.merge_thms;
);

fun print_rules ctxt =
  Pretty.writeln (Pretty.big_list "definitional transformations:"
    (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));

val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);


(* meta rewrite rules *)

fun meta_rewrite_conv ctxt =
  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
      addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
      addsimps (Rules.get (Context.Proof ctxt)));

val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;


(* rewriting with object-level rules *)

fun meta f ctxt = f o map (meta_rewrite_rule ctxt);

val unfold       = meta MetaSimplifier.rewrite_rule;
val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
val fold         = meta MetaSimplifier.fold_rule;
val fold_tac     = meta MetaSimplifier.fold_goals_tac;


(* derived defs -- potentially within the object-logic *)

fun derived_def ctxt conditional prop =
  let
    val ((c, T), rhs) = prop
      |> Thm.cterm_of (ProofContext.theory_of ctxt)
      |> meta_rewrite_conv ctxt
      |> (snd o Logic.dest_equals o Thm.prop_of)
      |> conditional ? Logic.strip_imp_concl
      |> (abs_def o #2 o cert_def ctxt);
    fun prove ctxt' def =
      let
        val frees = Term.fold_aterms (fn Free (x, _) =>
          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
      in
        Goal.prove ctxt' frees [] prop (K (ALLGOALS
          (CONVERSION (meta_rewrite_conv ctxt') THEN'
            MetaSimplifier.rewrite_goal_tac [def] THEN'
            resolve_tac [Drule.reflexive_thm])))
        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
      end;
  in (((c, T), rhs), prove) end;

end;