1.1 --- a/src/Pure/isac/#Isac_Mathengine.thy#	Thu Jul 22 10:40:19 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,176 +0,0 @@
     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 -