rewrite: use distinct names for unnamed abstractions
authornoschinl
Thu Apr 16 15:55:55 2015 +0200 (2015-04-16)
changeset 600880a064330a885
parent 60087 bc57cb0c5001
child 60101 f5c4b49c8c9a
child 60104 243cee7c1e19
child 60108 d7fe3e0aca85
rewrite: use distinct names for unnamed abstractions
src/HOL/Library/rewrite.ML
src/HOL/ex/Rewrite_Examples.thy
     1.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 15 22:27:31 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Thu Apr 16 15:55:55 2015 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  (* A focusterm represents a subterm. It is a tuple (t, p), consisting
     1.6    of the subterm t itself and its subterm position p. *)
     1.7 -type focusterm = Type.tyenv * term * subterm_position
     1.8 +type focusterm = (Type.tyenv * Proof.context) * term * subterm_position
     1.9  
    1.10  val dummyN = Name.internal "__dummy"
    1.11  val holeN = Name.internal "_hole"
    1.12 @@ -96,7 +96,7 @@
    1.13  
    1.14  (* focus terms *)
    1.15  
    1.16 -fun ft_abs ctxt (s,T) (tyenv, u, pos) =
    1.17 +fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) =
    1.18    case try (fastype_of #> dest_funT) u of
    1.19      NONE => raise TERM ("ft_abs: no function type", [u])
    1.20    | SOME (U, _) =>
    1.21 @@ -104,14 +104,18 @@
    1.22          val tyenv' =
    1.23            if T = dummyT then tyenv
    1.24            else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    1.25 -        val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    1.26 +        val (s', u_ctxt') =
    1.27 +          case s of
    1.28 +           NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt
    1.29 +          | SOME s => (s, u_ctxt)
    1.30 +        val x = Free (s', Envir.norm_type tyenv' T)
    1.31          val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    1.32          fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    1.33          val (u', pos') =
    1.34            case u of
    1.35              Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    1.36            | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    1.37 -      in (tyenv', u', pos') end
    1.38 +      in ((tyenv', u_ctxt'), u', pos') end
    1.39        handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    1.40  
    1.41  fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
    1.42 @@ -235,10 +239,10 @@
    1.43            let val (_, ts) = strip_comb t
    1.44            in map fastype_of (snd (take_suffix is_Var ts)) end
    1.45  
    1.46 -        fun do_match (tyenv, u, pos) =
    1.47 -          case try (Pattern.match thy (t,u)) (tyenv, Vartab.empty) of
    1.48 +        fun do_match ((tyenv, u_ctxt), u, pos) =
    1.49 +          case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of
    1.50              NONE => NONE
    1.51 -          | SOME (tyenv', _) => SOME (off (tyenv', u, pos))
    1.52 +          | SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos))
    1.53  
    1.54          fun match_argT T u =
    1.55            let val (U, _) = dest_funT (fastype_of u)
    1.56 @@ -246,12 +250,12 @@
    1.57            handle TYPE _ => K NONE
    1.58  
    1.59          fun desc [] ft = do_match ft
    1.60 -          | desc (T :: Ts) (ft as (tyenv , u, pos)) =
    1.61 +          | desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) =
    1.62              case do_match ft of
    1.63                NONE =>
    1.64                  (case match_argT T u tyenv of
    1.65                    NONE => NONE
    1.66 -                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) (tyenv', u, pos)))
    1.67 +                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos)))
    1.68              | SOME ft => SOME ft
    1.69        in desc eta_expands ft end
    1.70  
    1.71 @@ -349,7 +353,7 @@
    1.72        in map (map_term_pattern f) end
    1.73  
    1.74      val pattern' = interpret_term_patterns ctxt pattern
    1.75 -    val matches = find_matches ctxt pattern' (Vartab.empty, Thm.term_of ct, I)
    1.76 +    val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I)
    1.77  
    1.78      val thms' = maps (prep_meta_eq ctxt) thms
    1.79  
    1.80 @@ -361,7 +365,7 @@
    1.81          NONE => th
    1.82        | SOME (th', _) => th'
    1.83  
    1.84 -    fun conv ((tyenv, _, position) : focusterm) =
    1.85 +    fun conv (((tyenv, _), _, position) : focusterm) =
    1.86        distinct_prems o position (rewrite_conv (to, tyenv)) ctxt []
    1.87  
    1.88    in Seq.map (fn ft => conv ft) matches end
     2.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Wed Apr 15 22:27:31 2015 +0200
     2.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Thu Apr 16 15:55:55 2015 +0200
     2.3 @@ -254,5 +254,22 @@
     2.4      |> Seq.list_of
     2.5  \<close>
     2.6  
     2.7 +section \<open>Regression tests\<close>
     2.8 +
     2.9 +ML \<open>
    2.10 +  val ct = @{cterm "(\<lambda>b :: int. (\<lambda>a. b + a))"}
    2.11 +  val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context}
    2.12 +  val pat = [
    2.13 +    Rewrite.In,
    2.14 +    Rewrite.Term (@{const plus(int)} $ Var (("c", 0), @{typ int}) $ Var (("c", 0), @{typ int}), [])
    2.15 +    ]
    2.16 +  val to = NONE
    2.17 +  val ct_ths = Rewrite.rewrite ctxt (pat, to) @{thms add.commute} ct
    2.18 +  val _ = case Seq.pull ct_ths of      NONE => ()
    2.19 +    | _ => error "should not have matched anything"
    2.20 +\<close>
    2.21 +
    2.22 +
    2.23 +
    2.24  end
    2.25