src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41003 7e2a7bd55a00
parent 41002 11a442b472c7
child 41004 01f33bf79596
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -669,6 +669,12 @@
     1.4     [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
     1.5     [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
     1.6  
     1.7 +val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
     1.8 +val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
     1.9 +val conj_triple = ("\<and>", conj_clauses, @{const conj})
    1.10 +val disj_triple = ("\<or>", disj_clauses, @{const disj})
    1.11 +val imp_triple = ("\<implies>", imp_clauses, @{const implies})
    1.12 +
    1.13  fun add_annotation_clause_from_quasi_clause _ NONE = NONE
    1.14    | add_annotation_clause_from_quasi_clause [] accum = accum
    1.15    | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum =
    1.16 @@ -733,6 +739,21 @@
    1.17      #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
    1.18      #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
    1.19  
    1.20 +fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
    1.21 +                        (accum as ({frame, ...}, _)) =
    1.22 +  let
    1.23 +    val mtype_for = fresh_mtype_for_type mdata false
    1.24 +    val frame1 = fresh_frame mdata (SOME Tru) NONE frame
    1.25 +    val frame2 = fresh_frame mdata (SOME Fls) NONE frame
    1.26 +    val (m1, accum) = accum |>> set_frame frame1 |> do_t1
    1.27 +    val (m2, accum) = accum |>> set_frame frame2 |> do_t2
    1.28 +  in
    1.29 +    (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    1.30 +     accum |>> set_frame frame
    1.31 +           ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
    1.32 +                                            frame2))
    1.33 +  end
    1.34 +
    1.35  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
    1.36                               max_fresh, ...}) =
    1.37    let
    1.38 @@ -792,18 +813,8 @@
    1.39          M as MPair (a_M, b_M) =>
    1.40          pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
    1.41        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
    1.42 -    and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
    1.43 -      let
    1.44 -        val frame1 = fresh_frame mdata (SOME Tru) NONE frame
    1.45 -        val frame2 = fresh_frame mdata (SOME Fls) NONE frame
    1.46 -        val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
    1.47 -        val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
    1.48 -      in
    1.49 -        (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    1.50 -         accum |>> set_frame frame
    1.51 -               ||> apsnd (add_connective_frames conn mk_quasi_clauses
    1.52 -                                                frame frame1 frame2))
    1.53 -      end
    1.54 +    and do_connect triple t1 t2 =
    1.55 +      consider_connective mdata triple (do_term t1) (do_term t2)
    1.56      and do_term t
    1.57              (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
    1.58                         cset)) =
    1.59 @@ -960,15 +971,10 @@
    1.60                          val (m', accum) =
    1.61                            do_term t' (accum |>> push_bound aa T M)
    1.62                        in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
    1.63 -         | @{const Not} $ t1 =>
    1.64 -           do_connect "\<implies>" imp_clauses @{const implies} t1
    1.65 -                      @{const False} accum
    1.66 -         | (t0 as @{const conj}) $ t1 $ t2 =>
    1.67 -           do_connect "\<and>" conj_clauses t0 t1 t2 accum
    1.68 -         | (t0 as @{const disj}) $ t1 $ t2 =>
    1.69 -           do_connect "\<or>" disj_clauses t0 t1 t2 accum
    1.70 -         | (t0 as @{const implies}) $ t1 $ t2 =>
    1.71 -           do_connect "\<implies>" imp_clauses t0 t1 t2 accum
    1.72 +         | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
    1.73 +         | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
    1.74 +         | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
    1.75 +         | @{const implies} $ t1 $ t2 => do_connect imp_triple t1 t2 accum
    1.76           | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.77             do_term (betapply (t2, t1)) accum
    1.78           | t1 $ t2 =>
    1.79 @@ -1047,6 +1053,9 @@
    1.80                     MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
    1.81               accum |>> pop_bound)
    1.82            end
    1.83 +        fun do_connect triple neg1 t1 t2 =
    1.84 +          consider_connective mdata triple
    1.85 +              (do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
    1.86          fun do_equals x t1 t2 =
    1.87            case sn of
    1.88              Plus => do_term t accum
    1.89 @@ -1064,11 +1073,6 @@
    1.90               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    1.91                      m1), accum)
    1.92             end
    1.93 -         | @{const Not} $ t1 =>
    1.94 -           let val (m1, accum) = do_formula (negate_sign sn) t1 accum in
    1.95 -             (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
    1.96 -              accum)
    1.97 -           end
    1.98           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    1.99             do_quantifier x s1 T1 t1
   1.100           | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
   1.101 @@ -1083,22 +1087,15 @@
   1.102             do_equals x t1 t2
   1.103           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   1.104             do_formula sn (betapply (t2, t1)) accum
   1.105 -         | (t0 as Const (s0, _)) $ t1 $ t2 =>
   1.106 -           if s0 = @{const_name "==>"} orelse
   1.107 -              s0 = @{const_name Pure.conjunction} orelse
   1.108 -              s0 = @{const_name conj} orelse s0 = @{const_name disj} orelse
   1.109 -              s0 = @{const_name implies} then
   1.110 -             let
   1.111 -               val impl = (s0 = @{const_name "==>"} orelse
   1.112 -                           s0 = @{const_name implies})
   1.113 -               val (m1, accum) = do_formula (sn |> impl ? negate_sign) t1 accum
   1.114 -               val (m2, accum) = do_formula sn t2 accum
   1.115 -             in
   1.116 -               (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.117 -                accum)
   1.118 -             end
   1.119 -           else
   1.120 -             do_term t accum
   1.121 +         | @{const Pure.conjunction} $ t1 $ t2 =>
   1.122 +           do_connect meta_conj_triple false t1 t2 accum
   1.123 +         | @{const "==>"} $ t1 $ t2 =>
   1.124 +           do_connect meta_imp_triple true t1 t2 accum
   1.125 +         | @{const Not} $ t1 =>
   1.126 +           do_connect imp_triple true t1 @{const False} accum
   1.127 +         | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
   1.128 +         | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
   1.129 +         | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
   1.130           | _ => do_term t accum)
   1.131        end
   1.132        |> tap (fn (m, (gamma, _)) =>