wneuper/isa: test/Tools/isac/ADDTESTS/All

     1 (* Title:  "ADDTESTS/All_Ctxt.thy"

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     5   this theory is evaluated BEFORE Test_Isac.thy opens structures.

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

     8 theory All_Ctxt imports Isac.Build_Isac

     9 begin

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

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

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

    16 ML \<open>

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

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

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

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

    21 \<close> ML \<open>

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

    23 \<close>

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

    26 text \<open>variables known from formalisation provide type-inference

    27   for further input\<close>

    29 ML \<open>

    30   val ctxt = Ctree.get_ctxt pt p;

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

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

    33   if type_of known_x = HOLogic.realT andalso

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

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

    36 \<close>

    38 ML \<open>

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

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

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

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

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

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

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

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

    47 \<close>

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

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

    52 ML \<open>

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

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

    55 \<close>

    57 ML \<open>

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

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

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

    61 \<close>

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

    64 text \<open>

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

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

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

    69   val ctxt = Ctree.get_ctxt pt p;

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

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

    72   if type_of known_x = HOLogic.realT andalso

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

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

    75 \<close>

    77 ML \<open>

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

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

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

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

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

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

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

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

    86 \<close>

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

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

    92 ML \<open>

    93 \<close> ML \<open>

    94 \<close>

    96 ML \<open>

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

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

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

   100 \<close>

   102 ML \<open>

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

   104 \<close>

   106 ML \<open>

   107   "artifically inject assumptions";

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

   109   val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out",

   110                                  TermC.str2term "a < sub_asm_local"] cres;

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

   112 \<close>

   114 ML \<open>

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

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

   117 \<close>

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

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

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

   123 \<close>

   125 ML \<open>

   126 eq_set

   127 \<close>

   129 ML \<open>

   130 \<close> ML \<open>

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

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

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

   134 \<close>

   136 ML \<open>

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

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

   139 \<close>

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

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

   145 ML \<open>

   146 \<close> ML \<open>

   147 \<close>

   149 ML \<open>

   150 \<close> ML \<open>

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

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

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

   154 \<close>

   156 ML \<open>

   157   Chead.show_pt pt;

   158 \<close>

   160 ML \<open>

   161 \<close> ML \<open>

   162 \<close>

   164 end

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 10 Apr 2020 18:32:36 +0200
changeset 59868	d77aa0992e0f
parent 59861	65ec9f679c3f
child 59977	e635534c5f63
permissions	-rw-r--r--