tfl/src/RW.sml

803 datatype solver  = Solver of simpls -> thm list -> term -> thm;
813 fun Rewrite Once (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
816  | Rewrite Fully (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
819  | Rewrite(Special f)(Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
822  | Rewrite Once (Default thl,Context cntxt,Congs congs,Solver solver) =
826  | Rewrite Once (Pure thl,Context cntxt,Congs congs,Solver solver) =
829  | Rewrite Fully (Default thl,Context cntxt,Congs congs,Solver solver) =
833  | Rewrite Fully (Pure thl,Context cntxt,Congs congs,Solver solver) =
836  | Rewrite (Special f) (Default thl,Context cntxt,Congs congs,Solver solver) =
839  | Rewrite (Special f) (Pure thl,Context cntxt,Congs congs,Solver solver) =
889              then Lib.say("Solver: trying to lookup in context\n"
892                       Lib.say "Solver: couldn't find it.\n"
905     if !monitoring > 0 then Lib.say "Solver: found it.\n" else ();
918              then Lib.say("Solver: attempting to prove (by rewriting)\n  "
926                      then Lib.say("Solver: proved\n"^thm_to_string th^"\n\n")
927                      else Lib.say("Solver: unable to prove.\n\n")
954                                   Congs[],Solver rw_solver)
957                                  Congs[],Solver std_solver)
960                                       Congs[],Solver std_solver)
963                                 Congs[],Solver std_solver)
966                                           Congs[],Solver std_solver);
972                                        Congs[],Solver rw_solver);
974                                       Congs[],Solver std_solver);
976                                           Congs[], Solver std_solver);
978                                            Congs[],Solver std_solver);
980                                                Congs[],Solver std_solver);
986 ASM_REWRITE_RULE Fully (Default thl,Context([],ADD),Congs[],Solver rw_solver);
989 ASM_REWRITE_RULE Fully (Default thl,Context([],ADD),Congs[],Solver std_solver);
992 ASM_REWRITE_RULE Once (Default thl,Context([],ADD),Congs[],Solver std_solver);
996                         Congs[],Solver std_solver);
1000                        Congs[],Solver std_solver);
1006 REWRITE_TAC Fully (Default thl,Context([],ADD),Congs[],Solver rw_solver);
1009 REWRITE_TAC Fully (Default thl,Context([],ADD),Congs[],Solver std_solver);
1012 REWRITE_TAC Once(Default thl,Context([],ADD),Congs[],Solver std_solver);
1015 REWRITE_TAC Fully (Pure thl,Context([],DONT_ADD),Congs[],Solver std_solver);
1018 REWRITE_TAC Once (Pure thl,Context([],DONT_ADD), Congs[],Solver std_solver);
1024 ASM_REWRITE_TAC Fully (Default thl,Context([],ADD),Congs[],Solver rw_solver);
1027 ASM_REWRITE_TAC Fully (Default thl,Context([],ADD),Congs[],Solver std_solver);
1031                       Congs[],Solver std_solver);
1035                        Congs[],Solver std_solver);
1038 ASM_REWRITE_TAC Once (Pure thl,Context([],DONT_ADD),Congs[],Solver std_solver);
1043                                      Congs[],Solver std_solver)