author blanchet Mon Dec 06 13:30:36 2010 +0100 (2010-12-06) changeset 40997 67e11a73532a parent 40996 63112be4a469 child 40998 bcd23ddeecef
implemented connectives in new monotonicity calculus
```     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:29:23 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:36 2010 +0100
1.3 @@ -378,14 +378,15 @@
1.4  fun add_assign_disjunct _ NONE = NONE
1.5    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
1.6
1.7 +val add_assign_clause = insert (op =)
1.8 +
1.9  fun annotation_comp Eq a1 a2 = (a1 = a2)
1.10    | annotation_comp Neq a1 a2 = (a1 <> a2)
1.11    | annotation_comp Leq a1 a2 = (a1 = a2 orelse a2 = Gen)
1.12
1.13 -fun comp_op_sign Eq = Plus
1.14 -  | comp_op_sign Neq = Minus
1.15 -  | comp_op_sign Leq =
1.16 -    raise BAD ("Nitpick_Mono.comp_op_sign", "unexpected \"Leq\"")
1.17 +fun sign_for_comp_op Eq = Plus
1.18 +  | sign_for_comp_op Neq = Minus
1.19 +  | sign_for_comp_op Leq = raise BAD ("sign_for_comp_op", "unexpected \"Leq\"")
1.20
1.21  fun do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
1.22      (case (aa1, aa2) of
1.23 @@ -395,15 +396,14 @@
1.24      (case (aa1, aa2) of
1.25         (A a1, A a2) => if annotation_comp cmp a1 a2 then SOME cset else NONE
1.26       | (V x1, A a2) =>
1.27 -       clauses |> add_assign_literal (x1, (comp_op_sign cmp, a2))
1.28 +       clauses |> add_assign_literal (x1, (sign_for_comp_op cmp, a2))
1.29                 |> Option.map (pair comps)
1.30       | (A _, V _) => do_annotation_atom_comp cmp [] aa2 aa1 cset
1.31       | (V _, V _) => SOME (insert (op =) (aa1, aa2, cmp, []) comps, clauses))
1.32    | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
1.33      SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses)
1.34
1.35 -fun add_annotation_atom_comp cmp xs aa1 aa2
1.36 -                             ((comps, clauses) : constraint_set) =
1.37 +fun add_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
1.38    (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
1.39                         string_for_comp_op cmp ^ " " ^
1.40                         string_for_annotation_atom aa2);
1.41 @@ -482,7 +482,7 @@
1.42   | do_notin_mtype_fv _ _ M _ =
1.43     raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
1.44
1.45 -fun add_notin_mtype_fv sn M ((comps, clauses) : constraint_set) =
1.46 +fun add_notin_mtype_fv sn M (comps, clauses) =
1.47    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
1.48                         (case sn of Minus => "concrete" | Plus => "complete"));
1.49     case SOME clauses |> do_notin_mtype_fv sn [] M of
1.50 @@ -610,11 +610,6 @@
1.51     frees: (styp * mtyp) list,
1.52     consts: (styp * mtyp) list}
1.53
1.54 -val string_for_frame =
1.55 -  map (fn (j, aa) => "#" ^ string_of_int j ^ " |-> " ^
1.56 -                     string_for_annotation_atom aa)
1.57 -  #> commas #> enclose "[" "]"
1.58 -
1.59  type accumulator = mtype_context * constraint_set
1.60
1.61  val initial_gamma =
1.62 @@ -638,11 +633,7 @@
1.63
1.64  (* FIXME: make sure tracing messages are complete *)
1.65
1.66 -fun add_comp_frame a cmp frame =
1.67 -  (trace_msg (fn () => "*** Add " ^ string_for_annotation a ^ " " ^
1.68 -                       string_for_comp_op cmp ^ " " ^
1.69 -                       string_for_frame frame);
1.70 -   fold (add_annotation_atom_comp cmp [] (A a) o snd) frame)
1.71 +fun add_comp_frame a cmp = fold (add_annotation_atom_comp cmp [] (A a) o snd)
1.72
1.73  fun add_bound_frame j frame =
1.74    let
1.75 @@ -652,38 +643,62 @@
1.76      #> add_comp_frame Gen Eq gen_frame
1.77    end
1.78
1.79 -fun fresh_imp_frame ({max_fresh, ...} : mdata) sn =
1.80 -  let
1.81 -    fun do_var (j, A Fls) = (j, A (case sn of Plus => Fls | Minus => Tru))
1.82 -      | do_var (j, A Gen) = (j, A Gen)
1.83 -      | do_var (j, _) = (j, V (Unsynchronized.inc max_fresh))
1.84 -  in map do_var end
1.85 +fun fresh_frame ({max_fresh, ...} : mdata) fls tru =
1.86 +  map (apsnd (fn aa =>
1.87 +                 case (aa, fls, tru) of
1.88 +                   (A Fls, SOME a, _) => A a
1.89 +                 | (A Tru, _, SOME a) => A a
1.90 +                 | (A Gen, _, _) => A Gen
1.91 +                 | _ => V (Unsynchronized.inc max_fresh)))
1.92
1.93 -fun do_not_var j aa0 aa1 _ = I
1.94 -(*
1.95 -x1 ~= T | x0 = F
1.96 -x1 ~= F | x0 = T
1.97 -x1 ~= G | x0 = G
1.98 -x1 ~= N | x0 = G
1.99 -*)
1.100 +fun conj_clauses res_aa aa1 aa2 =
1.101 +  [[(aa1, (Neq, Tru)), (aa2, (Neq, Tru)), (res_aa, (Eq, Tru))],
1.102 +   [(aa1, (Neq, Fls)), (res_aa, (Eq, Fls))],
1.103 +   [(aa2, (Neq, Fls)), (res_aa, (Eq, Fls))],
1.104 +   [(aa1, (Neq, Gen)), (aa2, (Eq, Fls)), (res_aa, (Eq, Gen))],
1.105 +   [(aa1, (Neq, New)), (aa2, (Eq, Fls)), (res_aa, (Eq, Gen))],
1.106 +   [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
1.107 +   [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
1.108 +
1.109 +fun disj_clauses res_aa aa1 aa2 =
1.110 +  [[(aa1, (Neq, Tru)), (res_aa, (Eq, Tru))],
1.111 +   [(aa2, (Neq, Tru)), (res_aa, (Eq, Tru))],
1.112 +   [(aa1, (Neq, Fls)), (aa2, (Neq, Fls)), (res_aa, (Eq, Fls))],
1.113 +   [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
1.114 +   [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
1.115 +   [(aa1, (Eq, Tru)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
1.116 +   [(aa1, (Eq, Tru)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
1.117
1.118 -fun do_conj_var j aa0 aa1 aa2 = I
1.119 -(*
1.120 -  (x1 ≠ T | x2 ≠ T | x0 = T) &
1.121 -  (x1 ≠ F | x0 = F) &
1.122 -  (x2 ≠ F | x0 = F) &
1.123 -  (x1 ≠ G | x2 = F | x0 = G) &
1.124 -  (x1 ≠ N | x2 = F | x0 = G) &
1.125 -  (x1 = F | x2 ≠ G | x0 = G) &
1.126 -  (x1 = F | x2 ≠ N | x0 = G)"
1.127 -*)
1.128 +fun imp_clauses res_aa aa1 aa2 =
1.129 +  [[(aa1, (Neq, Fls)), (res_aa, (Eq, Tru))],
1.130 +   [(aa2, (Neq, Tru)), (res_aa, (Eq, Tru))],
1.131 +   [(aa1, (Neq, Tru)), (aa2, (Neq, Fls)), (res_aa, (Eq, Fls))],
1.132 +   [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
1.133 +   [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
1.134 +   [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
1.135 +   [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
1.136 +
1.137 +fun annotation_literal_from_quasi_literal (aa, (cmp, a)) =
1.138 +  case aa of
1.139 +    A a' => if annotation_comp cmp a' a then NONE
1.140 +            else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
1.141 +  | V x => SOME (x, (sign_for_comp_op cmp, a))
1.142
1.143 -fun do_disj_var j aa0 aa1 aa2 = I
1.144 -fun do_imp_var j aa0 aa1 aa2 = I
1.145 +val annotation_clause_from_quasi_clause =
1.146 +  map_filter annotation_literal_from_quasi_literal
1.147 +
1.149
1.150 -fun add_connective_frames do_var res_frame frame1 frame2 =
1.151 -  fold I (map3 (fn (j, aa0) => fn (_, aa1) => fn (_, aa2) =>
1.152 -                   do_var j aa0 aa1 aa2) res_frame frame1 frame2)
1.153 +fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 =
1.154 +  (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^
1.155 +                       string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^
1.156 +                       string_for_annotation_atom aa2);
1.157 +   fold add_quasi_clause (mk_quasi_clauses res_aa aa1 aa2))
1.158 +
1.159 +fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
1.160 +  fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
1.161 +                   add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
1.162 +               res_frame frame1 frame2)
1.163
1.164  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
1.165                               max_fresh, ...}) =
1.166 @@ -705,10 +720,13 @@
1.167           (gamma, cset |> add_mtype_is_complete abs_M))
1.168        end
1.169      fun do_equals T (gamma, cset) =
1.170 -      let val M = mtype_for (domain_type T) in
1.171 -        (MFun (M, A Gen, MFun (M, V (Unsynchronized.inc max_fresh),
1.172 -                               mtype_for (nth_range_type 2 T))),
1.173 -         (gamma, cset |> add_mtype_is_concrete M))
1.174 +      let
1.175 +        val M = mtype_for (domain_type T)
1.176 +        val aa = V (Unsynchronized.inc max_fresh)
1.177 +      in
1.178 +        (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))),
1.179 +         (gamma, cset |> add_mtype_is_concrete M
1.180 +                      |> add_annotation_atom_comp Leq [] (A Fls) aa))
1.181        end
1.182      fun do_robust_set_operation T (gamma, cset) =
1.183        let
1.184 @@ -761,16 +779,18 @@
1.185                                   MApp (bound_m, MRaw (Bound 0, M1))),
1.186                             body_m))), accum)
1.187        end
1.188 -    and do_connect do_var t0 t1 t2 (accum as ({bound_frame, ...}, _)) =
1.189 +    and do_connect conn mk_quasi_clauses t0 t1 t2
1.190 +                   (accum as ({bound_frame, ...}, _)) =
1.191        let
1.192 -        val frame1 = fresh_imp_frame mdata Minus bound_frame
1.193 -        val frame2 = fresh_imp_frame mdata Plus bound_frame
1.194 +        val frame1 = fresh_frame mdata (SOME Tru) NONE bound_frame
1.195 +        val frame2 = fresh_frame mdata (SOME Fls) NONE bound_frame
1.196          val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
1.197          val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
1.198        in
1.199          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
1.200           accum |>> set_frame bound_frame
1.201 -               ||> add_connective_frames do_var bound_frame frame1 frame2)
1.202 +               ||> apsnd (add_connective_frames conn mk_quasi_clauses
1.203 +                                                bound_frame frame1 frame2))
1.204        end
1.205      and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
1.206                               cset)) =
1.207 @@ -929,29 +949,20 @@
1.208                            do_term t' (accum |>> push_bound aa T M)
1.209                        in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
1.210           | (t0 as Const (@{const_name All}, _))
1.211 -           \$ Abs (s', T', (t10 as @{const HOL.implies})
1.212 -                          \$ (t11 \$ Bound 0) \$ t12) =>
1.213 +           \$ Abs (s', T', (t10 as @{const implies}) \$ (t11 \$ Bound 0) \$ t12) =>
1.214             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
1.215           | (t0 as Const (@{const_name Ex}, _))
1.216 -           \$ Abs (s', T', (t10 as @{const HOL.conj})
1.217 -                          \$ (t11 \$ Bound 0) \$ t12) =>
1.218 +           \$ Abs (s', T', (t10 as @{const conj}) \$ (t11 \$ Bound 0) \$ t12) =>
1.219             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
1.220 -         | (t0 as @{const Not}) \$ t1 =>
1.221 -           let
1.222 -             val frame1 = fresh_imp_frame mdata Minus bound_frame
1.223 -             val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
1.224 -           in
1.225 -             (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1),
1.226 -              accum |>> set_frame bound_frame
1.227 -                    ||> add_connective_frames do_not_var bound_frame frame1
1.228 -                                                         frame1)
1.229 -           end
1.230 +         | @{const Not} \$ t1 =>
1.231 +           do_connect "\<implies>" imp_clauses @{const implies} t1
1.232 +                      @{const False} accum
1.233           | (t0 as @{const conj}) \$ t1 \$ t2 =>
1.234 -           do_connect do_conj_var t0 t1 t2 accum
1.235 +           do_connect "\<and>" conj_clauses t0 t1 t2 accum
1.236           | (t0 as @{const disj}) \$ t1 \$ t2 =>
1.237 -           do_connect do_disj_var t0 t1 t2 accum
1.238 +           do_connect "\<or>" disj_clauses t0 t1 t2 accum
1.239           | (t0 as @{const implies}) \$ t1 \$ t2 =>
1.240 -           do_connect do_imp_var t0 t1 t2 accum
1.241 +           do_connect "\<implies>" imp_clauses t0 t1 t2 accum
1.242           | Const (@{const_name Let}, _) \$ t1 \$ t2 =>
1.243             do_term (betapply (t2, t1)) accum
1.244           | t1 \$ t2 =>
1.245 @@ -1053,12 +1064,12 @@
1.246             | (t0 as Const (s0, _)) \$ t1 \$ t2 =>
1.247               if s0 = @{const_name "==>"} orelse
1.248                  s0 = @{const_name Pure.conjunction} orelse
1.249 -                s0 = @{const_name HOL.conj} orelse
1.250 -                s0 = @{const_name HOL.disj} orelse
1.251 -                s0 = @{const_name HOL.implies} then
1.252 +                s0 = @{const_name conj} orelse
1.253 +                s0 = @{const_name disj} orelse
1.254 +                s0 = @{const_name implies} then
1.255                 let
1.256                   val impl = (s0 = @{const_name "==>"} orelse
1.257 -                             s0 = @{const_name HOL.implies})
1.258 +                             s0 = @{const_name implies})
1.259                   val (m1, accum) =
1.260                     do_formula (sn |> impl ? negate_sign) t1 accum
1.261                   val (m2, accum) = do_formula sn t2 accum
1.262 @@ -1146,8 +1157,8 @@
1.263              do_all t0 s0 T1 t1 accum
1.264            | Const (x as (@{const_name HOL.eq}, _)) \$ t1 \$ t2 =>
1.265              consider_general_equals mdata true x t1 t2 accum
1.266 -          | (t0 as @{const HOL.conj}) \$ t1 \$ t2 => do_conjunction t0 t1 t2 accum
1.267 -          | (t0 as @{const HOL.implies}) \$ t1 \$ t2 => do_implies t0 t1 t2 accum
1.268 +          | (t0 as @{const conj}) \$ t1 \$ t2 => do_conjunction t0 t1 t2 accum
1.269 +          | (t0 as @{const implies}) \$ t1 \$ t2 => do_implies t0 t1 t2 accum
1.270            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
1.271                               \do_formula", [t])
1.272      in do_formula t end
```