(* Title:  BaseDefinitions/thmC.sml

   Author: Walther Neuper

   (c) due to copyright terms

This structure could be dropped due to improved reflection in Isabelle;

but ThmC.sym_thm requires still an identifying string thm_id.

*)

signature THEOREM_ISAC =

sig

  type T = ThmC_Def.T

  type id = ThmC_Def.id (* shortest possible *)

  type long_id          (* e.g. "Test.radd_left_commute"*)

  val cut_id: string -> id

  val long_id: T -> long_id

  val string_of_thm: thm -> string

  val string_of_thms: thm list -> string

  val id_of_thm: thm -> id

  val of_thm: thm -> T

  val from_rule : Rule.rule -> T

  val member': id list -> Rule.rule -> bool

  val is_sym: id -> bool

  val thm_from_thy: theory -> ThmC_Def.id -> thm

  val revert_sym_rule: theory -> Rule.rule -> Rule.rule

  val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule

\<^isac_test>\<open>

  val dest_eq_concl: thm -> term * term

  val string_of_thm_in_thy: theory -> thm -> string

  val id_drop_sym: id -> id

\<close>

  val make_sym_rule: Rule.rule -> Rule.rule

  val make_sym_rule_set: Rule_Set.T -> Rule_Set.T

  val sym_thm: thm -> thm

end

(**)

structure ThmC(**): THEOREM_ISAC(**) =

struct

(**)

(** types and conversions **)

type T = ThmC_Def.T;

type id = ThmC_Def.id;

type long_id = string;

fun long_id (thmID, _) = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint

fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into Know_Store*)

val string_of_thm = ThmC_Def.string_of_thm;

val string_of_thms = ThmC_Def.string_of_thms;

fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;

fun of_thm thm = (id_of_thm thm, thm);

fun from_rule (Rule.Thm (id, thm)) = (id, thm)

  | from_rule r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);

\<^isac_test>\<open>

fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.to_ctxt thy) (Thm.prop_of thm);

\<close>

fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm))

  handle ERROR _ => false

(** handle symmetric equalities, generated by deriving input terms **)

fun is_sym id =

  case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true

  | _ => false;

fun id_drop_sym id =

  case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id

  | _ => id

(* get the theorem associated with the xstring-identifier;

   if the identifier starts with "sym_" then swap "lhs = rhs" around "=";

   in case identifiers starting with "#" come from Eval and

   get an ad-hoc theorem (containing numerals only) -- rejected here

*)

fun thm_from_thy thy thmid =

  case Symbol.explode thmid of

    "s" :: "y" :: "m" :: "_" :: "#" :: _ =>

      raise ERROR ("thm_from_thy not impl.for " ^ thmid)

  | "s" :: "y" :: "m" :: "_" :: id =>

      ((Global_Theory.get_thm thy) (implode id)) RS sym

  | "#" :: _ =>

      raise ERROR ("thm_from_thy not impl.for " ^ thmid)

  | _ =>

      thmid |> Global_Theory.get_thm thy

fun dest_eq_concl thm =

  (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of

    NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm])

  | SOME eq => eq);

(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)

(*NB: careful instantiation avoids shifting of schematic variables*)

fun sym_thm thm =

  let

    val thy = Thm.theory_of_thm thm;

    val certT = Thm.global_ctyp_of thy;

    val cert = Thm.global_cterm_of thy;

    val (lhs, rhs) = dest_eq_concl thm |> apply2 cert;

    val A = Thm.typ_of_cterm lhs;

    val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};

    val (t, s) = dest_eq_concl sym_rule;

    val instT = map (rpair A) (Term.add_tvars t []);

    val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, []));

    val cinstT = map (apsnd certT) instT;

    val cinst = [(s', lhs), (t', rhs)];

  in

    thm

    |> Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule)

    |> Thm.put_name_hint (Thm.get_name_hint thm)

  end;

fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty

  | make_sym_rule_set (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

    Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

      rules = rules, rew_ord = rew_ord, preconds = preconds}

  | make_sym_rule_set (Rule_Set.Sequence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

    Rule_Set.Sequence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

      rules = rules, rew_ord = rew_ord, preconds = preconds}

  | make_sym_rule_set (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = 

    Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc,  errpatts = errpatts, erls = erls,

      prepat = prepat, rew_ord = rew_ord}

(* toggles sym_* and keeps "#:" for ad-hoc theorems *)

fun make_sym_rule (Rule.Thm (thmID, thm)) =

      let

        val thm' = sym_thm thm

        val thmID' = case Symbol.explode thmID of

          "s" :: "y" :: "m" :: "_" :: id => implode id

        | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'

        | _ => "sym_" ^ thmID

      in Rule.Thm (thmID', thm') end

  | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)

  | make_sym_rule r = raise ERROR ("make_sym_rule: not for " ^  Rule.to_string r)

fun revert_sym_rule thy (Rule.Thm (id, thm)) =

      if is_sym (cut_id id)

      then 

        let 

          val id' = id_drop_sym id

          val thm' = thm_from_thy thy id'

          val id'' = Thm.get_name_hint thm'

        in Rule.Thm (id'', thm') end

      else Rule.Thm (Thm.get_name_hint thm, thm)

  | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)

(* ML antiquotations *)

val sym_prefix = "sym_";

fun make_rule ctxt symmetric (xname, pos) =

  let

    val _ =

      if String.isPrefix sym_prefix xname

      then error ("Bad theorem name with sym-prefix " ^ quote xname ^ Position.here pos) else ();

    val context = Context.Proof ctxt;

    val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);

    val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos);

    val thm =

      if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)

      else Facts.the_single (name, pos) thms;

    val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);

  in Rule.Thm (xname', thm') end;

fun antiquotation binding sym =

  ML_Antiquotation.value_embedded binding

    (Scan.lift Args.embedded_position >> (fn name =>

      "ThmC.make_rule ML_context " ^ Bool.toString sym ^

        ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position name));

val _ =

  Theory.setup

    (antiquotation \<^binding>\<open>rule_thm\<close> false #>

     antiquotation \<^binding>\<open>rule_thm_sym\<close> true);

(**)end(**)