(* Title:  "ADDTESTS/All_Ctxt.thy"

    Author: Walther Neuper

    (c) due to copyright terms

   this theory is evaluated BEFORE Test_Isac.thy opens structures.

   So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/* *)

 theory All_Ctxt imports Isac.Build_Isac

 begin

 text \<open>all changes of context are demonstrated in a mini example.

   see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 ---\<close>

 section \<open>start of the mini example\<close>

 ML \<open>

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

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

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

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

 \<close> ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];

 \<close>

 section \<open>start of specify phase\<close>

 text \<open>

   variables known from formalisation provide type-inference for further input

 \<close>

 ML \<open>

 (*+*)if ((fst p) |> get_obj g_origin pt |> LibraryC.fst3) <> []

 (*+*)then () else error "check correct of get_ctxt at start of (sub-)problem";

   val ctxt = Ctree.get_ctxt pt p; 

   (*must NOT check ThyC.id_empty in specify_data.spec,      .. is still empty in this case  

     but for References_Def.T in specify_data.origin.        .. is already assigned in this case

                                                                and in case of CAS-cmd          *)

   val SOME known_x = TermC.parseNEW ctxt "x + y + z";

   val SOME unknown = TermC.parseNEW ctxt "a + b + c";

   if type_of known_x = HOLogic.realT andalso 

      type_of unknown = TFree ("'a",["Groups.plus"])

   then () else error "All_Ctx: type constraints beginning specification of root-problem ";

 \<close>

 ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

 \<close>

 section \<open>start interpretation of method\<close>

 text \<open>preconditions are known at start of interpretation of (root-)method\<close>

 ML \<open>

   if UnparseC.terms_to_strings (Ctree.get_assumptions pt p) = ["precond_rootmet x"]

   then () else error "All_Ctx: asms after start interpretation of root-method";

 \<close>

 ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

 \<close>

 section \<open>start a subproblem: specification\<close>

 text \<open>

   ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args"

   and extended with the types of the variables in args.\<close>

 ML \<open>(*not significant in this example*)

   val ctxt = Ctree.get_ctxt pt p;

   val SOME known_x = TermC.parseNEW ctxt "x+y+z";

   val SOME unknown = TermC.parseNEW ctxt "a+b+c";

   if type_of known_x = HOLogic.realT andalso 

      type_of unknown = TFree ("'a",["Groups.plus"])

   then () else error "All_Ctx: type constraints beginning specification of SubProblem ";

 \<close>

 ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt; 

 \<close>

 section \<open>interpretation of subproblem's method\<close>

 text \<open>preconds are known at start of interpretation of (sub-)method\<close>

 ML \<open>

 \<close> ML \<open>

 UnparseC.terms_to_strings (Ctree.get_assumptions pt p);

 (*"precond_rootmet (x::real)" -- fix in Model_Pattern? *)

 \<close> ML \<open>

 \<close>

 ML \<open>

   if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

     ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"])

   then () else error "All_Ctx: asms after start interpretation of SubProblem";

 \<close>

 ML \<open>

  val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt; 

 \<close>

 ML \<open>

   "artifically inject assumptions";

   val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);

   val ctxt = ContextC.insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",

                                  TermC.parse_test @{context} "a < sub_asm_local"] cres;

   val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));

 \<close>

 ML \<open>

 val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

 val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

 \<close>

 section \<open>finish subproblem, return to calling method\<close>

 text \<open>transfer non-local assumptions and result from sub-method to root-method.

   non-local assumptions are those contaning a variable known in root-method.

 \<close>

 ML \<open>

 eq_set

 \<close>

 ML \<open>

   if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

     ["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])

   then () else error "All_Ctx: asms after finishing SubProblem";

 \<close>

 ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

   val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt;

 \<close>

 section \<open>finish Lucas interpretation\<close>

 text \<open>assumptions collected during lucas-interpretation for proof of postcondition\<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 ML \<open>

   if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

     ["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])

   then () else error "All_Ctx at final result";

 \<close>

 ML \<open>

   Test_Tool.show_pt pt;

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 end