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