src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33978 2380c1dac86e
parent 33968 f94fb13ecbb3
child 34121 5e831d805118
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 04 15:30:36 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 04 17:17:52 2009 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Nitpick/Tools/nitpick_hol.ML
     1.5 +(*  Title:      HOL/Tools/Nitpick/nitpick_hol.ML
     1.6      Author:     Jasmin Blanchette, TU Muenchen
     1.7      Copyright   2008, 2009
     1.8  
     1.9 @@ -78,6 +78,7 @@
    1.10    val mk_flat_tuple : typ -> term list -> term
    1.11    val dest_n_tuple : int -> term -> term list
    1.12    val instantiate_type : theory -> typ -> typ -> typ -> typ
    1.13 +  val is_real_datatype : theory -> string -> bool
    1.14    val is_codatatype : theory -> typ -> bool
    1.15    val is_pure_typedef : theory -> typ -> bool
    1.16    val is_univ_typedef : theory -> typ -> bool
    1.17 @@ -1985,11 +1986,13 @@
    1.18      fun do_term Ts def t args seen =
    1.19        case t of
    1.20          (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
    1.21 -        do_eq_or_imp Ts def t0 t1 t2 seen
    1.22 -      | (t0 as @{const "==>"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
    1.23 +        do_eq_or_imp Ts true def t0 t1 t2 seen
    1.24 +      | (t0 as @{const "==>"}) $ t1 $ t2 =>
    1.25 +        do_eq_or_imp Ts false def t0 t1 t2 seen
    1.26        | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.27 -        do_eq_or_imp Ts def t0 t1 t2 seen
    1.28 -      | (t0 as @{const "op -->"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
    1.29 +        do_eq_or_imp Ts true def t0 t1 t2 seen
    1.30 +      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
    1.31 +        do_eq_or_imp Ts false def t0 t1 t2 seen
    1.32        | Abs (s, T, t') =>
    1.33          let val (t', seen) = do_term (T :: Ts) def t' [] seen in
    1.34            (list_comb (Abs (s, T, t'), args), seen)
    1.35 @@ -1999,11 +2002,12 @@
    1.36            do_term Ts def t1 (t2 :: args) seen
    1.37          end
    1.38        | _ => pull_out_constr_comb thy Ts def k 0 t args seen
    1.39 -    (* typ list -> bool -> term -> term -> term -> term list
    1.40 +    (* typ list -> bool -> bool -> term -> term -> term -> term list
    1.41         -> term * term list *)
    1.42 -    and do_eq_or_imp Ts def t0 t1 t2 seen =
    1.43 +    and do_eq_or_imp Ts eq def t0 t1 t2 seen =
    1.44        let
    1.45 -        val (t2, seen) = do_term Ts def t2 [] seen
    1.46 +        val (t2, seen) = if eq andalso def then (t2, seen)
    1.47 +                         else do_term Ts false t2 [] seen
    1.48          val (t1, seen) = do_term Ts false t1 [] seen
    1.49        in (t0 $ t1 $ t2, seen) end
    1.50      val (concl, seen) = do_term [] def t [] []