wneuper@59577: (* Title:  "ProgLang/contextC.sml"
wneuper@59577:    Author: Walther Neuper
wneuper@59577:    (c) due to copyright terms
wneuper@59577: *)
wneuper@59577: 
wneuper@59577: "-----------------------------------------------------------------------------------------------";
Walther@60424: "This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks ";
Walther@60424: "-----------------------------------------------------------------------------------------------";
wneuper@59577: "table of contents -----------------------------------------------------------------------------";
wneuper@59577: "-----------------------------------------------------------------------------------------------";
wneuper@59582: "----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
wneuper@59582: "-----------------------------------------------------------------------------------------------";
wneuper@59582: "----------- fun initialise --------------------------------------------------------------------";
wneuper@59582: "----------- build fun initialise'--------------------------------------------------------------";
walther@59842: "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
wneuper@59582: "----------- fun transfer_asms_from_to ---------------------------------------------------------";
walther@59842: "----------- fun avoid_contradict --------------------------------------------------------------";
walther@59842: "----------- fun subpbl_to_caller --------------------------------------------------------------";
Walther@60558: "----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
wneuper@59577: "-----------------------------------------------------------------------------------------------";
wneuper@59577: "-----------------------------------------------------------------------------------------------";
wneuper@59577: "-----------------------------------------------------------------------------------------------";
wneuper@59577: 
wneuper@59577: 
wneuper@59582: "----------- fun initialise --------------------------------------------------------------------";
wneuper@59582: "----------- fun initialise --------------------------------------------------------------------";
wneuper@59582: "----------- fun initialise --------------------------------------------------------------------";
walther@60330: val t = @{term "a * b + - 123 * c :: real"};
wneuper@59582: val ctxt = initialise "Rational" (vars t)
wneuper@59582: 
wneuper@59582: (*----- now parsing infers the type *)
wneuper@59582: val SOME t = parseNEW ctxt "x";
wneuper@59582: if type_of t = HOLogic.realT then error "type inference failed 1" else ();
wneuper@59582: 
wneuper@59582: val SOME t = parseNEW ctxt "a";
wneuper@59582: if type_of t = HOLogic.realT then () else error "type inference failed 2";
wneuper@59582: 
wneuper@59582: "----------- build fun initialise'--------------------------------------------------------------";
wneuper@59582: "----------- build fun initialise'--------------------------------------------------------------";
wneuper@59582: "----------- build fun initialise'--------------------------------------------------------------";
walther@59997: val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
wneuper@59582: 	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
wneuper@59582: 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
wneuper@59582:        "AbleitungBiegelinie dy"];
wneuper@59582: val (thy, fmz) = (@{theory Biegelinie}, fmz);
wneuper@59582: 
wneuper@59582: initialise' thy fmz;
wneuper@59582: 
wneuper@59582:     val ctxt = thy |> Proof_Context.init_global
walther@60017:     val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct op =
wneuper@59582:     val _ = TermC.raise_type_conflicts ts;
wneuper@59582: 
walther@59842: "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
walther@59842: "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
walther@59842: "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
walther@59728: val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
walther@59728: val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
walther@59842: val asms = ContextC.get_assumptions ctxt;
wneuper@59582: if asms = [@{term "x * v"}, @{term "2 * u"}]
wneuper@59582: then () else error "mstools.sml insert_/get_assumptions changed 1.";
wneuper@59582: 
wneuper@59582: "----------- fun transfer_asms_from_to ---------------------------------------------------------";
wneuper@59582: "----------- fun transfer_asms_from_to ---------------------------------------------------------";
wneuper@59582: "----------- fun transfer_asms_from_to ---------------------------------------------------------";
wneuper@59592: val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
walther@59728: val from_ctxt = ContextC.insert_assumptions
Walther@60565:   [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
walther@59728: val to_ctxt = ContextC.insert_assumptions
Walther@60565:   [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
wneuper@59582: val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
walther@59868: if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
wneuper@59582: then () else error "fun transfer_asms_from_to changed"
wneuper@59582: 
walther@59842: 
walther@59842: "----------- fun avoid_contradict --------------------------------------------------------------";
walther@59842: "----------- fun avoid_contradict --------------------------------------------------------------";
walther@59842: "----------- fun avoid_contradict --------------------------------------------------------------";
walther@59842: val preds = [
Walther@60565: (*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: (*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: (*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: (*0.asm*)TermC.parse_test @{context}  "x \<noteq> 0",             (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
Walther@60565: (*0.asm*)TermC.parse_test @{context}  "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
walther@59842: ];
walther@59842: 
Walther@60565: val t = TermC.parse_test @{context} "[x = 0, x = 6 / 5]";
walther@59842: val (t', for_asm) = avoid_contradict t preds;
walther@59868: if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"]
walther@59842: then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
walther@59842: 
Walther@60565: val t = TermC.parse_test @{context} "x = 0";
walther@59842: val (t', for_asm) = avoid_contradict t preds;
walther@59868: if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = []
walther@59842: then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
walther@59842: 
Walther@60565: val t = TermC.parse_test @{context} "x = 1";
walther@59842: val (t', for_asm) = avoid_contradict t preds;
walther@59868: if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"]
walther@59842: then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
walther@59842: 
Walther@60565: val t = TermC.parse_test @{context} "a + b";
walther@59842: val (t', for_asm) = avoid_contradict t preds;
walther@59868: if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = []
walther@59842: then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
walther@59842: 
Walther@60565: val t = TermC.parse_test @{context} "[a + b]";
walther@59842: val (t', for_asm) = avoid_contradict t preds;
walther@59868: if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = []
walther@59842: then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
walther@59842: 
walther@59842: 
walther@59842: "----------- fun subpbl_to_caller --------------------------------------------------------------";
walther@59842: "----------- fun subpbl_to_caller --------------------------------------------------------------";
walther@59842: "----------- fun subpbl_to_caller --------------------------------------------------------------";
wneuper@59592: val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
walther@59842: 
walther@59728: val sub_ctxt = ContextC.insert_assumptions
Walther@60565:   [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
Walther@60565: val prog_res = TermC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
walther@59842: 
walther@59842: (* NO contradiction ..*)
walther@59728: val caller_ctxt = ContextC.insert_assumptions
Walther@60565:   [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
walther@59842: val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
wneuper@59582: 
walther@59868: if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
walther@59842:   ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
walther@59842: then () else error "fun subpbl_to_caller changed 1";
walther@59842: 
walther@59842: (* a contradiction ..*)
walther@59842: val caller_ctxt = ContextC.insert_assumptions
Walther@60565:   [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt
walther@59842: val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
walther@59842: 
walther@59868: if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
walther@59842:   ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]
walther@59842: then () else error "fun subpbl_to_caller changed 2";
wneuper@59582: 
wneuper@59582: 
Walther@60558: "----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
Walther@60558: "----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
Walther@60558: "----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
walther@59842: (*ER-7*) (*Schalk I s.87 Bsp 55b*)
walther@60242: val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
walther@59997: 	   "solveFor x", "solutions L"];
Walther@60543: val spec = ((** )"RatEq"( **)"PolyEq"(**),["univariate", "equation"],["no_met"]);
walther@59842: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];                          (* 0. specify-phase *)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: 
walther@59842: (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: (*+*)case nxt of  Apply_Method ["RatEq", "solve_rat_equation"] => ()
walther@59842: (*+*)| _ => error "55b root specification broken";
walther@59842: 
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                         (* 0. solve-phase*)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60330: 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: 
walther@59868: (*+*)if (Ctree.get_assumptions pt p |> map UnparseC.term) =
walther@59842: (*+*)  ["x \<noteq> 0", 
walther@60330: (*+*)  "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0", 
walther@60242: (*+*)  "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
walther@59842: (*+*)then () else error "assumptions before 1. Subproblem CHANGED";
walther@60330: (*+*)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: (*+*)then
walther@59842: (*+*)  ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
walther@59846: (*+*)  | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
walther@59842: (*+*)else error "1. Subproblem -- call changed";
walther@59842: 
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 1. specify-phase *)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: 
walther@59842: (*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
walther@59842: | _ => error "55b normalise_poly specification broken 1";
walther@59842: 
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                       (* 1. solve-phase *)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@60242: val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
walther@59842: 
walther@60344: if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
walther@59842: then
walther@59842:   ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
walther@59846:   | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
walther@60344: else error "Subproblem ([4, 3], Res) CHANGED";
walther@59842: 
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 2. specify-phase *)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: 
walther@59842: (*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
walther@59842: case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
walther@59842: | _ => error "55b normalise_poly specification broken 2";
walther@59842: 
walther@60242: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x \<up> 2 = 0"*)    (* 2. solve-phase *)
walther@59842: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59842: 
walther@59842: (*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
walther@59842: (*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
walther@59842: (*[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: 
walther@59868: (*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
walther@60242: (*0.pre*)  "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
walther@60344: (*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: (*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: (*2.pre*)  "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x", 
walther@60344: (*2.pre*)  "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
walther@59842: (*0.asm*)  "x \<noteq> 0", 
walther@60344: (*0.asm*)  "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
walther@59842: (*     *)])
walther@59842: (*     *)then () else error "assumptions at end 2. Subproblem CHANGED";
walther@59842: (*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
walther@59842: 
walther@59842: (*/--------- step into 2. Check_Postcond -----------------------------------------------------\*)
walther@59842: "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
walther@59842: 
walther@59842:     val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)
walther@59842:       Step.by_tactic tac (pt, p) (*of*);
walther@59842: "~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
walther@59921:     val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
walther@59842: 	    (*if*) Tactic.for_specify' m (*else*);
walther@59842: 
walther@59842:     val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =
walther@59842: Step_Solve.by_tactic m ptp;
walther@59842: "~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Check_Postcond' _), (ptp as (pt, p))) = (m, ptp);
walther@59842: 
walther@59842:         LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
walther@59843: "~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
walther@59842:   = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
walther@59842:       val parent_pos = par_pblobj pt p
Walther@60559:       val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
walther@59842:       val prog_res =
walther@59842:          case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
walther@59842: (*OLD*)    Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
walther@59843:   |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
walther@59842: (*OLD*)  | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
walther@59842: (*OLD* )   vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
walther@59842: (*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
walther@59842: (*OLD*)    Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
walther@59844: (*OLD*)  | _ => Ctree.get_assumptions pt pos);
walther@59842: (*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
walther@59842: ( *OLD*)
walther@59842:       (*if*) parent_pos = [] (*else*);
walther@59842: (*NEW*)   val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
walther@59842: (*NEW*)     (Pstate i, c) => (i, c)
walther@59842: (*NEW*)   | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
walther@59842: 
walther@59868: (*     *)if eq_set op = (map UnparseC.term (get_assumptions ctxt_parent), [
walther@60344: (*0.pre*)  "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x", 
walther@60344: (*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: (*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: (*0.asm*)  "x \<noteq> 0", 
walther@60344: (*0.asm*)  "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
walther@59842: (*     *)])
walther@59842: (*     *)then () else error "assumptions at xxx CHANGED";
walther@59842: 
walther@59842: 	        val (prog_res', ctxt') =
walther@59842:   ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
walther@59868: (*     *)if eq_set op = (map UnparseC.term (get_assumptions ctxt'), [
walther@60242: (*0.pre*)  "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
walther@60344: (*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: (*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: (*0.asm*)  "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
walther@59842: (*0.asm*)  "x \<noteq> 0",             (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
walther@60344: (*2.pre*)  "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x", 
walther@60344: (*2.pre*)  "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
walther@59842: (*2.res*)  (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)
walther@59842: (*     *)])
walther@59842: (*     *)then () else error "assumptions at xxx CHANGED";
walther@59842: 
walther@59842: "~~~~~ fun subpbl_to_caller , args:"; val (sub_ctxt, prog_res, caller_ctxt)
walther@59842:   = (sub_ctxt, prog_res, ctxt_parent);
walther@59842: val xxxxx = caller_ctxt
walther@59842:   |> get_assumptions 
walther@59842:   |> avoid_contradict prog_res
walther@59842:   |> apsnd (insert_assumptions_cao caller_ctxt)
walther@59842:   |> apsnd (transfer_asms_from_to sub_ctxt);
walther@59842: 
walther@59842:      xxxxx (*return from xxx*);
walther@59842: "~~~~~ from fun subpbl_to_caller \<longrightarrow>fun by_tactic , return:"; val (prog_res', ctxt')
walther@59842:   = (xxxxx);
walther@59843: (*NEW*)   val tac = Tactic.Check_Postcond' (pI, prog_res')
walther@59842: (*NEW*)   val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
walther@59932: (*NEW*)   val ((p, p_), ps, _, pt) = Step.add tac (ist', ctxt') (pt, (parent_pos, Res));
walther@59842: 
walther@59842: (*NEW*)   ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
walther@59842:            (*return from xxx*);
walther@59842: "~~~~~ 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:   = ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))));
walther@59842:   val ("ok", (ts as (_, _, _) :: _, _, _)) =
walther@59842:     (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
walther@59842:   	  val tac = 
walther@59842:         case ts of 
walther@59842:           tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
walther@59842:   		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
walther@59842:                               
walther@59842: "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
walther@59842:   = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), 
walther@59937:   	    tac, Celem.Sundef, pt);
walther@59842: (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
walther@59842: 
walther@59842: (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
walther@59842: (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
walther@59842: 
walther@59842: (*/-------- final test -----------------------------------------------------------------------\*)
walther@60344: if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) = [
walther@60344:   "x = 6 / 5",
walther@60344:   "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:   "\<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:   "x \<noteq> 0",
walther@60344:   "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
walther@60242:   "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
walther@59842: then () else error "test CHANGED";