src/Provers/typedsimp.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 0 a5a9c433f639
child 15574 b1d1b5bfc464
permissions -rw-r--r--
Move towards standard functions.
     1 (*  Title: 	typedsimp
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Functor for constructing simplifiers.  Suitable for Constructive Type
     7 Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try
     8 simp.ML.
     9 *)
    10 
    11 signature TSIMP_DATA =
    12   sig
    13   val refl: thm		(*Reflexive law*)
    14   val sym: thm		(*Symmetric law*)
    15   val trans: thm	(*Transitive law*)
    16   val refl_red: thm	(* reduce(a,a) *)
    17   val trans_red: thm	(* [|a=b; reduce(b,c) |] ==> a=c *)
    18   val red_if_equal: thm (* a=b ==> reduce(a,b) *)
    19   (*Built-in rewrite rules*)
    20   val default_rls: thm list
    21   (*Type checking or similar -- solution of routine conditions*)
    22   val routine_tac: thm list -> int -> tactic
    23   end;
    24 
    25 signature TSIMP =
    26   sig
    27   val asm_res_tac: thm list -> int -> tactic   
    28   val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic
    29   val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic
    30   val norm_tac: (thm list * thm list) -> tactic
    31   val process_rules: thm list -> thm list * thm list
    32   val rewrite_res_tac: int -> tactic   
    33   val split_eqn: thm
    34   val step_tac: (thm list * thm list) -> int -> tactic
    35   val subconv_res_tac: thm list -> int -> tactic   
    36   end;
    37 
    38 
    39 functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 
    40 struct
    41 local open TSimp_data
    42 in
    43 
    44 (*For simplifying both sides of an equation:
    45       [| a=c; b=c |] ==> b=a
    46   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    47 val split_eqn = standard (sym RSN (2,trans) RS sym);
    48 
    49 
    50 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
    51 val red_trans = standard (trans RS red_if_equal);
    52 
    53 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
    54   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    55 fun simp_rule rl = rl RS trans;
    56 
    57 (*For REWRITE rule: Make rule for resimplifying if possible, e.g.
    58   [| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c)  *)
    59 fun resimp_rule rl = rl RS red_trans;
    60 
    61 (*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b)
    62   Make rule for simplifying subterms, e.g.
    63   [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N   *)
    64 fun subconv_rule rl = rl RS trans_red;
    65 
    66 (*If the rule proves an equality then add both forms to simp_rls
    67   else add the rule to other_rls*)
    68 fun add_rule (rl, (simp_rls, other_rls)) =
    69     (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    70     handle THM _ => (simp_rls, rl :: other_rls);
    71 
    72 (*Given the list rls, return the pair (simp_rls, other_rls).*)
    73 fun process_rules rls = Library.foldr add_rule (rls, ([],[]));
    74 
    75 (*Given list of rewrite rules, return list of both forms, reject others*)
    76 fun process_rewrites rls = 
    77   case process_rules rls of
    78       (simp_rls,[])  =>  simp_rls
    79     | (_,others) => raise THM 
    80 	("process_rewrites: Ill-formed rewrite", 0, others);
    81 
    82 (*Process the default rewrite rules*)
    83 val simp_rls = process_rewrites default_rls;
    84 
    85 (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
    86   will fail!  The filter will pass all the rules, and the bound permits
    87   no ambiguity.*)
    88 
    89 (*Resolution with rewrite/sub rules.  Builds the tree for filt_resolve_tac.*)
    90 val rewrite_res_tac = filt_resolve_tac simp_rls 2;
    91 
    92 (*The congruence rules for simplifying subterms.  If subgoal is too flexible
    93     then only refl,refl_red will be used (if even them!). *)
    94 fun subconv_res_tac congr_rls =
    95   filt_resolve_tac (map subconv_rule congr_rls) 2
    96   ORELSE'  filt_resolve_tac [refl,refl_red] 1;
    97 
    98 (*Resolve with asms, whether rewrites or not*)
    99 fun asm_res_tac asms =
   100     let val (xsimp_rls,xother_rls) = process_rules asms
   101     in 	routine_tac xother_rls  ORELSE'  
   102 	filt_resolve_tac xsimp_rls 2
   103     end;
   104 
   105 (*Single step for simple rewriting*)
   106 fun step_tac (congr_rls,asms) =
   107     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   108     subconv_res_tac congr_rls;
   109 
   110 (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
   111 fun cond_step_tac (prove_cond_tac, congr_rls, asms) =
   112     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   113     (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'  
   114     subconv_res_tac congr_rls;
   115 
   116 (*Unconditional normalization tactic*)
   117 fun norm_tac arg = REPEAT_FIRST (step_tac arg)  THEN
   118     TRYALL (resolve_tac [red_if_equal]);
   119 
   120 (*Conditional normalization tactic*)
   121 fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg)  THEN
   122     TRYALL (resolve_tac [red_if_equal]);
   123 
   124 end;
   125 end;
   126 
   127