Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/rateq.sml
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
equal deleted inserted replaced
37990:24609758d219 37991:028442673981 
    44 "---------(1/x=5) ---------------------";
 
    44 "---------(1/x=5) ---------------------";
 
    45 val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
 
    45 val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
 
    46 (* refine fmz ["univariate","equation"];
 
    46 (* refine fmz ["univariate","equation"];
 
    47    *)
 
    47    *)
 
    48 
    48 
    49 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
 
    49 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 
    50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    51 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    51 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    52    --------------------------------------- Refine_Tacitly*)
 
    52    --------------------------------------- Refine_Tacitly*)
 
    53 (*  nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
 
    53 (*  nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
 
    54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    59 (* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*)
 
    59 (* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)
 
    60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    61 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    61 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    62    --------------------------------------- Refine_Tacitly*)
 
    62    --------------------------------------- Refine_Tacitly*)
 
    63 (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*) 
    63 (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*) 
    64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    71    *)
 
    71    *)
 
    72 
    72 
    73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    74 (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
 
    74 (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
 
    75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    76 (* val nxt = ("Subproblem",  Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
 
    76 (* val nxt = ("Subproblem",  Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 
    77 
    77 
    78 
    78 
    79 
    79 
    80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   102 	   "solveFor x","solutions L"];*)
 
   102 	   "solveFor x","solutions L"];*)
 
   103 
   103 
   104 (* refine fmz ["univariate","equation"];
 
   104 (* refine fmz ["univariate","equation"];
 
   105 *)
 
   105 *)
 
   106 
   106 
   107 val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
 
   107 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 
   108 (*val p = e_pos'; 
   108 (*val p = e_pos'; 
   109 val c = []; 
   109 val c = []; 
   110 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   110 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   111 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   111 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   112 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   112 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   121 (* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
 
   121 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
 
   122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   123 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
 
   123 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
 
   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   130 (* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
 
   130 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
 
   131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   132 (* nxt = ("Model_Problem", Model_Problem
 
   132 (* nxt = ("Model_Problem", Model_Problem
 
   133      ["abcFormula","degree_2","polynomial","univariate","equation"])*)
 
   133      ["abcFormula","degree_2","polynomial","univariate","equation"])*)
 
   134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
wneuper/isa