1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,174 @@
1.4 +(* Title: ~~~/isac/Isac_Mathengine.thy
1.5 + Author: Walther Neuper, TU Graz
1.6 +
1.7 +$ cd /usr/local/Isabelle2009-1/src/Pure/isac
1.8 +$ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
1.9 +$ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
1.10 +
1.11 +OR tty (unusable: after errors wrong toplevel):
1.12 +$ cd "/home/neuper/proto2/isac/src/sml"
1.13 +$ isabelle-process HOL HOL-Isac
1.14 +ML> use_thy "Isac_Mathengine";
1.15 +*)
1.16 +
1.17 +header {* Loading the isac mathengine *}
1.18 +
1.19 +theory Isac_Mathengine
1.20 +(*imports Complex_Main*)
1.21 +imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
1.22 +begin
1.23 +
1.24 +ML {* Toplevel.debug := true; *}
1.25 +
1.26 +use "library.sml"
1.27 +use "calcelems.sml"
1.28 +ML {* check_guhs_unique := true *}
1.29 +
1.30 +use "Scripts/term_G.sml"
1.31 +use "Scripts/calculate.sml"
1.32 +
1.33 +use "Scripts/rewrite.sml"
1.34 +use_thy"Scripts/Script"
1.35 +
1.36 +use "Scripts/scrtools.sml"
1.37 +
1.38 +(*
1.39 +use "ME/mstools.sml"
1.40 +use "ME/ctree.sml"
1.41 +use "ME/ptyps.sml"
1.42 +use "ME/generate.sml"
1.43 +use "ME/calchead.sml"
1.44 +use "ME/appl.sml"
1.45 +use "ME/rewtools.sml"
1.46 +use "ME/script.sml"
1.47 +use "ME/solve.sml"
1.48 +use "ME/inform.sml"
1.49 +use "ME/mathengine.sml"
1.50 +
1.51 +use "xmlsrc/mathml.sml"
1.52 +use "xmlsrc/datatypes.sml"
1.53 +use "xmlsrc/pbl-met-hierarchy.sml"
1.54 +use "xmlsrc/thy-hierarchy.sml"
1.55 +use "xmlsrc/interface-xml.sml"
1.56 +
1.57 +use "FE-interface/messages.sml"
1.58 +use "FE-interface/states.sml"
1.59 +use "FE-interface/interface.sml"
1.60 +
1.61 +use "print_exn_G.sml"
1.62 +
1.63 +text "**** build math-engine complete *************************"
1.64 +*)(*
1.65 +setup {*
1.66 + Code_Preproc.setup
1.67 + #> Code_ML.setup
1.68 + #> Code_Haskell.setup
1.69 + #> Nbe.setup
1.70 +*}
1.71 +*)
1.72 +
1.73 +
1.74 +(*cleaner output from...*)
1.75 +ML_command {*
1.76 +"----- ";
1.77 +writeln "werwerw";
1.78 +*}
1.79 +
1.80 +ML {* @{prop "False"} *}
1.81 +(*ML {* @{type "int"} *} only new version*)
1.82 +ML {* @{thm conjI} *}
1.83 +ML {* @{thms conjI TrueI} *}
1.84 +ML {* @{theory} *}
1.85 +
1.86 +ML{* @{const_name plus} *} (*creates long names (extern names)*)
1.87 +term plus
1.88 +
1.89 +term foo
1.90 +(*ML{* @{const_name foo} *} only new version*)
1.91 +
1.92 +text {*
1.93 +werwer
1.94 + *}
1.95 +
1.96 +ML {*
1.97 + fun inc_by_five x =
1.98 + x |> (fn x => x + 1)
1.99 +*}
1.100 +
1.101 +(*canonical argument order introduced after 1997*)
1.102 +
1.103 +text{*
1.104 +this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
1.105 +@{ML fold}
1.106 +
1.107 +@{ML fold_rev}
1.108 +
1.109 +for accumulating side results in |>
1.110 +@{ML fold_map}
1.111 +*}
1.112 +
1.113 +ML {*
1.114 + val items = 1 upto 10;
1.115 + val l1 = fold cons items []; (*alternating useful frequently*)
1.116 +*}
1.117 +
1.118 +ML{*
1.119 + fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
1.120 +*}
1.121 +ML{*
1.122 + merge_list (op =) ([3,2,1], [7,5,3,1]);
1.123 + merge_list (op =) ([3,2,1], [7,5,3,1]);
1.124 +*}
1.125 +
1.126 +(*session 2-------Christian+Makarius---------------*)
1.127 +ML{*
1.128 +let
1.129 + val ctxt = @{context}
1.130 +in 1 end
1.131 +*}
1.132 +
1.133 +(* build and handle tables THIS IS THE ACCESS-STRUCTURE...
1.134 +ML{*
1.135 + structure Data = Theory_Data
1.136 + (
1.137 + type T = term Symtab.table
1.138 + val empty = Symtab.empty
1.139 + val extend = O
1.140 + fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
1.141 + )
1.142 +*}
1.143 +*)
1.144 +(*session 3-------Blanchette--------------------
1.145 +working on nitpic, ML level tool
1.146 +
1.147 +SEE THESE LECTURE NOTES !!!*)
1.148 +
1.149 +(*
1.150 +ML{*
1.151 +Const ("x", dummyT) |> Syntax.check_term @{context}
1.152 + ^^^^^^^^^^^^^^^^^
1.153 +*}
1.154 +*)
1.155 +
1.156 +text{*
1.157 +SEE funs for
1.158 +# deleting identifiers
1.159 +# handle Bounds when made visible
1.160 +# kill trivial quantifiers, e.g. \foral x. (NO x)
1.161 +# handling name clashes in Abs
1.162 +# which constants, free vars ... occur in a term !!!!!!!!!!!
1.163 +# Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
1.164 +# get fresh Const, Var
1.165 +# use the "Name" structure
1.166 +
1.167 +*}
1.168 +
1.169 +ML{* val context = Name.make_context ["d"] *}
1.170 +
1.171 +(*
1.172 +ML{* Name.invents context "foo" 10 *}
1.173 +(*ML{* Name variants ... *}*)
1.174 +*)
1.175 +
1.176 +end
1.177 +