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