Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ADDTESTS/All_Ctxt.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 22 Aug 2019 11:26:14 +0200
changeset 59582 23984b62804f
parent 59577 60d191402598
child 59592 99c8d2ff63eb
permissions -rw-r--r--
lucin: clarify initialisation of ctxt by ContextC.initialise, initialise'

notes:
* this required more type constraints in formalisations
* this required partially replacing thy --> ctxt
* additional extensions of certain tests for future devel.
* additional code polishing makes CS longer than necessary 
     1 (* Title:  "ADDTESTS/All_Ctxt.thy"

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 

     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/* *)

     7 

     8 theory All_Ctxt imports Isac.Isac

     9 begin

    10 

    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>

    13 

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

    15 

    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   val (p,_,f,nxt,_,pt) = Math_Engine.CalcTreeTEST [(fmz, (dI',pI',mI'))];

    22 \<close>

    23 

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

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

    26   for further input\<close>

    27 

    28 ML \<open>

    29   val ctxt = Ctree.get_ctxt pt p;

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

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

    32   if type_of known_x = HOLogic.realT andalso 

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

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

    35 \<close>

    36 

    37 ML \<open>

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

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

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

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

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

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

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

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

    46 \<close>

    47 

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

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

    50 

    51 ML \<open>

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

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

    54 \<close>

    55 

    56 ML \<open>

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

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

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

    60 \<close>

    61 

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

    63 text \<open>

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

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

    66 

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

    68   val ctxt = Ctree.get_ctxt pt p;

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

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

    71   if type_of known_x = HOLogic.realT andalso 

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

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

    74 \<close>

    75 

    76 ML \<open>

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

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

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

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

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

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

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

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

    85 \<close>

    86 

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

    88 

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

    90 

    91 ML \<open>

    92 \<close> ML \<open>

    93 p = ([1], Res)

    94 \<close> ML \<open>

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

    96 \<close> ML \<open>

    97 \<close>

    98 

    99 ML \<open>

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

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

   102 \<close>

   103 

   104 ML \<open>

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

   106 \<close>

   107 

   108 ML \<open>

   109   "artifically inject assumptions";

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

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

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

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

   114 \<close>

   115 

   116 ML \<open>

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

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

   119 \<close>

   120 

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

   122 

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

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

   125 \<close>

   126 

   127 ML \<open>

   128 Rule.terms2strs (Ctree.get_assumptions_ pt p)

   129 \<close>

   130 

   131 ML \<open>

   132 \<close> ML \<open>

   133   if Rule.terms2strs (Ctree.get_assumptions_ pt p) = 

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

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

   136 \<close>

   137 

   138 ML \<open>

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

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

   141 \<close>

   142 

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

   144 

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

   146 

   147 ML \<open>

   148 \<close> ML \<open>

   149 Rule.terms2strs (Ctree.get_assumptions_ pt p)

   150 \<close>

   151 

   152 ML \<open>

   153 \<close> ML \<open>

   154   if Rule.terms2strs (Ctree.get_assumptions_ pt p) = 

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

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

   157 \<close>

   158 

   159 ML \<open>

   160   Chead.show_pt pt;

   161 \<close>

   162 

   163 ML \<open>

   164 \<close> ML \<open>

   165 \<close>

   166 

   167 end
wneuper/isa