Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml
author wneuper <Walther.Neuper@jku.at>
Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789 8fa678b678e8
parent 60725 25233d8f7019
permissions -rw-r--r--
Doc/Specify_Phase 4: start use antiquotations from isar-ref 
     1 (* Title:  "Minisubpbl/790-complete-NEXT_STEP.sml"

     2    Author: Walther Neuper 1105

     3    (c) copyright due to lincense terms.

     4 *)

     5 

     6 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     7 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     8 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     9 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

    10 val (dI',pI',mI') =

    11   ("Test", ["sqroot-test", "univariate", "equation", "test"],

    12    ["Test", "squ-equ-test-subpbl1"]);

    13 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

    14 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac;

    15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac;

    16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac;

    17 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;

    18 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;

    19 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac;

    20 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "Test_simplify" = tac;

    21 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = tac;

    22 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac;

    23 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac;

    24 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["LINEAR", "univariate", "equation", "test"] = tac;

    25 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["Test", "solve_linear"] = tac;

    26 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["Test", "solve_linear"] = tac;

    27 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;

    28 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "Test_simplify" = tac;

    29 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_Postcond ["LINEAR", "univariate", "equation", "test"] = tac;

    30 

    31 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

    32 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)

    33 (* there are questionable assumptions either --------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)

    34 

    35 (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_elementwise "Assumptions" = tac;

    36 

    37 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

    38 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"precond_rootmet 1\"]";(*REP*)

    39 

    40 (*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Check_Postcond ["sqroot-test", "univariate", "equation", "test"] = tac;

    41 

    42 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[]";(*isa*)

    43 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms @{context}) = "[\"precond_rootmet 1\"]";(*REP*)

    44 

    45 (*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)

    46 

    47 (*/--------------------- final test ----------------------------------\\*)

    48 val (res, asm) = (get_obj g_result pt (fst p));

    49 

    50 if UnparseC.term @{context} res = "[x = 1]" andalso

    51   map (UnparseC.term @{context}) asm = []    (* assumptions have gone to the ctxt *)

    52 then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_step CHANGED";

    53 

    54 if p = ([], Und)

    55 then

    56   case get_obj g_tac pt (fst p) of

    57     Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()

    58   | _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"

    59 else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1";

    60 

    61 Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
wneuper/isa