wneuper@59577
|
1 |
(* Title: "ProgLang/contextC.sml"
|
wneuper@59577
|
2 |
Author: Walther Neuper
|
wneuper@59577
|
3 |
(c) due to copyright terms
|
wneuper@59577
|
4 |
*)
|
wneuper@59577
|
5 |
|
wneuper@59577
|
6 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60424
|
7 |
"This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks ";
|
Walther@60424
|
8 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59577
|
9 |
"table of contents -----------------------------------------------------------------------------";
|
wneuper@59577
|
10 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59582
|
11 |
"----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
|
wneuper@59582
|
12 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59582
|
13 |
"----------- fun initialise --------------------------------------------------------------------";
|
wneuper@59582
|
14 |
"----------- build fun initialise'--------------------------------------------------------------";
|
walther@59842
|
15 |
"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
|
wneuper@59582
|
16 |
"----------- fun transfer_asms_from_to ---------------------------------------------------------";
|
walther@59842
|
17 |
"----------- fun avoid_contradict --------------------------------------------------------------";
|
walther@59842
|
18 |
"----------- fun subpbl_to_caller --------------------------------------------------------------";
|
Walther@60558
|
19 |
"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
|
wneuper@59577
|
20 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59577
|
21 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59577
|
22 |
"-----------------------------------------------------------------------------------------------";
|
wneuper@59577
|
23 |
|
wneuper@59577
|
24 |
|
wneuper@59582
|
25 |
"----------- fun initialise --------------------------------------------------------------------";
|
wneuper@59582
|
26 |
"----------- fun initialise --------------------------------------------------------------------";
|
wneuper@59582
|
27 |
"----------- fun initialise --------------------------------------------------------------------";
|
walther@60330
|
28 |
val t = @{term "a * b + - 123 * c :: real"};
|
wneuper@59582
|
29 |
val ctxt = initialise "Rational" (vars t)
|
wneuper@59582
|
30 |
|
wneuper@59582
|
31 |
(*----- now parsing infers the type *)
|
wneuper@59582
|
32 |
val SOME t = parseNEW ctxt "x";
|
wneuper@59582
|
33 |
if type_of t = HOLogic.realT then error "type inference failed 1" else ();
|
wneuper@59582
|
34 |
|
wneuper@59582
|
35 |
val SOME t = parseNEW ctxt "a";
|
wneuper@59582
|
36 |
if type_of t = HOLogic.realT then () else error "type inference failed 2";
|
wneuper@59582
|
37 |
|
wneuper@59582
|
38 |
"----------- build fun initialise'--------------------------------------------------------------";
|
wneuper@59582
|
39 |
"----------- build fun initialise'--------------------------------------------------------------";
|
wneuper@59582
|
40 |
"----------- build fun initialise'--------------------------------------------------------------";
|
walther@59997
|
41 |
val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
wneuper@59582
|
42 |
"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
|
wneuper@59582
|
43 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
wneuper@59582
|
44 |
"AbleitungBiegelinie dy"];
|
wneuper@59582
|
45 |
val (thy, fmz) = (@{theory Biegelinie}, fmz);
|
wneuper@59582
|
46 |
|
wneuper@59582
|
47 |
initialise' thy fmz;
|
wneuper@59582
|
48 |
|
wneuper@59582
|
49 |
val ctxt = thy |> Proof_Context.init_global
|
walther@60017
|
50 |
val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct op =
|
wneuper@59582
|
51 |
val _ = TermC.raise_type_conflicts ts;
|
wneuper@59582
|
52 |
|
walther@59842
|
53 |
"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
|
walther@59842
|
54 |
"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
|
walther@59842
|
55 |
"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
|
walther@59728
|
56 |
val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
|
walther@59728
|
57 |
val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
|
walther@59842
|
58 |
val asms = ContextC.get_assumptions ctxt;
|
wneuper@59582
|
59 |
if asms = [@{term "x * v"}, @{term "2 * u"}]
|
wneuper@59582
|
60 |
then () else error "mstools.sml insert_/get_assumptions changed 1.";
|
wneuper@59582
|
61 |
|
wneuper@59582
|
62 |
"----------- fun transfer_asms_from_to ---------------------------------------------------------";
|
wneuper@59582
|
63 |
"----------- fun transfer_asms_from_to ---------------------------------------------------------";
|
wneuper@59582
|
64 |
"----------- fun transfer_asms_from_to ---------------------------------------------------------";
|
wneuper@59592
|
65 |
val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
|
walther@59728
|
66 |
val from_ctxt = ContextC.insert_assumptions
|
Walther@60565
|
67 |
[TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
|
walther@59728
|
68 |
val to_ctxt = ContextC.insert_assumptions
|
Walther@60565
|
69 |
[TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
|
wneuper@59582
|
70 |
val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
|
walther@59868
|
71 |
if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
|
wneuper@59582
|
72 |
then () else error "fun transfer_asms_from_to changed"
|
wneuper@59582
|
73 |
|
walther@59842
|
74 |
|
walther@59842
|
75 |
"----------- fun avoid_contradict --------------------------------------------------------------";
|
walther@59842
|
76 |
"----------- fun avoid_contradict --------------------------------------------------------------";
|
walther@59842
|
77 |
"----------- fun avoid_contradict --------------------------------------------------------------";
|
walther@59842
|
78 |
val preds = [
|
Walther@60565
|
79 |
(*0.pre*)TermC.parse_test @{context} "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
|
Walther@60565
|
80 |
(*1.pre*)TermC.parse_patt_test @{theory} ("\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
|
walther@60330
|
81 |
(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x"),
|
Walther@60565
|
82 |
(*0.asm*)TermC.parse_test @{context} "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
|
Walther@60565
|
83 |
(*0.asm*)TermC.parse_test @{context} "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
|
walther@59842
|
84 |
];
|
walther@59842
|
85 |
|
Walther@60565
|
86 |
val t = TermC.parse_test @{context} "[x = 0, x = 6 / 5]";
|
walther@59842
|
87 |
val (t', for_asm) = avoid_contradict t preds;
|
walther@59868
|
88 |
if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"]
|
walther@59842
|
89 |
then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
|
walther@59842
|
90 |
|
Walther@60565
|
91 |
val t = TermC.parse_test @{context} "x = 0";
|
walther@59842
|
92 |
val (t', for_asm) = avoid_contradict t preds;
|
walther@59868
|
93 |
if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = []
|
walther@59842
|
94 |
then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
|
walther@59842
|
95 |
|
Walther@60565
|
96 |
val t = TermC.parse_test @{context} "x = 1";
|
walther@59842
|
97 |
val (t', for_asm) = avoid_contradict t preds;
|
walther@59868
|
98 |
if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"]
|
walther@59842
|
99 |
then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
|
walther@59842
|
100 |
|
Walther@60565
|
101 |
val t = TermC.parse_test @{context} "a + b";
|
walther@59842
|
102 |
val (t', for_asm) = avoid_contradict t preds;
|
walther@59868
|
103 |
if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = []
|
walther@59842
|
104 |
then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
|
walther@59842
|
105 |
|
Walther@60565
|
106 |
val t = TermC.parse_test @{context} "[a + b]";
|
walther@59842
|
107 |
val (t', for_asm) = avoid_contradict t preds;
|
walther@59868
|
108 |
if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = []
|
walther@59842
|
109 |
then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
|
walther@59842
|
110 |
|
walther@59842
|
111 |
|
walther@59842
|
112 |
"----------- fun subpbl_to_caller --------------------------------------------------------------";
|
walther@59842
|
113 |
"----------- fun subpbl_to_caller --------------------------------------------------------------";
|
walther@59842
|
114 |
"----------- fun subpbl_to_caller --------------------------------------------------------------";
|
wneuper@59592
|
115 |
val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
|
walther@59842
|
116 |
|
walther@59728
|
117 |
val sub_ctxt = ContextC.insert_assumptions
|
Walther@60565
|
118 |
[TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
|
Walther@60565
|
119 |
val prog_res = TermC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
|
walther@59842
|
120 |
|
walther@59842
|
121 |
(* NO contradiction ..*)
|
walther@59728
|
122 |
val caller_ctxt = ContextC.insert_assumptions
|
Walther@60565
|
123 |
[TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
|
walther@59842
|
124 |
val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
|
wneuper@59582
|
125 |
|
walther@59868
|
126 |
if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
|
walther@59842
|
127 |
["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
|
walther@59842
|
128 |
then () else error "fun subpbl_to_caller changed 1";
|
walther@59842
|
129 |
|
walther@59842
|
130 |
(* a contradiction ..*)
|
walther@59842
|
131 |
val caller_ctxt = ContextC.insert_assumptions
|
Walther@60565
|
132 |
[TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt
|
walther@59842
|
133 |
val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
|
walther@59842
|
134 |
|
walther@59868
|
135 |
if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
|
walther@59842
|
136 |
["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]
|
walther@59842
|
137 |
then () else error "fun subpbl_to_caller changed 2";
|
wneuper@59582
|
138 |
|
wneuper@59582
|
139 |
|
Walther@60558
|
140 |
"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
|
Walther@60558
|
141 |
"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
|
Walther@60558
|
142 |
"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
|
walther@59842
|
143 |
(*ER-7*) (*Schalk I s.87 Bsp 55b*)
|
walther@60242
|
144 |
val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
|
walther@59997
|
145 |
"solveFor x", "solutions L"];
|
Walther@60543
|
146 |
val spec = ((** )"RatEq"( **)"PolyEq"(**),["univariate", "equation"],["no_met"]);
|
walther@59842
|
147 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 0. specify-phase *)
|
walther@59842
|
148 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
149 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
150 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
151 |
|
walther@59842
|
152 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
153 |
(*+*)case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
|
walther@59842
|
154 |
(*+*)| _ => error "55b root specification broken";
|
walther@59842
|
155 |
|
walther@59842
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 0. solve-phase*)
|
walther@59842
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60330
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)";
|
walther@59842
|
159 |
|
walther@59868
|
160 |
(*+*)if (Ctree.get_assumptions pt p |> map UnparseC.term) =
|
walther@59842
|
161 |
(*+*) ["x \<noteq> 0",
|
walther@60330
|
162 |
(*+*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
|
walther@60242
|
163 |
(*+*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
|
walther@59842
|
164 |
(*+*)then () else error "assumptions before 1. Subproblem CHANGED";
|
walther@60330
|
165 |
(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)"
|
walther@59842
|
166 |
(*+*)then
|
walther@59842
|
167 |
(*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
|
walther@59846
|
168 |
(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
|
walther@59842
|
169 |
(*+*)else error "1. Subproblem -- call changed";
|
walther@59842
|
170 |
|
walther@59842
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
|
walther@59842
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
174 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
175 |
|
walther@59842
|
176 |
(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
177 |
case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
|
walther@59842
|
178 |
| _ => error "55b normalise_poly specification broken 1";
|
walther@59842
|
179 |
|
walther@59842
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
|
walther@59842
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@60242
|
182 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
|
walther@59842
|
183 |
|
walther@60344
|
184 |
if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
|
walther@59842
|
185 |
then
|
walther@59842
|
186 |
((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
|
walther@59846
|
187 |
| _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
|
walther@60344
|
188 |
else error "Subproblem ([4, 3], Res) CHANGED";
|
walther@59842
|
189 |
|
walther@59842
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
|
walther@59842
|
191 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
192 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
193 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
194 |
|
walther@59842
|
195 |
(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
|
walther@59842
|
196 |
case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
|
walther@59842
|
197 |
| _ => error "55b normalise_poly specification broken 2";
|
walther@59842
|
198 |
|
walther@60242
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x \<up> 2 = 0"*) (* 2. solve-phase *)
|
walther@59842
|
200 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
walther@59842
|
201 |
|
walther@59842
|
202 |
(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
|
walther@59842
|
203 |
(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
|
walther@59842
|
204 |
(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
|
walther@59842
|
205 |
|
walther@59868
|
206 |
(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
|
walther@60242
|
207 |
(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
|
walther@60344
|
208 |
(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
|
walther@60344
|
209 |
(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
|
walther@60344
|
210 |
(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
|
walther@60344
|
211 |
(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
|
walther@59842
|
212 |
(*0.asm*) "x \<noteq> 0",
|
walther@60344
|
213 |
(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
|
walther@59842
|
214 |
(* *)])
|
walther@59842
|
215 |
(* *)then () else error "assumptions at end 2. Subproblem CHANGED";
|
walther@59842
|
216 |
(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
|
walther@59842
|
217 |
|
walther@59842
|
218 |
(*/--------- step into 2. Check_Postcond -----------------------------------------------------\*)
|
walther@59842
|
219 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
walther@59842
|
220 |
|
walther@59842
|
221 |
val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)
|
walther@59842
|
222 |
Step.by_tactic tac (pt, p) (*of*);
|
walther@59842
|
223 |
"~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@59921
|
224 |
val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
|
walther@59842
|
225 |
(*if*) Tactic.for_specify' m (*else*);
|
walther@59842
|
226 |
|
walther@59842
|
227 |
val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =
|
walther@59842
|
228 |
Step_Solve.by_tactic m ptp;
|
walther@59842
|
229 |
"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Check_Postcond' _), (ptp as (pt, p))) = (m, ptp);
|
walther@59842
|
230 |
|
walther@59842
|
231 |
LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
|
walther@59843
|
232 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
|
walther@59842
|
233 |
= (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
|
walther@59842
|
234 |
val parent_pos = par_pblobj pt p
|
Walther@60559
|
235 |
val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
|
walther@59842
|
236 |
val prog_res =
|
walther@59842
|
237 |
case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
|
walther@59842
|
238 |
(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
|
walther@59843
|
239 |
|(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
|
walther@59842
|
240 |
(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
|
walther@59842
|
241 |
(*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
|
walther@59842
|
242 |
(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
|
walther@59842
|
243 |
(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
|
walther@59844
|
244 |
(*OLD*) | _ => Ctree.get_assumptions pt pos);
|
walther@59842
|
245 |
(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
|
walther@59842
|
246 |
( *OLD*)
|
walther@59842
|
247 |
(*if*) parent_pos = [] (*else*);
|
walther@59842
|
248 |
(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
|
walther@59842
|
249 |
(*NEW*) (Pstate i, c) => (i, c)
|
walther@59842
|
250 |
(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
|
walther@59842
|
251 |
|
walther@59868
|
252 |
(* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt_parent), [
|
walther@60344
|
253 |
(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
|
walther@60344
|
254 |
(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
|
walther@60344
|
255 |
(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
|
walther@59842
|
256 |
(*0.asm*) "x \<noteq> 0",
|
walther@60344
|
257 |
(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
|
walther@59842
|
258 |
(* *)])
|
walther@59842
|
259 |
(* *)then () else error "assumptions at xxx CHANGED";
|
walther@59842
|
260 |
|
walther@59842
|
261 |
val (prog_res', ctxt') =
|
walther@59842
|
262 |
ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
|
walther@59868
|
263 |
(* *)if eq_set op = (map UnparseC.term (get_assumptions ctxt'), [
|
walther@60242
|
264 |
(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
|
walther@60344
|
265 |
(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
|
walther@60344
|
266 |
(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
|
walther@60344
|
267 |
(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
|
walther@59842
|
268 |
(*0.asm*) "x \<noteq> 0", (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
|
walther@60344
|
269 |
(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
|
walther@60344
|
270 |
(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
|
walther@59842
|
271 |
(*2.res*) (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)
|
walther@59842
|
272 |
(* *)])
|
walther@59842
|
273 |
(* *)then () else error "assumptions at xxx CHANGED";
|
walther@59842
|
274 |
|
walther@59842
|
275 |
"~~~~~ fun subpbl_to_caller , args:"; val (sub_ctxt, prog_res, caller_ctxt)
|
walther@59842
|
276 |
= (sub_ctxt, prog_res, ctxt_parent);
|
walther@59842
|
277 |
val xxxxx = caller_ctxt
|
walther@59842
|
278 |
|> get_assumptions
|
walther@59842
|
279 |
|> avoid_contradict prog_res
|
walther@59842
|
280 |
|> apsnd (insert_assumptions_cao caller_ctxt)
|
walther@59842
|
281 |
|> apsnd (transfer_asms_from_to sub_ctxt);
|
walther@59842
|
282 |
|
walther@59842
|
283 |
xxxxx (*return from xxx*);
|
walther@59842
|
284 |
"~~~~~ from fun subpbl_to_caller \<longrightarrow>fun by_tactic , return:"; val (prog_res', ctxt')
|
walther@59842
|
285 |
= (xxxxx);
|
walther@59843
|
286 |
(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
|
walther@59842
|
287 |
(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
|
walther@59932
|
288 |
(*NEW*) val ((p, p_), ps, _, pt) = Step.add tac (ist', ctxt') (pt, (parent_pos, Res));
|
walther@59842
|
289 |
|
walther@59842
|
290 |
(*NEW*) ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
|
walther@59842
|
291 |
(*return from xxx*);
|
walther@59842
|
292 |
"~~~~~ from fun LI.by_tactic \<longrightarrow>fun Step_Solve.by_tactic \<longrightarrow>fun Step.by_tactic \<longrightarrow>fun me, return:"; val (("ok", (_, _, (pt, p))))
|
walther@59842
|
293 |
= ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))));
|
walther@59842
|
294 |
val ("ok", (ts as (_, _, _) :: _, _, _)) =
|
walther@59842
|
295 |
(*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
walther@59842
|
296 |
val tac =
|
walther@59842
|
297 |
case ts of
|
walther@59842
|
298 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@59842
|
299 |
| _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
walther@59842
|
300 |
|
walther@59842
|
301 |
"~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
|
walther@59842
|
302 |
= (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
|
walther@59937
|
303 |
tac, Celem.Sundef, pt);
|
walther@59842
|
304 |
(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
|
walther@59842
|
305 |
|
walther@59842
|
306 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
|
walther@59842
|
307 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
|
walther@59842
|
308 |
|
walther@59842
|
309 |
(*/-------- final test -----------------------------------------------------------------------\*)
|
walther@60344
|
310 |
if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) = [
|
walther@60344
|
311 |
"x = 6 / 5",
|
walther@60344
|
312 |
"lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x", "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
|
walther@60344
|
313 |
"\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
|
walther@60344
|
314 |
"x \<noteq> 0",
|
walther@60344
|
315 |
"9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
|
walther@60242
|
316 |
"x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
|
walther@59842
|
317 |
then () else error "test CHANGED";
|