author blanchet Mon Dec 06 13:33:09 2010 +0100 (2010-12-06) changeset 41003 7e2a7bd55a00 parent 41002 11a442b472c7 child 41004 01f33bf79596
proper handling of frames for connectives in monotonicity calculus
```     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, _)) =>
```