more standard Isabelle/ML tool setup;
authorwenzelm
Wed Apr 08 21:24:27 2015 +0200 (2015-04-08)
changeset 59975da10875adf8e
parent 59974 b911c8ba0b69
child 59976 046399298519
more standard Isabelle/ML tool setup;
proper file headers;
tuned whitespace;
src/HOL/Library/Rewrite.thy
src/HOL/Library/cconv.ML
src/HOL/Library/rewrite.ML
     1.1 --- a/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:08:26 2015 +0200
     1.2 +++ b/src/HOL/Library/Rewrite.thy	Wed Apr 08 21:24:27 2015 +0200
     1.3 @@ -1,17 +1,22 @@
     1.4 +(*  Title:      HOL/Library/Rewrite.thy
     1.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     1.6 +
     1.7 +Proof method "rewrite" with support for subterm-selection based on patterns.
     1.8 +*)
     1.9 +
    1.10  theory Rewrite
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -consts rewrite_HOLE :: "'a :: {}"
    1.15 +consts rewrite_HOLE :: "'a::{}"
    1.16  notation rewrite_HOLE ("HOLE")
    1.17  notation rewrite_HOLE ("\<box>")
    1.18  
    1.19  lemma eta_expand:
    1.20 -  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
    1.21 -  by (rule reflexive)
    1.22 +  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    1.23 +  shows "f \<equiv> \<lambda>x. f x" .
    1.24  
    1.25  ML_file "cconv.ML"
    1.26  ML_file "rewrite.ML"
    1.27 -setup Rewrite.setup
    1.28  
    1.29  end
     2.1 --- a/src/HOL/Library/cconv.ML	Wed Apr 08 21:08:26 2015 +0200
     2.2 +++ b/src/HOL/Library/cconv.ML	Wed Apr 08 21:24:27 2015 +0200
     2.3 @@ -1,3 +1,9 @@
     2.4 +(*  Title:      HOL/Library/cconv.ML
     2.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     2.6 +
     2.7 +FIXME!?
     2.8 +*)
     2.9 +
    2.10  infix 1 then_cconv
    2.11  infix 0 else_cconv
    2.12  
    2.13 @@ -170,7 +176,8 @@
    2.14  fun prems_cconv 0 cv ct = cv ct
    2.15    | prems_cconv n cv ct =
    2.16        (case ct |> Thm.term_of of
    2.17 -        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    2.18 +        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
    2.19 +          ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    2.20        | _ =>  cv ct)
    2.21  
    2.22  (*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
    2.23 @@ -212,7 +219,7 @@
    2.24        end
    2.25    | NONE => raise THM ("gconv_rule", i, [th]))
    2.26  
    2.27 -  (* Conditional conversions as tactics. *)
    2.28 +(* Conditional conversions as tactics. *)
    2.29  fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
    2.30    handle THM _ => Seq.empty
    2.31         | CTERM _ => Seq.empty
     3.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 08 21:08:26 2015 +0200
     3.2 +++ b/src/HOL/Library/rewrite.ML	Wed Apr 08 21:24:27 2015 +0200
     3.3 @@ -1,24 +1,26 @@
     3.4 -(* Author: Christoph Traut, Lars Noschinski
     3.5 +(*  Title:      HOL/Library/rewrite.ML
     3.6 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     3.7  
     3.8 -  This is a rewrite method supports subterm-selection based on patterns.
     3.9 +This is a rewrite method that supports subterm-selection based on patterns.
    3.10  
    3.11 -  The patterns accepted by rewrite are of the following form:
    3.12 -    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
    3.13 -    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
    3.14 -    <args>    ::= [<pattern>] ("to" <term>) <thms>
    3.15 +The patterns accepted by rewrite are of the following form:
    3.16 +  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
    3.17 +  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
    3.18 +  <args>    ::= [<pattern>] ("to" <term>) <thms>
    3.19  
    3.20 -  This syntax was clearly inspired by Gonthier's and Tassi's language of
    3.21 -  patterns but has diverged significantly during its development.
    3.22 +This syntax was clearly inspired by Gonthier's and Tassi's language of
    3.23 +patterns but has diverged significantly during its development.
    3.24  
    3.25 -  We also allow introduction of identifiers for bound variables,
    3.26 -  which can then be used to match arbitary subterms inside abstractions.
    3.27 +We also allow introduction of identifiers for bound variables,
    3.28 +which can then be used to match arbitrary subterms inside abstractions.
    3.29  *)
    3.30  
    3.31 -signature REWRITE1 = sig
    3.32 -  val setup : theory -> theory
    3.33 +signature REWRITE =
    3.34 +sig
    3.35 +  (* FIXME proper ML interface!? *)
    3.36  end
    3.37  
    3.38 -structure Rewrite : REWRITE1 =
    3.39 +structure Rewrite : REWRITE =
    3.40  struct
    3.41  
    3.42  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
    3.43 @@ -68,8 +70,10 @@
    3.44    let
    3.45      fun add_ident NONE _ l = l
    3.46        | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
    3.47 -    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    3.48 +    fun inner rewr ctxt idents =
    3.49 +      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    3.50    in inner end
    3.51 +
    3.52  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
    3.53  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
    3.54  
    3.55 @@ -80,17 +84,19 @@
    3.56    case try (fastype_of #> dest_funT) u of
    3.57      NONE => raise TERM ("ft_abs: no function type", [u])
    3.58    | SOME (U, _) =>
    3.59 -  let
    3.60 -    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    3.61 -    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    3.62 -    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    3.63 -    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    3.64 -    val (u', pos') =
    3.65 -      case u of
    3.66 -        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    3.67 -      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    3.68 -  in (tyenv', u', pos') end
    3.69 -  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    3.70 +      let
    3.71 +        val tyenv' =
    3.72 +          if T = dummyT then tyenv
    3.73 +          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    3.74 +        val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    3.75 +        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    3.76 +        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    3.77 +        val (u', pos') =
    3.78 +          case u of
    3.79 +            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    3.80 +          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    3.81 +      in (tyenv', u', pos') end
    3.82 +      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    3.83  
    3.84  fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
    3.85    | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
    3.86 @@ -127,7 +133,8 @@
    3.87            | (x :: xs) => (xs , desc o ft_all ctxt x)
    3.88          end
    3.89        | f rev_idents _ = (rev_idents, I)
    3.90 -  in case f (rev idents) t of
    3.91 +  in
    3.92 +    case f (rev idents) t of
    3.93        ([], ft') => SOME (ft' ft)
    3.94      | _ => NONE
    3.95    end
    3.96 @@ -153,7 +160,8 @@
    3.97  fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
    3.98    let
    3.99      val recurse = find_subterms ctxt condition
   3.100 -    val recursive_matches = case t of
   3.101 +    val recursive_matches =
   3.102 +      case t of
   3.103          _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
   3.104        | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
   3.105        | _ => Seq.empty
   3.106 @@ -250,7 +258,6 @@
   3.107      fun apply_pats ft = ft
   3.108        |> Seq.single
   3.109        |> fold apply_pat pattern_list
   3.110 -
   3.111    in
   3.112      apply_pats
   3.113    end
   3.114 @@ -322,9 +329,9 @@
   3.115      val tac = rewrite_goal_with_thm ctxt pattern thms'
   3.116    in tac end
   3.117  
   3.118 -val setup =
   3.119 +val _ =
   3.120 +  Theory.setup
   3.121    let
   3.122 -
   3.123      fun mk_fix s = (Binding.name s, NONE, NoSyn)
   3.124  
   3.125      val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
   3.126 @@ -342,11 +349,11 @@
   3.127  
   3.128        in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
   3.129  
   3.130 -    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
   3.131 +    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
   3.132        let
   3.133          val (r, toks') = scan toks
   3.134 -        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
   3.135 -      in (r', (ctxt', toks' : Token.T list))end
   3.136 +        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
   3.137 +      in (r', (context', toks' : Token.T list)) end
   3.138  
   3.139      fun read_fixes fixes ctxt =
   3.140        let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
   3.141 @@ -354,7 +361,6 @@
   3.142  
   3.143      fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
   3.144        let
   3.145 -
   3.146          fun add_constrs ctxt n (Abs (x, T, t)) =
   3.147              let
   3.148                val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
   3.149 @@ -470,10 +476,11 @@
   3.150  
   3.151      val subst_parser =
   3.152        let val scan = raw_pattern -- to_parser -- Parse.xthms1
   3.153 -      in ctxt_lift scan prep_args end
   3.154 +      in context_lift scan prep_args end
   3.155    in
   3.156      Method.setup @{binding rewrite} (subst_parser >>
   3.157 -      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
   3.158 +      (fn (pattern, inthms, inst) => fn ctxt =>
   3.159 +        SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
   3.160        "single-step rewriting, allowing subterm selection via patterns."
   3.161    end
   3.162  end