(* theory collecting all knowledge defined for the isac mathengine

   WN.11.00

 *)

theory Build_Thydata

imports Isac

begin

text {* This theory collects data of theorems and axioms defined and used in ISAC *}

ML {*

(** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **)

(*local*)

  val first_ProgLang_thy = @{theory ListC}

  val first_Knowledge_thy = @{theory Delete}  (*see WN120321.TODO rearrange theories*)

  val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};

  val isabthys' =

    drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

  val isacthys' =

    take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

  val knowthys' =

    take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');

  val progthys' =                   (*WN120321.TODO rearrange theories -------vvv*)

    drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');

  val isacrlsthms = ! ruleset'

    |> map (thms_of_rls o #2 o #2)

    |> flat

    |> map thm_of_thm

    |> gen_distinct Thm.eq_thm 

    |> map (` I)

    |> map (apfst Thm.get_name_hint)

    |> map (apsnd prop_of)  (*this adapts to Theory.axioms_of*)

    : (thmDeriv * term) list;

  val isacthms =

    (flat o (map Theory.axioms_of)) isacthys': (thmDeriv * term) list; 

(*in*)

    isabthys := isabthys';

    knowthys := knowthys';

    progthys := progthys';

    theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*)

    val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); 

(*end;(*local*)*)

(*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:

  see tests

  --- OLD compute rlsthmsNOTisac by eq_thmID ---

  --- compute val rlsthmsNOTisac ---

  for improvements (###sym_* etc)

*)

val rlsthmsNOTisac =

 [("HOL.refl", (prop_of o num_str) @{thm refl}),

  ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),

  (*/------------these are not found in ListC.thy, because they are no axioms---\*)

  ("ListC.del.del_base", (prop_of o num_str) @{thm del_base}), 

  ("ListC.del.del_rec", (prop_of o num_str) @{thm del_rec}),

  ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}), 

  ("ListC.LENGTH.LENGTH_NIL", (prop_of o num_str) @{thm LENGTH_NIL}), 

  ("ListC.list_diff_def", (prop_of o num_str) @{thm list_diff_def}), 

  (*\------------these are not found in ListC.thy, because they are no axioms---/*)

  ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}),

  ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}),

  ("List.if_True", (prop_of o num_str) @{thm if_True}),

  ("HOL.if_False", (prop_of o num_str) @{thm if_False}),

  (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)

  ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),

  ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),

  (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)

  (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)

  ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),

  (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*)

  ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}),

  ("Rings.mult_zero_class.mult_zero_left", (prop_of o num_str) @{thm mult_zero_left}),

  ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}),

  ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),

  ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),

  ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),

  (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)

  ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}),

  ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),

  ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),

  ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),

  ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),

  ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),

  ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),

  ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}),

  ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}),

  (*###("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),*)

  ("Rings.ring_class.left_diff_distrib", (prop_of o num_str) @{thm left_diff_distrib}),

  ("Rings.ring_class.right_diff_distrib", (prop_of o num_str) @{thm right_diff_distrib}),

  ("Rings.division_ring_class.minus_divide_left", (prop_of o num_str) @{thm minus_divide_left}),

  ("Rings.division_ring_class.times_divide_eq_right", (prop_of o num_str) @{thm times_divide_eq_right}),

  ("Fields.field_class.times_divide_eq_left", (prop_of o num_str) @{thm times_divide_eq_left}),

  ("Fields.field_inverse_zero_class.divide_divide_eq_left", (prop_of o num_str) @{thm divide_divide_eq_left}),

  ("Fields.field_inverse_zero_class.divide_divide_eq_right", (prop_of o num_str) @{thm divide_divide_eq_right}),

  ("Rings.division_ring_class.divide_1", (prop_of o num_str) @{thm divide_1}),

  ("Rings.division_ring_class.add_divide_distrib", (prop_of o num_str) @{thm add_divide_distrib }),

  (*###("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")*)

  (* thms in Scripts: *)

  ("Int.divide_minus1", (prop_of o num_str) @{thm divide_minus1}),

  ("Groups.group_add_class.neg_equal_iff_equal", (prop_of o num_str) @{thm neg_equal_iff_equal})]

  : (thmDeriv * term) list;

(*.set up the list using 'val first_isac_thy' (see ListC.thy).*)

(*isab_thm_thy := make_isab rlsthmsNOTisac isabthys;*)

  isab_thm_thy := rlsthmsNOTisac; (*WN120320 remove ref*)

(*.create the hierarchy of theory elements from IsacKnowledge

   including thms from Isabelle used in rls;

   elements store_*d in any *.thy are not overwritten.*)

(*========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======

  WN130620: instead of building thehier correctly, the elements required for tests

  are inserted at "=== inhibit exn WN130620 (1.4.1) below: fill thehier ===" 

  according to (1.4.1) below.

thehier := the_hier (! thehier) (collect_thydata ()); (*ME_Isa: thy 'Script' not in system*)

tracing("----------------------------------\n" ^

	"*** insert: not found ... IS OK : \n" ^

	"comes from fill_parents           \n" ^

	"----------------------------------\n");

========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======*)

*}

text {* interface for dialog-authoring *}

ML {*

(*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)

store_thy @{theory "Diff"} ["Isabelle2011-->12"];

store_isa ["IsacKnowledge","Diff","Theorems"] ["Isabelle2011-->12"];

store_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})

   ["Isabelle2011-->12"];

store_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})

   ["Isabelle2011-->12"];

store_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})

   ["Isabelle2011-->12"];

store_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})

   ["Isabelle2011-->12"];

store_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})

   ["Isabelle2011-->12"];

store_isa ["IsacKnowledge","Diff","Rulesets"] ["Isabelle2011-->12"];

store_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"];

store_thy @{theory "Test"} ["Isabelle2011-->12"];

store_isa ["IsacKnowledge","Test","Theorems"] ["Isabelle2011-->12"];

store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute

})

   ["Isabelle2011-->12"];

(*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)

*}

ML {*

insert_errpats ["diff","differentiate_on_R"]

 ([("chain-rule-diff-both",

    [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",

     parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",

     parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",

     parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",

     parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],

    [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 

     @{thm diff_ln_chain}, @{thm  diff_exp_chain}])]: errpat list);

insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]

 ([("fill-d_d-arg",

     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   ("fill-both-args",

     parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   ("fill-d_d",

     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),

   ("fill-inner-deriv",

     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),

   ("fill-all",

     parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);

insert_errpats ["simplification","of_rationals"]

 ([("addition-of-fractions",

   [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",

    parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",

    parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",

    parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",

    parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],

   [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1},

    @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc},

    @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list);

(*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)

(* TODO insert_errpats overwrites instead of appending

insert_errpats ["simplification","of_rationals"]

 (("cancel", (*see master thesis gdarocy*)

    [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",

     (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",

     (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",

     (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",

     (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",

     (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",

     (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",

     (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",

     (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",

     (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",

     (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],

    [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));

val fillpats = [

  ("fill-cancel-left-num",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),

  ("fill-cancel-left-den",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),

  ("fill-cancel-none",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),

  ("fill-cancel-left-add-num1",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),

  ("fill-cancel-left-add-num2",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),

  ("fill-cancel-left-add-num3",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),

  ("fill-cancel-left-add-num4",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),

  ("fill-cancel-left-add-num5",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),

  ("fill-cancel-left-add-num6",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),

  ("fill-cancel-left-add-none",

    parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),

  ("fill-cancel-left-add-den1",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-den2",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-den3",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-den4",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-den5",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-den6",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

  ("fill-cancel-left-add-none",

    parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")

 ]: fillpat list;

*)

(* still ununsed; planned for stepToErrorpattern: this is just a reminder... *)

insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]

  (["chain-rule-diff-both", "cancel"]: errpatID list);

(* ...and all other related rls by hand;

   TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)

*}

section {* Plans for updating isac from Isabelle2011 to Isabelle2012 and Isabelle2013 *}

subsection {* (1) problem analysis *}

subsubsection {* (1.1) "Unsynchronized.ref" are not conformant with parallel Isabelle *}

text {* 

  "Unsynchronized.ref" make "Test_Isac.thy" unreliable, too: in Isabelle2009-2

  a (bad) trick with "check_unsynchronized_ref ()" was a way out; 

  however, this trick doesn't work anymore in Isabelle2011 

  (remarkably, "Interpret/calchead.sml" sometimes has an error, sometimes not

  when cutting/pasting check_unsynchronized_ref in Isabelle2011; 

  but this is permanently without errors in Isabelle2012).

  The major cases of "Unsynchronized.ref" are those in "~~/src/Tools/isac/calcelems.sml",

  thehier, ptyps, mets, theory', rew_ord', ruleset', calclist', 

  which shall be handled by "Theory_Data", see 

  "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml".

  The transition from the above "Unsynchronized.ref" to "Theory_Data" is a task 

  to be scheduled for several days. An exception is "thehier", see (1.2) (1.3) below.

*}

subsubsection {* (1.2) Removing "Unsynchronized.ref" depends on special cases *}

text {* 

  The difficulties in removing "Unsynchronized.ref" differ largely:

  * Rational.thy will be cleared by Diana Meindl's GCD_Poly.thy, this is easy;

  * other cases seem easy to clear, too

  * clearing "thehier" became harder from Isabelle2009-2 to Isabelle2011;

    for instance, isac's Context has been broken already there, because 

    essential functions from Isabelle2009-2 were dropped in Isabelle2011,

    see for instance "fun context_thy".

    Another obstacle for this case also seems "fun num_str".

  So (1.2) depends on (1.3).

*}

subsubsection {* (1.3) isac's numerals are not conformant with Isabelle *}

text {* 

  In 2002 isac already strived for floating point numbers. Since that time

  isac represents numerals as "Free", see below (*1*). These experiments are

  unsatisfactory with respect to logical soundness.

  Since Isabelle now has started to care about floating point numbers, it is high 

  time to adopt these together with the other numerals. Isabelle2012/13's numerals

  are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".

  The transition from "Free" to standard numerals is a task to be scheduled for 

  several weeks. The urgency of this task follows from the experience, 

  that (1.2) for "thehier" is very hard, because "num_str" seems to destroy 

  some of the long identifiers of theorems which would tremendously simplify

  building a hierarchy of theorems according to (1.2), see (*2*) below.

*}

ML {*(*1*) Free ("123.456", HOLogic.realT) *}

ML {*(*2*)

val unknown = filter ((curry op= "??.unknown") o fst) isacrlsthms;

unknown |> nth 1 |> snd 

  |> Print_Mode.setmp [] (Syntax.string_of_term (Proof_Context.init_global @{theory}));

unknown |> nth 2 |> snd 

  |> Print_Mode.setmp [] (Syntax.string_of_term (Proof_Context.init_global @{theory}));

(*but these seem ok:*)

  Thm.get_name_hint @{thm add_0};

  Thm.get_name_hint (num_str @{thm add_0});

*}

subsubsection {* (1.4) "axioms" are a legacy feature disappearing soon *}

text {*

  isac works with (many!) rewrite rules, which are defined as "axioms" since Isabelle2002

  and before: isac saved time by not proving any theorem.

  We have the message "Legacy feature! Old 'axioms' command -- use 'axiomatization' instead"

  for some time; Isabelle2013 still accepts it.

  This task affects collection of rewrite rules in "thehier".

*}

subsection {* (2) possible solutions *}

subsubsection {* (2.1) Tackle (1.1) (1.2) (1.3) (1.4) already in Isabelle2011 *}

text {*

  Advantage: we have a perfect "Test_Isac.thy" in all transitions Isabelle2011-->12-->13

  Disadvantage: (1.3) would require effort twice: Isabelle2011-->12 and 12-->13,

    because numerals in Isabelle2011 are quite different from Isabelle2012/13.

*}

subsubsection {* (2.2) Transition Isabelle2011-->12 with minimal effort *}

text {*

  Postpone (1.1) (1.2) (1.3) (1.4) and 

  * (1.4.1) manually insert those elements into "thehier" which are required for tests

  * make "Test_Isac.thy" perform equivalenty on Isabelle2011 and on Isabelle2012

    (and then on Isabelle2013).

    This might enforce to outcomment tests in Isabelle2011 marked "Isabelle2011-->12"

  Advantages:

    * the transition Isabelle2011-->12 can be accomplished within few days,

      and hopefully Isabelle2012-->13 in the same way

    * student projects (which seem independent of the outcommented tests "Isabelle2011-->12") 

      can start immediately

  Disadvantage:

    * we do not yet know details about the transition Isabelle2012-->13,

      which might be very different from Isabelle2011-->12

    * some tests are outcommented;

      However, if new regression tests come from new student project, 

      these provisionally do not concern "thehier".

*}

end