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