1 (* 1.if-te-else- 8.02 f"ur Richard
4 use"tests/rationals2.sml";
9 (*---------------- 25.7.02 ---------------------*)
11 val thy = (theory "Isac_Knowledge");
12 val t = (Thm.term_of o the o (TermC.parse thy)) "contains_root (sqrt(x)=1)";
13 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
15 val t = (Thm.term_of o the o (TermC.parse thy)) "is_rootequation_in (sqrt(x)=1) x";
16 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
19 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
20 val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*x)";
22 val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(#3+#4*a)";
24 val t = (Thm.term_of o the o (TermC.parse thy)) "#1 + #2*sqrt(#3+#4*x)";
26 val t = (Thm.term_of o the o (TermC.parse thy)) "x + #2*sqrt(#3+#4*a)";
29 val t = (Thm.term_of o the o (TermC.parse thy))
30 "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
31 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
33 val t = (Thm.term_of o the o (TermC.parse thy))
34 "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
35 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
37 val t = (Thm.term_of o the o (TermC.parse Test.thy))
38 "is_rootequation_in (sqrt(x)=1) x";
39 TermC.atom_trace_detail @{context} t;
40 val t = (Thm.term_of o the o (TermC.parse (theory "Isac_Knowledge")))
41 "is_rootequation_in (sqrt(x)=1) x";
42 TermC.atom_trace_detail @{context} t;
45 val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
47 val SOME(tt,_) = rewrite_set_ (theory "Isac_Knowledge") true tval_rls t;
49 rewrite_set "Isac_Knowledge" true
50 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
51 rewrite_set "Test" true
52 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
55 (*WN: \<up> --- bitte nimm vorerst immer (theory "Isac_Knowledge"), damit wird richtig gematcht,
56 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
59 [Problem.prep_input (*Test.thy*) (theory "Isac_Knowledge")
60 (["rootX", "univariate", "equation", "test"],
61 [("#Given" ,["equality e_e", "solveFor v_v"]),
62 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
63 ("#Find" ,["solutions v_i_"])],
64 Rule_Set.append_rules Rule_Set.empty [Eval ("Test.is_rootequation_in", eval_is_rootequation_in "")],
65 [("Test", "methode")])]
68 M_Match.match_pbl ["equality (sqrt(x)=1)", "solveFor x", "solutions L"] (Problem.from_store ["rootX", "univariate", "equation", "test"]);
71 [Problem.prep_input (theory "Isac_Knowledge")
72 (["approximate", "univariate", "equation", "test"],
73 [("#Given", ["equality e_e", "solveFor v_v", "errorBound err_"]),
74 ("#Where", ["matches (?a = ?b) e_e"]),
75 ("#Find", ["solutions v_i_"])],
76 Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.TermC.matches",eval_matches "#matches_")], [])]
79 methods:= overwritel (!methods,
82 (("Isac_Knowledge", "solve_univar_err"):metID,
83 [("#Given" ,["equality e_e", "solveFor v_v", "errorBound err_"]),
84 ("#Find" ,["solutions v_i_"])
86 {rew_ord="tless_true",rls'="tval_rls",asm_rls=Rule_Set.empty,where_rls=Rule_Set.empty,calc=[],
87 asm_rls=[],asm_thm=[]},
88 "Program Solve_univar_err (e_e::bool) (v_::real) (err_::bool) = \
89 \ (if (is_rootequation_in e_e v_v)\
90 \ then ((SubProblem (IsacX,[squareroot,univariate,equation],\
91 \ (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\
92 \ else ((SubProblem (IsacX,[linear,univariate,equation],\
93 \ (RatArith_,solve_linear)) [BOOL e_e, REAL v_])))"
96 val fmz = ["equality (1+2*x=0)", "solveFor x", "errorBound (eps=0)",
99 ("Isac_Knowledge",["approximate", "univariate", "equation", "test"],
100 ("Isac_Knowledge", "solve_univar_err"));
101 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 (*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge", "solve_univar_err"))*)
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
111 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 (*val nxt = ("Apply_Method",Apply_Method ("RatArith", "solve_linear"))*)
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))
126 andalso nxt = ("End_Proof'",End_Proof') then ()
127 else error "new behaviour in testexample rationals2.sml 1+2*x=0";
129 (*---------------------------------*)
130 "-------------- is_rootequ_in - SubProblem -------------------------";
131 "-------------- is_rootequ_in - SubProblem -------------------------";
132 "-------------- is_rootequ_in - SubProblem -------------------------";
133 val fmz = ["equality (sqrt(x) - 1 = 0)", "solveFor x", "errorBound (eps=0)",
136 ("Isac_Knowledge",["approximate", "univariate", "equation", "test"],
137 ("Isac_Knowledge", "solve_univar_err"));
138 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
146 (*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge", "solve_univar_err"))*)
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 if p = ([1,1],Frm) andalso
159 f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso
160 nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then ()
161 else error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";