wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              CalcTreeTEST;

    10   open LItool;                 arguments_from_model;

    11   open Sub_Problem;

    12   open Fetch_Tacs;

    13   open Step

    14   open Env;

    15   open LI;                     scan_dn;

    16   open Istate;

    17   open Error_Pattern;

    18   open Error_Pattern_Def;

    19   open Specification;

    20   open Ctree;                  append_problem;

    21   open Pos;

    22   open Program;

    23   open Prog_Tac;

    24   open Tactical;

    25   open Prog_Expr;

    26   open Auto_Prog;              rule2stac;

    27   open Input_Descript;

    28   open Specify;

    29   open Specify;

    30   open Step_Specify;

    31   open Step_Solve;

    32   open Step;

    33   open Solve;                  (* NONE *)

    34   open ContextC;               transfer_asms_from_to;

    35   open Tactic;                 (* NONE *)

    36   open I_Model;

    37   open O_Model;

    38   open P_Model;                (* NONE *)

    39   open Rewrite;

    40   open Eval;                   get_pair;

    41   open TermC;                  atomt;

    42   open Rule;

    43   open Rule_Set;               Sequence;

    44   open Eval_Def

    45   open ThyC

    46   open ThmC_Def

    47   open ThmC

    48   open Rewrite_Ord

    49   open UnparseC

    50 \<close>

    51 ML_file "BridgeJEdit/parseC.sml"

    53 section \<open>code for copy & paste ===============================================================\<close>

    54 ML \<open>

    55 "~~~~~ fun xxx , args:"; val () = ();

    56 "~~~~~ and xxx , args:"; val () = ();

    57 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    58 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);

    59 "xx"

    60 ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)

    61 (*/------------------- step into XXXXX -----------------------------------------------------\*)

    62 (*-------------------- stop step into XXXXX -------------------------------------------------*)

    63 (*\------------------- step into XXXXX -----------------------------------------------------/*)

    64 (*-------------------- contiue step into XXXXX ----------------------------------------------*)

    65 (*/------------------- check entry to XXXXX ------------------------------------------------\*)

    66 (*\------------------- check entry to XXXXX ------------------------------------------------/*)

    67 (*/------------------- check within XXXXX --------------------------------------------------\*)

    68 (*\------------------- check within XXXXX --------------------------------------------------/*)

    69 (*/------------------- check result of XXXXX -----------------------------------------------\*)

    70 (*\------------------- check result of XXXXX -----------------------------------------------/*)

    71 (* final test ...*)

    72 (*/------------------- build new fun XXXXX -------------------------------------------------\*)

    73 (*\------------------- build new fun XXXXX -------------------------------------------------/*)

    74 \<close> ML \<open>

    75 \<close>

    76 ML \<open>

    77 \<close> ML \<open>

    78 \<close> ML \<open>

    79 \<close>

    80 text \<open>

    81   declare [[show_types]]

    82   declare [[show_sorts]]

    83   find_theorems "?a <= ?a"

    85   print_theorems

    86   print_facts

    87   print_statement ""

    88   print_theory

    89   ML_command \<open>Pretty.writeln prt\<close>

    90   declare [[ML_print_depth = 999]]

    91   declare [[ML_exception_trace]]

    92 \<close>

    94 section \<open>====== ML_file "MathEngBasic/thmC.sml" ============================================\<close>

    95 ML \<open>

    96 \<close> ML \<open>

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

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

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

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

   101   (@{theory Isac_Knowledge},

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

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

   105 else error "input to revert_sym_rule CHANGED";

   107 \<close> ML \<open>

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

   109 \<close> ML \<open>

   110           val id' = id_drop_sym id

   111 \<close> ML \<open>

   112           val thm' = thm_from_thy thy id'

   113 \<close> ML \<open>

   114           val id'' = Thm.get_name_hint thm'

   115 \<close> ML \<open>

   116 val thy = @{theory Isac_Knowledge}

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

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

   119 ;

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

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

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

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

   125 ;

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

   127 then () else error "fun revert_sym_rule changed 2"

   128 \<close> ML \<open>

   129 \<close> ML \<open>

   130 \<close> ML \<open>

   131 \<close> ML \<open>

   132 \<close> ML \<open>

   133 \<close> ML \<open>

   134 \<close> ML \<open>

   135 \<close> ML \<open>

   136 \<close> ML \<open>

   137 \<close>

   139 section \<open>=========== ML_file "BridgeLibisabelle/thy-hierarchy.sml" ======================\<close>

   140 ML \<open>

   141 \<close> ML \<open>

   142 \<close> ML \<open>

   143 "----------- fun ThmC_Def.make_thm ------------------------------------";

   144 "----------- fun ThmC_Def.make_thm ------------------------------------";

   145 "----------- fun ThmC_Def.make_thm ------------------------------------";

   146 "~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Write.authors)) =

   147   (@{theory "Biegelinie"}, "IsacKnowledge",

   148     ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),

   149 	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);

   150     val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID

   151     val theID = Thy_Present.guh2theID guh;

   152 if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso

   153   theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]

   154 then () else error "store_thm: guh | theID changed";

   156 \<close> ML \<open> (*ERROR "??.unknown"*)

   157 "----------- fun thms_of_rlss ------------------------------------";

   158 "----------- fun thms_of_rlss ------------------------------------";

   159 "----------- fun thms_of_rlss ------------------------------------";

   160 \<close> ML \<open>

   161 val rlss =

   162   [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),

   163   ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]:

   164    (id                          * (id             * Rule_Def.rule_set)) list

   165 ;

   166 \<close> ML \<open>

   167 (*--- fun ThmC_Def.make_thm --- avoids ERROR BELOW Undefined fact: "real_mult_minus1"*)

   168 (*+*)thms_of_rlss thy rlss (* = [("??.unknown", "?a - ?b = ?a + -1 * ?b")]: (string * thm) list*)

   169 \<close> ML \<open>

   170 (*+*)Rule_Set.empty: Rule_Def.rule_set

   171 \<close> ML \<open>

   172 (*+*)discard_minus: Rule_Def.rule_set

   173 \<close> ML \<open>

   174 val [_, (thmID, term)] = thms_of_rlss thy rlss;

   176 \<close> ML \<open>

   177 if thmID = "real_mult_minus1" (* WAS "??.unknown" *)

   178 then () else error "thms_of_rlss changed";

   180 \<close> ML \<open>

   181 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);

   182 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)

   183   |> map (Thy_Present.thms_of_rls o #2 o #2)

   184     (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),

   185       Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)

   186   |> flat

   187     (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),

   188       Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)

   189   |> map (ThmC.revert_sym_rule thy)

   190     (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),

   191       Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)

   192   |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))

   193     (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,

   194       ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)

   195   |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);

   196 \<close> ML \<open>

   197 \<close> ML \<open>

   198 \<close> ML \<open>

   199 \<close> ML \<open>

   200 \<close> ML \<open>

   201 \<close> ML \<open>

   202 \<close> ML \<open>

   203 \<close> ML \<open>

   204 \<close> ML \<open>

   205 \<close> ML \<open>

   206 \<close>

   208 section \<open>===================================================================================\<close>

   209 ML \<open>

   210 \<close> ML \<open>

   211 \<close> ML \<open>

   212 \<close> ML \<open>

   213 \<close>

   215 section \<open>code for copy & paste ===============================================================\<close>

   216 ML \<open>

   217 "~~~~~ fun xxx , args:"; val () = ();

   218 "~~~~~ and xxx , args:"; val () = ();

   219 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

   220 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*);

   221 "xx"

   222 ^ "xxx"   (*+*)

   223 \<close>

   224 end

author	wenzelm
	Mon, 19 Apr 2021 19:55:31 +0200
changeset 60236	de0ccac9f862
parent 60223	740ebee5948b
child 60258	a5eed208b22f
permissions	-rw-r--r--