(* 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

(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)

(*val string_of:*)

  val string_of_thm_PIDE: Proof.context -> thm -> string

  val string_of_thms_PIDE: Proof.context -> thm list -> string

  val id_of_thm: thm -> id

  val of_thm: thm -> T

  val from_rule : Proof.context -> Rule.rule -> T

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

  val is_sym: id -> bool

  val thm_from_thy: theory -> id -> thm

  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

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

\<close>

  val make_sym_rule: Proof.context -> 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;

val string_of_thm_PIDE = ThmC_Def.string_of_thm_PIDE;

val string_of_thms_PIDE = ThmC_Def.string_of_thms_PIDE;

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 ctxt r =

    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r);

\<^isac_test>\<open>

fun string_of_thm_in_thy thy thm =

  UnparseC.term_in_ctxt (Proof_Context.init_global 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 = TVars.map (K (K A)) (TVars.build (TVars.add_tvars t));

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

    val cinstT = TVars.map (K certT) instT;

    val cinst = Vars.make [(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, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =

    Rule_Def.Repeat {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls, 

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

  | make_sym_rule_set (Rule_Set.Sequence {id, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =

    Rule_Set.Sequence {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls, 

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

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

    Rule_Set.Rrls {id = "sym_" ^ id, program = program, calc = calc,  errpatts = errpatts, asm_rls = asm_rls,

      prepat = prepat, rew_ord = rew_ord}

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

fun make_sym_rule ctxt (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_PIDE ctxt 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 ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string ctxt r)

\<^isac_test>\<open>

(* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)

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

                            (*this ^^ might come from the user, who doesn't care about thy*)

      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'      (*recover the thy the thm comes from*)

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

      else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)

  | revert_sym_rule thy rule =

    raise ERROR ("ThmC.revert_sym_rule: NOT for " ^

      Rule.to_string (Proof_Context.init_global thy) rule)

\<close>

(* 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 Parse.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(**)