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

  val numerals_to_Free: thm -> thm

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

  val string_of_thm: thm -> string

  val string_of_thms: thm list -> string

  val cut_id: string -> string

  val id_of_thm: thm -> string

  val of_thm: thm -> T

  val is_sym: id -> bool

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

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val string_of_thm_in_thy: theory -> thm -> string

  val id_drop_sym: id -> id

  val make_sym_rule: Rule.rule -> Rule.rule

  val make_sym_rule_set: Rule_Set.T -> Rule_Set.T

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val sym_thm: thm -> thm

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

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

struct

(**)

type T = ThmC_Def.T;

type id = ThmC_Def.id;

val string_of_thm = ThmC_Def.string_of_thm;

val string_of_thms = ThmC_Def.string_of_thms;

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

fun id_of_thm thm = (cut_id o Thm.get_name_hint) thm;

fun of_thm thm = (id_of_thm thm, thm);

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

(** convert Isabelle's numerals to ISAC's specific format, LEGACY **)

val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)

(* 

  "metaview" as seen from programs and from user input;

  both are parsed as terms by the function package.

*)

fun id_Isac_to_Isabelle thy thmid = (* Isac uses thmid *)

  let val thmid' = case thmid of

      "add_commute" => "add.commute"

    | "mult_commute" => "mult.commute"

    | "add_left_commute" => "add.left_commute"

    | "mult_left_commute" => "mult.left_commute"

    | "add_assoc" => "add.assoc"

    | "mult_assoc" => "mult.assoc"

    | _ => thmid

  in (Global_Theory.get_thm thy) thmid' end;

(**)

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

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

  | "#" :: _ =>

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

  | _ =>

    (**)thmid |> id_Isac_to_Isabelle thy |> numerals_to_Free(**)

    (** )thmid |> Global_Theory.get_thm thy |> numerals_to_Free( **)

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

fun sym_thm thm =

  let 

    val (deriv,

      {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 

      prop = prop}) = Thm.rep_thm_G thm

    val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop

    val prop' = case TermC.strip_imp_prems' prop of

        NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))

      | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))

  in

    Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop'

  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.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

    Rule_Set.Seqence {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 = 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)

(**)end(**)