# HG changeset patch # User wenzelm # Date 1428521067 -7200 # Node ID da10875adf8e7cd05513cf34008240aea6c4aa4c # Parent b911c8ba0b699b8b9f1213089548e1cb8d1889e8 more standard Isabelle/ML tool setup; proper file headers; tuned whitespace; diff -r b911c8ba0b69 -r da10875adf8e src/HOL/Library/Rewrite.thy --- a/src/HOL/Library/Rewrite.thy Wed Apr 08 21:08:26 2015 +0200 +++ b/src/HOL/Library/Rewrite.thy Wed Apr 08 21:24:27 2015 +0200 @@ -1,17 +1,22 @@ +(* Title: HOL/Library/Rewrite.thy + Author: Christoph Traut, Lars Noschinski, TU Muenchen + +Proof method "rewrite" with support for subterm-selection based on patterns. +*) + theory Rewrite imports Main begin -consts rewrite_HOLE :: "'a :: {}" +consts rewrite_HOLE :: "'a::{}" notation rewrite_HOLE ("HOLE") notation rewrite_HOLE ("\") lemma eta_expand: - fixes f :: "'a :: {} \ 'b :: {}" shows "f \ (\x. f x)" - by (rule reflexive) + fixes f :: "'a::{} \ 'b::{}" + shows "f \ \x. f x" . ML_file "cconv.ML" ML_file "rewrite.ML" -setup Rewrite.setup end diff -r b911c8ba0b69 -r da10875adf8e src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Wed Apr 08 21:08:26 2015 +0200 +++ b/src/HOL/Library/cconv.ML Wed Apr 08 21:24:27 2015 +0200 @@ -1,3 +1,9 @@ +(* Title: HOL/Library/cconv.ML + Author: Christoph Traut, Lars Noschinski, TU Muenchen + +FIXME!? +*) + infix 1 then_cconv infix 0 else_cconv @@ -170,7 +176,8 @@ fun prems_cconv 0 cv ct = cv ct | prems_cconv n cv ct = (case ct |> Thm.term_of of - (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct + (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => + ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct | _ => cv ct) (*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*) @@ -212,7 +219,7 @@ end | NONE => raise THM ("gconv_rule", i, [th])) - (* Conditional conversions as tactics. *) +(* Conditional conversions as tactics. *) fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st) handle THM _ => Seq.empty | CTERM _ => Seq.empty diff -r b911c8ba0b69 -r da10875adf8e src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Wed Apr 08 21:08:26 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Wed Apr 08 21:24:27 2015 +0200 @@ -1,24 +1,26 @@ -(* Author: Christoph Traut, Lars Noschinski +(* Title: HOL/Library/rewrite.ML + Author: Christoph Traut, Lars Noschinski, TU Muenchen - This is a rewrite method supports subterm-selection based on patterns. +This is a rewrite method that supports subterm-selection based on patterns. - The patterns accepted by rewrite are of the following form: - ::= | "concl" | "asm" | "for" "(" ")" - ::= (in | at ) [] - ::= [] ("to" ) +The patterns accepted by rewrite are of the following form: + ::= | "concl" | "asm" | "for" "(" ")" + ::= (in | at ) [] + ::= [] ("to" ) - This syntax was clearly inspired by Gonthier's and Tassi's language of - patterns but has diverged significantly during its development. +This syntax was clearly inspired by Gonthier's and Tassi's language of +patterns but has diverged significantly during its development. - We also allow introduction of identifiers for bound variables, - which can then be used to match arbitary subterms inside abstractions. +We also allow introduction of identifiers for bound variables, +which can then be used to match arbitrary subterms inside abstractions. *) -signature REWRITE1 = sig - val setup : theory -> theory +signature REWRITE = +sig + (* FIXME proper ML interface!? *) end -structure Rewrite : REWRITE1 = +structure Rewrite : REWRITE = struct datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list @@ -68,8 +70,10 @@ let fun add_ident NONE _ l = l | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l - fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt + fun inner rewr ctxt idents = + CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt in inner end + val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr @@ -80,17 +84,19 @@ case try (fastype_of #> dest_funT) u of NONE => raise TERM ("ft_abs: no function type", [u]) | SOME (U, _) => - let - val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv - val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T) - val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand} - fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds - val (u', pos') = - case u of - Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s) - | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s) - in (tyenv', u', pos') end - handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u]) + let + val tyenv' = + if T = dummyT then tyenv + else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv + val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T) + val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand} + fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds + val (u', pos') = + case u of + Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s) + | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s) + in (tyenv', u', pos') end + handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u]) fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv) | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft @@ -127,7 +133,8 @@ | (x :: xs) => (xs , desc o ft_all ctxt x) end | f rev_idents _ = (rev_idents, I) - in case f (rev idents) t of + in + case f (rev idents) t of ([], ft') => SOME (ft' ft) | _ => NONE end @@ -153,7 +160,8 @@ fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) = let val recurse = find_subterms ctxt condition - val recursive_matches = case t of + val recursive_matches = + case t of _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse) | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse | _ => Seq.empty @@ -250,7 +258,6 @@ fun apply_pats ft = ft |> Seq.single |> fold apply_pat pattern_list - in apply_pats end @@ -322,9 +329,9 @@ val tac = rewrite_goal_with_thm ctxt pattern thms' in tac end -val setup = +val _ = + Theory.setup let - fun mk_fix s = (Binding.name s, NONE, NoSyn) val raw_pattern : (string, binding * string option * mixfix) pattern list parser = @@ -342,11 +349,11 @@ in Scan.repeat sep_atom >> (flat #> rev #> append_default) end - fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) => + fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) => let val (r, toks') = scan toks - val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt - in (r', (ctxt', toks' : Token.T list))end + val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context + in (r', (context', toks' : Token.T list)) end fun read_fixes fixes ctxt = let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx) @@ -354,7 +361,6 @@ fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) = let - fun add_constrs ctxt n (Abs (x, T, t)) = let val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt @@ -470,10 +476,11 @@ val subst_parser = let val scan = raw_pattern -- to_parser -- Parse.xthms1 - in ctxt_lift scan prep_args end + in context_lift scan prep_args end in Method.setup @{binding rewrite} (subst_parser >> - (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms))) + (fn (pattern, inthms, inst) => fn ctxt => + SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms))) "single-step rewriting, allowing subterm selection via patterns." end end