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