src/Provers/typedsimp.ML
changeset 32960 69916a850301
parent 32957 675c0c7e6a37
child 33339 d41f77196338
equal deleted inserted replaced
32959:23a8c5ac35f8 32960:69916a850301
     1 (*  Title: 	typedsimp
     1 (*  Title:      Provers/typedsimp.ML
     2     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     3     Copyright   1993  University of Cambridge
     4 
     4 
     5 Functor for constructing simplifiers.  Suitable for Constructive Type
     5 Functor for constructing simplifiers.  Suitable for Constructive Type
     6 Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try
     6 Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try
     7 simp.ML.
     7 simp.ML.
     8 *)
     8 *)
     9 
     9 
    10 signature TSIMP_DATA =
    10 signature TSIMP_DATA =
    11   sig
    11   sig
    12   val refl: thm		(*Reflexive law*)
    12   val refl: thm         (*Reflexive law*)
    13   val sym: thm		(*Symmetric law*)
    13   val sym: thm          (*Symmetric law*)
    14   val trans: thm	(*Transitive law*)
    14   val trans: thm        (*Transitive law*)
    15   val refl_red: thm	(* reduce(a,a) *)
    15   val refl_red: thm     (* reduce(a,a) *)
    16   val trans_red: thm	(* [|a=b; reduce(b,c) |] ==> a=c *)
    16   val trans_red: thm    (* [|a=b; reduce(b,c) |] ==> a=c *)
    17   val red_if_equal: thm (* a=b ==> reduce(a,b) *)
    17   val red_if_equal: thm (* a=b ==> reduce(a,b) *)
    18   (*Built-in rewrite rules*)
    18   (*Built-in rewrite rules*)
    19   val default_rls: thm list
    19   val default_rls: thm list
    20   (*Type checking or similar -- solution of routine conditions*)
    20   (*Type checking or similar -- solution of routine conditions*)
    21   val routine_tac: thm list -> int -> tactic
    21   val routine_tac: thm list -> int -> tactic
    74 (*Given list of rewrite rules, return list of both forms, reject others*)
    74 (*Given list of rewrite rules, return list of both forms, reject others*)
    75 fun process_rewrites rls = 
    75 fun process_rewrites rls = 
    76   case process_rules rls of
    76   case process_rules rls of
    77       (simp_rls,[])  =>  simp_rls
    77       (simp_rls,[])  =>  simp_rls
    78     | (_,others) => raise THM 
    78     | (_,others) => raise THM 
    79 	("process_rewrites: Ill-formed rewrite", 0, others);
    79         ("process_rewrites: Ill-formed rewrite", 0, others);
    80 
    80 
    81 (*Process the default rewrite rules*)
    81 (*Process the default rewrite rules*)
    82 val simp_rls = process_rewrites default_rls;
    82 val simp_rls = process_rewrites default_rls;
    83 
    83 
    84 (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
    84 (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
    95   ORELSE'  filt_resolve_tac [refl,refl_red] 1;
    95   ORELSE'  filt_resolve_tac [refl,refl_red] 1;
    96 
    96 
    97 (*Resolve with asms, whether rewrites or not*)
    97 (*Resolve with asms, whether rewrites or not*)
    98 fun asm_res_tac asms =
    98 fun asm_res_tac asms =
    99     let val (xsimp_rls,xother_rls) = process_rules asms
    99     let val (xsimp_rls,xother_rls) = process_rules asms
   100     in 	routine_tac xother_rls  ORELSE'  
   100     in  routine_tac xother_rls  ORELSE'  
   101 	filt_resolve_tac xsimp_rls 2
   101         filt_resolve_tac xsimp_rls 2
   102     end;
   102     end;
   103 
   103 
   104 (*Single step for simple rewriting*)
   104 (*Single step for simple rewriting*)
   105 fun step_tac (congr_rls,asms) =
   105 fun step_tac (congr_rls,asms) =
   106     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   106     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'