implemented connectives in new monotonicity calculus
authorblanchet
Mon Dec 06 13:30:36 2010 +0100 (2010-12-06)
changeset 4099767e11a73532a
parent 40996 63112be4a469
child 40998 bcd23ddeecef
implemented connectives in new monotonicity calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     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.148 +val add_quasi_clause = annotation_clause_from_quasi_clause #> add_assign_clause
   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