# HG changeset patch # User blanchet # Date 1291638636 -3600 # Node ID 67e11a73532a82efeca771715d3d43715b3b01f4 # Parent 63112be4a46975b59d5a6dce645656ce71478a1f implemented connectives in new monotonicity calculus diff -r 63112be4a469 -r 67e11a73532a src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:29:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:30:36 2010 +0100 @@ -378,14 +378,15 @@ fun add_assign_disjunct _ NONE = NONE | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs) +val add_assign_clause = insert (op =) + fun annotation_comp Eq a1 a2 = (a1 = a2) | annotation_comp Neq a1 a2 = (a1 <> a2) | annotation_comp Leq a1 a2 = (a1 = a2 orelse a2 = Gen) -fun comp_op_sign Eq = Plus - | comp_op_sign Neq = Minus - | comp_op_sign Leq = - raise BAD ("Nitpick_Mono.comp_op_sign", "unexpected \"Leq\"") +fun sign_for_comp_op Eq = Plus + | sign_for_comp_op Neq = Minus + | sign_for_comp_op Leq = raise BAD ("sign_for_comp_op", "unexpected \"Leq\"") fun do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) = (case (aa1, aa2) of @@ -395,15 +396,14 @@ (case (aa1, aa2) of (A a1, A a2) => if annotation_comp cmp a1 a2 then SOME cset else NONE | (V x1, A a2) => - clauses |> add_assign_literal (x1, (comp_op_sign cmp, a2)) + clauses |> add_assign_literal (x1, (sign_for_comp_op cmp, a2)) |> Option.map (pair comps) | (A _, V _) => do_annotation_atom_comp cmp [] aa2 aa1 cset | (V _, V _) => SOME (insert (op =) (aa1, aa2, cmp, []) comps, clauses)) | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) = SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses) -fun add_annotation_atom_comp cmp xs aa1 aa2 - ((comps, clauses) : constraint_set) = +fun add_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) = (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ " " ^ string_for_annotation_atom aa2); @@ -482,7 +482,7 @@ | do_notin_mtype_fv _ _ M _ = raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], []) -fun add_notin_mtype_fv sn M ((comps, clauses) : constraint_set) = +fun add_notin_mtype_fv sn M (comps, clauses) = (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^ (case sn of Minus => "concrete" | Plus => "complete")); case SOME clauses |> do_notin_mtype_fv sn [] M of @@ -610,11 +610,6 @@ frees: (styp * mtyp) list, consts: (styp * mtyp) list} -val string_for_frame = - map (fn (j, aa) => "#" ^ string_of_int j ^ " |-> " ^ - string_for_annotation_atom aa) - #> commas #> enclose "[" "]" - type accumulator = mtype_context * constraint_set val initial_gamma = @@ -638,11 +633,7 @@ (* FIXME: make sure tracing messages are complete *) -fun add_comp_frame a cmp frame = - (trace_msg (fn () => "*** Add " ^ string_for_annotation a ^ " " ^ - string_for_comp_op cmp ^ " " ^ - string_for_frame frame); - fold (add_annotation_atom_comp cmp [] (A a) o snd) frame) +fun add_comp_frame a cmp = fold (add_annotation_atom_comp cmp [] (A a) o snd) fun add_bound_frame j frame = let @@ -652,38 +643,62 @@ #> add_comp_frame Gen Eq gen_frame end -fun fresh_imp_frame ({max_fresh, ...} : mdata) sn = - let - fun do_var (j, A Fls) = (j, A (case sn of Plus => Fls | Minus => Tru)) - | do_var (j, A Gen) = (j, A Gen) - | do_var (j, _) = (j, V (Unsynchronized.inc max_fresh)) - in map do_var end +fun fresh_frame ({max_fresh, ...} : mdata) fls tru = + map (apsnd (fn aa => + case (aa, fls, tru) of + (A Fls, SOME a, _) => A a + | (A Tru, _, SOME a) => A a + | (A Gen, _, _) => A Gen + | _ => V (Unsynchronized.inc max_fresh))) -fun do_not_var j aa0 aa1 _ = I -(* -x1 ~= T | x0 = F -x1 ~= F | x0 = T -x1 ~= G | x0 = G -x1 ~= N | x0 = G -*) +fun conj_clauses res_aa aa1 aa2 = + [[(aa1, (Neq, Tru)), (aa2, (Neq, Tru)), (res_aa, (Eq, Tru))], + [(aa1, (Neq, Fls)), (res_aa, (Eq, Fls))], + [(aa2, (Neq, Fls)), (res_aa, (Eq, Fls))], + [(aa1, (Neq, Gen)), (aa2, (Eq, Fls)), (res_aa, (Eq, Gen))], + [(aa1, (Neq, New)), (aa2, (Eq, Fls)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] + +fun disj_clauses res_aa aa1 aa2 = + [[(aa1, (Neq, Tru)), (res_aa, (Eq, Tru))], + [(aa2, (Neq, Tru)), (res_aa, (Eq, Tru))], + [(aa1, (Neq, Fls)), (aa2, (Neq, Fls)), (res_aa, (Eq, Fls))], + [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], + [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Tru)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Tru)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] -fun do_conj_var j aa0 aa1 aa2 = I -(* - (x1 ≠ T | x2 ≠ T | x0 = T) & - (x1 ≠ F | x0 = F) & - (x2 ≠ F | x0 = F) & - (x1 ≠ G | x2 = F | x0 = G) & - (x1 ≠ N | x2 = F | x0 = G) & - (x1 = F | x2 ≠ G | x0 = G) & - (x1 = F | x2 ≠ N | x0 = G)" -*) +fun imp_clauses res_aa aa1 aa2 = + [[(aa1, (Neq, Fls)), (res_aa, (Eq, Tru))], + [(aa2, (Neq, Tru)), (res_aa, (Eq, Tru))], + [(aa1, (Neq, Tru)), (aa2, (Neq, Fls)), (res_aa, (Eq, Fls))], + [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], + [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], + [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] + +fun annotation_literal_from_quasi_literal (aa, (cmp, a)) = + case aa of + A a' => if annotation_comp cmp a' a then NONE + else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) + | V x => SOME (x, (sign_for_comp_op cmp, a)) -fun do_disj_var j aa0 aa1 aa2 = I -fun do_imp_var j aa0 aa1 aa2 = I +val annotation_clause_from_quasi_clause = + map_filter annotation_literal_from_quasi_literal + +val add_quasi_clause = annotation_clause_from_quasi_clause #> add_assign_clause -fun add_connective_frames do_var res_frame frame1 frame2 = - fold I (map3 (fn (j, aa0) => fn (_, aa1) => fn (_, aa2) => - do_var j aa0 aa1 aa2) res_frame frame1 frame2) +fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 = + (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^ + string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^ + string_for_annotation_atom aa2); + fold add_quasi_clause (mk_quasi_clauses res_aa aa1 aa2)) + +fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 = + fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => + add_connective_var conn mk_quasi_clauses res_aa aa1 aa2) + res_frame frame1 frame2) fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T, max_fresh, ...}) = @@ -705,10 +720,13 @@ (gamma, cset |> add_mtype_is_complete abs_M)) end fun do_equals T (gamma, cset) = - let val M = mtype_for (domain_type T) in - (MFun (M, A Gen, MFun (M, V (Unsynchronized.inc max_fresh), - mtype_for (nth_range_type 2 T))), - (gamma, cset |> add_mtype_is_concrete M)) + let + val M = mtype_for (domain_type T) + val aa = V (Unsynchronized.inc max_fresh) + in + (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))), + (gamma, cset |> add_mtype_is_concrete M + |> add_annotation_atom_comp Leq [] (A Fls) aa)) end fun do_robust_set_operation T (gamma, cset) = let @@ -761,16 +779,18 @@ MApp (bound_m, MRaw (Bound 0, M1))), body_m))), accum) end - and do_connect do_var t0 t1 t2 (accum as ({bound_frame, ...}, _)) = + and do_connect conn mk_quasi_clauses t0 t1 t2 + (accum as ({bound_frame, ...}, _)) = let - val frame1 = fresh_imp_frame mdata Minus bound_frame - val frame2 = fresh_imp_frame mdata Plus bound_frame + val frame1 = fresh_frame mdata (SOME Tru) NONE bound_frame + val frame2 = fresh_frame mdata (SOME Fls) NONE bound_frame val (m1, accum) = accum |>> set_frame frame1 |> do_term t1 val (m2, accum) = accum |>> set_frame frame2 |> do_term t2 in (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum |>> set_frame bound_frame - ||> add_connective_frames do_var bound_frame frame1 frame2) + ||> apsnd (add_connective_frames conn mk_quasi_clauses + bound_frame frame1 frame2)) end and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts}, cset)) = @@ -929,29 +949,20 @@ do_term t' (accum |>> push_bound aa T M) in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end)) | (t0 as Const (@{const_name All}, _)) - $ Abs (s', T', (t10 as @{const HOL.implies}) - $ (t11 $ Bound 0) $ t12) => + $ Abs (s', T', (t10 as @{const implies}) $ (t11 $ Bound 0) $ t12) => do_bounded_quantifier t0 s' T' t10 t11 t12 accum | (t0 as Const (@{const_name Ex}, _)) - $ Abs (s', T', (t10 as @{const HOL.conj}) - $ (t11 $ Bound 0) $ t12) => + $ Abs (s', T', (t10 as @{const conj}) $ (t11 $ Bound 0) $ t12) => do_bounded_quantifier t0 s' T' t10 t11 t12 accum - | (t0 as @{const Not}) $ t1 => - let - val frame1 = fresh_imp_frame mdata Minus bound_frame - val (m1, accum) = accum |>> set_frame frame1 |> do_term t1 - in - (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), - accum |>> set_frame bound_frame - ||> add_connective_frames do_not_var bound_frame frame1 - frame1) - end + | @{const Not} $ t1 => + do_connect "\" imp_clauses @{const implies} t1 + @{const False} accum | (t0 as @{const conj}) $ t1 $ t2 => - do_connect do_conj_var t0 t1 t2 accum + do_connect "\" conj_clauses t0 t1 t2 accum | (t0 as @{const disj}) $ t1 $ t2 => - do_connect do_disj_var t0 t1 t2 accum + do_connect "\" disj_clauses t0 t1 t2 accum | (t0 as @{const implies}) $ t1 $ t2 => - do_connect do_imp_var t0 t1 t2 accum + do_connect "\" imp_clauses t0 t1 t2 accum | Const (@{const_name Let}, _) $ t1 $ t2 => do_term (betapply (t2, t1)) accum | t1 $ t2 => @@ -1053,12 +1064,12 @@ | (t0 as Const (s0, _)) $ t1 $ t2 => if s0 = @{const_name "==>"} orelse s0 = @{const_name Pure.conjunction} orelse - s0 = @{const_name HOL.conj} orelse - s0 = @{const_name HOL.disj} orelse - s0 = @{const_name HOL.implies} then + s0 = @{const_name conj} orelse + s0 = @{const_name disj} orelse + s0 = @{const_name implies} then let val impl = (s0 = @{const_name "==>"} orelse - s0 = @{const_name HOL.implies}) + s0 = @{const_name implies}) val (m1, accum) = do_formula (sn |> impl ? negate_sign) t1 accum val (m2, accum) = do_formula sn t2 accum @@ -1146,8 +1157,8 @@ do_all t0 s0 T1 t1 accum | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => consider_general_equals mdata true x t1 t2 accum - | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum - | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum + | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum + | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\ \do_formula", [t]) in do_formula t end