wneuper/isa: comparison src/Tools/isac/ProgLang/Atools.thy

equal deleted inserted replaced

-:d44ce0c098a0
+:e0e3d41ef86c
 *)
 theory Atools imports Descript Script
 begin
+subsection \<open>preparation to build up a program from rules\<close>
 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
 where "auto_generated t_t = t_t"
 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
 where "auto_generated_inst t_t v =  t_t"
+subsection \<open>use preparation\<close>
 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
+subsection \<open>consts & axiomatization\<close>
 consts
 Arbfix           :: "real"
 Undef            :: "real"
 some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
 occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
 pow              :: "[real, real] => real"    (infixr "^^^" 80)
 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
 ~~~~     ~~~~    ~~~~     ~~~*)
 (*WN0603 at FE-interface encoded strings to '^',
 	see 'fun encode', fun 'decode'*)
 abs              :: "real => real"            ("(|| _ ||)")
 		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
 rat_leq3:	      "b ~= 0 ==>
 		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
+subsection \<open>Coding standards\<close>
 text \<open>copy from doc/math-eng.tex WN.28.3.03
 WN071228 extended\<close>
-section \<open>Coding standards\<close>
+subsubsection \<open>Identifiers\<close>
-subsection \<open>Identifiers\<close>
 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).
 This are the preliminary rules for naming identifiers>
 \begin{description}
 \item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
 \item [???] ???
 \item [???] ???
 \end{description}
 %WN071228 extended\<close>
-subsection \<open>Rule sets\<close>
+subsubsection \<open>Rule sets\<close>
 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.
 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.
 \begin{description}
 \end{description}
 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
 \<close>
+subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>
 ML \<open>
 val thy = @{theory};
-(** evaluation of numerals and special predicates on the meta-level **)
 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
 fun eval_occurs_in _ "Atools.occurs'_in"
 *)
 \<close>
+subsection \<open>evaluation on the meta-level\<close>
 ML \<open>
-(** evaluation on the metalevel **)
 (*. evaluate HOL.divide .*)
 (*("DIVIDE" ,("Rings.divide_class.divide"  ,eval_cancel "#divide_e"))*)
 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
 	val sum = list2sum lhss
 in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
 	  HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
 end
 | eval_boollist2sum _ _ _ _ = NONE;
+\<close>
+subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>
+ML \<open>
 local
 open Term;
 in
 fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
 end;
-(** rule set, for evaluating list-expressions in scripts 8.01.02 **)
 val list_rls = Rule.append_rls "list_rls" list_rls
 	 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
 		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 		Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
 scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
 });
 *)
 "******* Atools.ML end *******";
 \<close>
+subsection \<open>write to KEStore: calcs, rule-sets\<close>
 setup \<open>KEStore_Elems.add_calcs
 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
 ("some_occur_in",
 ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
 ("is_atom"  ,("Atools.is'_atom", eval_is_atom "#is_atom_")),

changeset 59549	e0e3d41ef86c
parent 59547	a6dcec53aec0
child 59585	0bb418c3855a