(* this theory is evaluated BEFORE Test_Isac.thy opens structures.

  So, if you encounter errors here, first fix them in ~~/test/Tools/isac/Minimsubpbl/* *)

theory All_Ctxt imports "~~/src/Tools/isac/Knowledge/Isac"

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 = 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 ";

*}

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 Rule.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 = 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 ";

*}

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 {*

*} ML {*

p = ([1], Res)

*} ML {*

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

*} ML {*

*}

ML {*

  if Rule.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 = Stool.insert_assumptions [TermC.str2term "x < sub_asm_out",

                                 TermC.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 {*

*} ML {*

Rule.terms2strs (Ctree.get_assumptions_ pt p)

*}

ML {*

  if Rule.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 {*

*} ML {*

Rule.terms2strs (Ctree.get_assumptions_ pt p)

*}

ML {*

  if Rule.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;

*}

ML {*

*} ML {*

*}

end