src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41003 7e2a7bd55a00
parent 41002 11a442b472c7
child 41004 01f33bf79596
equal deleted inserted replaced
41002:11a442b472c7 41003:7e2a7bd55a00
   667    [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
   667    [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
   668    [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
   668    [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))],
   669    [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
   669    [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
   670    [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
   670    [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
   671 
   671 
       
   672 val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
       
   673 val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
       
   674 val conj_triple = ("\<and>", conj_clauses, @{const conj})
       
   675 val disj_triple = ("\<or>", disj_clauses, @{const disj})
       
   676 val imp_triple = ("\<implies>", imp_clauses, @{const implies})
       
   677 
   672 fun add_annotation_clause_from_quasi_clause _ NONE = NONE
   678 fun add_annotation_clause_from_quasi_clause _ NONE = NONE
   673   | add_annotation_clause_from_quasi_clause [] accum = accum
   679   | add_annotation_clause_from_quasi_clause [] accum = accum
   674   | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum =
   680   | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum =
   675     case aa of
   681     case aa of
   676       A a' => if annotation_comp cmp a' a then NONE
   682       A a' => if annotation_comp cmp a' a then NONE
   730 fun add_app _ [] [] = I
   736 fun add_app _ [] [] = I
   731   | add_app fun_aa res_frame arg_frame =
   737   | add_app fun_aa res_frame arg_frame =
   732     add_comp_frame (A New) Leq arg_frame
   738     add_comp_frame (A New) Leq arg_frame
   733     #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
   739     #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
   734     #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
   740     #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
       
   741 
       
   742 fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
       
   743                         (accum as ({frame, ...}, _)) =
       
   744   let
       
   745     val mtype_for = fresh_mtype_for_type mdata false
       
   746     val frame1 = fresh_frame mdata (SOME Tru) NONE frame
       
   747     val frame2 = fresh_frame mdata (SOME Fls) NONE frame
       
   748     val (m1, accum) = accum |>> set_frame frame1 |> do_t1
       
   749     val (m2, accum) = accum |>> set_frame frame2 |> do_t2
       
   750   in
       
   751     (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
       
   752      accum |>> set_frame frame
       
   753            ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
       
   754                                             frame2))
       
   755   end
   735 
   756 
   736 fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   757 fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   737                              max_fresh, ...}) =
   758                              max_fresh, ...}) =
   738   let
   759   let
   739     fun is_enough_eta_expanded t =
   760     fun is_enough_eta_expanded t =
   790     fun do_nth_pair_sel n T =
   811     fun do_nth_pair_sel n T =
   791       case mtype_for (domain_type T) of
   812       case mtype_for (domain_type T) of
   792         M as MPair (a_M, b_M) =>
   813         M as MPair (a_M, b_M) =>
   793         pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   814         pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   794       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   815       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   795     and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
   816     and do_connect triple t1 t2 =
   796       let
   817       consider_connective mdata triple (do_term t1) (do_term t2)
   797         val frame1 = fresh_frame mdata (SOME Tru) NONE frame
       
   798         val frame2 = fresh_frame mdata (SOME Fls) NONE frame
       
   799         val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
       
   800         val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
       
   801       in
       
   802         (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
       
   803          accum |>> set_frame frame
       
   804                ||> apsnd (add_connective_frames conn mk_quasi_clauses
       
   805                                                 frame frame1 frame2))
       
   806       end
       
   807     and do_term t
   818     and do_term t
   808             (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
   819             (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
   809                        cset)) =
   820                        cset)) =
   810       (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   821       (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   811                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   822                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   958                         val M = mtype_for T
   969                         val M = mtype_for T
   959                         val aa = V (Unsynchronized.inc max_fresh)
   970                         val aa = V (Unsynchronized.inc max_fresh)
   960                         val (m', accum) =
   971                         val (m', accum) =
   961                           do_term t' (accum |>> push_bound aa T M)
   972                           do_term t' (accum |>> push_bound aa T M)
   962                       in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   973                       in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   963          | @{const Not} $ t1 =>
   974          | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
   964            do_connect "\<implies>" imp_clauses @{const implies} t1
   975          | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
   965                       @{const False} accum
   976          | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
   966          | (t0 as @{const conj}) $ t1 $ t2 =>
   977          | @{const implies} $ t1 $ t2 => do_connect imp_triple t1 t2 accum
   967            do_connect "\<and>" conj_clauses t0 t1 t2 accum
       
   968          | (t0 as @{const disj}) $ t1 $ t2 =>
       
   969            do_connect "\<or>" disj_clauses t0 t1 t2 accum
       
   970          | (t0 as @{const implies}) $ t1 $ t2 =>
       
   971            do_connect "\<implies>" imp_clauses t0 t1 t2 accum
       
   972          | Const (@{const_name Let}, _) $ t1 $ t2 =>
   978          | Const (@{const_name Let}, _) $ t1 $ t2 =>
   973            do_term (betapply (t2, t1)) accum
   979            do_term (betapply (t2, t1)) accum
   974          | t1 $ t2 =>
   980          | t1 $ t2 =>
   975            let
   981            let
   976              fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
   982              fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
  1045             (MApp (MRaw (Const quant_x,
  1051             (MApp (MRaw (Const quant_x,
  1046                          MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
  1052                          MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
  1047                    MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
  1053                    MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
  1048              accum |>> pop_bound)
  1054              accum |>> pop_bound)
  1049           end
  1055           end
       
  1056         fun do_connect triple neg1 t1 t2 =
       
  1057           consider_connective mdata triple
       
  1058               (do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
  1050         fun do_equals x t1 t2 =
  1059         fun do_equals x t1 t2 =
  1051           case sn of
  1060           case sn of
  1052             Plus => do_term t accum
  1061             Plus => do_term t accum
  1053           | Minus => consider_general_equals mdata false x t1 t2 accum
  1062           | Minus => consider_general_equals mdata false x t1 t2 accum
  1054       in
  1063       in
  1062          | @{const Trueprop} $ t1 =>
  1071          | @{const Trueprop} $ t1 =>
  1063            let val (m1, accum) = do_formula sn t1 accum in
  1072            let val (m1, accum) = do_formula sn t1 accum in
  1064              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
  1073              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
  1065                     m1), accum)
  1074                     m1), accum)
  1066            end
  1075            end
  1067          | @{const Not} $ t1 =>
       
  1068            let val (m1, accum) = do_formula (negate_sign sn) t1 accum in
       
  1069              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
       
  1070               accum)
       
  1071            end
       
  1072          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
  1076          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
  1073            do_quantifier x s1 T1 t1
  1077            do_quantifier x s1 T1 t1
  1074          | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
  1078          | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
  1075            (case sn of
  1079            (case sn of
  1076               Plus => do_quantifier x0 s1 T1 t1'
  1080               Plus => do_quantifier x0 s1 T1 t1'
  1081                           $ Abs (Name.uu, T1, @{const False}))) accum)
  1085                           $ Abs (Name.uu, T1, @{const False}))) accum)
  1082          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
  1086          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
  1083            do_equals x t1 t2
  1087            do_equals x t1 t2
  1084          | Const (@{const_name Let}, _) $ t1 $ t2 =>
  1088          | Const (@{const_name Let}, _) $ t1 $ t2 =>
  1085            do_formula sn (betapply (t2, t1)) accum
  1089            do_formula sn (betapply (t2, t1)) accum
  1086          | (t0 as Const (s0, _)) $ t1 $ t2 =>
  1090          | @{const Pure.conjunction} $ t1 $ t2 =>
  1087            if s0 = @{const_name "==>"} orelse
  1091            do_connect meta_conj_triple false t1 t2 accum
  1088               s0 = @{const_name Pure.conjunction} orelse
  1092          | @{const "==>"} $ t1 $ t2 =>
  1089               s0 = @{const_name conj} orelse s0 = @{const_name disj} orelse
  1093            do_connect meta_imp_triple true t1 t2 accum
  1090               s0 = @{const_name implies} then
  1094          | @{const Not} $ t1 =>
  1091              let
  1095            do_connect imp_triple true t1 @{const False} accum
  1092                val impl = (s0 = @{const_name "==>"} orelse
  1096          | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
  1093                            s0 = @{const_name implies})
  1097          | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
  1094                val (m1, accum) = do_formula (sn |> impl ? negate_sign) t1 accum
  1098          | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
  1095                val (m2, accum) = do_formula sn t2 accum
       
  1096              in
       
  1097                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
       
  1098                 accum)
       
  1099              end
       
  1100            else
       
  1101              do_term t accum
       
  1102          | _ => do_term t accum)
  1099          | _ => do_term t accum)
  1103       end
  1100       end
  1104       |> tap (fn (m, (gamma, _)) =>
  1101       |> tap (fn (m, (gamma, _)) =>
  1105                  trace_msg (fn () => string_for_mcontext ctxt t gamma ^
  1102                  trace_msg (fn () => string_for_mcontext ctxt t gamma ^
  1106                                      " \<turnstile> " ^
  1103                                      " \<turnstile> " ^