1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Aug 24 13:16:17 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 26 09:20:07 2019 +0200
1.3 @@ -582,7 +582,7 @@
1.4 let
1.5 val (po, p_) = pos
1.6 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_input_tactic " ^ pos_2str p_)
1.7 - val (p'',_,_,pt'') = Generate.generate1 thy tac' (Istate.Pstate is, ctxt) (po', p_) pt
1.8 + val (p'',_,_,pt'') = Generate.generate1 @{theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
1.9 in
1.10 Unsafe_Step ((pt'',p''), Istate.Pstate is, get_ctxt ctree pos', tac')
1.11 end
2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sat Aug 24 13:16:17 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon Aug 26 09:20:07 2019 +0200
2.3 @@ -1,4 +1,5 @@
2.4 theory Base_Tools
2.5 -imports "../ProgLang/ProgLang" "../Interpret/Interpret" "../xmlsrc/xmlsrc"
2.6 + imports "../ProgLang/ProgLang" "../Interpret/Interpret" "../xmlsrc/xmlsrc"
2.7 + (*^^^ for KEStore_Elems.add_thes *)
2.8 begin
2.9 end
2.10 \ No newline at end of file
3.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Sat Aug 24 13:16:17 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Mon Aug 26 09:20:07 2019 +0200
3.3 @@ -40,9 +40,13 @@
3.4 val [aaa, bbb, ccc, ddd, eee] = KEStore_Elems.get_rlss @{theory};
3.5
3.6 \<close> ML \<open>
3.7 +\<close> ML \<open>
3.8 +\<close> ML \<open>
3.9 +\<close> ML \<open>
3.10 +\<close> ML \<open>
3.11 case aaa of ("list_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 1";
3.12 -case ccc of ("e_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 2";
3.13 -case bbb of ("e_rrls", _) => () | _ => error "test/../thy-hierarchy CHANGED 3";
3.14 +case bbb of ("e_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 2";
3.15 +case ccc of ("e_rrls", _) => () | _ => error "test/../thy-hierarchy CHANGED 3";
3.16 \<close> ML \<open>
3.17 case ddd of
3.18 ("rls111",
4.1 --- a/src/Tools/isac/ProgLang/Atools.thy Sat Aug 24 13:16:17 2019 +0200
4.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Mon Aug 26 09:20:07 2019 +0200
4.3 @@ -6,32 +6,32 @@
4.4 theory Atools imports Descript Program
4.5 begin
4.6
4.7 -subsection \<open>preparation to build up a program from rules\<close>
4.8 +subsection \<open>consts for programs automatically built from rules\<close>
4.9
4.10 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
4.11 where "auto_generated t_t = t_t"
4.12 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
4.13 where "auto_generated_inst t_t v = t_t"
4.14
4.15 -subsection \<open>use preparation\<close>
4.16 +text \<open>use above consts\<close>
4.17 ML_file scrtools.sml
4.18
4.19 -subsection \<open>consts & axiomatization\<close>
4.20
4.21 +subsection \<open>General consts\<close>
4.22 consts
4.23 -
4.24 Arbfix :: "real"
4.25 - Undef :: "real"
4.26 - dummy :: "real"
4.27 -
4.28 - some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
4.29 - occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
4.30 + Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
4.31
4.32 pow :: "[real, real] => real" (infixr "^^^" 80)
4.33 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
4.34 ~~~~ ~~~~ ~~~~ ~~~*)
4.35 -(*WN0603 at FE-interface encoded strings to '^',
4.36 - see 'fun encode', fun 'decode'*)
4.37 + (*WN0603 at FE-interface encoded strings to '^',
4.38 + see 'fun encode', fun 'decode'*)
4.39 +
4.40 +subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
4.41 +consts
4.42 + some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
4.43 + occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
4.44
4.45 abs :: "real => real" ("(|| _ ||)")
4.46 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
4.47 @@ -53,18 +53,27 @@
4.48 boollist2sum :: "bool list => real"
4.49 lastI :: "'a list \<Rightarrow> 'a"
4.50
4.51 +subsection \<open>theorems for Base_Tools\<close>
4.52 axiomatization where (*for evaluating the assumptions of conditional rules*)
4.53
4.54 - last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
4.55 + last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
4.56 real_unari_minus: "- a = (-1) * a" and
4.57 + radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
4.58 + (* should be in Rational.thy, but:
4.59 + needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
4.60 + rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
4.61 + ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
4.62 + rat_leq2: "d ~= 0 ==>
4.63 + ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
4.64 + rat_leq3: "b ~= 0 ==>
4.65 + ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
4.66
4.67 - rle_refl: "(n::real) <= n" and
4.68 - radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
4.69 - not_true: "(~ True) = False" and
4.70 - not_false: "(~ False) = True"
4.71
4.72 axiomatization where (*..if replaced by "and" we get error:
4.73 Type unification failed: No type arity bool :: zero ...*)
4.74 + rle_refl: "(n::real) <= n" and
4.75 + not_true: "(~ True) = False" and
4.76 + not_false: "(~ False) = True" and
4.77 and_true: "(a & True) = a" and
4.78 and_false: "(a & False) = False" and
4.79 or_true: "(a | True) = True" and
4.80 @@ -72,69 +81,8 @@
4.81 and_commute: "(a & b) = (b & a)" and
4.82 or_commute: "(a | b) = (b | a)"
4.83
4.84 - (*.should be in Rational.thy, but:
4.85 - needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
4.86 -axiomatization where (*..if replaced by "and" we get error:
4.87 -Type unification failed: No type arity bool :: zero ...*)
4.88 - rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
4.89 - ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
4.90 - rat_leq2: "d ~= 0 ==>
4.91 - ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
4.92 - rat_leq3: "b ~= 0 ==>
4.93 - ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
4.94 -
4.95 -
4.96 -subsection \<open>Coding standards\<close>
4.97 -text \<open>copy from doc/math-eng.tex WN.28.3.03
4.98 -WN071228 extended\<close>
4.99 -
4.100 -subsubsection \<open>Identifiers\<close>
4.101 -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).
4.102 -
4.103 -This are the preliminary rules for naming identifiers>
4.104 -\begin{description}
4.105 -\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}.
4.106 -\item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
4.107 -\item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
4.108 -\item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
4.109 -\item [???] ???
4.110 -\item [???] ???
4.111 -\end{description}
4.112 -%WN071228 extended\<close>
4.113 -
4.114 -subsubsection \<open>Rule sets\<close>
4.115 -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.
4.116 -
4.117 -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.
4.118 -\begin{description}
4.119 -
4.120 -\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents).
4.121 -
4.122 -\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student.
4.123 -
4.124 -\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only.
4.125 -WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise).
4.126 -\end{description}
4.127 -
4.128 -The above rulesets are all visible to the user, and also may be input;
4.129 -thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
4.130 -KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
4.131 -using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
4.132 -The following rulesets are used for internal purposes and usually invisible to the (naive) user:
4.133 -\begin{description}
4.134 -
4.135 -\item [*\_erls] TODO
4.136 -\item [*\_prls]
4.137 -\item [*\_srls]
4.138 -
4.139 -\end{description}
4.140 -{\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
4.141 -\<close>
4.142 -
4.143 -subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>
4.144 +subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
4.145 ML \<open>
4.146 -val thy = @{theory};
4.147 -
4.148 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
4.149
4.150 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
4.151 @@ -166,13 +114,9 @@
4.152 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
4.153 | eval_some_occur_in _ _ _ _ = NONE;
4.154
4.155 -
4.156 -
4.157 -
4.158 -(*evaluate 'is_atom'*)
4.159 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
4.160 fun eval_is_atom (thmid:string) "Atools.is'_atom"
4.161 - (t as (Const(op0,_) $ arg)) thy =
4.162 + (t as (Const _ $ arg)) _ =
4.163 (case arg of
4.164 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
4.165 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
4.166 @@ -180,11 +124,10 @@
4.167 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
4.168 | eval_is_atom _ _ _ _ = NONE;
4.169
4.170 -(*evaluate 'is_even'*)
4.171 fun even i = (i div 2) * 2 = i;
4.172 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
4.173 fun eval_is_even (thmid:string) "Atools.is'_even"
4.174 - (t as (Const(op0,_) $ arg)) thy =
4.175 + (t as (Const _ $ arg)) _ =
4.176 (case arg of
4.177 Free (n,_) =>
4.178 (case TermC.int_of_str_opt n of
4.179 @@ -200,7 +143,7 @@
4.180 (*evaluate 'is_const'*)
4.181 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
4.182 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
4.183 - (t as (Const(op0,t0) $ arg)) (thy:theory) =
4.184 + (t as (Const _ $ arg)) _ =
4.185 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
4.186 (case arg of
4.187 Const (n1,_) =>
4.188 @@ -236,13 +179,13 @@
4.189 (string_of_int p21)^","^(string_of_int p22)^"))";
4.190
4.191 (*.convert int and float to internal floatingpoint prepresentation.*)
4.192 -fun numeral (Free (str, T)) =
4.193 +fun numeral (Free (str, _)) =
4.194 (case TermC.int_of_str_opt str of
4.195 SOME i => SOME ((i, 0), (0, 0))
4.196 | NONE => NONE)
4.197 | numeral (Const ("Float.Float", _) $
4.198 (Const ("Product_Type.Pair", _) $
4.199 - (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
4.200 + (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
4.201 (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
4.202 (case (TermC.int_of_str_opt v1, TermC.int_of_str_opt v2, TermC.int_of_str_opt p1, TermC.int_of_str_opt p2) of
4.203 (SOME v1', SOME v2', SOME p1', SOME p2') =>
4.204 @@ -266,7 +209,7 @@
4.205 ((a * c, b + d), (0, 0))
4.206 | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
4.207 ((a div c, 0), (0, 0))
4.208 - | calcul "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
4.209 + | calcul "Atools.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
4.210 ((Calc.power a c, 0), (0, 0))
4.211 | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
4.212 error ("calcul: not impl. for Float (("^
4.213 @@ -339,7 +282,7 @@
4.214
4.215 (*** evaluate binary associative operations ***)
4.216 ML \<open>
4.217 -fun eval_binop (thmid : string) (op_: string)
4.218 +fun eval_binop (_(*thmid*) : string) (op_: string)
4.219 (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
4.220 if op0 = op0' then
4.221 case (numeral t1, numeral t2) of
4.222 @@ -354,7 +297,7 @@
4.223 in SOME ("#: " ^ Rule.term2str prop, prop) end
4.224 | _ => NONE
4.225 else NONE
4.226 - | eval_binop (thmid : string) (op_ : string)
4.227 + | eval_binop _ (op_ : string)
4.228 (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
4.229 if op0 = op0' then
4.230 case (numeral t1, numeral t2) of
4.231 @@ -368,7 +311,7 @@
4.232 in SOME ("#: " ^ Rule.term2str prop, prop) end
4.233 | _ => NONE
4.234 else NONE
4.235 - | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
4.236 + | eval_binop _ _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
4.237 (case (numeral t1, numeral t2) of
4.238 (SOME n1, SOME n2) =>
4.239 let
4.240 @@ -389,12 +332,11 @@
4.241 val it = "-1 * (-1 * a) = 1 * a"*)
4.242
4.243
4.244 -
4.245 (*.evaluate < and <= for numerals.*)
4.246 (*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
4.247 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
4.248 -fun eval_equ (thmid:string) (op_:string) (t as
4.249 - (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
4.250 +fun eval_equ (thmid:string) (_(*op_*)) (t as
4.251 + (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
4.252 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
4.253 (SOME n1', SOME n2') =>
4.254 if Calc.calc_equ (strip_thy op0) (n1', n2')
4.255 @@ -434,7 +376,7 @@
4.256 the arguments: thus special handling by 'fun eval_binop'*)
4.257 (*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
4.258 fun eval_ident (thmid:string) "Atools.ident" (t as
4.259 - (Const (op0,t0) $ t1 $ t2 )) thy =
4.260 + (Const _(*op0, t0*) $ t1 $ t2 )) thy =
4.261 if t1 = t2
4.262 then SOME (TermC.mk_thmid thmid
4.263 ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
4.264 @@ -466,7 +408,7 @@
4.265 (*.evaluate identity of terms, which stay ready for evaluation in turn;
4.266 thus returns False only for atoms.*)
4.267 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
4.268 -fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy =
4.269 +fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
4.270 if t1 = t2
4.271 then SOME (TermC.mk_thmid thmid
4.272 ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
4.273 @@ -505,54 +447,45 @@
4.274 val it = "(0 = 0) = True" : string
4.275 *)
4.276
4.277 -
4.278 -\<close>
4.279 -
4.280 -subsection \<open>evaluation on the meta-level\<close>
4.281 -ML \<open>
4.282 (*. evaluate HOL.divide .*)
4.283 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
4.284 -fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
4.285 - (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
4.286 +fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
4.287 + (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
4.288 (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
4.289 - (SOME n1', SOME n2') =>
4.290 - let
4.291 - val sg = Calc.sign_mult n1' n2';
4.292 - val (T1,T2,Trange) = TermC.dest_binop_typ t0;
4.293 - val gcd' = Calc.gcd (abs n1') (abs n2');
4.294 - in if gcd' = abs n2'
4.295 - then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
4.296 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
4.297 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
4.298 - else if 0 < n2' andalso gcd' = 1 then NONE
4.299 - else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
4.300 - ((abs n2') div gcd')
4.301 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
4.302 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
4.303 - end
4.304 - | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
4.305 -
4.306 + (SOME n1', SOME n2') =>
4.307 + let
4.308 + val sg = Calc.sign_mult n1' n2';
4.309 + val (T1,T2,Trange) = TermC.dest_binop_typ t0;
4.310 + val gcd' = Calc.gcd (abs n1') (abs n2');
4.311 + in if gcd' = abs n2'
4.312 + then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
4.313 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
4.314 + in SOME (TermC.mk_thmid thmid n1 n2, prop) end
4.315 + else if 0 < n2' andalso gcd' = 1 then NONE
4.316 + else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
4.317 + ((abs n2') div gcd')
4.318 + val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
4.319 + in SOME (TermC.mk_thmid thmid n1 n2, prop) end
4.320 + end
4.321 + | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
4.322 | eval_cancel _ _ _ _ = NONE;
4.323
4.324 -(*. get the argument from a function-definition.*)
4.325 -(*("argument_in" ,("Atools.argument'_in",
4.326 - eval_argument_in "Atools.argument'_in"))*)
4.327 +(* get the argument from a function-definition *)
4.328 +(*("argument_in" ,("Atools.argument'_in", eval_argument_in "Atools.argument'_in"))*)
4.329 fun eval_argument_in _ "Atools.argument'_in"
4.330 - (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
4.331 + (t as (Const ("Atools.argument'_in", _) $ (_(*f*) $ arg))) _ =
4.332 if is_Free arg (*could be something to be simplified before*)
4.333 - then SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
4.334 - HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
4.335 + then
4.336 + SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
4.337 + HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
4.338 else NONE
4.339 | eval_argument_in _ _ _ _ = NONE;
4.340
4.341 -(*.check if the function-identifier of the first argument matches
4.342 - the function-identifier of the lhs of the second argument.*)
4.343 -(*("sameFunId" ,("Atools.sameFunId",
4.344 - eval_same_funid "Atools.sameFunId"))*)
4.345 +(* check if the function-identifier of the first argument matches
4.346 + the function-identifier of the lhs of the second argument *)
4.347 +(*("sameFunId" ,("Atools.sameFunId", eval_same_funid "Atools.sameFunId"))*)
4.348 fun eval_sameFunId _ "Atools.sameFunId"
4.349 - (p as Const ("Atools.sameFunId",_) $
4.350 - (f1 $ _) $
4.351 - (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
4.352 + (p as Const ("Atools.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
4.353 if f1 = f2
4.354 then SOME ((Rule.term2str p) ^ " = True",
4.355 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
4.356 @@ -579,46 +512,149 @@
4.357 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
4.358 | eval_filter_sameFunId _ _ _ _ = NONE;
4.359
4.360 -
4.361 -(*make a list of terms to a sum*)
4.362 +(* make a list of terms to a sum *)
4.363 fun list2sum [] = error ("list2sum called with []")
4.364 | list2sum [s] = s
4.365 | list2sum (s::ss) =
4.366 - let fun sum su [s'] =
4.367 - Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
4.368 - $ su $ s'
4.369 - | sum su (s'::ss') =
4.370 - sum (Const ("Groups.plus_class.plus", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
4.371 - $ su $ s') ss'
4.372 + let
4.373 + fun sum su [s'] = Const ("Groups.plus_class.plus",
4.374 + [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
4.375 + | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",
4.376 + [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
4.377 + | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
4.378 in sum s ss end;
4.379
4.380 -(*make a list of equalities to the sum of the lhs*)
4.381 +(* make a list of equalities to the sum of the lhs *)
4.382 (*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
4.383 fun eval_boollist2sum _ "Atools.boollist2sum"
4.384 - (p as Const ("Atools.boollist2sum", _) $
4.385 - (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
4.386 - let val isal = TermC.isalist2list l
4.387 - val lhss = map Tools.lhs isal
4.388 - val sum = list2sum lhss
4.389 - in SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
4.390 - HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
4.391 + (p as Const ("Atools.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
4.392 + let
4.393 + val isal = TermC.isalist2list l
4.394 + val lhss = map Tools.lhs isal
4.395 + val sum = list2sum lhss
4.396 + in
4.397 + SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
4.398 + HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
4.399 end
4.400 -| eval_boollist2sum _ _ _ _ = NONE;
4.401 + | eval_boollist2sum _ _ _ _ = NONE;
4.402 \<close>
4.403
4.404 -subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>
4.405 +subsection \<open>setup for ML-functions\<close>
4.406 +text \<open>required by "eval_binop" below\<close>
4.407 +setup \<open>KEStore_Elems.add_calcs
4.408 + [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
4.409 + ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
4.410 + ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
4.411 + ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
4.412 + ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
4.413 + ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
4.414 + ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
4.415 + ("ident", ("Atools.ident", eval_ident "#ident_")),
4.416 + ("equal", ("HOL.eq", eval_equal "#equal_")),
4.417 + ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
4.418 + ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
4.419 + ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
4.420 + ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
4.421 + ("POWER",("Atools.pow", eval_binop "#power_")),
4.422 + ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
4.423 +
4.424 +subsection \<open>rewrite-order for rule-sets\<close>
4.425 ML \<open>
4.426 +\<close> ML \<open>
4.427 local
4.428 + open Term;
4.429 +in
4.430 + fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
4.431 + fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
4.432 +end;
4.433 +\<close>
4.434
4.435 -open Term;
4.436 +subsection \<open>rewrite-order for rule-sets\<close>
4.437 +ML \<open>
4.438 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
4.439 +val tless_true = Rule.dummy_ord;
4.440 +Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
4.441 + [("tless_true", tless_true),
4.442 + ("e_rew_ord'", tless_true),
4.443 + ("dummy_ord", Rule.dummy_ord)]);
4.444 +\<close>
4.445
4.446 -in
4.447 -fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
4.448 -fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
4.449 -end;
4.450 +subsection \<open>rule-sets\<close>
4.451 +ML \<open>
4.452 +val calculate_Base_Tools = Rule.append_rls "calculate_Atools" Rule.e_rls
4.453 + [ Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
4.454 + Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
4.455 + Rule.Calc ("HOL.eq", eval_equal "#equal_"),
4.456
4.457 + Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
4.458 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.459 + Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
4.460 + Rule.Calc ("Groups.times_class.times", eval_binop "#mult_")
4.461 + ];
4.462 +
4.463 +\<close> ML \<open>
4.464 +val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
4.465 + [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
4.466 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
4.467 + (*"(~ True) = False"*)
4.468 + Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
4.469 + (*"(~ False) = True"*)
4.470 + Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
4.471 + (*"(?a & True) = ?a"*)
4.472 + Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
4.473 + (*"(?a & False) = False"*)
4.474 + Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
4.475 + (*"(?a | True) = True"*)
4.476 + Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
4.477 + (*"(?a | False) = ?a"*)
4.478 +
4.479 + Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
4.480 + Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
4.481 + Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
4.482 + Rule.Thm ("refl", TermC.num_str @{thm refl}),
4.483 + Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
4.484 + Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
4.485 +
4.486 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
4.487 + Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
4.488 +
4.489 + Rule.Calc ("Atools.ident", eval_ident "#ident_"),
4.490 + Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
4.491 + Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
4.492 + Rule.Calc ("Tools.matches", Tools.eval_matches "")];
4.493 +\<close>
4.494 +
4.495 +ML \<open>
4.496 +val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
4.497 + [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
4.498 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
4.499 + Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
4.500 + Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
4.501 + Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
4.502 + Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
4.503 + Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
4.504 +
4.505 + Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
4.506 + Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
4.507 + Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
4.508 + Rule.Thm ("refl", TermC.num_str @{thm refl}),
4.509 + Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
4.510 + Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
4.511 +
4.512 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
4.513 + Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
4.514 +
4.515 + Rule.Calc ("Atools.ident", eval_ident "#ident_"),
4.516 + Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
4.517 + Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
4.518 + Rule.Calc ("Tools.matches", Tools.eval_matches "")];
4.519 +\<close>
4.520 +
4.521 +subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
4.522 +text \<open>requires "eval_binop" from above\<close>
4.523 +ML \<open>
4.524 val list_rls = Rule.append_rls "list_rls" list_rls
4.525 - [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
4.526 + [ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
4.527 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.528 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.529 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.530 @@ -628,165 +664,21 @@
4.531 Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
4.532
4.533 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
4.534 - Rule.Thm ("if_False",TermC.num_str @{thm if_False})
4.535 - ];
4.536 -\<close>
4.537 -ML \<open>
4.538 + Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
4.539
4.540 -(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
4.541 -val tless_true = Rule.dummy_ord;
4.542 -Rule.rew_ord' := overwritel (! Rule.rew_ord',
4.543 - [("tless_true", tless_true),
4.544 - ("e_rew_ord'", tless_true),
4.545 - ("dummy_ord", Rule.dummy_ord)]);
4.546 -
4.547 -val calculate_Base_Tools =
4.548 - Rule.append_rls "calculate_Atools" Rule.e_rls
4.549 - [Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.550 - Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.551 - Rule.Calc ("HOL.eq",eval_equal "#equal_"),
4.552 -
4.553 - Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
4.554 - Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
4.555 - Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
4.556 - Rule.Calc ("Groups.times_class.times",eval_binop "#mult_")
4.557 - ];
4.558 -
4.559 -\<close>
4.560 -
4.561 -find_theorems (9) "?n <= ?n"
4.562 -
4.563 -ML \<open>
4.564 -val Atools_erls =
4.565 - Rule.append_rls "Atools_erls" Rule.e_rls
4.566 - [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
4.567 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
4.568 - (*"(~ True) = False"*)
4.569 - Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
4.570 - (*"(~ False) = True"*)
4.571 - Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
4.572 - (*"(?a & True) = ?a"*)
4.573 - Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
4.574 - (*"(?a & False) = False"*)
4.575 - Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
4.576 - (*"(?a | True) = True"*)
4.577 - Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
4.578 - (*"(?a | False) = ?a"*)
4.579 -
4.580 - Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
4.581 - Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
4.582 - Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
4.583 - Rule.Thm ("refl",TermC.num_str @{thm refl}),
4.584 - Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
4.585 - Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
4.586 -
4.587 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.588 - Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.589 -
4.590 - Rule.Calc ("Atools.ident",eval_ident "#ident_"),
4.591 - Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
4.592 - Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
4.593 - Rule.Calc ("Tools.matches", Tools.eval_matches "")
4.594 - ];
4.595 -
4.596 -\<close>
4.597 -
4.598 -ML \<open>
4.599 -val Atools_crls =
4.600 - Rule.append_rls "Atools_crls" Rule.e_rls
4.601 - [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
4.602 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
4.603 - Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
4.604 - Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
4.605 - Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
4.606 - Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
4.607 - Rule.Thm ("or_false",TermC.num_str @{thm or_false}),
4.608 -
4.609 - Rule.Thm ("rat_leq1",TermC.num_str @{thm rat_leq1}),
4.610 - Rule.Thm ("rat_leq2",TermC.num_str @{thm rat_leq2}),
4.611 - Rule.Thm ("rat_leq3",TermC.num_str @{thm rat_leq3}),
4.612 - Rule.Thm ("refl",TermC.num_str @{thm refl}),
4.613 - Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
4.614 - Rule.Thm ("radd_left_cancel_le",TermC.num_str @{thm radd_left_cancel_le}),
4.615 -
4.616 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.617 - Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.618 -
4.619 - Rule.Calc ("Atools.ident",eval_ident "#ident_"),
4.620 - Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
4.621 - Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
4.622 - Rule.Calc ("Tools.matches", Tools.eval_matches "")
4.623 - ];
4.624 -
4.625 -(*val atools_erls = ... waere zu testen ...
4.626 - Rule.merge_rls calculate_Atools
4.627 - (Rule.append_rls Atools_erls (*i.A. zu viele rules*)
4.628 - [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
4.629 - Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
4.630 - Rule.Calc ("Atools.occurs'_in",
4.631 - eval_occurs_in "#occurs_in"),
4.632 - Rule.Calc ("Tools.matches",eval_matches "#matches")
4.633 - ] (*i.A. zu viele rules*)
4.634 - );*)
4.635 -(* val atools_erls = prep_rls'( (*outcommented*)
4.636 - Rule.Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
4.637 - erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
4.638 - rules = [Rule.Thm ("refl",num_str @{thm refl}),
4.639 - Rule.Thm ("order_refl",num_str @{thm order_refl}),
4.640 - Rule.Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
4.641 - Rule.Thm ("not_true",num_str @{thm not_true}),
4.642 - Rule.Thm ("not_false",num_str @{thm not_false}),
4.643 - Rule.Thm ("and_true",num_str @{thm and_true}),
4.644 - Rule.Thm ("and_false",num_str @{thm and_false}),
4.645 - Rule.Thm ("or_true",num_str @{thm or_true}),
4.646 - Rule.Thm ("or_false",num_str @{thm or_false}),
4.647 - Rule.Thm ("and_commute",num_str @{thm and_commute}),
4.648 - Rule.Thm ("or_commute",num_str @{thm or_commute}),
4.649 -
4.650 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.651 - Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.652 -
4.653 - Rule.Calc ("Atools.ident",eval_ident "#ident_"),
4.654 - Rule.Calc ("Atools.is'_const",eval_const "#is_const_"),
4.655 - Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),
4.656 - Rule.Calc ("Tools.matches",eval_matches "")
4.657 - ],
4.658 - scr = Rule.Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
4.659 - });
4.660 -*)
4.661 -"******* Atools.ML end *******";
4.662 -\<close>
4.663 -subsection \<open>write to KEStore: calcs, rule-sets\<close>
4.664 -setup \<open>KEStore_Elems.add_calcs
4.665 - [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
4.666 - ("some_occur_in",
4.667 - ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
4.668 - ("is_atom" ,("Atools.is'_atom", eval_is_atom "#is_atom_")),
4.669 - ("is_even" ,("Atools.is'_even", eval_is_even "#is_even_")),
4.670 - ("is_const" ,("Atools.is'_const", eval_const "#is_const_")),
4.671 - ("le" ,("Orderings.ord_class.less", eval_equ "#less_")),
4.672 - ("leq" ,("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
4.673 - ("ident" ,("Atools.ident", eval_ident "#ident_")),
4.674 - ("equal" ,("HOL.eq", eval_equal "#equal_")),
4.675 - ("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
4.676 - ("MINUS" ,("Groups.minus_class.minus", eval_binop "#sub_")),
4.677 - ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
4.678 - ("DIVIDE" ,("Rings.divide_class.divide", eval_cancel "#divide_e")),
4.679 - ("POWER" ,("Atools.pow", eval_binop "#power_")),
4.680 - ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
4.681 -ML \<open>
4.682 val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
4.683 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
4.684 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
4.685 - erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
4.686 - rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.687 - Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
4.688 - (* ~~~~~~ for nth_Cons_*)],
4.689 - scr = Rule.EmptyScr},
4.690 + erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
4.691 + rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.692 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
4.693 + (* ~~~~~~ for nth_Cons_*)],
4.694 + scr = Rule.EmptyScr},
4.695 srls = Rule.Erls, calc = [], errpatts = [],
4.696 rules = [], scr = Rule.EmptyScr})
4.697 list_rls);
4.698 \<close>
4.699 +subsection \<open>setup for extended rule-set\<close>
4.700 setup \<open>KEStore_Elems.add_rlss
4.701 [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>
4.702
5.1 --- a/src/Tools/isac/ProgLang/Descript.thy Sat Aug 24 13:16:17 2019 +0200
5.2 +++ b/src/Tools/isac/ProgLang/Descript.thy Mon Aug 26 09:20:07 2019 +0200
5.3 @@ -5,6 +5,7 @@
5.4
5.5 theory Descript imports Tools begin
5.6
5.7 +subsection \<open>consts for general descriptions of input in specify-phase\<close>
5.8 consts
5.9 (*TODO.180331: review for localisation of model-patterns and of method's guards*)
5.10 someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
6.1 --- a/src/Tools/isac/ProgLang/Tools.thy Sat Aug 24 13:16:17 2019 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Mon Aug 26 09:20:07 2019 +0200
6.3 @@ -10,13 +10,7 @@
6.4 ML_file calculate.sml
6.5 ML_file rewrite.sml
6.6
6.7 -(*belongs to theory ListC*)
6.8 -ML \<open>
6.9 -(*val first_isac_thy = @{theory ListC}*)
6.10 -\<close>
6.11 -
6.12 -(*for Descript.thy*)
6.13 -
6.14 +subsection \<open>typedecl for descriptions of input in specify-phase\<close>
6.15 (****************>***************************************************************)
6.16 (* 'fun is_dsc' in ProgLang/scrtools.sml MUST contain ALL these types !! *)
6.17 (****************>***************************************************************)
6.18 @@ -33,10 +27,12 @@
6.19 (* 'fun is_dsc' in ProgLang/scrtools.smlMUST contain ALL these types !! *)
6.20 (****************>***************************************************************)
6.21
6.22 +subsection \<open>const UniversalList for Or_to_List\<close>
6.23 consts
6.24 + UniversalList :: "bool list"
6.25
6.26 - UniversalList :: "bool list"
6.27 -
6.28 +subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
6.29 +consts
6.30 lhs :: "bool => real" (*of an equality*)
6.31 rhs :: "bool => real" (*of an equality*)
6.32 Vars :: "'a => real list" (*get the variables of a term *)
6.33 @@ -50,6 +46,7 @@
6.34 "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*)
6.35 *)
6.36
6.37 +subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
6.38 ML \<open>(*the former Tools.ML*)
6.39 signature TOOLS =
6.40 sig
6.41 @@ -61,7 +58,6 @@
6.42 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
6.43 val eval_var: string -> string -> term -> theory -> (string * term) option
6.44 val lhs: term -> term
6.45 - val list_rls: Rule.rls
6.46 val matchsub: theory -> term -> term -> bool
6.47 val or2list: term -> term
6.48 val rhs: term -> term
6.49 @@ -236,12 +232,17 @@
6.50 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
6.51 | eval_rhs _ _ _ _ = NONE;
6.52
6.53 -
6.54 -(*for evaluating scripts*)
6.55 -
6.56 -val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Tools.rhs", eval_rhs "")];
6.57 end (*struct*)
6.58 \<close>
6.59 +
6.60 +subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
6.61 +ML \<open>
6.62 +val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Tools.rhs", Tools.eval_rhs "")];
6.63 +\<close> ML \<open>
6.64 +\<close>
6.65 +
6.66 +subsection \<open>setup for rule-sets and ML-functions\<close>
6.67 +setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
6.68 setup \<open>KEStore_Elems.add_calcs
6.69 [("matches", ("Tools.matches", Tools.eval_matches "#matches_")),
6.70 ("matchsub", ("Tools.matchsub", Tools.eval_matchsub "#matchsub_")),
7.1 --- a/src/Tools/isac/TODO.thy Sat Aug 24 13:16:17 2019 +0200
7.2 +++ b/src/Tools/isac/TODO.thy Mon Aug 26 09:20:07 2019 +0200
7.3 @@ -15,6 +15,21 @@
7.4 \begin{itemize}
7.5 \item separate code required in both, ProgLang & Interpret
7.6 \begin{itemize}
7.7 + \item xxx
7.8 + \item /-------------------------------------------------------------------
7.9 + \item Atools.thy (*> tests*) -> /test/.. wait for Specify/* MathEngine/*
7.10 + \item Atools.thy then SOME
7.11 + HOLogic ... indentations
7.12 + \item check occurences of KEStore_Elems.add_rlss [("list_rls",
7.13 + \item rename list_rls accordingly
7.14 + \item ------------------------------------------------------------------/
7.15 + \item xxx
7.16 + \item lucas-interpreter.sml ----- vvvvvvvvv
7.17 + val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
7.18 + \item xxx
7.19 + \item fun fun eval_* //thy//
7.20 + \item rm Float
7.21 + \item xxx
7.22 \item signature LIBRARY_C
7.23 \item Program.thy (*=========== record these ^^^ in 'tacs' in program.ML =========*)
7.24 \item sig/struc ..elems --> elem
7.25 @@ -36,7 +51,6 @@
7.26 \item xxx
7.27 \item xxx
7.28 \end{itemize}
7.29 - \item xxx
7.30 \item Isac.thy --> All_Knowledge.thy
7.31 \item xxx
7.32 \item xxx
7.33 @@ -170,6 +184,8 @@
7.34 \begin{itemize}
7.35 \item rename field scr in meth
7.36 \item xxx
7.37 + \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
7.38 + \item xxx
7.39 \item check match between args of partial_function and model-pattern of meth;
7.40 provide error message.
7.41 \item xxx
7.42 @@ -186,7 +202,6 @@
7.43 (which checks for Check_Postcond separated by another tactic)
7.44 This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
7.45 \item xxx
7.46 - \item xxx
7.47 \end{itemize}
7.48 \<close>
7.49 subsection \<open>Questionable\<close>
7.50 @@ -350,6 +365,13 @@
7.51 MathEngine.solve, ...,
7.52 ? or identify "layers" like in Isabelle?
7.53 \<close>
7.54 +subsection \<open>Redesign thms for equation solver\<close>
7.55 +text \<open>
7.56 + Existing solver is structured along the WRONG assumption,
7.57 + that Poly.thy must be the LAST thy among all thys involved.
7.58 +
7.59 + Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
7.60 +\<close>
7.61 subsection \<open>Finetunig required for xmldata\<close>
7.62 text \<open>
7.63 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
7.64 @@ -360,6 +382,72 @@
7.65 section \<open>Hints for further development\<close>
7.66 text \<open>
7.67 \<close>
7.68 +subsection \<open>Coding standards & some explanations for math-authors\<close>
7.69 +text \<open>copy from doc/math-eng.tex WN.28.3.03
7.70 +WN071228 extended\<close>
7.71 +
7.72 +subsubsection \<open>Identifiers\<close>
7.73 +text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
7.74 + not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
7.75 + reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
7.76 + problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
7.77 + However, all the cases (1)..(4) require different typing for one and the same
7.78 + identifier {\tt probe} which is impossible, and actually leads to strange errors
7.79 + (for instance (1) is used as string, except in a script addressing a Subproblem).
7.80 +
7.81 + These are the preliminary rules for naming identifiers>
7.82 + \begin{description}
7.83 + \item [elements of a key] into the hierarchy of problems or methods must not contain
7.84 + capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
7.85 + \item [descriptions in problem-patterns] must contain at least 1 capital letter and
7.86 + must not contain underscores, e.g. {\tt Probe, forPolynomials}.
7.87 + \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
7.88 + beware of conflicts~!
7.89 + \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
7.90 + \item [???] ???
7.91 + \item [???] ???
7.92 + \end{description}
7.93 +%WN071228 extended\<close>
7.94 +
7.95 +subsubsection \<open>Rule sets\<close>
7.96 +text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
7.97 + where it can be viewed using the knowledge browsers.
7.98 +
7.99 + There are rulesets visible to the student, and there are rulesets visible (in general) only for
7.100 + math authors. There are also rulesets which {\em must} exist for {\em each} theory;
7.101 + these contain the identifier of the respective theory (including all capital letters)
7.102 + as indicated by {\it Thy} below.
7.103 +
7.104 + \begin{description}
7.105 + \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
7.106 + normalform for all terms which can be expressed by the definitions of the respective theory
7.107 + (and the respective parents).
7.108 + \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
7.109 + which can be expressed by the definitions of the respective theory (and the respective parents)
7.110 + such, that the rewrites can be presented to the student.
7.111 + \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
7.112 + numerical constants only (i.e. all terms which can be expressed by the definitions of
7.113 + the respective theory and the respective parent theories). In particular, this ruleset includes
7.114 + evaluating in/equalities with numerical constants only.
7.115 + WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
7.116 + are logically equivalent, where the latter often add to the assumptions
7.117 + (e.g. in Check_elementwise).
7.118 + \end{description}
7.119 +
7.120 + The above rulesets are all visible to the user, and also may be input;
7.121 + thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
7.122 + KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
7.123 + using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
7.124 + The following rulesets are used for internal purposes and usually invisible to the (naive) user:
7.125 +
7.126 + \begin{description}
7.127 + \item [*\_erls] TODO
7.128 + \item [*\_prls]
7.129 + \item [*\_srls]
7.130 + \end{description}
7.131 +{\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
7.132 +\<close>
7.133 +
7.134 subsection \<open>get proof-state\<close>
7.135 text \<open>
7.136 Re: [isabelle] Programatically get "this"
7.137 @@ -410,6 +498,8 @@
7.138 section \<open>Questions to Isabelle experts\<close>
7.139 text \<open>
7.140 \begin{itemize}
7.141 +\item what is the actual replacement of "hg log --follow" ?
7.142 +\item xxx
7.143 \item how HANDLE these exceptions, e.g.:
7.144 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
7.145 GIVES
8.1 --- a/test/Tools/isac/Interpret/calchead.sml Sat Aug 24 13:16:17 2019 +0200
8.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Aug 26 09:20:07 2019 +0200
8.3 @@ -62,7 +62,7 @@
8.4 "valuesFor [a,b::real]",
8.5 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
8.6 "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",
8.7 - "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",
8.8 + "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
8.9
8.10 "boundVariable a","boundVariable b","boundVariable alpha",
8.11 "interval {x::real. 0 <= x & x <= 2*r}",