src/HOL/Library/rewrite.ML
changeset 59975 da10875adf8e
parent 59970 e9f73d87d904
child 60050 dc6ac152d864
     1.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 08 21:08:26 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Wed Apr 08 21:24:27 2015 +0200
     1.3 @@ -1,24 +1,26 @@
     1.4 -(* Author: Christoph Traut, Lars Noschinski
     1.5 +(*  Title:      HOL/Library/rewrite.ML
     1.6 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     1.7  
     1.8 -  This is a rewrite method supports subterm-selection based on patterns.
     1.9 +This is a rewrite method that supports subterm-selection based on patterns.
    1.10  
    1.11 -  The patterns accepted by rewrite are of the following form:
    1.12 -    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
    1.13 -    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
    1.14 -    <args>    ::= [<pattern>] ("to" <term>) <thms>
    1.15 +The patterns accepted by rewrite are of the following form:
    1.16 +  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
    1.17 +  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
    1.18 +  <args>    ::= [<pattern>] ("to" <term>) <thms>
    1.19  
    1.20 -  This syntax was clearly inspired by Gonthier's and Tassi's language of
    1.21 -  patterns but has diverged significantly during its development.
    1.22 +This syntax was clearly inspired by Gonthier's and Tassi's language of
    1.23 +patterns but has diverged significantly during its development.
    1.24  
    1.25 -  We also allow introduction of identifiers for bound variables,
    1.26 -  which can then be used to match arbitary subterms inside abstractions.
    1.27 +We also allow introduction of identifiers for bound variables,
    1.28 +which can then be used to match arbitrary subterms inside abstractions.
    1.29  *)
    1.30  
    1.31 -signature REWRITE1 = sig
    1.32 -  val setup : theory -> theory
    1.33 +signature REWRITE =
    1.34 +sig
    1.35 +  (* FIXME proper ML interface!? *)
    1.36  end
    1.37  
    1.38 -structure Rewrite : REWRITE1 =
    1.39 +structure Rewrite : REWRITE =
    1.40  struct
    1.41  
    1.42  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
    1.43 @@ -68,8 +70,10 @@
    1.44    let
    1.45      fun add_ident NONE _ l = l
    1.46        | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
    1.47 -    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    1.48 +    fun inner rewr ctxt idents =
    1.49 +      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    1.50    in inner end
    1.51 +
    1.52  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
    1.53  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
    1.54  
    1.55 @@ -80,17 +84,19 @@
    1.56    case try (fastype_of #> dest_funT) u of
    1.57      NONE => raise TERM ("ft_abs: no function type", [u])
    1.58    | SOME (U, _) =>
    1.59 -  let
    1.60 -    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    1.61 -    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    1.62 -    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    1.63 -    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    1.64 -    val (u', pos') =
    1.65 -      case u of
    1.66 -        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    1.67 -      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    1.68 -  in (tyenv', u', pos') end
    1.69 -  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    1.70 +      let
    1.71 +        val tyenv' =
    1.72 +          if T = dummyT then tyenv
    1.73 +          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    1.74 +        val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    1.75 +        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    1.76 +        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    1.77 +        val (u', pos') =
    1.78 +          case u of
    1.79 +            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    1.80 +          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    1.81 +      in (tyenv', u', pos') end
    1.82 +      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    1.83  
    1.84  fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
    1.85    | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
    1.86 @@ -127,7 +133,8 @@
    1.87            | (x :: xs) => (xs , desc o ft_all ctxt x)
    1.88          end
    1.89        | f rev_idents _ = (rev_idents, I)
    1.90 -  in case f (rev idents) t of
    1.91 +  in
    1.92 +    case f (rev idents) t of
    1.93        ([], ft') => SOME (ft' ft)
    1.94      | _ => NONE
    1.95    end
    1.96 @@ -153,7 +160,8 @@
    1.97  fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
    1.98    let
    1.99      val recurse = find_subterms ctxt condition
   1.100 -    val recursive_matches = case t of
   1.101 +    val recursive_matches =
   1.102 +      case t of
   1.103          _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
   1.104        | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
   1.105        | _ => Seq.empty
   1.106 @@ -250,7 +258,6 @@
   1.107      fun apply_pats ft = ft
   1.108        |> Seq.single
   1.109        |> fold apply_pat pattern_list
   1.110 -
   1.111    in
   1.112      apply_pats
   1.113    end
   1.114 @@ -322,9 +329,9 @@
   1.115      val tac = rewrite_goal_with_thm ctxt pattern thms'
   1.116    in tac end
   1.117  
   1.118 -val setup =
   1.119 +val _ =
   1.120 +  Theory.setup
   1.121    let
   1.122 -
   1.123      fun mk_fix s = (Binding.name s, NONE, NoSyn)
   1.124  
   1.125      val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
   1.126 @@ -342,11 +349,11 @@
   1.127  
   1.128        in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
   1.129  
   1.130 -    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
   1.131 +    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
   1.132        let
   1.133          val (r, toks') = scan toks
   1.134 -        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
   1.135 -      in (r', (ctxt', toks' : Token.T list))end
   1.136 +        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
   1.137 +      in (r', (context', toks' : Token.T list)) end
   1.138  
   1.139      fun read_fixes fixes ctxt =
   1.140        let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
   1.141 @@ -354,7 +361,6 @@
   1.142  
   1.143      fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
   1.144        let
   1.145 -
   1.146          fun add_constrs ctxt n (Abs (x, T, t)) =
   1.147              let
   1.148                val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
   1.149 @@ -470,10 +476,11 @@
   1.150  
   1.151      val subst_parser =
   1.152        let val scan = raw_pattern -- to_parser -- Parse.xthms1
   1.153 -      in ctxt_lift scan prep_args end
   1.154 +      in context_lift scan prep_args end
   1.155    in
   1.156      Method.setup @{binding rewrite} (subst_parser >>
   1.157 -      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
   1.158 +      (fn (pattern, inthms, inst) => fn ctxt =>
   1.159 +        SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
   1.160        "single-step rewriting, allowing subterm selection via patterns."
   1.161    end
   1.162  end