src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 56245 84fc7dfa3cd4
parent 56243 2e10a36b8d46
child 58634 9f10d82e8188
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -36,9 +36,9 @@
     1.4  
     1.5  val may_use_binary_ints =
     1.6    let
     1.7 -    fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
     1.8 +    fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) =
     1.9          aux def t1 andalso aux false t2
    1.10 -      | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
    1.11 +      | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def t2
    1.12        | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
    1.13          aux def t1 andalso aux false t2
    1.14        | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
    1.15 @@ -145,7 +145,7 @@
    1.16        case t of
    1.17          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
    1.18        | Const (s0, _) $ t1 $ _ =>
    1.19 -        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
    1.20 +        if s0 = @{const_name Pure.eq} orelse s0 = @{const_name HOL.eq} then
    1.21            let
    1.22              val (t', args) = strip_comb t1
    1.23              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
    1.24 @@ -187,12 +187,12 @@
    1.25        end
    1.26      and do_term new_Ts old_Ts polar t =
    1.27        case t of
    1.28 -        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
    1.29 +        Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
    1.30          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
    1.31 -      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
    1.32 +      | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 =>
    1.33          do_equals new_Ts old_Ts s0 T0 t1 t2
    1.34 -      | @{const "==>"} $ t1 $ t2 =>
    1.35 -        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
    1.36 +      | @{const Pure.imp} $ t1 $ t2 =>
    1.37 +        @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1
    1.38          $ do_term new_Ts old_Ts polar t2
    1.39        | @{const Pure.conjunction} $ t1 $ t2 =>
    1.40          @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
    1.41 @@ -334,9 +334,9 @@
    1.42      val k = maxidx_of_term t + 1
    1.43      fun do_term Ts def t args seen =
    1.44        case t of
    1.45 -        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
    1.46 +        (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 =>
    1.47          do_eq_or_imp Ts true def t0 t1 t2 seen
    1.48 -      | (t0 as @{const "==>"}) $ t1 $ t2 =>
    1.49 +      | (t0 as @{const Pure.imp}) $ t1 $ t2 =>
    1.50          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
    1.51        | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.52          do_eq_or_imp Ts true def t0 t1 t2 seen
    1.53 @@ -401,9 +401,9 @@
    1.54      val num_occs_of_var =
    1.55        fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
    1.56                      | _ => I) t (K 0)
    1.57 -    fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
    1.58 +    fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) =
    1.59          aux_eq Ts careful true t0 t1 t2
    1.60 -      | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
    1.61 +      | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) =
    1.62          t0 $ aux Ts false t1 $ aux Ts careful t2
    1.63        | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
    1.64          aux_eq Ts careful true t0 t1 t2
    1.65 @@ -455,22 +455,22 @@
    1.66  
    1.67  (** Destruction of universal and existential equalities **)
    1.68  
    1.69 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
    1.70 +fun curry_assms (@{const Pure.imp} $ (@{const Trueprop}
    1.71                                     $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
    1.72      curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
    1.73 -  | curry_assms (@{const "==>"} $ t1 $ t2) =
    1.74 -    @{const "==>"} $ curry_assms t1 $ curry_assms t2
    1.75 +  | curry_assms (@{const Pure.imp} $ t1 $ t2) =
    1.76 +    @{const Pure.imp} $ curry_assms t1 $ curry_assms t2
    1.77    | curry_assms t = t
    1.78  
    1.79  val destroy_universal_equalities =
    1.80    let
    1.81      fun aux prems zs t =
    1.82        case t of
    1.83 -        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
    1.84 +        @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2
    1.85        | _ => Logic.list_implies (rev prems, t)
    1.86      and aux_implies prems zs t1 t2 =
    1.87        case t1 of
    1.88 -        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
    1.89 +        Const (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
    1.90        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
    1.91          aux_eq prems zs z t' t1 t2
    1.92        | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
    1.93 @@ -591,10 +591,10 @@
    1.94                               not (is_higher_order_type abs_T)) polar t)
    1.95        in
    1.96          case t of
    1.97 -          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
    1.98 +          Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
    1.99            do_quantifier s0 T0 s1 T1 t1
   1.100 -        | @{const "==>"} $ t1 $ t2 =>
   1.101 -          @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   1.102 +        | @{const Pure.imp} $ t1 $ t2 =>
   1.103 +          @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   1.104            $ aux ss Ts js skolemizable polar t2
   1.105          | @{const Pure.conjunction} $ t1 $ t2 =>
   1.106            @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
   1.107 @@ -654,7 +654,7 @@
   1.108  
   1.109  (** Function specialization **)
   1.110  
   1.111 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
   1.112 +fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2
   1.113    | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
   1.114    | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
   1.115      snd (strip_comb t1)
   1.116 @@ -866,7 +866,7 @@
   1.117        if exists_subterm (curry (op aconv) u) def then NONE else SOME u
   1.118    in
   1.119      case t of
   1.120 -      Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def
   1.121 +      Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def
   1.122      | @{const Trueprop}
   1.123        $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
   1.124        do_equals u def
   1.125 @@ -918,7 +918,7 @@
   1.126      and add_def_axiom depth = add_axiom fst apfst true depth
   1.127      and add_nondef_axiom depth = add_axiom snd apsnd false depth
   1.128      and add_maybe_def_axiom depth t =
   1.129 -      (if head_of t <> @{const "==>"} then add_def_axiom
   1.130 +      (if head_of t <> @{const Pure.imp} then add_def_axiom
   1.131         else add_nondef_axiom) depth t
   1.132      and add_eq_axiom depth t =
   1.133        (if is_constr_pattern_formula ctxt t then add_def_axiom