src/Provers/typedsimp.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 59498 50b60f501b05
permissions -rw-r--r--
more robust sorted_entries;
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 =
wenzelm@59164
    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*)
wenzelm@58963
    21
  val routine_tac: Proof.context -> thm list -> int -> tactic
wenzelm@59164
    22
end;
clasohm@0
    23
clasohm@0
    24
signature TSIMP =
wenzelm@59164
    25
sig
wenzelm@59164
    26
  val asm_res_tac: Proof.context -> thm list -> int -> tactic
wenzelm@58963
    27
  val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
wenzelm@58963
    28
  val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
wenzelm@58963
    29
  val norm_tac: Proof.context -> (thm list * thm list) -> tactic
clasohm@0
    30
  val process_rules: thm list -> thm list * thm list
wenzelm@59164
    31
  val rewrite_res_tac: Proof.context -> int -> tactic
clasohm@0
    32
  val split_eqn: thm
wenzelm@58963
    33
  val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
wenzelm@59164
    34
  val subconv_res_tac: Proof.context -> thm list -> int -> tactic
wenzelm@59164
    35
end;
clasohm@0
    36
wenzelm@59164
    37
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
clasohm@0
    38
struct
clasohm@0
    39
local open TSimp_data
clasohm@0
    40
in
clasohm@0
    41
clasohm@0
    42
(*For simplifying both sides of an equation:
clasohm@0
    43
      [| a=c; b=c |] ==> b=a
clasohm@0
    44
  Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
wenzelm@45659
    45
val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym);
clasohm@0
    46
clasohm@0
    47
clasohm@0
    48
(*    [| a=b; b=c |] ==> reduce(a,c)  *)
wenzelm@45659
    49
val red_trans = Drule.zero_var_indexes (trans RS red_if_equal);
clasohm@0
    50
clasohm@0
    51
(*For REWRITE rule: Make a reduction rule for simplification, e.g.
clasohm@0
    52
  [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
clasohm@0
    53
fun simp_rule rl = rl RS trans;
clasohm@0
    54
clasohm@0
    55
(*For REWRITE rule: Make rule for resimplifying if possible, e.g.
clasohm@0
    56
  [| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c)  *)
clasohm@0
    57
fun resimp_rule rl = rl RS red_trans;
clasohm@0
    58
clasohm@0
    59
(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b)
clasohm@0
    60
  Make rule for simplifying subterms, e.g.
clasohm@0
    61
  [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N   *)
clasohm@0
    62
fun subconv_rule rl = rl RS trans_red;
clasohm@0
    63
clasohm@0
    64
(*If the rule proves an equality then add both forms to simp_rls
clasohm@0
    65
  else add the rule to other_rls*)
wenzelm@33339
    66
fun add_rule rl (simp_rls, other_rls) =
clasohm@0
    67
    (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
clasohm@0
    68
    handle THM _ => (simp_rls, rl :: other_rls);
clasohm@0
    69
clasohm@0
    70
(*Given the list rls, return the pair (simp_rls, other_rls).*)
wenzelm@33339
    71
fun process_rules rls = fold_rev add_rule rls ([], []);
clasohm@0
    72
clasohm@0
    73
(*Given list of rewrite rules, return list of both forms, reject others*)
wenzelm@59164
    74
fun process_rewrites rls =
clasohm@0
    75
  case process_rules rls of
clasohm@0
    76
      (simp_rls,[])  =>  simp_rls
wenzelm@59164
    77
    | (_,others) => raise THM
wenzelm@32960
    78
        ("process_rewrites: Ill-formed rewrite", 0, others);
clasohm@0
    79
clasohm@0
    80
(*Process the default rewrite rules*)
clasohm@0
    81
val simp_rls = process_rewrites default_rls;
wenzelm@59164
    82
val simp_net = Tactic.build_net simp_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.*)
wenzelm@59164
    89
fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net;
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!). *)
wenzelm@59164
    93
fun subconv_res_tac ctxt congr_rls =
wenzelm@59164
    94
  filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls))
wenzelm@59164
    95
  ORELSE'  filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]);
clasohm@0
    96
clasohm@0
    97
(*Resolve with asms, whether rewrites or not*)
wenzelm@58963
    98
fun asm_res_tac ctxt asms =
wenzelm@59164
    99
    let val (xsimp_rls, xother_rls) = process_rules asms
wenzelm@59164
   100
    in  routine_tac ctxt xother_rls  ORELSE'
wenzelm@59164
   101
        filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls)
clasohm@0
   102
    end;
clasohm@0
   103
clasohm@0
   104
(*Single step for simple rewriting*)
wenzelm@59164
   105
fun step_tac ctxt (congr_rls, asms) =
wenzelm@59164
   106
    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac ctxt  ORELSE'
wenzelm@59164
   107
    subconv_res_tac ctxt congr_rls;
clasohm@0
   108
clasohm@0
   109
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
wenzelm@58963
   110
fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
wenzelm@59164
   111
    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac ctxt  ORELSE'
wenzelm@59498
   112
    (resolve_tac ctxt [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'
wenzelm@59164
   113
    subconv_res_tac ctxt congr_rls;
clasohm@0
   114
clasohm@0
   115
(*Unconditional normalization tactic*)
wenzelm@58963
   116
fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
wenzelm@59498
   117
    TRYALL (resolve_tac ctxt [red_if_equal]);
clasohm@0
   118
clasohm@0
   119
(*Conditional normalization tactic*)
wenzelm@58963
   120
fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg)  THEN
wenzelm@59498
   121
    TRYALL (resolve_tac ctxt [red_if_equal]);
clasohm@0
   122
clasohm@0
   123
end;
clasohm@0
   124
end;
clasohm@0
   125