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