(* this is evaluated BEFORE Test_Isac.thu opens structures*)

 theory All_Ctxt imports 

   "~~/src/Tools/isac/Knowledge/Isac"

 (*Isac ...ERROR Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/Isac.thy") 

   from Isac.thy ...*)

 begin

 text {* all changes of context are demonstrated in a mini example.

   see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 --- *}

 section {* start of the mini example *}

 ML {*

   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"]);

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

 *}

 section {* start of specify phase *}

 text {* variables known from formalisation provide type-inference 

   for further input *}

 ML {*

   val ctxt = Ctree.get_ctxt pt p;

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

   val SOME unknown = 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 ";

 *}

 ML {*

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

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

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

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

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

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

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

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

 *}

 section {* start interpretation of method *}

 text {* preconditions are known at start of interpretation of (root-)method *}

 ML {*

   if terms2strs (Ctree.get_assumptions_ pt p) = ["precond_rootmet x"]

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

 *}

 ML {*

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

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

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

 *}

 section {* start a subproblem: specification *}

 text {* 

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

   and extended with the types of the variables in args. *}

 ML {* (*not significant in this example*)

   val ctxt = Ctree.get_ctxt pt p;

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

   val SOME unknown = 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 ";

 *}

 ML {*

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

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

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

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

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

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

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

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

 *}

 section {* interpretation of subproblem's method *}

 text {* preconds are known at start of interpretation of (sub-)method *}

 ML {*

   if terms2strs (Ctree.get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)"]

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

 *}

 ML {*

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

 *}

 ML {*

   "artifically inject assumptions";

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

   val ctxt = insert_assumptions [str2term "x < sub_asm_out",

                                  str2term "a < sub_asm_local"] cres;

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

 *}

 ML {* 

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

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

 *}

 section {* finish subproblem, return to calling method*}

 text {* transfer non-local assumptions and result from sub-method to root-method.

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

 *}

 ML {*

   if terms2strs (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";

 *}

 ML {*

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

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

 *}

 section {* finish Lucas interpretation *}

 text {* assumptions collected during lucas-interpretation for proof of postcondition *}

 ML {*

   if terms2strs (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";

 *}

 ML {*

   Chead.show_pt pt;

 *}

 end