neuper@37906
|
1 |
(* Title: ~~~/isac/Isac_Mathengine.thy
|
neuper@37906
|
2 |
Author: Walther Neuper, TU Graz
|
neuper@37906
|
3 |
|
neuper@37910
|
4 |
$ cd /usr/local/Isabelle2009-1/src/Tools/isac
|
neuper@37906
|
5 |
$ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
|
neuper@37906
|
6 |
$ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
OR tty (unusable: after errors wrong toplevel):
|
neuper@37906
|
9 |
$ cd "/home/neuper/proto2/isac/src/sml"
|
neuper@37906
|
10 |
$ isabelle-process HOL HOL-Isac
|
neuper@37906
|
11 |
ML> use_thy "Isac_Mathengine";
|
neuper@37924
|
12 |
|
neuper@37924
|
13 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@37924
|
14 |
10 20 30 40 50 60 70 80
|
neuper@37906
|
15 |
*)
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
header {* Loading the isac mathengine *}
|
neuper@37906
|
18 |
|
neuper@37906
|
19 |
theory Isac_Mathengine
|
neuper@37906
|
20 |
(*imports Complex_Main*)
|
neuper@37906
|
21 |
imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
|
neuper@37906
|
22 |
begin
|
neuper@37906
|
23 |
|
neuper@37906
|
24 |
ML {* Toplevel.debug := true; *}
|
neuper@37906
|
25 |
use "library.sml"
|
neuper@37906
|
26 |
use "calcelems.sml"
|
neuper@37906
|
27 |
ML {* check_guhs_unique := true *}
|
neuper@37906
|
28 |
|
neuper@37906
|
29 |
use "Scripts/term_G.sml"
|
neuper@37906
|
30 |
use "Scripts/calculate.sml"
|
neuper@37906
|
31 |
use "Scripts/rewrite.sml"
|
neuper@37906
|
32 |
use_thy"Scripts/Script"
|
neuper@37906
|
33 |
use "Scripts/scrtools.sml"
|
neuper@37906
|
34 |
|
neuper@37925
|
35 |
use "ME/mstools.sml"
|
neuper@37925
|
36 |
use "ME/ctree.sml"
|
neuper@37927
|
37 |
use "ME/ptyps.sml"
|
neuper@37925
|
38 |
|
neuper@37925
|
39 |
|
neuper@37924
|
40 |
ML {*
|
neuper@37924
|
41 |
member;
|
neuper@37924
|
42 |
@{term 111};
|
neuper@37924
|
43 |
*}
|
neuper@37924
|
44 |
|
neuper@37924
|
45 |
|
neuper@37906
|
46 |
(*
|
neuper@37906
|
47 |
use "ME/generate.sml"
|
neuper@37906
|
48 |
use "ME/calchead.sml"
|
neuper@37906
|
49 |
use "ME/appl.sml"
|
neuper@37906
|
50 |
use "ME/rewtools.sml"
|
neuper@37906
|
51 |
use "ME/script.sml"
|
neuper@37906
|
52 |
use "ME/solve.sml"
|
neuper@37906
|
53 |
use "ME/inform.sml"
|
neuper@37906
|
54 |
use "ME/mathengine.sml"
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
use "xmlsrc/mathml.sml"
|
neuper@37906
|
57 |
use "xmlsrc/datatypes.sml"
|
neuper@37906
|
58 |
use "xmlsrc/pbl-met-hierarchy.sml"
|
neuper@37906
|
59 |
use "xmlsrc/thy-hierarchy.sml"
|
neuper@37906
|
60 |
use "xmlsrc/interface-xml.sml"
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
use "FE-interface/messages.sml"
|
neuper@37906
|
63 |
use "FE-interface/states.sml"
|
neuper@37906
|
64 |
use "FE-interface/interface.sml"
|
neuper@37906
|
65 |
|
neuper@37906
|
66 |
use "print_exn_G.sml"
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
text "**** build math-engine complete *************************"
|
neuper@37906
|
69 |
*)(*
|
neuper@37906
|
70 |
setup {*
|
neuper@37906
|
71 |
Code_Preproc.setup
|
neuper@37906
|
72 |
#> Code_ML.setup
|
neuper@37906
|
73 |
#> Code_Haskell.setup
|
neuper@37906
|
74 |
#> Nbe.setup
|
neuper@37906
|
75 |
*}
|
neuper@37906
|
76 |
*)
|
neuper@37906
|
77 |
|
neuper@37925
|
78 |
(*--------------------------shift to some isac-10 -------------------
|
neuper@37906
|
79 |
(*cleaner output from...*)
|
neuper@37906
|
80 |
ML_command {*
|
neuper@37906
|
81 |
"----- ";
|
neuper@37906
|
82 |
writeln "werwerw";
|
neuper@37906
|
83 |
*}
|
neuper@37906
|
84 |
|
neuper@37906
|
85 |
ML {* @{prop "False"} *}
|
neuper@37906
|
86 |
(*ML {* @{type "int"} *} only new version*)
|
neuper@37906
|
87 |
ML {* @{thm conjI} *}
|
neuper@37906
|
88 |
ML {* @{thms conjI TrueI} *}
|
neuper@37906
|
89 |
ML {* @{theory} *}
|
neuper@37906
|
90 |
|
neuper@37906
|
91 |
ML{* @{const_name plus} *} (*creates long names (extern names)*)
|
neuper@37906
|
92 |
term plus
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
term foo
|
neuper@37906
|
95 |
(*ML{* @{const_name foo} *} only new version*)
|
neuper@37906
|
96 |
|
neuper@37906
|
97 |
text {*
|
neuper@37906
|
98 |
werwer
|
neuper@37906
|
99 |
*}
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
ML {*
|
neuper@37906
|
102 |
fun inc_by_five x =
|
neuper@37906
|
103 |
x |> (fn x => x + 1)
|
neuper@37906
|
104 |
*}
|
neuper@37906
|
105 |
|
neuper@37906
|
106 |
(*canonical argument order introduced after 1997*)
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
text{*
|
neuper@37906
|
109 |
this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
|
neuper@37906
|
110 |
@{ML fold}
|
neuper@37906
|
111 |
|
neuper@37906
|
112 |
@{ML fold_rev}
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
for accumulating side results in |>
|
neuper@37906
|
115 |
@{ML fold_map}
|
neuper@37906
|
116 |
*}
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
ML {*
|
neuper@37906
|
119 |
val items = 1 upto 10;
|
neuper@37906
|
120 |
val l1 = fold cons items []; (*alternating useful frequently*)
|
neuper@37906
|
121 |
*}
|
neuper@37906
|
122 |
|
neuper@37906
|
123 |
ML{*
|
neuper@37906
|
124 |
fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
|
neuper@37906
|
125 |
*}
|
neuper@37906
|
126 |
ML{*
|
neuper@37906
|
127 |
merge_list (op =) ([3,2,1], [7,5,3,1]);
|
neuper@37906
|
128 |
merge_list (op =) ([3,2,1], [7,5,3,1]);
|
neuper@37906
|
129 |
*}
|
neuper@37906
|
130 |
|
neuper@37906
|
131 |
(*session 2-------Christian+Makarius---------------*)
|
neuper@37906
|
132 |
ML{*
|
neuper@37906
|
133 |
let
|
neuper@37906
|
134 |
val ctxt = @{context}
|
neuper@37906
|
135 |
in 1 end
|
neuper@37906
|
136 |
*}
|
neuper@37906
|
137 |
|
neuper@37906
|
138 |
(* build and handle tables THIS IS THE ACCESS-STRUCTURE...
|
neuper@37906
|
139 |
ML{*
|
neuper@37906
|
140 |
structure Data = Theory_Data
|
neuper@37906
|
141 |
(
|
neuper@37906
|
142 |
type T = term Symtab.table
|
neuper@37906
|
143 |
val empty = Symtab.empty
|
neuper@37906
|
144 |
val extend = O
|
neuper@37906
|
145 |
fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
|
neuper@37906
|
146 |
)
|
neuper@37906
|
147 |
*}
|
neuper@37906
|
148 |
*)
|
neuper@37906
|
149 |
(*session 3-------Blanchette--------------------
|
neuper@37906
|
150 |
working on nitpic, ML level tool
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
SEE THESE LECTURE NOTES !!!*)
|
neuper@37906
|
153 |
|
neuper@37906
|
154 |
(*
|
neuper@37906
|
155 |
ML{*
|
neuper@37906
|
156 |
Const ("x", dummyT) |> Syntax.check_term @{context}
|
neuper@37906
|
157 |
^^^^^^^^^^^^^^^^^
|
neuper@37906
|
158 |
*}
|
neuper@37906
|
159 |
*)
|
neuper@37906
|
160 |
|
neuper@37906
|
161 |
text{*
|
neuper@37906
|
162 |
SEE funs for
|
neuper@37906
|
163 |
# deleting identifiers
|
neuper@37906
|
164 |
# handle Bounds when made visible
|
neuper@37906
|
165 |
# kill trivial quantifiers, e.g. \foral x. (NO x)
|
neuper@37906
|
166 |
# handling name clashes in Abs
|
neuper@37906
|
167 |
# which constants, free vars ... occur in a term !!!!!!!!!!!
|
neuper@37906
|
168 |
# Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
|
neuper@37906
|
169 |
# get fresh Const, Var
|
neuper@37906
|
170 |
# use the "Name" structure
|
neuper@37906
|
171 |
|
neuper@37906
|
172 |
*}
|
neuper@37906
|
173 |
|
neuper@37906
|
174 |
ML{* val context = Name.make_context ["d"] *}
|
neuper@37906
|
175 |
|
neuper@37906
|
176 |
(*
|
neuper@37906
|
177 |
ML{* Name.invents context "foo" 10 *}
|
neuper@37906
|
178 |
(*ML{* Name variants ... *}*)
|
neuper@37906
|
179 |
*)
|
neuper@37925
|
180 |
--------------------------shift to some isac-10 -------------------*)
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
end
|
neuper@37906
|
183 |
|