src/HOL/Library/rewrite.ML
author noschinl
Thu, 16 Apr 2015 15:55:55 +0200
changeset 60088 0a064330a885
parent 60079 ef4fe30e9ef1
child 60102 820e8e704ba6
child 60108 d7fe3e0aca85
permissions -rw-r--r--
rewrite: use distinct names for unnamed abstractions
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
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    18
signature REWRITE =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    19
sig
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    20
  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
    21
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    22
  val mk_hole: int -> typ -> term
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    23
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    24
  val rewrite: Proof.context
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    25
    -> (term * (string * typ) list, string * typ option) pattern list * term option
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    26
    -> thm list
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    27
    -> cterm
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    28
    -> thm Seq.seq
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    29
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    30
  val rewrite_tac: Proof.context
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    31
    -> (term * (string * typ) list, string * typ option) pattern list * term option
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    32
    -> thm list
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    33
    -> int
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
    34
    -> tactic
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    35
end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    36
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    37
structure Rewrite : REWRITE =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    38
struct
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    39
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    40
datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    41
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    42
fun map_term_pattern f (Term x) = f x
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    43
  | map_term_pattern _ (For ss) = (For ss)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    44
  | map_term_pattern _ At = At
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    45
  | map_term_pattern _ In = In
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    46
  | map_term_pattern _ Concl = Concl
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    47
  | map_term_pattern _ Asm = Asm
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    48
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    49
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    50
exception NO_TO_MATCH
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    51
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    52
fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    53
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    54
(* We rewrite subterms using rewrite conversions. These are conversions
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    55
   that also take a context and a list of identifiers for bound variables
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    56
   as parameters. *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    57
type rewrite_conv = Proof.context -> (string * term) list -> conv
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    58
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    59
(* To apply such a rewrite conversion to a subterm of our goal, we use
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    60
   subterm positions, which are just functions that map a rewrite conversion,
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    61
   working on the top level, to a new rewrite conversion, working on
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    62
   a specific subterm.
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    63
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    64
   During substitution, we are traversing the goal to find subterms that
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    65
   we can rewrite. For each of these subterms, a subterm position is
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    66
   created and later used in creating a conversion that we use to try and
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    67
   rewrite this subterm. *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    68
type subterm_position = rewrite_conv -> rewrite_conv
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    69
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    70
(* A focusterm represents a subterm. It is a tuple (t, p), consisting
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    71
  of the subterm t itself and its subterm position p. *)
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
    72
type focusterm = (Type.tyenv * Proof.context) * term * subterm_position
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    73
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    74
val dummyN = Name.internal "__dummy"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    75
val holeN = Name.internal "_hole"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    76
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    77
fun prep_meta_eq ctxt =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    78
  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    79
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    80
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    81
(* rewrite conversions *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    82
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    83
fun abs_rewr_cconv ident : subterm_position =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    84
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    85
    fun add_ident NONE _ l = l
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    86
      | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    87
    fun inner rewr ctxt idents =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    88
      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    89
  in inner end
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
    90
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    91
val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    92
val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
60050
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
    93
val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
60054
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60053
diff changeset
    94
val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    95
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    96
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    97
(* focus terms *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    98
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
    99
fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   100
  case try (fastype_of #> dest_funT) u of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   101
    NONE => raise TERM ("ft_abs: no function type", [u])
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   102
  | SOME (U, _) =>
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   103
      let
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   104
        val tyenv' =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   105
          if T = dummyT then tyenv
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   106
          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   107
        val (s', u_ctxt') =
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   108
          case s of
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   109
           NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   110
          | SOME s => (s, u_ctxt)
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   111
        val x = Free (s', Envir.norm_type tyenv' T)
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   112
        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   113
        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   114
        val (u', pos') =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   115
          case u of
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   116
            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   117
          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   118
      in ((tyenv', u_ctxt'), u', pos') end
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   119
      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   120
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   121
fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   122
  | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   123
  | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   124
60050
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   125
local
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   126
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   127
fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv)
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   128
  | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   129
  | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t])
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   130
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   131
in
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   132
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   133
val ft_arg = ft_arg_gen arg_rewr_cconv
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   134
val ft_imp = ft_arg_gen imp_rewr_cconv
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   135
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   136
end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   137
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   138
(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   139
fun ft_params ctxt (ft as (_, t, _) : focusterm) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   140
  case t of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   141
    Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   142
      (ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   143
  | Const (@{const_name "Pure.all"}, _) =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   144
      (ft_params ctxt o ft_arg ctxt) ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   145
  | _ => ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   146
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   147
fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   148
    let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   149
      val def_U = T |> dest_funT |> fst |> dest_funT |> fst
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   150
      val ident' = apsnd (the_default (def_U)) ident
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   151
    in (ft_abs ctxt ident' o ft_arg ctxt) ft end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   152
  | ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t])
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   153
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   154
fun ft_for ctxt idents (ft as (_, t, _) : focusterm) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   155
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   156
    fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   157
        let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   158
         val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   159
        in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   160
          case rev_idents' of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   161
            [] => ([], desc o ft_all ctxt (NONE, NONE))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   162
          | (x :: xs) => (xs , desc o ft_all ctxt x)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   163
        end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   164
      | f rev_idents _ = (rev_idents, I)
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   165
  in
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   166
    case f (rev idents) t of
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   167
      ([], ft') => SOME (ft' ft)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   168
    | _ => NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   169
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   170
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   171
fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   172
  case t of
60050
dc6ac152d864 rewrite: propagate premises to new subgoals
noschinl
parents: 59975
diff changeset
   173
    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   174
  | _ => ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   175
60054
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60053
diff changeset
   176
fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) =
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60053
diff changeset
   177
      (tyenv, l, pos o with_prems_rewr_cconv)
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60053
diff changeset
   178
  | ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t])
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   179
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   180
fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59739
diff changeset
   181
  if Object_Logic.is_judgment ctxt t
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   182
  then ft_arg ctxt ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   183
  else ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   184
60055
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   185
(* Find all subterms that might be a valid point to apply a rule. *)
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   186
fun valid_match_points ctxt (ft : focusterm) =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   187
  let
60055
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   188
    fun descend (_, _ $ _, _) = [ft_fun ctxt, ft_arg ctxt]
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   189
      | descend (_, Abs (_, T, _), _) = [ft_abs ctxt (NONE, T)]
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   190
      | descend _ = []
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   191
    fun subseq ft =
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   192
      descend ft |> Seq.of_list |> Seq.maps (fn f => ft |> f |> valid_match_points ctxt)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   193
    fun is_valid (l $ _) = is_valid l
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   194
      | is_valid (Abs (_, _, a)) = is_valid a
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   195
      | is_valid (Var _) = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   196
      | is_valid (Bound _) = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   197
      | is_valid _ = true
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   198
  in
60055
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   199
    Seq.make (fn () => SOME (ft, subseq ft))
aa3d2a6dd99e rewrite: tuned code, no semantic changes
noschinl
parents: 60054
diff changeset
   200
    |> Seq.filter (#2 #> is_valid)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   201
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   202
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   203
fun mk_hole i T = Var ((holeN, i), T)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   204
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   205
fun is_hole (Var ((name, _), _)) = (name = holeN)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   206
  | is_hole _ = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   207
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   208
fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   209
  | is_hole_const _ = false
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   210
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   211
val hole_syntax =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   212
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   213
    (* Modified variant of Term.replace_hole *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   214
    fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i =
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   215
          (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   216
      | replace_hole Ts (Abs (x, T, t)) i =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   217
          let val (t', i') = replace_hole (T :: Ts) t i
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   218
          in (Abs (x, T, t'), i') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   219
      | replace_hole Ts (t $ u) i =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   220
          let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   221
            val (t', i') = replace_hole Ts t i
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   222
            val (u', i'') = replace_hole Ts u i'
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   223
          in (t' $ u', i'') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   224
      | replace_hole _ a i = (a, i)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   225
    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   226
  in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   227
    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   228
    #> Proof_Context.set_mode Proof_Context.mode_pattern
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   229
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   230
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   231
(* Find a subterm of the focusterm matching the pattern. *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   232
fun find_matches ctxt pattern_list =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   233
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   234
    fun move_term ctxt (t, off) (ft : focusterm) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   235
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   236
        val thy = Proof_Context.theory_of ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   237
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   238
        val eta_expands =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   239
          let val (_, ts) = strip_comb t
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   240
          in map fastype_of (snd (take_suffix is_Var ts)) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   241
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   242
        fun do_match ((tyenv, u_ctxt), u, pos) =
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   243
          case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   244
            NONE => NONE
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   245
          | SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos))
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   246
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   247
        fun match_argT T u =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   248
          let val (U, _) = dest_funT (fastype_of u)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   249
          in try (Sign.typ_match thy (T,U)) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   250
          handle TYPE _ => K NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   251
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   252
        fun desc [] ft = do_match ft
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   253
          | desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   254
            case do_match ft of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   255
              NONE =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   256
                (case match_argT T u tyenv of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   257
                  NONE => NONE
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   258
                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos)))
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   259
            | SOME ft => SOME ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   260
      in desc eta_expands ft end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   261
60052
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   262
    fun move_assms ctxt (ft: focusterm) =
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   263
      let
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   264
        fun f () = case try (ft_assm ctxt) ft of
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   265
            NONE => NONE
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   266
          | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   267
      in Seq.make f end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   268
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   269
    fun apply_pat At = Seq.map (ft_judgment ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   270
      | apply_pat In = Seq.maps (valid_match_points ctxt)
60052
616a17640229 rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents: 60051
diff changeset
   271
      | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   272
      | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   273
      | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   274
      | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   275
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   276
    fun apply_pats ft = ft
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   277
      |> Seq.single
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   278
      |> fold apply_pat pattern_list
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   279
  in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   280
    apply_pats
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   281
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   282
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   283
fun instantiate_normalize_env ctxt env thm =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   284
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   285
    fun certs f = map (apply2 (f ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   286
    val prop = Thm.prop_of thm
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   287
    val norm_type = Envir.norm_type o Envir.type_env
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   288
    val insts = Term.add_vars prop []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   289
      |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   290
      |> certs Thm.cterm_of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   291
    val tyinsts = Term.add_tvars prop []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   292
      |> map (fn x => (TVar x, norm_type env (TVar x)))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   293
      |> certs Thm.ctyp_of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   294
  in Drule.instantiate_normalize (tyinsts, insts) thm end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   295
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   296
fun unify_with_rhs context to env thm =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   297
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   298
    val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   299
    val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   300
      handle Pattern.Unif => raise NO_TO_MATCH
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   301
  in env' end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   302
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   303
fun inst_thm_to _ (NONE, _) thm = thm
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   304
  | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   305
      instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   306
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   307
fun inst_thm ctxt idents (to, tyenv) thm =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   308
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   309
    (* Replace any identifiers with their corresponding bound variables. *)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   310
    val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   311
    val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   312
    val replace_idents =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   313
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   314
        fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   315
          | subst _ t = t
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   316
      in Term.map_aterms (subst idents) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   317
60051
noschinl
parents: 60050
diff changeset
   318
    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   319
    val thm' = Thm.incr_indexes (maxidx + 1) thm
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   320
  in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   321
  handle NO_TO_MATCH => NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   322
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   323
local
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   324
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   325
fun rewrite_raw ctxt (pattern, to) thms ct =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   326
  let
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   327
    fun interpret_term_patterns ctxt =
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   328
      let
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   329
    
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   330
        fun descend_hole fixes (Abs (_, _, t)) =
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   331
            (case descend_hole fixes t of
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   332
              NONE => NONE
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   333
            | SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix))
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   334
            | SOME ([], _) => raise Match (* XXX -- check phases modified binding *))
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   335
          | descend_hole fixes (t as l $ r) =
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   336
            let val (f, _) = strip_comb t
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   337
            in
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   338
              if is_hole f
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   339
              then SOME (fixes, I)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   340
              else
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   341
                (case descend_hole fixes l of
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   342
                  SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   343
                | NONE =>
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   344
                  (case descend_hole fixes r of
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   345
                    SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   346
                  | NONE => NONE))
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   347
            end
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   348
          | descend_hole fixes t =
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   349
            if is_hole t then SOME (fixes, I) else NONE
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   350
    
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   351
        fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   352
    
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   353
      in map (map_term_pattern f) end
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   354
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   355
    val pattern' = interpret_term_patterns ctxt pattern
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   356
    val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I)
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   357
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   358
    val thms' = maps (prep_meta_eq ctxt) thms
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   359
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   360
    fun rewrite_conv insty ctxt bounds =
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   361
      CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) thms')
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   362
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   363
    fun distinct_prems th =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   364
      case Seq.pull (distinct_subgoals_tac th) of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   365
        NONE => th
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   366
      | SOME (th', _) => th'
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   367
60088
0a064330a885 rewrite: use distinct names for unnamed abstractions
noschinl
parents: 60079
diff changeset
   368
    fun conv (((tyenv, _), _, position) : focusterm) =
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   369
      distinct_prems o position (rewrite_conv (to, tyenv)) ctxt []
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   370
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   371
  in Seq.map (fn ft => conv ft) matches end
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   372
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   373
in
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   374
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   375
fun rewrite ctxt pat thms ct =
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   376
  rewrite_raw ctxt pat thms ct |> Seq.map_filter (fn cv => try cv ct)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   377
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   378
fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   379
  let
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   380
    val export = case pat_ctxt of
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   381
        NONE => I
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   382
      | SOME inner => singleton (Proof_Context.export inner ctxt)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   383
    val tac = CSUBGOAL (fn (ct, i) =>
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   384
      rewrite_raw ctxt pat thms ct
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   385
      |> Seq.map (fn cv => CCONVERSION (export o cv) i)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   386
      |> SEQ_CONCAT)
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   387
  in tac end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   388
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   389
fun rewrite_tac ctxt pat = rewrite_export_tac ctxt (pat, NONE)
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   390
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   391
end
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   392
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   393
val _ =
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   394
  Theory.setup
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   395
  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   396
    fun mk_fix s = (Binding.name s, NONE, NoSyn)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   397
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   398
    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   399
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   400
        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   401
        val atom =  (Args.$$$ "asm" >> K Asm) ||
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   402
          (Args.$$$ "concl" >> K Concl) ||
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   403
          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   404
          (Parse.term >> Term)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   405
        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   406
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   407
        fun append_default [] = [Concl, In]
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   408
          | append_default (ps as Term _ :: _) = Concl :: In :: ps
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   409
          | append_default ps = ps
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   410
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   411
      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   412
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   413
    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   414
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   415
        val (r, toks') = scan toks
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   416
        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
   417
      in (r', (context', toks' : Token.T list)) end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   418
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   419
    fun read_fixes fixes ctxt =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   420
      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
   421
      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   422
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   423
    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   424
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   425
        fun add_constrs ctxt n (Abs (x, T, t)) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   426
            let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   427
              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   428
            in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   429
              (case add_constrs ctxt' (n+1) t of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   430
                NONE => NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   431
              | SOME ((ctxt'', n', xs), t') =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   432
                  let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   433
                    val U = Type_Infer.mk_param n []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   434
                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   435
                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   436
            end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   437
          | add_constrs ctxt n (l $ r) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   438
            (case add_constrs ctxt n l of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   439
              SOME (c, l') => SOME (c, l' $ r)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   440
            | NONE =>
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   441
              (case add_constrs ctxt n r of
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   442
                SOME (c, r') => SOME (c, l $ r')
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   443
              | NONE => NONE))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   444
          | add_constrs ctxt n t =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   445
            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   446
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   447
        fun prep (Term s) (n, ctxt) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   448
            let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   449
              val t = Syntax.parse_term ctxt s
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   450
              val ((ctxt', n', bs), t') =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   451
                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   452
            in (Term (t', bs), (n', ctxt')) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   453
          | prep (For ss) (n, ctxt) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   454
            let val (ns, ctxt') = read_fixes ss ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   455
            in (For ns, (n, ctxt')) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   456
          | prep At (n,ctxt) = (At, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   457
          | prep In (n,ctxt) = (In, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   458
          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   459
          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   460
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   461
        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   462
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   463
      in (xs, ctxt') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   464
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   465
    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   466
      let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   467
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   468
        fun check_terms ctxt ps to =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   469
          let
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   470
            fun safe_chop (0: int) xs = ([], xs)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   471
              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   472
              | safe_chop _ _ = raise Match
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   473
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   474
            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   475
                let val (cs', ts') = safe_chop (length cs) ts
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   476
                in (Term (t, map dest_Free cs'), ts') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   477
              | reinsert_pat _ (Term _) [] = raise Match
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   478
              | reinsert_pat ctxt (For ss) ts =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   479
                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   480
                in (For fixes, ts) end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   481
              | reinsert_pat _ At ts = (At, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   482
              | reinsert_pat _ In ts = (In, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   483
              | reinsert_pat _ Concl ts = (Concl, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   484
              | reinsert_pat _ Asm ts = (Asm, ts)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   485
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   486
            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   487
            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   488
              | mk_free_constrs _ = []
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   489
60051
noschinl
parents: 60050
diff changeset
   490
            val ts = maps mk_free_constrs ps @ the_list to
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   491
              |> Syntax.check_terms (hole_syntax ctxt)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   492
            val ctxt' = fold Variable.declare_term ts ctxt
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   493
            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   494
              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   495
            val _ = case ts' of (_ :: _) => raise Match | [] => ()
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   496
          in ((ps', to'), ctxt') end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   497
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   498
        val (pats, ctxt') = prep_pats ctxt raw_pats
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   499
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   500
        val ths = Attrib.eval_thms ctxt' raw_ths
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   501
        val to = Option.map (Syntax.parse_term ctxt') raw_to
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   502
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   503
        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   504
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   505
      in ((pats', ths, (to', ctxt)), ctxt'') end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   506
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   507
    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   508
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   509
    val subst_parser =
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   510
      let val scan = raw_pattern -- to_parser -- Parse.xthms1
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59970
diff changeset
   511
      in context_lift scan prep_args end
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   512
  in
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   513
    Method.setup @{binding rewrite} (subst_parser >>
60079
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   514
      (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
ef4fe30e9ef1 rewrite: add ML interface
noschinl
parents: 60055
diff changeset
   515
        SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   516
      "single-step rewriting, allowing subterm selection via patterns."
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   517
  end
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
   518
end