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