(* Title:  "BaseDefinitions/thmC.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- fun sym_thm -----------------------------------------------------------------------";

"----------- fun revert_sym_rule ---------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- fun sym_thm -----------------------------------------------------------------------";

"----------- fun sym_thm -----------------------------------------------------------------------";

"----------- fun sym_thm -----------------------------------------------------------------------";

"~~~~~ fun sym_thm , args:"; val (thm) = (@{thm real_mult_minus1});

    val thy = Thm.theory_of_thm thm;

    val certT = Thm.global_ctyp_of thy: typ -> ctyp;

    val cert = Thm.global_cterm_of thy: term -> cterm;

    val (lhs, rhs) = dest_eq_concl thm |> apply2 cert; (*"- 1 * ?z", "- ?z"*)

    val A = Thm.typ_of_cterm lhs; (* "real"*)

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

if ThmC.string_of_thm sym_rule = "?s1 = ?t1 \<Longrightarrow> ?t1 = ?s1" then () else error "sym_thm 1";

    val (t, s) = dest_eq_concl sym_rule; (*Var (("t", 1), "?'a1"), Var (("s", 1), "?'a1")*)

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

      (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * typ) list*)

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

      (* = ( (("t", 1), "real"), (("s", 1), "real") )*)

    val cinstT = map (apsnd certT) instT;

      (* = [((("'a", 1), ["HOL.type"]), "real")]: ((indexname * sort) * ctyp) list*)

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

      (* = [((("s", 1), "real"), "- 1 * ?z"), ((("t", 1), "real"), "- ?z")] *)

val res = Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule) thm;

if ThmC.string_of_thm res = "- ?z = - 1 * ?z" then () else error "sym_thm - 1 * ?z = - ?z CHANGED"

"----------- fun revert_sym_rule ---------------------------------------------------------------";

"----------- fun revert_sym_rule ---------------------------------------------------------------";

"----------- fun revert_sym_rule ---------------------------------------------------------------";

"~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =

  (@{theory Isac_Knowledge},

    Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));

if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()

else error "input to revert_sym_rule CHANGED";

      (*if*) is_sym (cut_id id) (*then*);

          val id' = id_drop_sym id

          val thm' = thm_from_thy thy id'

          val id'' = Thm.get_name_hint thm'

(*GOON* )

val thy = @{theory Isac_Knowledge}

val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy

  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))

;

if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"

then () else error "fun revert_sym_rule changed 1";

val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy

  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))

;

if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"

then () else error "fun revert_sym_rule changed 2"

( *GOON*)