1.1 --- a/src/Tools/isac/ProgLang/Atools.thy Thu May 30 12:39:13 2019 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Sat Jun 01 11:09:19 2019 +0200
1.3 @@ -6,12 +6,18 @@
1.4 theory Atools imports Descript Script
1.5 begin
1.6
1.7 +subsection \<open>preparation to build up a program from rules\<close>
1.8 +
1.9 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
1.10 where "auto_generated t_t = t_t"
1.11 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
1.12 where "auto_generated_inst t_t v = t_t"
1.13 +
1.14 +subsection \<open>use preparation\<close>
1.15 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
1.16
1.17 +subsection \<open>consts & axiomatization\<close>
1.18 +
1.19 consts
1.20
1.21 Arbfix :: "real"
1.22 @@ -22,7 +28,7 @@
1.23 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
1.24
1.25 pow :: "[real, real] => real" (infixr "^^^" 80)
1.26 -(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
1.27 + (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
1.28 ~~~~ ~~~~ ~~~~ ~~~*)
1.29 (*WN0603 at FE-interface encoded strings to '^',
1.30 see 'fun encode', fun 'decode'*)
1.31 @@ -78,11 +84,11 @@
1.32 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
1.33
1.34
1.35 +subsection \<open>Coding standards\<close>
1.36 text \<open>copy from doc/math-eng.tex WN.28.3.03
1.37 WN071228 extended\<close>
1.38
1.39 -section \<open>Coding standards\<close>
1.40 -subsection \<open>Identifiers\<close>
1.41 +subsubsection \<open>Identifiers\<close>
1.42 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
1.43
1.44 This are the preliminary rules for naming identifiers>
1.45 @@ -96,7 +102,7 @@
1.46 \end{description}
1.47 %WN071228 extended\<close>
1.48
1.49 -subsection \<open>Rule sets\<close>
1.50 +subsubsection \<open>Rule sets\<close>
1.51 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
1.52
1.53 There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
1.54 @@ -125,11 +131,10 @@
1.55 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
1.56 \<close>
1.57
1.58 +subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>
1.59 ML \<open>
1.60 val thy = @{theory};
1.61
1.62 -(** evaluation of numerals and special predicates on the meta-level **)
1.63 -
1.64 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
1.65
1.66 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
1.67 @@ -415,9 +420,8 @@
1.68
1.69 \<close>
1.70
1.71 +subsection \<open>evaluation on the meta-level\<close>
1.72 ML \<open>
1.73 -(** evaluation on the metalevel **)
1.74 -
1.75 (*. evaluate HOL.divide .*)
1.76 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
1.77 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
1.78 @@ -512,9 +516,10 @@
1.79 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
1.80 end
1.81 | eval_boollist2sum _ _ _ _ = NONE;
1.82 +\<close>
1.83
1.84 -
1.85 -
1.86 +subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>
1.87 +ML \<open>
1.88 local
1.89
1.90 open Term;
1.91 @@ -524,10 +529,6 @@
1.92 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
1.93 end;
1.94
1.95 -
1.96 -(** rule set, for evaluating list-expressions in scripts 8.01.02 **)
1.97 -
1.98 -
1.99 val list_rls = Rule.append_rls "list_rls" list_rls
1.100 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.101 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.102 @@ -667,6 +668,7 @@
1.103 *)
1.104 "******* Atools.ML end *******";
1.105 \<close>
1.106 +subsection \<open>write to KEStore: calcs, rule-sets\<close>
1.107 setup \<open>KEStore_Elems.add_calcs
1.108 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
1.109 ("some_occur_in",