| author | wneuper <Walther.Neuper@jku.at> |
| Wed, 11 Jan 2023 09:23:18 +0100 | |
| changeset 60649 | b2ff1902420f |
| parent 60648 | 976b99bcfc96 |
| child 60658 | 1c089105f581 |
| permissions | -rw-r--r-- |
| walther@59603 | 1 |
theory Test_Some |
| walther@60387 | 2 |
imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" |
| wneuper@59265 | 3 |
begin |
| walther@59814 | 4 |
|
| walther@59814 | 5 |
ML \<open>open ML_System\<close> |
| wneuper@59472 | 6 |
ML \<open> |
| wneuper@59265 | 7 |
open Kernel; |
| walther@59814 | 8 |
open Math_Engine; |
| Walther@60571 | 9 |
open Test_Code; Test_Code.init_calc @{context};
|
| walther@60126 | 10 |
open LItool; arguments_from_model; |
| walther@59817 | 11 |
open Sub_Problem; |
| walther@59858 | 12 |
open Fetch_Tacs; |
| walther@59807 | 13 |
open Step |
| walther@59659 | 14 |
open Env; |
| walther@59814 | 15 |
open LI; scan_dn; |
| wneuper@59578 | 16 |
open Istate; |
| walther@59909 | 17 |
open Error_Pattern; |
| walther@59909 | 18 |
open Error_Pattern_Def; |
| walther@59977 | 19 |
open Specification; |
| walther@60126 | 20 |
open Ctree; append_problem; |
| walther@59696 | 21 |
open Pos; |
| walther@59618 | 22 |
open Program; |
| wneuper@59601 | 23 |
open Prog_Tac; |
| walther@59603 | 24 |
open Tactical; |
| walther@59603 | 25 |
open Prog_Expr; |
| walther@60126 | 26 |
open Auto_Prog; rule2stac; |
| walther@59618 | 27 |
open Input_Descript; |
| walther@59971 | 28 |
open Specify; |
| walther@59976 | 29 |
open Specify; |
| walther@59814 | 30 |
open Step_Specify; |
| walther@59814 | 31 |
open Step_Solve; |
| walther@59814 | 32 |
open Step; |
| wneuper@59316 | 33 |
open Solve; (* NONE *) |
| walther@60126 | 34 |
open ContextC; transfer_asms_from_to; |
| wneuper@59575 | 35 |
open Tactic; (* NONE *) |
| walther@60126 | 36 |
open I_Model; |
| walther@60126 | 37 |
open O_Model; |
| walther@60126 | 38 |
open P_Model; (* NONE *) |
| walther@59874 | 39 |
open Rewrite; |
| walther@60126 | 40 |
open Eval; get_pair; |
| wneuper@59417 | 41 |
open TermC; atomt; |
| walther@59858 | 42 |
open Rule; |
| walther@59969 | 43 |
open Rule_Set; Sequence; |
| walther@59919 | 44 |
open Eval_Def |
| walther@59858 | 45 |
open ThyC |
| walther@59865 | 46 |
open ThmC_Def |
| walther@59858 | 47 |
open ThmC |
| walther@59858 | 48 |
open Rewrite_Ord |
| Walther@60608 | 49 |
open UnparseC; |
| Walther@60608 | 50 |
|
| Walther@60608 | 51 |
Know_Store.set_ref_last_thy @{theory};
|
| Walther@60608 | 52 |
(*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*) |
| wenzelm@60223 | 53 |
\<close> |
| neuper@48765 | 54 |
|
| wneuper@59472 | 55 |
section \<open>code for copy & paste ===============================================================\<close> |
| wneuper@59472 | 56 |
ML \<open> |
| wneuper@59535 | 57 |
"~~~~~ fun xxx , args:"; val () = (); |
| walther@59655 | 58 |
"~~~~~ and xxx , args:"; val () = (); |
| walther@60220 | 59 |
"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
| Walther@60578 | 60 |
"~~~~~ continue fun xxx"; val () = (); |
| walther@60262 | 61 |
(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); |
| wneuper@59579 | 62 |
"xx" |
| Walther@60629 | 63 |
^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**) |
| Walther@60567 | 64 |
\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*) |
| Walther@60567 | 65 |
(*//----------------- adhoc inserted n ----------------------------------------------------\\*) |
| Walther@60567 | 66 |
(*\\------------------ adhoc inserted n ----------------------------------------------------//*) |
| Walther@60567 | 67 |
\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*) |
| Walther@60567 | 68 |
|
| Walther@60567 | 69 |
\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*) |
| Walther@60567 | 70 |
(*//------------------ step into XXXXX -----------------------------------------------------\\*) |
| Walther@60629 | 71 |
(*keep for continuing YYYYY*) |
| Walther@60578 | 72 |
\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*) |
| Walther@60578 | 73 |
(*-------------------- continuing XXXXX ------------------------------------------------------*) |
| Walther@60578 | 74 |
(*kept for continuing XXXXX*) |
| Walther@60567 | 75 |
(*-------------------- stop step into XXXXX --------------------------------------------------*) |
| Walther@60567 | 76 |
\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*) |
| Walther@60567 | 77 |
(*\\------------------ step into XXXXX -----------------------------------------------------//*) |
| Walther@60567 | 78 |
\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*) |
| Walther@60567 | 79 |
|
| Walther@60567 | 80 |
(*/------------------- check entry to XXXXX -------------------------------------------------\*) |
| Walther@60567 | 81 |
(*\------------------- check entry to XXXXX -------------------------------------------------/*) |
| Walther@60567 | 82 |
(*/------------------- check within XXXXX ---------------------------------------------------\*) |
| Walther@60567 | 83 |
(*\------------------- check within XXXXX ---------------------------------------------------/*) |
| Walther@60567 | 84 |
(*/------------------- check result of XXXXX ------------------------------------------------\*) |
| Walther@60567 | 85 |
(*\------------------- check result of XXXXX ------------------------------------------------/*) |
| Walther@60567 | 86 |
(* final test ... ----------------------------------------------------------------------------*) |
| Walther@60567 | 87 |
|
| Walther@60578 | 88 |
\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*) |
| Walther@60578 | 89 |
(*//------------------ inserted hidden code ------------------------------------------------\\*) |
| Walther@60578 | 90 |
(*\\------------------ inserted hidden code ------------------------------------------------//*) |
| Walther@60578 | 91 |
\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*) |
| Walther@60578 | 92 |
|
| Walther@60567 | 93 |
\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*) |
| Walther@60567 | 94 |
(*//------------------ build new fun XXXXX -------------------------------------------------\\*) |
| Walther@60567 | 95 |
(*\\------------------ build new fun XXXXX -------------------------------------------------//*) |
| Walther@60567 | 96 |
\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*) |
| wneuper@59472 | 97 |
\<close> |
| walther@59723 | 98 |
ML \<open> |
| walther@59723 | 99 |
\<close> ML \<open> |
| walther@59723 | 100 |
\<close> ML \<open> |
| walther@59723 | 101 |
\<close> |
| wneuper@59472 | 102 |
text \<open> |
| neuper@52101 | 103 |
declare [[show_types]] |
| Walther@60576 | 104 |
declare [[show_sorts]] |
| neuper@52101 | 105 |
find_theorems "?a <= ?a" |
| neuper@52101 | 106 |
|
| wneuper@59230 | 107 |
print_theorems |
| neuper@52101 | 108 |
print_facts |
| neuper@52101 | 109 |
print_statement "" |
| neuper@52101 | 110 |
print_theory |
| wneuper@59230 | 111 |
ML_command \<open>Pretty.writeln prt\<close> |
| wneuper@59230 | 112 |
declare [[ML_print_depth = 999]] |
| wneuper@59252 | 113 |
declare [[ML_exception_trace]] |
| wneuper@59472 | 114 |
\<close> |
| walther@59655 | 115 |
|
| walther@60260 | 116 |
section \<open>===================================================================================\<close> |
| walther@60007 | 117 |
ML \<open> |
| walther@60007 | 118 |
\<close> ML \<open> |
| walther@60007 | 119 |
\<close> ML \<open> |
| walther@60007 | 120 |
\<close> ML \<open> |
| walther@60007 | 121 |
\<close> |
| walther@60007 | 122 |
|
| Walther@60649 | 123 |
section \<open>===================================================================================\<close> |
| Walther@60531 | 124 |
ML \<open> |
| Walther@60531 | 125 |
\<close> ML \<open> |
| Walther@60531 | 126 |
\<close> ML \<open> |
| walther@60406 | 127 |
\<close> ML \<open> |
| walther@60406 | 128 |
\<close> |
| walther@60406 | 129 |
|
| Walther@60640 | 130 |
section \<open>===================================================================================\<close> |
| Walther@60631 | 131 |
ML \<open> |
| Walther@60631 | 132 |
\<close> ML \<open> |
| Walther@60631 | 133 |
\<close> ML \<open> |
| Walther@60632 | 134 |
\<close> ML \<open> |
| walther@59842 | 135 |
\<close> |
| walther@59834 | 136 |
|
| wneuper@59535 | 137 |
section \<open>code for copy & paste ===============================================================\<close> |
| wneuper@59535 | 138 |
ML \<open> |
| wneuper@59531 | 139 |
"~~~~~ fun xxx , args:"; val () = (); |
| Walther@60567 | 140 |
"~~~~~ and xxx , args:"; val () = (); |
| Walther@60567 | 141 |
"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
| Walther@60578 | 142 |
"~~~~~ continue fun xxx"; val () = (); |
| walther@60262 | 143 |
(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); |
| wneuper@59582 | 144 |
"xx" |
| Walther@60629 | 145 |
^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**) |
| Walther@60567 | 146 |
\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*) |
| Walther@60567 | 147 |
(*//----------------- adhoc inserted n ----------------------------------------------------\\*) |
| Walther@60567 | 148 |
(*\\------------------ adhoc inserted n ----------------------------------------------------//*) |
| Walther@60567 | 149 |
\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*) |
| Walther@60567 | 150 |
|
| Walther@60567 | 151 |
\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*) |
| Walther@60567 | 152 |
(*//------------------ step into XXXXX -----------------------------------------------------\\*) |
| Walther@60629 | 153 |
(*keep for continuing YYYYY*) |
| Walther@60578 | 154 |
\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*) |
| Walther@60578 | 155 |
(*-------------------- continuing XXXXX ------------------------------------------------------*) |
| Walther@60578 | 156 |
(*kept for continuing XXXXX*) |
| Walther@60567 | 157 |
(*-------------------- stop step into XXXXX --------------------------------------------------*) |
| Walther@60567 | 158 |
\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*) |
| Walther@60567 | 159 |
(*\\------------------ step into XXXXX -----------------------------------------------------//*) |
| Walther@60567 | 160 |
\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*) |
| Walther@60567 | 161 |
|
| Walther@60578 | 162 |
(*/------------------- check entry to XXXXX -------------------------------------------------\*) |
| Walther@60578 | 163 |
(*\------------------- check entry to XXXXX -------------------------------------------------/*) |
| Walther@60578 | 164 |
(*/------------------- check within XXXXX ---------------------------------------------------\*) |
| Walther@60578 | 165 |
(*\------------------- check within XXXXX ---------------------------------------------------/*) |
| Walther@60578 | 166 |
(*/------------------- check result of XXXXX ------------------------------------------------\*) |
| Walther@60578 | 167 |
(*\------------------- check result of XXXXX ------------------------------------------------/*) |
| Walther@60578 | 168 |
(* final test ... ----------------------------------------------------------------------------*) |
| Walther@60578 | 169 |
|
| Walther@60578 | 170 |
\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*) |
| Walther@60578 | 171 |
(*//------------------ inserted hidden code ------------------------------------------------\\*) |
| Walther@60578 | 172 |
(*\\------------------ inserted hidden code ------------------------------------------------//*) |
| Walther@60578 | 173 |
\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*) |
| Walther@60578 | 174 |
|
| Walther@60567 | 175 |
\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*) |
| Walther@60567 | 176 |
(*//------------------ build new fun XXXXX -------------------------------------------------\\*) |
| Walther@60567 | 177 |
(*\\------------------ build new fun XXXXX -------------------------------------------------//*) |
| Walther@60567 | 178 |
\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*) |
| wneuper@59535 | 179 |
\<close> |
| neuper@41943 | 180 |
end |