theory All_Ctxt imports 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) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

*}

section {* start of specify phase *}

text {* variables known from formalisation provide type-inference 

  for further input *}

ML {*

  val ctxt = 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) = me nxt p [] pt;

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

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

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

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

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

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

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

*}

section {* start interpretation of method *}

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

ML {*

  if terms2strs (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) = me nxt p [] pt;

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

  val (p,_,f,nxt,_,pt) = 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 = 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) = me nxt p [] pt;

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

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

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

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

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

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

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

*}

section {* interpretation of subproblem's method *}

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

ML {*

  if terms2strs (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) = me nxt p [] pt; 

*}

ML {*

  "artifically inject assumptions";

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

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

                                 str2term "a < sub_asm_local"] cres;

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

*}

ML {* 

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

val (p,_,f,nxt,_,pt) = 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 (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) = me nxt p [] pt;

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

*}

section {* finish Lucas interpretation *}

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

ML {*

  if terms2strs (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 {*

  show_pt pt;

*}

end