src/HOL/Library/rewrite.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63285 e9c777bfd78c
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     1
(*  Title:      HOL/Library/rewrite.ML
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
     3
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     4
This is a rewrite method that supports subterm-selection based on patterns.
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
     5
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     6
The patterns accepted by rewrite are of the following form:
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     7
  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     8
  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
     9
  <args>    ::= [<pattern>] ("to" <term>) <thms>
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    10
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    11
This syntax was clearly inspired by Gonthier's and Tassi's language of
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    12
patterns but has diverged significantly during its development.
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    13
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    14
We also allow introduction of identifiers for bound variables,
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    15
which can then be used to match arbitrary subterms inside abstractions.
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    16
*)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    17
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    18
infix 1 then_pconv;
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    19
infix 0 else_pconv;
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    20
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    21
signature REWRITE =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    22
sig
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    23
  type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    24
  val then_pconv: patconv * patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    25
  val else_pconv: patconv * patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    26
  val abs_pconv:  patconv -> string option * typ -> patconv (*XXX*)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    27
  val fun_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    28
  val arg_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    29
  val imp_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    30
  val params_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    31
  val forall_pconv: patconv -> string option * typ option -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    32
  val all_pconv: patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    33
  val for_pconv: patconv -> (string option * typ option) list -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    34
  val concl_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    35
  val asm_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    36
  val asms_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    37
  val judgment_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    38
  val in_pconv: patconv -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    39
  val match_pconv: patconv -> term * (string option * typ) list -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    40
  val rewrs_pconv: term option -> thm list -> patconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    41
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    42
  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    43
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    44
  val mk_hole: int -> typ -> term
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    45
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    46
  val rewrite_conv: Proof.context
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    47
    -> (term * (string * typ) list, string * typ option) pattern list * term option
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    48
    -> thm list
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    49
    -> conv
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    50
end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    51
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    52
structure Rewrite : REWRITE =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    53
struct
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    54
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    55
datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    56
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    57
exception NO_TO_MATCH
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    58
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    59
val holeN = Name.internal "_hole"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    60
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    61
fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    62
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    63
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    64
(* holes *)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    65
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    66
fun mk_hole i T = Var ((holeN, i), T)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    67
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    68
fun is_hole (Var ((name, _), _)) = (name = holeN)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    69
  | is_hole _ = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    70
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    71
fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    72
  | is_hole_const _ = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    73
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    74
val hole_syntax =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    75
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    76
    (* Modified variant of Term.replace_hole *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    77
    fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i =
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    78
          (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    79
      | replace_hole Ts (Abs (x, T, t)) i =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    80
          let val (t', i') = replace_hole (T :: Ts) t i
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    81
          in (Abs (x, T, t'), i') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    82
      | replace_hole Ts (t $ u) i =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    83
          let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    84
            val (t', i') = replace_hole Ts t i
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    85
            val (u', i'') = replace_hole Ts u i'
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    86
          in (t' $ u', i'') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    87
      | replace_hole _ a i = (a, i)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    88
    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    89
  in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    90
    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    91
    #> Proof_Context.set_mode Proof_Context.mode_pattern
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    92
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    93
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    94
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    95
(* pattern conversions *)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    96
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    97
type patconv = Proof.context -> Type.tyenv * (string * term) list -> cterm -> thm
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    98
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
    99
fun (cv1 then_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv then_conv cv2 ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   100
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   101
fun (cv1 else_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv else_conv cv2 ctxt tytenv) ct
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   102
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   103
fun raw_abs_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   104
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   105
    Abs _ => CConv.abs_cconv (fn (x, ctxt') => cv x ctxt' tytenv) ctxt ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   106
  | t => raise TERM ("raw_abs_pconv", [t])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   107
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   108
fun raw_fun_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   109
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   110
    _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   111
  | t => raise TERM ("raw_fun_pconv", [t])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   112
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   113
fun raw_arg_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   114
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   115
    _ $ _ => CConv.arg_cconv (cv ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   116
  | t => raise TERM ("raw_arg_pconv", [t])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   117
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   118
fun abs_pconv cv (s,T) ctxt (tyenv, ts) ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   119
  let val u = Thm.term_of ct
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   120
  in
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   121
    case try (fastype_of #> dest_funT) u of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   122
      NONE => raise TERM ("abs_pconv: no function type", [u])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   123
    | SOME (U, _) =>
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   124
        let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   125
          val tyenv' =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   126
            if T = dummyT then tyenv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   127
            else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   128
          val eta_expand_cconv =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   129
            case u of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   130
              Abs _=> Thm.reflexive
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   131
            | _ => CConv.rewr_cconv @{thm eta_expand}
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   132
          fun add_ident NONE _ l = l
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   133
            | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   134
          val abs_cv = CConv.abs_cconv (fn (ct, ctxt) => cv ctxt (tyenv', add_ident s ct ts)) ctxt
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   135
        in (eta_expand_cconv then_conv abs_cv) ct end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   136
        handle Pattern.MATCH => raise TYPE ("abs_pconv: types don't match", [T,U], [u])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   137
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   138
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   139
fun fun_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   140
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   141
    _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   142
  | Abs (_, T, _ $ Bound 0) => abs_pconv (fun_pconv cv) (NONE, T) ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   143
  | t => raise TERM ("fun_pconv", [t])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   144
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   145
local
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   146
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   147
fun arg_pconv_gen cv0 cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   148
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   149
    _ $ _ => cv0 (cv ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   150
  | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   151
  | t => raise TERM ("arg_pconv_gen", [t])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   152
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   153
in
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   154
60122
eb08fefd5c05 make SML/NJ happy;
wenzelm
parents: 60117
diff changeset
   155
fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt
eb08fefd5c05 make SML/NJ happy;
wenzelm
parents: 60117
diff changeset
   156
fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   157
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   158
end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   159
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   160
(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   161
fun params_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   162
  let val pconv =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   163
    case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   164
      Const (@{const_name "Pure.all"}, _) $ Abs _ => (raw_arg_pconv o raw_abs_pconv) (fn _ => params_pconv cv)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   165
    | Const (@{const_name "Pure.all"}, _) => raw_arg_pconv (params_pconv cv)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   166
    | _ => cv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   167
  in pconv ctxt tytenv ct end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   168
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   169
fun forall_pconv cv ident ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   170
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   171
    Const (@{const_name "Pure.all"}, T) $ _ =>
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   172
      let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   173
        val def_U = T |> dest_funT |> fst |> dest_funT |> fst
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   174
        val ident' = apsnd (the_default (def_U)) ident
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   175
      in arg_pconv (abs_pconv cv ident') ctxt tytenv ct end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   176
  | t => raise TERM ("forall_pconv", [t])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   177
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   178
fun all_pconv _ _ = Thm.reflexive
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   179
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   180
fun for_pconv cv idents ctxt tytenv ct =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   181
  let
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   182
    fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   183
        let val (rev_idents', cv') = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   184
        in
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   185
          case rev_idents' of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   186
            [] => ([], forall_pconv cv' (NONE, NONE))
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   187
          | (x :: xs) => (xs, forall_pconv cv' x)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   188
        end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   189
      | f rev_idents _ = (rev_idents, cv)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   190
  in
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   191
    case f (rev idents) (Thm.term_of ct) of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   192
      ([], cv') => cv' ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   193
    | _ => raise CTERM ("for_pconv", [ct])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   194
  end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   195
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   196
fun concl_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   197
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   198
    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => imp_pconv (concl_pconv cv) ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   199
  | _ => cv ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   200
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   201
fun asm_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   202
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   203
    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => CConv.with_prems_cconv ~1 (cv ctxt tytenv) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   204
  | t => raise TERM ("asm_pconv", [t])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   205
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   206
fun asms_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   207
  case Thm.term_of ct of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   208
    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   209
      ((CConv.with_prems_cconv ~1 oo cv) else_pconv imp_pconv (asms_pconv cv)) ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   210
  | t => raise TERM ("asms_pconv", [t])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   211
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   212
fun judgment_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   213
  if Object_Logic.is_judgment ctxt (Thm.term_of ct)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   214
  then arg_pconv cv ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   215
  else cv ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   216
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   217
fun in_pconv cv ctxt tytenv ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   218
  (cv else_pconv 
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   219
   raw_fun_pconv (in_pconv cv) else_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   220
   raw_arg_pconv (in_pconv cv) else_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   221
   raw_abs_pconv (fn _  => in_pconv cv))
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   222
  ctxt tytenv ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   223
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   224
fun replace_idents idents t =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   225
  let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   226
    fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   227
      | subst _ t = t
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   228
  in Term.map_aterms (subst idents) t end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   229
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   230
fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   231
  let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   232
    val t' = replace_idents env_ts t
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   233
    val thy = Proof_Context.theory_of ctxt
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   234
    val u = Thm.term_of ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   235
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   236
    fun descend_hole fixes (Abs (_, _, t)) =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   237
        (case descend_hole fixes t of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   238
          NONE => NONE
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   239
        | SOME (fix :: fixes', pos) => SOME (fixes', abs_pconv pos fix)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   240
        | SOME ([], _) => raise Match (* less fixes than abstractions on path to hole *))
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   241
      | descend_hole fixes (t as l $ r) =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   242
        let val (f, _) = strip_comb t
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   243
        in
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   244
          if is_hole f
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   245
          then SOME (fixes, cv)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   246
          else
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   247
            (case descend_hole fixes l of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   248
              SOME (fixes', pos) => SOME (fixes', fun_pconv pos)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   249
            | NONE =>
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   250
              (case descend_hole fixes r of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   251
                SOME (fixes', pos) => SOME (fixes', arg_pconv pos)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   252
              | NONE => NONE))
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   253
        end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   254
      | descend_hole fixes t =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   255
        if is_hole t then SOME (fixes, cv) else NONE
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   256
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   257
    val to_hole = descend_hole (rev fixes) #> the_default ([], cv) #> snd
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   258
  in
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   259
    case try (Pattern.match thy (apply2 Logic.mk_term (t',u))) (tyenv, Vartab.empty) of
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   260
      NONE => raise TERM ("match_pconv: Does not match pattern", [t, t',u])
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   261
    | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   262
  end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   263
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   264
fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   265
  let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   266
    fun instantiate_normalize_env ctxt env thm =
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   267
      let
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   268
        val prop = Thm.prop_of thm
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   269
        val norm_type = Envir.norm_type o Envir.type_env
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   270
        val insts = Term.add_vars prop []
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60122
diff changeset
   271
          |> map (fn x as (s, T) =>
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60122
diff changeset
   272
              ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   273
        val tyinsts = Term.add_tvars prop []
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60122
diff changeset
   274
          |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   275
      in Drule.instantiate_normalize (tyinsts, insts) thm end
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   276
    
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   277
    fun unify_with_rhs context to env thm =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   278
      let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   279
        val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   280
        val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   281
          handle Pattern.Unif => raise NO_TO_MATCH
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   282
      in env' end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   283
    
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   284
    fun inst_thm_to _ (NONE, _) thm = thm
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   285
      | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   286
          instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   287
    
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   288
    fun inst_thm ctxt idents (to, tyenv) thm =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   289
      let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   290
        (* Replace any identifiers with their corresponding bound variables. *)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   291
        val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   292
        val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   293
        val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   294
        val thm' = Thm.incr_indexes (maxidx + 1) thm
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   295
      in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   296
      handle NO_TO_MATCH => NONE
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   297
    
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   298
  in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   299
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   300
fun rewrite_conv ctxt (pattern, to) thms ct =
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   301
  let
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   302
    fun apply_pat At = judgment_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   303
      | apply_pat In = in_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   304
      | apply_pat Asm = params_pconv o asms_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   305
      | apply_pat Concl = params_pconv o concl_pconv
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   306
      | apply_pat (For idents) = (fn cv => for_pconv cv (map (apfst SOME) idents))
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   307
      | apply_pat (Term x) = (fn cv => match_pconv cv (apsnd (map (apfst SOME)) x))
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   308
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   309
    val cv = fold_rev apply_pat pattern
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   310
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   311
    fun distinct_prems th =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   312
      case Seq.pull (distinct_subgoals_tac th) of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   313
        NONE => th
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   314
      | SOME (th', _) => th'
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   315
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   316
    val rewrite = rewrs_pconv to (maps (prep_meta_eq ctxt) thms)
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   317
  in cv rewrite ctxt (Vartab.empty, []) ct |> distinct_prems end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   318
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   319
fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   320
  let
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   321
    val export = case pat_ctxt of
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   322
        NONE => I
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   323
      | SOME inner => singleton (Proof_Context.export inner ctxt)
60117
2712f40d6309 rewrite: work purely conversion-based
noschinl
parents: 60109
diff changeset
   324
  in CCONVERSION (export o rewrite_conv ctxt pat thms) end
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   325
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   326
val _ =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   327
  Theory.setup
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   328
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   329
    fun mk_fix s = (Binding.name s, NONE, NoSyn)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   330
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   331
    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   332
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   333
        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   334
        val atom =  (Args.$$$ "asm" >> K Asm) ||
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   335
          (Args.$$$ "concl" >> K Concl) ||
63285
e9c777bfd78c clarified syntax;
wenzelm
parents: 62969
diff changeset
   336
          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   337
          (Parse.term >> Term)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   338
        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   339
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   340
        fun append_default [] = [Concl, In]
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   341
          | append_default (ps as Term _ :: _) = Concl :: In :: ps
60108
d7fe3e0aca85 rewrite: add default pattern "in concl" for more cases
noschinl
parents: 60088
diff changeset
   342
          | append_default [For x, In] = [For x, Concl, In]
d7fe3e0aca85 rewrite: add default pattern "in concl" for more cases
noschinl
parents: 60088
diff changeset
   343
          | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   344
          | append_default ps = ps
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   345
61476
1884c40f1539 tuned signature;
wenzelm
parents: 60642
diff changeset
   346
      in Scan.repeats sep_atom >> (rev #> append_default) end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   347
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   348
    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   349
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   350
        val (r, toks') = scan toks
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   351
        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   352
      in (r', (context', toks' : Token.T list)) end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   353
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   354
    fun read_fixes fixes ctxt =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   355
      let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   356
      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   357
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   358
    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   359
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   360
        fun add_constrs ctxt n (Abs (x, T, t)) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   361
            let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   362
              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   363
            in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   364
              (case add_constrs ctxt' (n+1) t of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   365
                NONE => NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   366
              | SOME ((ctxt'', n', xs), t') =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   367
                  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   368
                    val U = Type_Infer.mk_param n []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   369
                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   370
                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   371
            end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   372
          | add_constrs ctxt n (l $ r) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   373
            (case add_constrs ctxt n l of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   374
              SOME (c, l') => SOME (c, l' $ r)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   375
            | NONE =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   376
              (case add_constrs ctxt n r of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   377
                SOME (c, r') => SOME (c, l $ r')
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   378
              | NONE => NONE))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   379
          | add_constrs ctxt n t =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   380
            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   381
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   382
        fun prep (Term s) (n, ctxt) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   383
            let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   384
              val t = Syntax.parse_term ctxt s
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   385
              val ((ctxt', n', bs), t') =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   386
                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   387
            in (Term (t', bs), (n', ctxt')) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   388
          | prep (For ss) (n, ctxt) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   389
            let val (ns, ctxt') = read_fixes ss ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   390
            in (For ns, (n, ctxt')) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   391
          | prep At (n,ctxt) = (At, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   392
          | prep In (n,ctxt) = (In, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   393
          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   394
          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   395
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   396
        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   397
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   398
      in (xs, ctxt') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   399
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   400
    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   401
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   402
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   403
        fun check_terms ctxt ps to =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   404
          let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   405
            fun safe_chop (0: int) xs = ([], xs)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   406
              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   407
              | safe_chop _ _ = raise Match
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   408
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   409
            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   410
                let val (cs', ts') = safe_chop (length cs) ts
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   411
                in (Term (t, map dest_Free cs'), ts') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   412
              | reinsert_pat _ (Term _) [] = raise Match
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   413
              | reinsert_pat ctxt (For ss) ts =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   414
                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   415
                in (For fixes, ts) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   416
              | reinsert_pat _ At ts = (At, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   417
              | reinsert_pat _ In ts = (In, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   418
              | reinsert_pat _ Concl ts = (Concl, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   419
              | reinsert_pat _ Asm ts = (Asm, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   420
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   421
            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   422
            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   423
              | mk_free_constrs _ = []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   424
60051
noschinl
parents: 60050
diff changeset
   425
            val ts = maps mk_free_constrs ps @ the_list to
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   426
              |> Syntax.check_terms (hole_syntax ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   427
            val ctxt' = fold Variable.declare_term ts ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   428
            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   429
              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   430
            val _ = case ts' of (_ :: _) => raise Match | [] => ()
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   431
          in ((ps', to'), ctxt') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   432
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   433
        val (pats, ctxt') = prep_pats ctxt raw_pats
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   434
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   435
        val ths = Attrib.eval_thms ctxt' raw_ths
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   436
        val to = Option.map (Syntax.parse_term ctxt') raw_to
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   437
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   438
        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   439
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   440
      in ((pats', ths, (to', ctxt)), ctxt'') end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   441
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   442
    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   443
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   444
    val subst_parser =
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 61476
diff changeset
   445
      let val scan = raw_pattern -- to_parser -- Parse.thms1
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   446
      in context_lift scan prep_args end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   447
  in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   448
    Method.setup @{binding rewrite} (subst_parser >>
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   449
      (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   450
        SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   451
      "single-step rewriting, allowing subterm selection via patterns."
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   452
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   453
end