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/xmlsrc/datatypes.sml
changeset 59253 f0bb15a046ae
parent 59252 7d3dbc1171ff
child 59348 ddfabb53082c
equal deleted inserted replaced
59252:7d3dbc1171ff 59253:f0bb15a046ae 
   111 import isac.util.tactics.StringListTactic    ...not appropriately abstracted
 
   111 import isac.util.tactics.StringListTactic    ...not appropriately abstracted
 
   112 import isac.util.tactics.SubProblemTactic
 
   112 import isac.util.tactics.SubProblemTactic
 
   113 import isac.util.tactics.Tactic
 
   113 import isac.util.tactics.Tactic
 
   114 *)
 
   114 *)
 
   115 Rewrite: thm'' -> tac;
 
   115 Rewrite: thm'' -> tac;
 
   116 val tac = Rewrite("refl", str2term "a = a");
 
   116 val tac = Rewrite("refl", @{thm refl});
 
   117 if xmlstr 0 (xml_of_tac tac) =
 
   117 if xmlstr 0 (xml_of_tac tac) =
 
   118 (*---xml_of_tac------------------------------------------thm'_to_thm''--------------
 
   118 (*---xml_of_tac------------------------------------------thm'_to_thm''--------------
 
   119 "(REWRITETACTIC name=Rewrite)\n" ^ 
   119 "(REWRITETACTIC name=Rewrite)\n" ^ 
   120 ". (THEOREM)\n" ^ 
   120 ". (THEOREM)\n" ^ 
   121 ". . (ID)\n" ^ 
   121 ". . (ID)\n" ^ 
   124 ". . (FORMULA)\n" ^ 
   124 ". . (FORMULA)\n" ^ 
   125 ". . . (ISA)\n" ^ 
   125 ". . . (ISA)\n" ^ 
   126 ". . . . a = a\n" ^ 
   126 ". . . . a = a\n" ^ 
   127 ". . . (/ISA)\n" ^ 
   127 ". . . (/ISA)\n" ^ 
   128 ". . . (TERM)\n" ^ 
   128 ". . . (TERM)\n" ^ 
   129 ". . . . a = a\n" ^ 
   129 ". . . . ?t = ?t\n" ^ 
   130 ". . . (/TERM)\n" ^ 
   130 ". . . (/TERM)\n" ^ 
   131 ". . (/FORMULA)\n" ^ 
   131 ". . (/FORMULA)\n" ^ 
   132 ". (/THEOREM)\n" ^ 
   132 ". (/THEOREM)\n" ^ 
   133 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)
 
   133 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)
 
   134 "(REWRITETACTIC name=Rewrite)\n" ^ 
   134 "(REWRITETACTIC name=Rewrite)\n" ^ 
   135 ". (THEOREM)\n" ^ 
   135 ". (THEOREM)\n" ^ 
   136 ". . (ID)\n" ^ 
   136 ". . (ID)\n" ^ 
   137 ". . . refl\n" ^ 
   137 ". . . refl\n" ^ 
   138 ". . (/ID)\n" ^ 
   138 ". . (/ID)\n" ^ 
   139 ". . (FORMULA)\n" ^ 
   139 ". . (FORMULA)\n" ^ 
   140 ". . . a = a\n" ^ 
   140 ". . . ?t = ?t\n" ^ 
   141 ". . (/FORMULA)\n" ^ 
   141 ". . (/FORMULA)\n" ^ 
   142 ". (/THEOREM)\n" ^ 
   142 ". (/THEOREM)\n" ^ 
   143 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
 
   143 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
 
   144 
   144 
   145 Rewrite_Inst: subs * thm'' -> tac;
 
   145 Rewrite_Inst: subs * thm'' -> tac;
 
   146 val tac = Rewrite_Inst(["(bdv, x)"], ("refl", str2term "a = a"));
 
   146 val tac = Rewrite_Inst(["(bdv, x)"], ("refl", @{thm refl}));
 
   147 if xmlstr 0 (xml_of_tac tac) = 
   147 if xmlstr 0 (xml_of_tac tac) = 
   148 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^ 
   148 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^ 
   149 ". (SUBSTITUTION)\n" ^ 
   149 ". (SUBSTITUTION)\n" ^ 
   150 ". . (PAIR)\n" ^ 
   150 ". . (PAIR)\n" ^ 
   151 ". . . (VARIABLE)\n" ^ 
   151 ". . . (VARIABLE)\n" ^ 
   172 ". . (FORMULA)\n" ^  (* OK *)
 
   172 ". . (FORMULA)\n" ^  (* OK *)
 
   173 ". . . (ISA)\n" ^ 
   173 ". . . (ISA)\n" ^ 
   174 ". . . . a = a\n" ^ 
   174 ". . . . a = a\n" ^ 
   175 ". . . (/ISA)\n" ^ 
   175 ". . . (/ISA)\n" ^ 
   176 ". . . (TERM)\n" ^ 
   176 ". . . (TERM)\n" ^ 
   177 ". . . . a = a\n" ^ 
   177 ". . . ?t = ?t\n" ^ 
   178 ". . . (/TERM)\n" ^ 
   178 ". . . (/TERM)\n" ^ 
   179 ". . (/FORMULA)\n" ^ 
   179 ". . (/FORMULA)\n" ^ 
   180 ". (/THEOREM)\n" ^ 
   180 ". (/THEOREM)\n" ^ 
   181 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)
 
   181 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)
 
   182 ". (THEOREM)\n" ^ 
   182 ". (THEOREM)\n" ^ 
   183 ". . (ID)\n" ^ 
   183 ". . (ID)\n" ^ 
   184 ". . . refl\n" ^ 
   184 ". . . refl\n" ^ 
   185 ". . (/ID)\n" ^ 
   185 ". . (/ID)\n" ^ 
   186 ". . (FORMULA)\n" ^ 
   186 ". . (FORMULA)\n" ^ 
   187 ". . . a = a\n" ^ 
   187 ". . . ?t = ?t\n" ^ 
   188 ". . (/FORMULA)\n" ^ 
   188 ". . (/FORMULA)\n" ^ 
   189 ". (/THEOREM)\n" ^ 
   189 ". (/THEOREM)\n" ^ 
   190 "(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
 
   190 "(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
 
   191 
   191 
   192 Rewrite_Set: rls' -> tac;
 
   192 Rewrite_Set: rls' -> tac;
 
   320         <ISA>yyy</ISA>
 
   320         <ISA>yyy</ISA>
 
   321       </MATHML>
 
   321       </MATHML>
 
   322     </VALUE>
 
   322     </VALUE>
 
   323   </PAIR>
 
   323   </PAIR>
 
   324 </SUBSTITUTION>:*)
 
   324 </SUBSTITUTION>:*)
 
   325 val tac = Rewrite_Inst (subs, ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"));
 
   325 val tac = Rewrite_Inst (subs, ("diff_sin_chain", @{thm diff_sin_chain}));
 
   326 val xml = xml_of_tac tac;
 
   326 val xml = xml_of_tac tac;
 
   327 
   327 
   328 if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
 
   328 if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
 
   329 then () else error "xml_of_tac Rewrite_Inst CHANGED";
 
   329 then () else error "xml_of_tac Rewrite_Inst CHANGED";
 
   330 
   330 
   331 val Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;
 
   331 val Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;
 
   332 if term2str term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
 
   332 if (term2str o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
 
   333 then () else error "xml_to_tac Rewrite_Inst CHANGED";
 
   333 then () else error "xml_to_tac Rewrite_Inst CHANGED";
 
   334 
   334 
   335 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
 
   335 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
 
   336 e_sube: cterm' list;
 
   336 e_sube: cterm' list;
 
   337 e_sube: sube;
 
   337 e_sube: sube;
 
   365 val tac = Substitute sube;
 
   365 val tac = Substitute sube;
 
   366 val xml = xml_of_tac tac;
 
   366 val xml = xml_of_tac tac;
 
   367 
   367 
   368 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"
 
   368 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"
 
   369 then () else error "xml_of_tac Substitute CHANGED";
 
   369 then () else error "xml_of_tac Substitute CHANGED";
 
   370 if xml_to_tac xml = Substitute ["bdv_1 = xxx", "bdv_2 = yyy"]
 
   370 case xml_to_tac xml of Substitute ["bdv_1 = xxx", "bdv_2 = yyy"] => ()
 
   371 then () else error "xml_to_tac Substitute CHANGED";
 
   371 | _ => error "xml_to_tac Substitute CHANGED";
wneuper/isa