src/HOL/Library/rewrite.ML
changeset 60088 0a064330a885
parent 60079 ef4fe30e9ef1
child 60102 820e8e704ba6
child 60108 d7fe3e0aca85
     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