src/HOL/Import/shuffler.ML
changeset 27330 1af2598b5f7d
parent 27173 9ae98c3cd3d6
child 27865 27a8ad9612a3
     1.1 --- a/src/HOL/Import/shuffler.ML	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -159,13 +159,15 @@
     1.4          val cert = cterm_of Pure.thy
     1.5          val xT = TFree("'a",[])
     1.6          val yT = TFree("'b",[])
     1.7 +        val x = Free("x",xT)
     1.8 +        val y = Free("y",yT)
     1.9          val P = Free("P",xT-->yT-->propT)
    1.10 -        val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
    1.11 -        val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
    1.12 +        val lhs = Logic.all x (Logic.all y (P $ x $ y))
    1.13 +        val rhs = Logic.all y (Logic.all x (P $ x $ y))
    1.14          val cl = cert lhs
    1.15          val cr = cert rhs
    1.16 -        val cx = cert (Free("x",xT))
    1.17 -        val cy = cert (Free("y",yT))
    1.18 +        val cx = cert x
    1.19 +        val cy = cert y
    1.20          val th1 = assume cr
    1.21                           |> forall_elim_list [cy,cx]
    1.22                           |> forall_intr_list [cx,cy]
    1.23 @@ -415,6 +417,8 @@
    1.24  fun mk_free s t = Free (s,t)
    1.25  val xT = mk_tfree "a"
    1.26  val yT = mk_tfree "b"
    1.27 +val x = Free ("x", xT)
    1.28 +val y = Free ("y", yT)
    1.29  val P  = mk_free "P" (xT-->yT-->propT)
    1.30  val Q  = mk_free "Q" (xT-->yT)
    1.31  val R  = mk_free "R" (xT-->yT)
    1.32 @@ -436,7 +440,7 @@
    1.33  fun quant_simproc thy = Simplifier.simproc_i
    1.34                             thy
    1.35                             "Ordered rewriting of nested quantifiers"
    1.36 -                           [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
    1.37 +                           [Logic.all x (Logic.all y (P $ x $ y))]
    1.38                             quant_rewrite
    1.39  fun eta_expand_simproc thy = Simplifier.simproc_i
    1.40                           thy
    1.41 @@ -446,7 +450,7 @@
    1.42  fun eta_contract_simproc thy = Simplifier.simproc_i
    1.43                           thy
    1.44                           "Smart handling of eta-contractions"
    1.45 -                         [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
    1.46 +                         [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
    1.47                           eta_contract
    1.48  end
    1.49  
    1.50 @@ -582,8 +586,7 @@
    1.51  fun set_prop thy t =
    1.52      let
    1.53          val vars = add_term_frees (t,add_term_vars (t,[]))
    1.54 -        val closed_t = Library.foldr (fn (v, body) =>
    1.55 -      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
    1.56 +        val closed_t = fold_rev Logic.all vars t
    1.57          val rew_th = norm_term thy closed_t
    1.58          val rhs = Thm.rhs_of rew_th
    1.59