1 (* Title: ~~~/isac/Isac_Mathengine.thy
2 Author: Walther Neuper, TU Graz
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac
5 $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
6 $ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
8 OR tty (unusable: after errors wrong toplevel):
9 $ cd "/home/neuper/proto2/isac/src/sml"
10 $ isabelle-process HOL HOL-Isac
11 ML> use_thy "Isac_Mathengine";
13 12345678901234567890123456789012345678901234567890123456789012345678901234567890
14 10 20 30 40 50 60 70 80
17 header {* Loading the isac mathengine *}
19 theory Isac_Mathengine
20 (*imports Complex_Main*)
21 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
24 ML {* Toplevel.debug := true; *}
27 ML {* check_guhs_unique := true *}
29 use "Scripts/term_G.sml"
30 use "Scripts/calculate.sml"
31 use "Scripts/rewrite.sml"
32 use_thy"Scripts/Script"
33 use "Scripts/scrtools.sml"
53 use "ME/mathengine.sml"
55 use "xmlsrc/mathml.sml"
56 use "xmlsrc/datatypes.sml"
57 use "xmlsrc/pbl-met-hierarchy.sml"
58 use "xmlsrc/thy-hierarchy.sml"
59 use "xmlsrc/interface-xml.sml"
61 use "FE-interface/messages.sml"
62 use "FE-interface/states.sml"
63 use "FE-interface/interface.sml"
67 text "**** build math-engine complete *************************"
77 (*--------------------------shift to some isac-10 -------------------
78 (*cleaner output from...*)
84 ML {* @{prop "False"} *}
85 (*ML {* @{type "int"} *} only new version*)
87 ML {* @{thms conjI TrueI} *}
90 ML{* @{const_name plus} *} (*creates long names (extern names)*)
94 (*ML{* @{const_name foo} *} only new version*)
105 (*canonical argument order introduced after 1997*)
108 this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
113 for accumulating side results in |>
118 val items = 1 upto 10;
119 val l1 = fold cons items []; (*alternating useful frequently*)
123 fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
126 merge_list (op =) ([3,2,1], [7,5,3,1]);
127 merge_list (op =) ([3,2,1], [7,5,3,1]);
130 (*session 2-------Christian+Makarius---------------*)
133 val ctxt = @{context}
137 (* build and handle tables THIS IS THE ACCESS-STRUCTURE...
139 structure Data = Theory_Data
141 type T = term Symtab.table
142 val empty = Symtab.empty
144 fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
148 (*session 3-------Blanchette--------------------
149 working on nitpic, ML level tool
151 SEE THESE LECTURE NOTES !!!*)
155 Const ("x", dummyT) |> Syntax.check_term @{context}
162 # deleting identifiers
163 # handle Bounds when made visible
164 # kill trivial quantifiers, e.g. \foral x. (NO x)
165 # handling name clashes in Abs
166 # which constants, free vars ... occur in a term !!!!!!!!!!!
167 # Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
168 # get fresh Const, Var
169 # use the "Name" structure
173 ML{* val context = Name.make_context ["d"] *}
176 ML{* Name.invents context "foo" 10 *}
177 (*ML{* Name variants ... *}*)
179 --------------------------shift to some isac-10 -------------------*)