1.1 --- a/src/Tools/isac/CalcElements/termC.sml Wed Mar 25 11:01:02 2020 +0100
1.2 +++ b/src/Tools/isac/CalcElements/termC.sml Thu Mar 26 16:17:21 2020 +0100
1.3 @@ -33,6 +33,8 @@
1.4 val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *)
1.5
1.6 val is_atom: term -> bool
1.7 + val is_const: term -> bool
1.8 + val is_variable: term -> bool
1.9 val is_bdv: string -> bool
1.10 val is_bdv_subst: term -> bool
1.11 val guess_bdv_typ: term -> typ
1.12 @@ -42,6 +44,7 @@
1.13 val is_list: term -> bool
1.14 val is_num: term -> bool
1.15 val is_num': string -> bool
1.16 + val variable_constant_pair: term * term -> bool
1.17
1.18 val mk_add: term -> term -> term
1.19 val mk_free: typ -> string -> term
1.20 @@ -235,12 +238,21 @@
1.21 (case int_of_str_opt istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
1.22 | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
1.23
1.24 +fun is_const (Const _) = true | is_const _ = false;
1.25 +fun is_variable (t as Free _) = not (is_num t)
1.26 + | is_variable _ = false;
1.27 fun is_Free (Free _) = true | is_Free _ = false;
1.28 fun is_fun_id (Const _) = true
1.29 | is_fun_id (Free _) = true
1.30 | is_fun_id _ = false;
1.31 fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
1.32 | is_f_x _ = false;
1.33 +(* precondition: TermC.is_atom v andalso TermC.is_atom c *)
1.34 +fun variable_constant_pair (v, c) =
1.35 + if (is_variable v andalso (is_const c orelse is_num c)) orelse
1.36 + (is_variable c andalso (is_const v orelse is_num v))
1.37 + then true
1.38 + else false
1.39
1.40 fun vars t =
1.41 let
2.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Mar 25 11:01:02 2020 +0100
2.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Mar 26 16:17:21 2020 +0100
2.3 @@ -85,6 +85,11 @@
2.4
2.5 val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
2.6 (*\\------------------------- from Atools.thy------------------------------------------------//*)
2.7 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.8 + (*NONE*)
2.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.10 + (*NONE*)
2.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.12 end
2.13
2.14 (**)
2.15 @@ -126,8 +131,7 @@
2.16
2.17 (*. evaluate the predicate matches (match on whole term only) .*)
2.18 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
2.19 -fun eval_matches (_:string) "Prog_Expr.matches"
2.20 - (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
2.21 +fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
2.22 if TermC.matches thy tst pat
2.23 then
2.24 let
2.25 @@ -207,7 +211,7 @@
2.26
2.27 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
2.28 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
2.29 - (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
2.30 + (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
2.31 if matchsub thy tst pat
2.32 then
2.33 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
2.34 @@ -229,8 +233,7 @@
2.35 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
2.36 | lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");
2.37 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
2.38 -fun eval_lhs _ "Prog_Expr.lhs"
2.39 - (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
2.40 +fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
2.41 SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),
2.42 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
2.43 | eval_lhs _ _ _ _ = NONE;
2.44 @@ -245,8 +248,7 @@
2.45 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
2.46 | rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");
2.47 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
2.48 -fun eval_rhs _ "Prog_Expr.rhs"
2.49 - (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
2.50 +fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
2.51 SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,
2.52 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
2.53 | eval_rhs _ _ _ _ = NONE;
2.54 @@ -256,8 +258,7 @@
2.55 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
2.56
2.57 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
2.58 -fun eval_occurs_in _ "Prog_Expr.occurs'_in"
2.59 - (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
2.60 +fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
2.61 ((*tracing("#>@ eval_occurs_in: v= "^(Rule.term2str v));
2.62 tracing("#>@ eval_occurs_in: t= "^(Rule.term2str t));*)
2.63 if occurs_in v t
2.64 @@ -275,8 +276,7 @@
2.65 (*("some_occur_in", ("Prog_Expr.some'_occur'_in",
2.66 eval_some_occur_in "#eval_some_occur_in_"))*)
2.67 fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
2.68 - (p as (Const ("Prog_Expr.some'_occur'_in",_)
2.69 - $ vs $ t)) _ =
2.70 + (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
2.71 if some_occur_in (TermC.isalist2list vs) t
2.72 then SOME ((Rule.term2str p) ^ " = True",
2.73 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
2.74 @@ -412,47 +412,26 @@
2.75 val it = "(0 =!= 0) = True" : string
2.76 *)
2.77
2.78 -(*.evaluate identity of terms, which stay ready for evaluation in turn;
2.79 - thus returns False only for atoms.*)
2.80 +
2.81 +(* evaluate identity of terms, which stay ready for further evaluation;
2.82 + thus returns False only for atoms *)
2.83 (*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
2.84 fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
2.85 if t1 = t2
2.86 - then SOME (TermC.mk_thmid thmid
2.87 - ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
2.88 - ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
2.89 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
2.90 - else (case (TermC.is_atom t1, TermC.is_atom t2) of
2.91 - (true, true) =>
2.92 - SOME (TermC.mk_thmid thmid
2.93 - ("(" ^ Rule.term_to_string''' thy t1 ^ ")")
2.94 - ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
2.95 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
2.96 - | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
2.97 - | eval_equal _ _ _ _ = NONE; (* error-exit *)
2.98 -(*
2.99 -val t = str2term "x ~= 0";
2.100 -val NONE = eval_equal "equal_" "b" t thy;
2.101 -
2.102 -
2.103 -> val t = str2term "(x + 1) = (x + 1)";
2.104 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
2.105 -> Rule.term2str t';
2.106 -val str = "equal_(x + 1)_(x + 1)" : string
2.107 -val it = "(x + 1 = x + 1) = True" : string
2.108 -> val t = str2term "x = 0";
2.109 -> val NONE = eval_equal "equal_" "b" t thy;
2.110 -
2.111 -> val t = str2term "1 = 0";
2.112 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
2.113 -> Rule.term2str t';
2.114 -val str = "equal_(1)_(0)" : string
2.115 -val it = "(1 = 0) = False" : string
2.116 -> val t = str2term "0 = 0";
2.117 -> val SOME (str, t') = eval_equal "equal_" "b" t thy;
2.118 -> Rule.term2str t';
2.119 -val str = "equal_(0)_(0)" : string
2.120 -val it = "(0 = 0) = True" : string
2.121 -*)
2.122 + then
2.123 + SOME (TermC.mk_thmid thmid
2.124 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
2.125 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
2.126 + else
2.127 + (case (TermC.is_atom t1, TermC.is_atom t2) of
2.128 + (true, true) =>
2.129 + if TermC.variable_constant_pair (t1, t2)
2.130 + then NONE
2.131 + else SOME (TermC.mk_thmid thmid
2.132 + ("(" ^ Rule.term_to_string''' thy t1 ^ ")") ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
2.133 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
2.134 + | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
2.135 + | eval_equal _ _ _ _ = NONE; (* error-exit *)
2.136
2.137 (*. evaluate HOL.divide .*)
2.138 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
3.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Wed Mar 25 11:01:02 2020 +0100
3.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Mar 26 16:17:21 2020 +0100
3.3 @@ -121,18 +121,18 @@
3.4 (*asm false .. thm not applied ^^^; continue until False vvv*)
3.5 else chk (indets @ [t] @ a') asms);
3.6 in chk [] asms end
3.7 -and rewrite__set_ thy _ __ Rule.Erls t = (* rewrite with a rule set *)
3.8 +and rewrite__set_ thy _ __ Rule.Erls t = (* rewrite with a rule set *)
3.9 error ("rewrite__set_ called with 'Erls' for '" ^ Rule.t2str thy t ^ "'")
3.10 - | rewrite__set_ thy i _ _ (rrls as Rule.Rrls _) t = (* rewrite with a 'reverse rule set' *)
3.11 + | rewrite__set_ thy i _ _ (rrls as Rule.Rrls _) t = (* rewrite with a 'reverse rule set' *)
3.12 let
3.13 val _= trace i (" rls: " ^ Rule.id_rls rrls ^ " on: " ^ Rule.t2str thy t)
3.14 val (t', asm, rew) = app_rev thy (i + 1) rrls t
3.15 in if rew then SOME (t', distinct asm) else NONE end
3.16 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
3.17 let
3.18 - (* attention with cp to test/..: unbound thy, i, bdv, rls TODO1803? pull out to rewrite__*)
3.19 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
3.20 datatype switch = Appl | Noap;
3.21 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
3.22 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
3.23 | rew_once ruls asm ct Appl [] =
3.24 (case rls of Rule.Rls _ => rew_once ruls asm ct Noap ruls
3.25 | Rule.Seq _ => (ct, asm)
3.26 @@ -140,16 +140,16 @@
3.27 | rew_once ruls asm ct apno (rul :: thms) =
3.28 case rul of
3.29 Rule.Thm (thmid, thm) =>
3.30 - (trace1 i (" try thm: " ^ thmid);
3.31 + (trace1 i (" try thm: \"" ^ thmid ^ "\"");
3.32 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
3.33 ((#erls o Rule.rep_rls) rls) put_asm thm ct of
3.34 NONE => rew_once ruls asm ct apno thms
3.35 | SOME (ct', asm') =>
3.36 - (trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
3.37 + (trace1 i (" rewrites to: \"" ^ Rule.t2str thy ct' ^ "\"");
3.38 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
3.39 (* once again try the same rule, e.g. associativity against "()"*)
3.40 | Rule.Num_Calc (cc as (op_, _)) =>
3.41 - let val _= trace1 i (" try calc: " ^ op_ ^ "'")
3.42 + let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
3.43 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
3.44 in case Num_Calc.adhoc_thm thy cc ct of
3.45 NONE => rew_once ruls asm ct apno thms
4.1 --- a/src/Tools/isac/TODO.thy Wed Mar 25 11:01:02 2020 +0100
4.2 +++ b/src/Tools/isac/TODO.thy Thu Mar 26 16:17:21 2020 +0100
4.3 @@ -25,6 +25,14 @@
4.4 text \<open>
4.5 \begin{itemize}
4.6 \item xxx
4.7 + \item restore clarity of "trace_rewrite": "=====" seems to be lost:
4.8 + ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
4.9 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
4.10 + ##### try calc: HOL.eq'
4.11 + ##### try thm: not_true
4.12 + ##### try thm: not_false
4.13 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
4.14 + \item xxx
4.15 \item get_ctxt_LI should replace get_ctxt
4.16 \item xxx
4.17 \item change separate test ----------------------vvv
4.18 @@ -631,6 +639,13 @@
4.19 section \<open>Questions to Isabelle experts\<close>
4.20 text \<open>
4.21 \begin{itemize}
4.22 +\item xxx
4.23 +\item xxx
4.24 +\item xxx
4.25 +\item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
4.26 + ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
4.27 + ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
4.28 +\item xxx
4.29 \item what is the actual replacement of "hg log --follow" ?
4.30 \item xxx
4.31 \item how HANDLE these exceptions, e.g.:
5.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Wed Mar 25 11:01:02 2020 +0100
5.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Thu Mar 26 16:17:21 2020 +0100
5.3 @@ -733,9 +733,6 @@
5.4 writeln(pr_ctree pr_short pt);
5.5
5.6
5.7 -
5.8 -
5.9 -
5.10 "-------------- get_interval from ctree: incremental development--";
5.11 "-------------- get_interval from ctree: incremental development--";
5.12 "-------------- get_interval from ctree: incremental development--";
5.13 @@ -893,7 +890,7 @@
5.14 Subproblem
5.15 ("PolyEq",
5.16 ["normalise", "polynomial", "univariate", "equation"]),
5.17 - ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]) => ()
5.18 + ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]) => ()
5.19 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
5.20 (*WN060717 unintentionally changed some rls/ord while
5.21 completing knowl. for thes2file...
6.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Mar 25 11:01:02 2020 +0100
6.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Mar 26 16:17:21 2020 +0100
6.3 @@ -119,6 +119,7 @@
6.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
6.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
6.6 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
6.7 +
6.8 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
6.9 case tac of Or_to_List' _ => ()
6.10 | _ => error "Or_to_List broken ?"
7.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Wed Mar 25 11:01:02 2020 +0100
7.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Thu Mar 26 16:17:21 2020 +0100
7.3 @@ -7,14 +7,30 @@
7.4 "-----------------------------------------------------------------------------------------------";
7.5 "table of contents -----------------------------------------------------------------------------";
7.6 "-----------------------------------------------------------------------------------------------";
7.7 -"-------- xxx ------";
7.8 -"-------- xxx ------";
7.9 -"-------- xxx ------";
7.10 +"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
7.11 "-----------------------------------------------------------------------------------------------";
7.12 "-----------------------------------------------------------------------------------------------";
7.13 "-----------------------------------------------------------------------------------------------";
7.14
7.15
7.16 -"-------- xxx ------";
7.17 -"-------- xxx ------";
7.18 -"-------- xxx ------";
7.19 +"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
7.20 +"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
7.21 +"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
7.22 +val thy = @{theory}
7.23 +
7.24 +val t = str2term "x = 0";
7.25 +val NONE(*= indetermined*) = eval_equal "equal_" "HOL.eq" t thy;
7.26 +
7.27 +val t = str2term "(x + 1) = (x + 1)";
7.28 +val (Const _(*op0,t0*) $ t1 $ t2 ) = t
7.29 +val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" "HOL.eq" t thy;
7.30 +if term2str t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
7.31 +
7.32 +val t as Const _ $ v $ c = str2term "1 = 0";
7.33 +val false = variable_constant_pair (v, c);
7.34 +val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
7.35 +if term2str t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
7.36 +
7.37 +val t = str2term "0 = 0";
7.38 +val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
7.39 +if term2str t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
8.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Wed Mar 25 11:01:02 2020 +0100
8.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Thu Mar 26 16:17:21 2020 +0100
8.3 @@ -1,10 +1,6 @@
8.4 -(* Title: tests for ProgLang/rewrite.sml
8.5 - TODO.WN0509 collect typical tests from systest here !!!!!
8.6 +(* Title: "ProgLang/rewrite.sml"
8.7 Author: Walther Neuper 050908
8.8 (c) copyright due to lincense terms.
8.9 -
8.10 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
8.11 - 10 20 30 40 50 60 70 80
8.12 *)
8.13
8.14 "--------------------------------------------------------";
8.15 @@ -20,11 +16,12 @@
8.16 "----------- compare all prepat's existing 2010 ---------";
8.17 "----------- fun app_rev, Rrls, -------------------------";
8.18 "----------- 2011 thms with axclasses -------------------";
8.19 -"----------- repair NO asms from rls RatEq_eliminate ----";
8.20 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
8.21 "----------- fun assoc_thm' -----------------------------";
8.22 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
8.23 "----------- fun mk_thm ------------------------------------------------------------------------";
8.24 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
8.25 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
8.26 "--------------------------------------------------------";
8.27 "--------------------------------------------------------";
8.28 "--------------------------------------------------------";
8.29 @@ -514,40 +511,176 @@
8.30 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
8.31 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
8.32
8.33 -"----------- repair NO asms from rls RatEq_eliminate ----";
8.34 -"----------- repair NO asms from rls RatEq_eliminate ----";
8.35 -"----------- repair NO asms from rls RatEq_eliminate ----";
8.36 -val t = str2term "1 / x = 5";
8.37 -trace_rewrite := false;
8.38 -val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t;
8.39 -term2str t' = "1 = 5 * x";
8.40 -terms2str asm = "[\"x ~= 0\"]";
8.41 -(*
8.42 - ## eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x)
8.43 - ### rls: e_rls on: x ~= 0
8.44 - ## asms accepted: ["x ~= 0"] stored: ["x ~= 0"]
8.45 -*)
8.46 -trace_rewrite := false;
8.47 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
8.48 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
8.49 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
8.50 +val thy = @{theory RatEq};
8.51 +val ctxt = Proof_Context.init_global thy;
8.52 +val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
8.53 +val rls = assoc_rls "RatEq_eliminate"
8.54
8.55 -trace_rewrite := false;
8.56 -val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)
8.57 -term2str t' = "1 = 5 * x";
8.58 +val SOME (t''''', asm''''') =
8.59 + rewrite_set_ thy true rls t;
8.60 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
8.61 + rewrite__set_ thy 1 bool [] rls term;
8.62 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
8.63 + = (thy, 1, bool, []:(term * term) list, rls, term);
8.64 +
8.65 +(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
8.66 + datatype switch = Appl | Noap;
8.67 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
8.68 + | rew_once ruls asm ct Appl [] =
8.69 + (case rls of Rule.Rls _ => rew_once ruls asm ct Noap ruls
8.70 + | Rule.Seq _ => (ct, asm)
8.71 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
8.72 + | rew_once ruls asm ct apno (rul :: thms) =
8.73 + case rul of
8.74 + Rule.Thm (thmid, thm) =>
8.75 + (trace1 i (" try thm: " ^ thmid);
8.76 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
8.77 + ((#erls o Rule.rep_rls) rls) put_asm thm ct of
8.78 + NONE => rew_once ruls asm ct apno thms
8.79 + | SOME (ct', asm') =>
8.80 + (trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
8.81 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
8.82 + (* once again try the same rule, e.g. associativity against "()"*)
8.83 + | Rule.Num_Calc (cc as (op_, _)) =>
8.84 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
8.85 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
8.86 + in case Num_Calc.adhoc_thm thy cc ct of
8.87 + NONE => rew_once ruls asm ct apno thms
8.88 + | SOME (_, thm') =>
8.89 + let
8.90 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
8.91 + ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
8.92 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
8.93 + Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
8.94 + val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
8.95 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
8.96 + end
8.97 + | Rule.Cal1 (cc as (op_, _)) =>
8.98 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
8.99 + val ct = TermC.uminus_to_string ct
8.100 + in case Num_Calc.adhoc_thm1_ thy cc ct of
8.101 + NONE => (ct, asm)
8.102 + | SOME (_, thm') =>
8.103 + let
8.104 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
8.105 + ((#erls o Rule.rep_rls) rls) put_asm thm' ct;
8.106 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
8.107 + Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
8.108 + val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
8.109 + in the pairopt end
8.110 + end
8.111 + | Rule.Rls_ rls' =>
8.112 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
8.113 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
8.114 + | NONE => rew_once ruls asm ct apno thms)
8.115 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
8.116 + val ruls = (#rules o Rule.rep_rls) rls;
8.117 +(* val _ = trace i (" rls: " ^ Rule.id_rls rls ^ " on: " ^ Rule.t2str thy ct)*)
8.118 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
8.119 +"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
8.120 + = (ruls, []:term list, ct, Noap, ruls);
8.121 + val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
8.122 +
8.123 + val SOME (ct', asm') = (*case*)
8.124 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
8.125 + ((#erls o Rule.rep_rls) rls) put_asm thm ct (*of*);
8.126 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
8.127 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.rep_rls) rls),
8.128 + ((#erls o Rule.rep_rls) rls), put_asm, thm, ct);
8.129 +
8.130 + val (t', asms, _ (*lrd*), rew) =
8.131 + rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
8.132 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
8.133 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
8.134 + = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
8.135 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
8.136 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
8.137 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
8.138 +;
8.139 +(*+*)if term2str r' =
8.140 +(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
8.141 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
8.142 +(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
8.143 +(*+*) " 1 / x) =\n" ^
8.144 +(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
8.145 +(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
8.146 +(*+*)then () else error "instantiated rule CHANGED";
8.147 +
8.148 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
8.149 +;
8.150 +(*+*)if map term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
8.151 +(*+*)then () else error "stored assumptions CHANGED";
8.152 +
8.153 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
8.154 +;
8.155 +(*+*)if term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
8.156 +(*+*)then () else error "rewritten term (an equality) CHANGED";
8.157 +
8.158 + val (simpl_p', nofalse) =
8.159 + eval__true thy (i + 1) p' bdv rls;
8.160 +"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
8.161 + (*if*) asms = [@{term True}] orelse asms = [] (*else*);
8.162 +
8.163 +(*+*)if map term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
8.164 +(*+*)then () else error "asms before chk CHANGED";
8.165 +
8.166 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
8.167 + | chk indets (a :: asms) =
8.168 + (case rewrite__set_ thy (i + 1) false bdv rls a of
8.169 + NONE => (chk (indets @ [a]) asms)
8.170 + | SOME (t, a') =>
8.171 + if t = @{term True} then (chk (indets @ a') asms)
8.172 + else if t = @{term False} then ([], false)
8.173 + (*asm false .. thm not applied ^^^; continue until False vvv*)
8.174 + else chk (indets @ [t] @ a') asms);
8.175 +
8.176 + val (xxx, true) =
8.177 + chk [] asms; (*return from eval__true*);
8.178 +"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
8.179 +
8.180 +(*+*)val Rls {id = "rateq_erls", rules, ...} = rls;
8.181 +(*+*)(*val rules =
8.182 +(*+*) [Num_Calc ("Rings.divide_class.divide", fn),
8.183 +(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
8.184 +(*+*) :
8.185 +(*+*) Num_Calc ("HOL.eq", fn),
8.186 +(*+*) Thm ("not_true", "(\<not> True) = False"),
8.187 +(*+*) Thm ("not_false", "(\<not> False) = True"),
8.188 +(*+*) :
8.189 +(*+*) Num_Calc ("Prog_Expr.pow", fn),
8.190 +(*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
8.191 +(*+*) rule list*)
8.192 +(*+*)chk: term list -> term list -> term list * bool
8.193 +
8.194 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
8.195 +
8.196 +(*+*)trace_rewrite := true;
8.197 +
8.198 + (*this was False; vvvv--- means: indeterminate*)
8.199 + val (* SOME (t, a') *)NONE = (*case*)
8.200 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
8.201 +
8.202 +(*+*)term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
8.203 (*
8.204 :
8.205 - #### rls: rateq_erls on: x ~= 0
8.206 + #### rls: rateq_erls on: x \<noteq> 0
8.207 :
8.208 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
8.209 - ===== calc. to: ~ False
8.210 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
8.211 ##### try calc: HOL.eq'
8.212 ##### try thm: not_true
8.213 ##### try thm: not_false
8.214 - ===== rewrites to: True
8.215 - :
8.216 - ### asms accepted: ["x ~= 0"] stored: []
8.217 - :
8.218 -*)
8.219 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
8.220 + and True, False are NOT stored ...
8.221 + :
8.222 + ### asms accepted: [x \<noteq> 0] stored: []
8.223 + : *)
8.224 trace_rewrite := false;
8.225 -(* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
8.226 +( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
8.227 +
8.228
8.229 "----------- fun assoc_thm' -----------------------------";
8.230 "----------- fun assoc_thm' -----------------------------";
8.231 @@ -669,3 +802,4 @@
8.232
8.233 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
8.234 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
8.235 +
9.1 --- a/test/Tools/isac/Test_Some.thy Wed Mar 25 11:01:02 2020 +0100
9.2 +++ b/test/Tools/isac/Test_Some.thy Thu Mar 26 16:17:21 2020 +0100
9.3 @@ -76,296 +76,12 @@
9.4 declare [[ML_print_depth = 999]]
9.5 declare [[ML_exception_trace]]
9.6 \<close>
9.7 -ML \<open>
9.8 -
9.9 -\<close>
9.10
9.11 section \<open>===================================================================================\<close>
9.12 ML \<open>
9.13 \<close> ML \<open>
9.14 \<close> ML \<open>
9.15 -\<close>
9.16 -
9.17 -section \<open>===== new LI.by_tactic: Minisubplb/200-start-method.sml ==========================\<close>
9.18 -ML \<open>
9.19 -\<close> ML \<open>
9.20 -"----------- Minisubplb/200-start-method.sml -------------------------------------------------";
9.21 -"----------- Minisubplb/200-start-method.sml -------------------------------------------------";
9.22 -"----------- Minisubplb/200-start-method.sml -------------------------------------------------";
9.23 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
9.24 -val spec =
9.25 - ("Test", ["sqroot-test","univariate","equation","test"],
9.26 - ["Test","squ-equ-test-subpbl1"]);
9.27 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];
9.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.31 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.32 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem",..*)
9.33 -"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
9.34 -val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)
9.35 -(*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)
9.36 -"~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
9.37 -val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
9.38 -"~~~~~ fun me, args:"; val tac = nxt;
9.39 - val (pt, p) =
9.40 - (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
9.41 - case Step.by_tactic tac (pt,p) of
9.42 - ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"
9.43 -(* Step.do_next p ((pt, e_pos'),[]) ..ERROR = ("helpless",*)
9.44 -"~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
9.45 - (p, ((pt, e_pos'),[]));
9.46 -val pIopt = get_pblID (pt,ip);
9.47 -ip = ([],Res) (*= false*);
9.48 -tacis (* = []*);
9.49 -val SOME pI = pIopt;
9.50 -member op = [Pbl,Met] p_ (*= true*);
9.51 -(*nxt_specify_ (pt, ip) ..ERROR in creating the environment..*);
9.52 -
9.53 -val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
9.54 -"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
9.55 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* (@2) nxt = ("Apply_Method",..*)
9.56 -
9.57 -val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt;
9.58 -
9.59 -"~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
9.60 -"~~~~~ fun me, args:"; val tac = nxt;
9.61 -val ("ok", (_, _, (pt''''',p'''''))) = Step.by_tactic tac (pt,p);
9.62 -"~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
9.63 -val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)
9.64 - (*if*) Tactic.for_specify' m; (*false*)
9.65 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
9.66 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
9.67 -val PblObj {meth, ctxt, ...} = get_obj I pt p;
9.68 -val thy' = get_obj g_domID pt p;
9.69 -val thy = assoc_thy thy';
9.70 -val {srls, pre, prls, ...} = get_met mI;
9.71 -val pres = check_preconds thy prls pre meth |> map snd;
9.72 -val ctxt = ctxt |> ContextC.insert_assumptions pres;
9.73 -val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI;
9.74 -"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI)
9.75 - val actuals = itms2args thy metID itms
9.76 - val scr as Prog sc = (#scr o get_met) metID
9.77 - val formals = formal_args sc
9.78 - (*expects same sequence of (actual) args in itms and (formal) args in met*)
9.79 -fun msg_miss sc metID caller f formals actuals =
9.80 - "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
9.81 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
9.82 - "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
9.83 - "with:\n" ^
9.84 - (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
9.85 - (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
9.86 -fun msg_ambiguous sc metID f aas formals actuals =
9.87 - "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
9.88 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
9.89 - "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
9.90 - "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
9.91 - "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
9.92 - "with\n" ^
9.93 - "formals: " ^ Rule.terms2str formals ^ "\n" ^
9.94 - "actuals: " ^ Rule.terms2str actuals
9.95 - fun assoc_by_type f aa =
9.96 - case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
9.97 - [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)
9.98 - | [a] => (f, a)
9.99 - | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
9.100 - fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
9.101 - | relate_args env [] _ = env (*may drop Find?*)
9.102 - | relate_args env (f::ff) (aas as (a::aa)) =
9.103 - if type_of f = type_of a
9.104 - then relate_args (env @ [(f, a)]) ff aa
9.105 - else
9.106 - let val (f, a) = assoc_by_type f aas
9.107 - in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
9.108 - val env = relate_args [] formals actuals;
9.109 - (*val _ = trace_istate env;*)
9.110 - val {pre, prls, ...} = Specify.get_met metID;
9.111 - val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
9.112 - val ctxt = ctxt |> ContextC.insert_assumptions pres;
9.113 -
9.114 -"~~~~~ continue Step_Solve.by_tactic";
9.115 -val ini = init_form thy sc'''' env'''';
9.116 -val p = lev_dn p;
9.117 -val SOME t = ini;
9.118 -val (pos,c,_,pt) =
9.119 - generate1 (Apply_Method' (mI, SOME t, is'''', ctxt))
9.120 - (is'''', ctxt) (pt, (lev_on p, Frm))(*implicit Take*);
9.121 -("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is'''', ctxt),
9.122 - ((lev_on p, Frm), (is'''', ctxt)))], c, (pt,pos)):calcstate');
9.123 -
9.124 -val ctxt = get_ctxt pt pos;
9.125 -val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
9.126 -val SOME unknown = parseNEW ctxt "a+b+c";
9.127 -if type_of known_x = Type ("Real.real",[]) then ()
9.128 -else error "x+1=2 after start root-pbl wrong type-inference for known_x";
9.129 -if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
9.130 -else error "x+1=2 after start root-pbl wrong type-inference for unknown";
9.131 -
9.132 -"~~~~~ continue me (@3) after Step.by_tactic";
9.133 -val (pt, p) = (pt''''',p''''');
9.134 -"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
9.135 -"~~~~~ fun Step.do_next, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Pos.e_pos'),[]));
9.136 -val pIopt = get_pblID (pt,ip);
9.137 -ip = ([], Pos.Res) (* = false*);
9.138 -case tacis of [] => ();
9.139 -case pIopt of SONE => ();
9.140 -member op = [Pos.Pbl, Pos.Met] p_ (* = false*);
9.141 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
9.142 -Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
9.143 - val thy' = get_obj g_domID pt (par_pblobj pt p);
9.144 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
9.145 -"~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
9.146 - = ((pt, pos), sc, is);
9.147 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
9.148 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
9.149 - = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
9.150 - (*if*) path = [] (*then*);
9.151 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
9.152 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b)))) =
9.153 - (cc, (trans_scan_dn ist), (Program.body_of prog));
9.154 - (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
9.155 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
9.156 - = (cc, (ist |> path_down [L, R]), e);
9.157 - (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
9.158 -"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const ("Tactical.Try"(*2*), _) $ e))
9.159 - = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
9.160 - (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
9.161 -"~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t) =
9.162 - (cc, (ist |> path_down [R]), e);
9.163 - val (Program.Tac stac, a') =
9.164 - (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
9.165 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
9.166 -
9.167 -"~~~~~ fun tac_from_prog , args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
9.168 - (pt, (Proof_Context.theory_of ctxt), stac);
9.169 -
9.170 -(*+*)case LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac of (Rewrite_Set "norm_equation") => ()
9.171 -(*+*)| _ => error "tac_from_prog changed"
9.172 -
9.173 -"~~~~~ continue last scan_dn";
9.174 -val Applicable.Appl m' = Applicable.applicable_in p pt m;
9.175 -"~~~~~ fun result, args:"; val (m) = (m');
9.176 -"~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
9.177 - val fT = type_of f;
9.178 - val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
9.179 - $ HOLogic.mk_string (Rule.id_rls rls) $ f;
9.180 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
9.181 -
9.182 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
9.183 -
9.184 -(*/--------- final test ----------------------------------------------------------------------\*)
9.185 -\<close> ML \<open>
9.186 -if p = ([1], Frm)
9.187 -then
9.188 - case nxt of (Rewrite_Set _) => ()
9.189 - | _ => error "CHANGED 1"
9.190 -else error "CHANGED 2"
9.191 -\<close> ML \<open>
9.192 -\<close> ML \<open>
9.193 -\<close>
9.194 -
9.195 -section \<open>===== new LI.by_tactic: step-solve: Apply_Method with explicit Take ===============\<close>
9.196 -ML \<open>
9.197 -\<close> ML \<open>
9.198 -"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
9.199 -"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
9.200 -"----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";
9.201 -(*cp fom..*)
9.202 -"----------- me method [diff,integration] ---------------";
9.203 -val c = [];
9.204 -val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"];
9.205 -val spec = ("Integrate", ["integrate","function"], ["diff","integration"]);
9.206 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
9.207 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Add_Given "functionTerm (x ^^^ 2 + 1)"*)
9.208 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Add_Given "integrateBy x"*)
9.209 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Add_Find "Integrate.antiDerivative FF"*)
9.210 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Specify_Theory "Integrate"*)
9.211 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Specify_Problem ["integrate", "function"]*)
9.212 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Specify_Method ["diff", "integration"]*)
9.213 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Apply_Method ["diff", "integration"]*)
9.214 -
9.215 -(*+*)case nxt of (Apply_Method ["diff", "integration"]) => ()
9.216 -(*+*) | _ => error "integrate.sml -- me method [diff,integration] -- spec";
9.217 -
9.218 -\<close> ML \<open>
9.219 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "integration")*)
9.220 -(*/--------- step into Apply_Method ----------------------------------------------------------\*)
9.221 -(*\--------- step into Apply_Method ----------------------------------------------------------/*)
9.222 -\<close> ML \<open>
9.223 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>Check_Postcond ["integrate", "function"]*)
9.224 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*\<rightarrow>End_Proof'*)
9.225 -
9.226 -\<close> ML \<open>
9.227 -(*/--------- final test ----------------------------------------------------------------------\*)
9.228 -val (res, asm) = (get_obj g_result pt (fst p));
9.229 -if term2str res = "c + x + 1 / 3 * x ^^^ 3" then ()
9.230 -else error "Apply_Method with explicit Take CHANGED";
9.231 -\<close> ML \<open>
9.232 -\<close>
9.233 -
9.234 -section \<open>===== new LI.by_tactic: step-solve: biegel.7.70 Subproblem =======================\<close>
9.235 -ML \<open>
9.236 -\<close> ML \<open>
9.237 -"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
9.238 -"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
9.239 -"----------- Apply_Method with Subproblem as fst step by fun me --------------------------------";
9.240 -(*cp from biegelinie-4..*)
9.241 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
9.242 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
9.243 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
9.244 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
9.245 - "AbleitungBiegelinie dy"];
9.246 -val spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
9.247 -\<close> ML \<open>
9.248 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
9.249 -\<close> ML \<open>
9.250 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
9.251 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
9.252 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
9.253 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
9.254 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
9.255 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
9.256 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
9.257 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
9.258 -(*----------- 10 -----------*)
9.259 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
9.260 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy*)
9.261 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
9.262 -
9.263 -(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
9.264 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
9.265 -(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
9.266 -
9.267 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
9.268 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
9.269 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''"*)
9.270 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
9.271 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
9.272 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
9.273 -(*----------- 20 -----------*)
9.274 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
9.275 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.276 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.277 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.278 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.279 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.280 -(*----------- 30 -----------*)
9.281 -\<close> ML \<open>
9.282 -(*/--------- final test ----------------------------------------------------------------------\*)
9.283 -\<close> ML \<open>
9.284 -if p = ([1, 3], Pbl)
9.285 -then
9.286 - case f of PpcKF (Problem [],
9.287 - {Find = [Correct "antiDerivativeName Q"],
9.288 - Given = [Correct "functionTerm (- q_0)", Correct "integrateBy x"],
9.289 - Relate = [], Where = [], With = []}) => ()
9.290 - | _ =>
9.291 - (case nxt of
9.292 - Specify_Theory "Biegelinie" => ()
9.293 - | _ => error "CHANGED")
9.294 -else error "CHANGED"
9.295 -\<close> ML \<open>
9.296 -\<close>
9.297 +\<close>\<close>
9.298
9.299 section \<open>===================================================================================\<close>
9.300 ML \<open>
9.301 @@ -373,257 +89,129 @@
9.302 \<close> ML \<open>
9.303 \<close>
9.304
9.305 -section \<open>===== new LI.by_tactic: Minisubplb/200-start-method-NEXT_STEP.sml ================\<close>
9.306 +section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
9.307 +(*test below \<rightarrow> CalcElements/contextC.sml
9.308 + + cut to minimal for rateq + check other versions*)
9.309 ML \<open>
9.310 +"------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
9.311 +"------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
9.312 +"------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
9.313 +(*ER-7*) (*Schalk I s.87 Bsp 55b*)
9.314 +val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
9.315 + "solveFor x","solutions L"];
9.316 +val spec = ("RatEq",["univariate","equation"],["no_met"]);
9.317 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 1. specify-phase *)
9.318 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.319 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.320 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.321 +
9.322 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.323 +case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
9.324 +| _ => error "55b root specification broken";
9.325 \<close> ML \<open>
9.326 -"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
9.327 -"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
9.328 -"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
9.329 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
9.330 -val (dI',pI',mI') =
9.331 - ("Test", ["sqroot-test","univariate","equation","test"],
9.332 - ["Test","squ-equ-test-subpbl1"]);
9.333 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.334 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
9.335 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
9.336 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
9.337 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
9.338 -(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
9.339 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
9.340 -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
9.341 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(* Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
9.342 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
9.343 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
9.344 -(*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
9.345 -(*[3], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
9.346 -(*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
9.347 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
9.348 \<close> ML \<open>
9.349 -(*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
9.350 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "x / (x ^^^ 2 + -1 * (6 * x) + 9) + -1 * 1 / (x ^^^ 2 + -1 * (3 * x)) = 1 / x"
9.351 \<close> ML \<open>
9.352 -(*/--------- final test ----------------------------------------------------------------------\*)
9.353 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x"
9.354 +\<close> ML \<open> (*--- x \<noteq> 0 must come from here ^^^vvv ------------------------------------------------*)
9.355 +val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
9.356 +(*/--------- step into rewriting for x \<noteq> 0 --------------------------------------------------\*)
9.357 \<close> ML \<open>
9.358 -p
9.359 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
9.360 \<close> ML \<open>
9.361 + val ("ok", ([(Rewrite_Set "RatEq_eliminate", _, _)], _, _)) =
9.362 + (*case*) Step.by_tactic tac (pt, p) (*of*);
9.363 \<close> ML \<open>
9.364 -\<close>
9.365 +"~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
9.366 +\<close> ML \<open>
9.367 + val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
9.368 +\<close> ML \<open>
9.369 +val Rewrite_Set' (_, _, _, _, (xxx, yyy)) = m
9.370 +\<close> ML \<open>
9.371 +term2str xxx = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
9.372 +map term2str yyy = ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"];
9.373 +\<close> ML \<open>
9.374 +\<close> ML \<open>
9.375 +\<close> ML \<open>
9.376 +\<close> ML \<open>
9.377 +\<close> ML \<open>
9.378 +\<close> ML \<open>
9.379 +\<close> ML \<open>
9.380 +\<close> ML \<open>
9.381 +\<close> ML \<open>
9.382 +\<close> ML \<open>
9.383 +(*\--------- step into rewriting for x \<noteq> 0 --------------------------------------------------/*)
9.384 +\<close> ML \<open>
9.385 +(Ctree.get_assumptions_ pt''''' p''''' |> map term2str) = (*--- x \<noteq> 0 is missing -------------*)
9.386 + ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
9.387 + "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]
9.388 +\<close> ML \<open>
9.389 +if p''''' = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
9.390 +then
9.391 + ((case nxt''''' of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
9.392 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
9.393 +else error "1. Subproblem -- call changed";
9.394
9.395 -section \<open>===== new LI.by_tactic: step-solve: Apply_Method with explicit Take ===============\<close>
9.396 -ML \<open>
9.397 \<close> ML \<open>
9.398 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
9.399 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
9.400 -"----------- Apply_Method with explicit Take by Step.do_next -----------------------------------";
9.401 -val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"];
9.402 -val spec = ("Integrate", ["integrate","function"], ["diff","integration"]);
9.403 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (* 2. specify-phase *)
9.404 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.405 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.406 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.407
9.408 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];
9.409 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Model_Problem*)
9.410 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Specify_Theory "Integrate"*)
9.411 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Specify_Problem ["integrate", "function"]*)
9.412 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Specify_Method ["diff", "integration"]*)
9.413 -(*[1], Frm*)val (_, (_(*[(tac1, _, _), (tac2, _, _)]*), _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["diff", "integration"]
9.414 - Take "Integral x ^^^ 2 + 1 D x"*)
9.415 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Rewrite_Set_Inst (["(''bdv'', x)"], "integration")*)
9.416 -(*[], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-Check_Postcond ["integrate", "function"]*)
9.417 -(*[], Und*)val (_, ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>*)
9.418 +\<close> ML \<open>
9.419 +(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.420 +case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
9.421 +| _ => error "55b normalise_poly specification broken 1";
9.422
9.423 -(*/--------- final test ----------------------------------------------------------------------\*)
9.424 -val (res, asm) = (get_obj g_result pt (fst p));
9.425 -if term2str res = "c + x + 1 / 3 * x ^^^ 3" then ()
9.426 -else error "Apply_Method with initial Take CHANGED";
9.427 \<close> ML \<open>
9.428 -\<close>
9.429 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
9.430 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.431 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.432
9.433 -section \<open>===== new LI.by_tactic: step-solve: biegel.7.70 Subproblem =======================\<close>
9.434 -ML \<open>
9.435 \<close> ML \<open>
9.436 -"----------- Apply_Method with Subproblem as fst step by Step.do_next --------------------------";
9.437 -"----------- Apply_Method with Subproblem as fst step by Step.do_next --------------------------";
9.438 -"----------- Apply_Method with Subproblem as fst step by Step.do_next --------------------------";
9.439 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
9.440 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
9.441 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
9.442 - "AbleitungBiegelinie dy"];
9.443 -val spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
9.444 +if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"
9.445 +then
9.446 + ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
9.447 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))
9.448 +else error "xxx";
9.449 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 3. specify-phase *)
9.450 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.451 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.452 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.453 +
9.454 \<close> ML \<open>
9.455 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
9.456 +(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
9.457 +case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
9.458 +| _ => error "55b normalise_poly specification broken 2";
9.459 +
9.460 \<close> ML \<open>
9.461 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.462 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x ^^^ 2 = 0";
9.463 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
9.464 \<close> ML \<open>
9.465 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.466 +(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
9.467 \<close> ML \<open>
9.468 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.469 +(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_elementwise "Assumptions"*)
9.470 \<close> ML \<open>
9.471 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.472 +(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
9.473 \<close> ML \<open>
9.474 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.475 +(*[4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
9.476 \<close> ML \<open>
9.477 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.478 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
9.479 \<close> ML \<open>
9.480 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*<-*)
9.481 +(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_Postcond ["rational", "univariate", "equation"]*)
9.482 \<close> ML \<open>
9.483 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>End_Proof'*)
9.484 +
9.485 \<close> ML \<open>
9.486 -\<close>
9.487 +if f2str f = "[x = 0, x = 6 / 5]" then () else error "test CHANGED";
9.488 +\<close> text \<open>
9.489 +if terms2str (get_assumptions_ pt p) = "[\"x = 6 / 5\"," ^
9.490 + "\"x = 0\"," ^
9.491 + "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^
9.492 + "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]"
9.493 +then () else error "rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
9.494
9.495 -section \<open>===================================================================================\<close>
9.496 -ML \<open>
9.497 -\<close> ML \<open>
9.498 -\<close> ML \<open>
9.499 -\<close>
9.500 -
9.501 -section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
9.502 -ML \<open>
9.503 -(* here some code has been lost at or before 6871316e75c3 --
9.504 --- get back from test/../Knowledge/rateq.sml*)
9.505 -
9.506 -"~~~~~ fun xxx , args:"; val () = ();
9.507 -\<close> ML \<open>
9.508 - (*if*) ip = ([], Pos.Res) (*else*);
9.509 -\<close> ML \<open>
9.510 - val _ = (*case*) tacis (*of*);
9.511 -\<close> ML \<open>
9.512 - val SOME _ = (*case*) pIopt (*of*);
9.513 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.514 - switch_specify_solve p_ (pt, ip);
9.515 -\<close> ML \<open>
9.516 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
9.517 -\<close> ML \<open>
9.518 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
9.519 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.520 - LI.do_next (pt, input_pos);
9.521 -\<close> ML \<open>
9.522 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
9.523 -\<close> ML \<open>
9.524 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
9.525 -\<close> ML \<open>
9.526 - val thy' = get_obj g_domID pt (par_pblobj pt p);
9.527 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
9.528 -\<close> ML \<open>
9.529 -(*+*)Proof_Context.theory_of ctxt; (*..,Isac.RatEq}*)
9.530 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.531 - (*case*)
9.532 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
9.533 -\<close> ML \<open>
9.534 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
9.535 - = (sc, (pt, pos), ist, ctxt);
9.536 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.537 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
9.538 -\<close> ML \<open>
9.539 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) = ((prog, (ptp, ctxt)) ,(Pstate ist) );
9.540 -\<close> ML \<open>
9.541 - (*if*) path = [] (*then*);
9.542 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.543 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
9.544 -\<close> ML \<open>
9.545 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))))
9.546 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
9.547 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.548 - (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
9.549 -\<close> ML \<open>
9.550 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
9.551 - = (cc, (ist |> path_down [L, R]), e);
9.552 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.553 - (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
9.554 -\<close> ML \<open>
9.555 -"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const ("Tactical.Try"(*2*), _) $ e))
9.556 - = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
9.557 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.558 - (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
9.559 -\<close> ML \<open>
9.560 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
9.561 - = (cc, (ist |> path_down [R]), e);
9.562 -\<close> ML \<open>
9.563 - (*if*) Tactical.contained_in t (*else*);
9.564 -\<close> ML \<open>
9.565 - val (Program.Tac prog_tac, form_arg) =
9.566 - (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
9.567 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.568 - check_tac cc ist (prog_tac, form_arg)
9.569 -\<close> ML \<open>
9.570 -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) = (cc, ist, (prog_tac, form_arg));
9.571 -\<close> ML \<open>
9.572 -(*+*)Proof_Context.theory_of ctxt; (*..,Isac.RatEq}*)
9.573 -\<close> text \<open>(*Undefined fact: "all_left"*)
9.574 - val (m, m') =
9.575 - LItool.stac2tac_(*..see TODO.thy*)pt (Proof_Context.theory_of ctxt) prog_tac
9.576 -\<close> ML \<open>
9.577 -"~~~~~ fun stac2tac_ , args:"; val () = ();
9.578 -\<close> ML \<open>
9.579 -\<close> ML \<open>
9.580 -\<close> ML \<open>
9.581 -\<close> ML \<open>
9.582 -\<close> ML \<open>
9.583 -\<close> ML \<open>
9.584 -\<close> ML \<open>
9.585 -\<close> ML \<open>
9.586 -\<close> ML \<open>
9.587 -\<close> ML \<open>
9.588 -\<close> ML \<open>
9.589 -\<close> ML \<open>
9.590 -\<close> ML \<open>
9.591 -\<close> ML \<open>
9.592 -\<close> ML \<open>
9.593 -\<close> ML \<open>
9.594 -\<close> ML \<open>
9.595 -\<close> ML \<open>
9.596 -\<close> ML \<open>
9.597 -\<close> ML \<open>
9.598 -\<close> ML \<open>
9.599 -\<close> ML \<open>
9.600 -\<close> ML \<open>
9.601 -(*\\------------------ end step into --------------------------------------------------------//*)
9.602 -\<close> ML \<open>
9.603 -(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
9.604 -(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
9.605 -(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
9.606 -(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
9.607 -
9.608 -(*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
9.609 -(*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
9.610 -(*^^^ 2*15*)
9.611 -(*[4,3,1], Frm*)val (p'''''_',_,f,nxt'''''_',_,pt'''''_') = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
9.612 -(* f = FormKF "16 + 12 * x = 0" *)
9.613 -(*+*)(get_istate_LI pt'''''_' p'''''_' |> istate2str); (*false NOTok after tac found*)
9.614 -
9.615 -(*//------------------ begin step into 2 ----------------------------------------------------\\*)
9.616 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''''_', p'''''_', [], pt'''''_');
9.617 - val ("ok", (_, _, (pt, p))) = (*case*) Step.by_tactic tac (pt, p) (*of*);
9.618 -
9.619 -(*+*)if (get_istate_LI pt p |> istate2str)
9.620 -(*+*) = "Pstate ([\"\n(e_e, 16 + 12 * x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOME e_e, \nx = -1 * 16 / 12, ORundef, true, true)"
9.621 -(*+*)then () else error "rat-eq + subpbl: istate 1";
9.622 -
9.623 - val ("ok", (ts as (_, _, _) :: _, _, _)) =
9.624 - (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
9.625 -
9.626 - val tac =
9.627 - case ts of
9.628 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
9.629 - | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
9.630 -
9.631 - (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
9.632 - tac, Telem.Sundef, pt); (*return from me*)
9.633 -"~~~~~ from fun me\<longrightarrow>toplevel, return:"; val (p'''''_',_,f,nxt'''''_',_,pt'''''_')
9.634 - = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
9.635 - tac, Telem.Sundef, pt);
9.636 -
9.637 -(*+*)if (get_istate_LI pt'''''_' p'''''_' |> istate2str)
9.638 -(*+*) = "Pstate ([\"\n(e_e, 16 + 12 * x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOME e_e, \nx = -1 * 16 / 12, ORundef, true, true)"
9.639 -(*+*)then () else error "rat-eq + subpbl: istate 2";
9.640 -(*\\------------------ end step into 2 ------------------------------------------------------//*)
9.641 -
9.642 -(*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_';(*Rewrite_Set "polyeq_simplify"*)
9.643 -(*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)
9.644 -(*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
9.645 -(* f = FormKF "[x = -4 / 3]" *)
9.646 -(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
9.647 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
9.648 -(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
9.649 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)
9.650 -
9.651 -if p = ([], Res) andalso f2str f = "[x = -4 / 3]"
9.652 -then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"
9.653 -else error "rat-eq + subpbl: end CHANGED 2";
9.654 \<close> ML \<open>
9.655 \<close> ML \<open>
9.656 "~~~~~ fun xxx , args:"; val () = ();