author blanchet Mon Dec 06 13:26:23 2010 +0100 (2010-12-06) changeset 40994 3bdb8df0daf0 parent 40993 52ee2a187cdb child 40995 3cae30b60577
more work on frames in the new monotonicity calculus
```     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:26:23 2010 +0100
1.3 @@ -351,7 +351,7 @@
1.4  type comp = annotation_atom * annotation_atom * comp_op * var list
1.5  type assign_clause = assign list
1.6
1.7 -type constraint_set = assign list * comp list * assign_clause list
1.8 +type constraint_set = comp list * assign_clause list
1.9
1.10  fun string_for_comp_op Eq = "="
1.11    | string_for_comp_op Leq = "\<le>"
1.12 @@ -364,121 +364,117 @@
1.13    | string_for_assign_clause asgs =
1.14      space_implode " \<or> " (map string_for_assign asgs)
1.15
1.16 -fun add_assign_conjunct _ NONE = NONE
1.17 -  | add_assign_conjunct (x, a) (SOME asgs) =
1.18 -    case AList.lookup (op =) asgs x of
1.19 -      SOME a' => if a = a' then SOME asgs else NONE
1.20 -    | NONE => SOME ((x, a) :: asgs)
1.21 +fun add_assign (x, a) clauses =
1.22 +  if exists (fn [(x', a')] => x = x' andalso a <> a' | _ => false) clauses then
1.23 +    NONE
1.24 +  else
1.25 +    SOME ([(x, a)] :: clauses)fun add_assign_conjunct _ NONE = NONE
1.26
1.27  fun add_assign_disjunct _ NONE = NONE
1.28    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
1.29
1.30 -fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
1.31 +fun do_annotation_atom_comp Eq [] aa1 aa2 (cset as (comps, clauses)) =
1.32      (case (aa1, aa2) of
1.33 -       (A a1, A a2) => if a1 = a2 then SOME accum else NONE
1.34 +       (A a1, A a2) => if a1 = a2 then SOME cset else NONE
1.35       | (V x1, A a2) =>
1.36 -       SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
1.37 -     | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
1.38 -     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
1.39 -  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
1.40 +       clauses |> add_assign (x1, a2) |> Option.map (pair comps)
1.41 +     | (V _, V _) => SOME (insert (op =) (aa1, aa2, Eq, []) comps, clauses)
1.42 +     | _ => do_annotation_atom_comp Eq [] aa2 aa1 cset)
1.43 +  | do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
1.44      (case (aa1, aa2) of
1.45 -       (_, A Gen) => SOME accum
1.46 +       (_, A Gen) => SOME cset
1.47       | (A Gen, A _) => NONE
1.48 -     | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
1.49 -     | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
1.50 -  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
1.51 -    SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
1.52 +     | (A a1, A a2) => if a1 = a2 then SOME cset else NONE
1.53 +     | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses))
1.54 +  | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
1.55 +    SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses)
1.56
1.57  fun add_annotation_atom_comp cmp xs aa1 aa2
1.58 -                             ((asgs, comps, clauses) : constraint_set) =
1.59 +                             ((comps, clauses) : constraint_set) =
1.60    (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
1.61                         string_for_comp_op cmp ^ " " ^
1.62                         string_for_annotation_atom aa2);
1.63 -   case do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) of
1.64 +   case do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) of
1.65       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
1.66 -   | SOME (asgs, comps) => (asgs, comps, clauses))
1.67 +   | SOME cset => cset)
1.68
1.69  fun do_mtype_comp _ _ _ _ NONE = NONE
1.70 -  | do_mtype_comp _ _ MAlpha MAlpha accum = accum
1.71 +  | do_mtype_comp _ _ MAlpha MAlpha cset = cset
1.72    | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
1.73 -                  (SOME accum) =
1.74 -     accum |> do_annotation_atom_comp Eq xs aa1 aa2
1.75 -           |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
1.76 +                  (SOME cset) =
1.77 +    cset |> do_annotation_atom_comp Eq xs aa1 aa2
1.78 +         |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
1.79    | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
1.80 -                  (SOME accum) =
1.81 +                  (SOME cset) =
1.82      (if exists_alpha_sub_mtype M11 then
1.83 -       accum |> do_annotation_atom_comp Leq xs aa1 aa2
1.84 -             |> do_mtype_comp Leq xs M21 M11
1.85 -             |> (case aa2 of
1.86 -                   A Gen => I
1.87 -                 | A _ => do_mtype_comp Leq xs M11 M21
1.88 -                 | V x => do_mtype_comp Leq (x :: xs) M11 M21)
1.89 +       cset |> do_annotation_atom_comp Leq xs aa1 aa2
1.90 +            |> do_mtype_comp Leq xs M21 M11
1.91 +            |> (case aa2 of
1.92 +                  A Gen => I
1.93 +                | A _ => do_mtype_comp Leq xs M11 M21
1.94 +                | V x => do_mtype_comp Leq (x :: xs) M11 M21)
1.95       else
1.96 -       SOME accum)
1.97 +       SOME cset)
1.98      |> do_mtype_comp Leq xs M12 M22
1.99    | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
1.100 -                  accum =
1.101 -    (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
1.102 -     handle ListPair.UnequalLengths =>
1.103 +                  cset =
1.104 +    (cset |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
1.105 +     handle Library.UnequalLengths =>
1.106              raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
1.107 -  | do_mtype_comp _ _ (MType _) (MType _) accum =
1.108 -    accum (* no need to compare them thanks to the cache *)
1.109 +  | do_mtype_comp _ _ (MType _) (MType _) cset =
1.110 +    cset (* no need to compare them thanks to the cache *)
1.111    | do_mtype_comp cmp _ M1 M2 _ =
1.112      raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
1.113                   [M1, M2], [])
1.114
1.115 -fun add_mtype_comp cmp M1 M2 ((asgs, comps, clauses) : constraint_set) =
1.116 +fun add_mtype_comp cmp M1 M2 cset =
1.117    (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
1.118                         string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
1.119 -   case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
1.120 +   case SOME cset |> do_mtype_comp cmp [] M1 M2 of
1.121       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
1.122 -   | SOME (asgs, comps) => (asgs, comps, clauses))
1.123 +   | SOME cset => cset)
1.124
1.127
1.128  fun do_notin_mtype_fv _ _ _ NONE = NONE
1.129 -  | do_notin_mtype_fv Minus _ MAlpha accum = accum
1.130 +  | do_notin_mtype_fv Minus _ MAlpha cset = cset
1.131    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
1.132 -  | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, clauses)) =
1.133 -    SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
1.134 -  | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
1.135 -    SOME (asgs, insert (op =) clause clauses)
1.136 -  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) accum =
1.137 -    accum |> (if a <> Gen andalso sn = Plus then
1.138 -                do_notin_mtype_fv Plus clause M1
1.139 -              else
1.140 -                I)
1.141 -          |> (if a = Gen orelse sn = Plus then
1.142 -                do_notin_mtype_fv Minus clause M1
1.143 -              else
1.144 -                I)
1.145 -          |> do_notin_mtype_fv sn clause M2
1.146 -  | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) accum =
1.147 -    accum |> (case add_assign_disjunct (x, Gen) (SOME clause) of
1.148 -                NONE => I
1.149 -              | SOME clause' => do_notin_mtype_fv Plus clause' M1)
1.150 -          |> do_notin_mtype_fv Minus clause M1
1.151 -          |> do_notin_mtype_fv Plus clause M2
1.152 -  | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
1.153 -    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
1.154 -                        (SOME clause) of
1.155 -                NONE => I
1.156 -              | SOME clause' => do_notin_mtype_fv Plus clause' M1)
1.157 -          |> do_notin_mtype_fv Minus clause M2
1.158 -  | do_notin_mtype_fv sn clause (MPair (M1, M2)) accum =
1.159 -    accum |> fold (do_notin_mtype_fv sn clause) [M1, M2]
1.160 -  | do_notin_mtype_fv sn clause (MType (_, Ms)) accum =
1.161 -    accum |> fold (do_notin_mtype_fv sn clause) Ms
1.162 -  | do_notin_mtype_fv _ _ M _ =
1.163 -    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
1.164 +  | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME clauses) =
1.165 +    clauses |> add_assign (x, a)
1.166 +  | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) =
1.167 +    SOME (insert (op =) clause clauses)
1.168 +  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset =
1.169 +    cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus clause M1
1.170 +             else I)
1.171 +         |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus clause M1
1.172 +             else I)
1.173 +         |> do_notin_mtype_fv sn clause M2
1.174 +  | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset =
1.175 +    cset |> (case add_assign_disjunct (x, Gen) (SOME clause) of
1.176 +               NONE => I
1.177 +             | SOME clause' => do_notin_mtype_fv Plus clause' M1)
1.178 +         |> do_notin_mtype_fv Minus clause M1
1.179 +         |> do_notin_mtype_fv Plus clause M2
1.180 +  | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset =
1.181 +    cset |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
1.182 +                       (SOME clause) of
1.183 +               NONE => I
1.184 +             | SOME clause' => do_notin_mtype_fv Plus clause' M1)
1.185 +         |> do_notin_mtype_fv Minus clause M2
1.186 +  | do_notin_mtype_fv sn clause (MPair (M1, M2)) cset =
1.187 +    cset |> fold (do_notin_mtype_fv sn clause) [M1, M2]
1.188 +  | do_notin_mtype_fv sn clause (MType (_, Ms)) cset =
1.189 +    cset |> fold (do_notin_mtype_fv sn clause) Ms
1.190 + | do_notin_mtype_fv _ _ M _ =
1.191 +   raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
1.192
1.193 -fun add_notin_mtype_fv sn M ((asgs, comps, clauses) : constraint_set) =
1.194 +fun add_notin_mtype_fv sn M ((comps, clauses) : constraint_set) =
1.195    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
1.196                         (case sn of Minus => "concrete" | Plus => "complete"));
1.197 -   case do_notin_mtype_fv sn [] M (SOME (asgs, clauses)) of
1.198 +   case SOME clauses |> do_notin_mtype_fv sn [] M of
1.199       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
1.200 -   | SOME (asgs, clauses) => (asgs, comps, clauses))
1.201 +   | SOME clauses => (comps, clauses))
1.202
1.205 @@ -542,11 +538,11 @@
1.206                     :: accum)
1.207         (max_var downto 1) asgs
1.208
1.209 -fun print_problem asgs comps clauses =
1.210 -  trace_msg (fn () => "*** Problem:\n" ^
1.211 -                      cat_lines (map string_for_assign asgs @
1.212 -                                 map string_for_comp comps @
1.213 -                                 map string_for_assign_clause clauses))
1.214 +fun print_problem calculus comps clauses =
1.215 +  trace_msg (fn () =>
1.216 +                "*** Problem (calculus M" ^ string_of_int calculus ^ "):\n" ^
1.217 +                cat_lines (map string_for_comp comps @
1.218 +                           map string_for_assign_clause clauses))
1.219
1.220  fun print_solution asgs =
1.221    trace_msg (fn () => "*** Solution:\n" ^
1.222 @@ -557,13 +553,13 @@
1.223                               string_for_vars ", " xs)
1.224         |> space_implode "\n"))
1.225
1.226 -fun solve calculus max_var (asgs, comps, clauses) =
1.227 +fun solve calculus max_var (comps, clauses) =
1.228    let
1.229 +    val asgs = map_filter (fn [asg] => SOME asg | _ => NONE) clauses
1.230      fun do_assigns assigns =
1.231        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
1.232 -    val _ = print_problem asgs comps clauses
1.233 +    val _ = print_problem calculus comps clauses
1.234      val prop =
1.235 -      map prop_for_assign asgs @
1.236        map prop_for_comp comps @
1.237        map prop_for_assign_clause clauses @
1.238        (if calculus < 3 then
1.239 @@ -584,7 +580,7 @@
1.240        in
1.241          case snd (hd solvers) prop of
1.242            SatSolver.SATISFIABLE assigns => do_assigns assigns
1.243 -        | _ => NONE
1.244 +        | _ => (trace_msg (K "*** Unsolvable"); NONE)
1.245        end
1.246    end
1.247
1.248 @@ -596,6 +592,10 @@
1.249     frees: (styp * mtyp) list,
1.250     consts: (styp * mtyp) list}
1.251
1.252 +val string_for_frame =
1.253 +  commas o map (fn (j, aa) => "#" ^ string_of_int j ^ " |-> " ^
1.254 +                              string_for_annotation_atom aa)
1.255 +
1.256  type accumulator = mtype_context * constraint_set
1.257
1.258  val initial_gamma =
1.259 @@ -608,10 +608,45 @@
1.260  fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
1.261    {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
1.262     bound_frame = bound_frame
1.263 -                 |> filter_out (fn (depth, _) => depth = length bound_Ts - 1),
1.264 +                 |> filter_out (fn (j, _) => j = length bound_Ts - 1),
1.265     frees = frees, consts = consts}
1.266    handle List.Empty => initial_gamma (* FIXME: needed? *)
1.267
1.268 +fun set_frame bound_frame ({bound_Ts, bound_Ms, frees, consts, ...}
1.269 +                           : mtype_context) =
1.270 +  {bound_Ts = bound_Ts, bound_Ms = bound_Ms, bound_frame = bound_frame,
1.271 +   frees = frees, consts = consts}
1.272 +
1.273 +(* FIXME: make sure tracing messages are complete *)
1.274 +
1.275 +fun add_comp_frame a cmp frame =
1.276 +  (trace_msg (fn () => "*** Add " ^ string_for_annotation a ^
1.277 +                       string_for_comp_op cmp ^ " frame " ^
1.278 +                       string_for_frame frame);
1.279 +   fold (add_annotation_atom_comp cmp [] (A a) o snd) frame)
1.280 +
1.281 +fun add_bound_frame j frame =
1.282 +  let
1.283 +    val (new_frame, gen_frame) = List.partition (curry (op =) j o fst) frame
1.284 +  in
1.285 +    add_comp_frame New Leq new_frame
1.286 +    #> add_comp_frame Gen Eq gen_frame
1.287 +  end
1.288 +
1.289 +fun fresh_imp_frame ({max_fresh, ...} : mdata) sn =
1.290 +  let
1.291 +    fun do_var (j, A Fls) = (j, A (case sn of Plus => Fls | Minus => Tru))
1.292 +      | do_var (j, A Gen) = (j, A Gen)
1.293 +      | do_var (j, _) = (j, V (Unsynchronized.inc max_fresh))
1.294 +  in map do_var end
1.295 +
1.296 +fun add_imp_frames res_frame frame1 frame2 = I
1.297 +(*###
1.298 +  let
1.299 +    fun do_var_pair (j, aa0) (_, aa1) (_, aa2) =
1.300 +  in map3 do_var_pair res_frame frame1 frame2 end
1.301 +*)
1.302 +
1.303  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
1.304                               max_fresh, ...}) =
1.305    let
1.306 @@ -693,117 +728,115 @@
1.307        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
1.308                             Syntax.string_of_term ctxt t ^ " : _?");
1.309         case t of
1.310 -         Const (x as (s, T)) =>
1.311 +         @{const False} =>
1.312 +         (MRaw (t, bool_M), accum ||> add_comp_frame Fls Leq bound_frame)
1.313 +       | @{const True} =>
1.314 +         (MRaw (t, bool_M), accum ||> add_comp_frame Tru Leq bound_frame)
1.315 +       | Const (x as (s, T)) =>
1.316           (case AList.lookup (op =) consts x of
1.317              SOME M => (M, accum)
1.318            | NONE =>
1.319 -            case s of
1.320 -              @{const_name False} =>
1.321 -              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Fls))
1.322 -                                      (map snd bound_frame))
1.323 -            | @{const_name True} =>
1.324 -              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Tru))
1.325 -                                      (map snd bound_frame))
1.326 +            if not (could_exist_alpha_subtype alpha_T T) then
1.327 +              (mtype_for T, accum)
1.328 +            else case s of
1.329 +              @{const_name all} => do_all T accum
1.330 +            | @{const_name "=="} => do_equals T accum
1.331 +            | @{const_name All} => do_all T accum
1.332 +            | @{const_name Ex} =>
1.333 +              let val set_T = domain_type T in
1.334 +                do_term (Abs (Name.uu, set_T,
1.335 +                              @{const Not} \$ (HOLogic.mk_eq
1.336 +                                  (Abs (Name.uu, domain_type set_T,
1.337 +                                        @{const False}),
1.338 +                                   Bound 0)))) accum
1.339 +                |>> mtype_of_mterm
1.340 +              end
1.341 +            | @{const_name HOL.eq} => do_equals T accum
1.342 +            | @{const_name The} =>
1.343 +              (trace_msg (K "*** The"); raise UNSOLVABLE ())
1.344 +            | @{const_name Eps} =>
1.345 +              (trace_msg (K "*** Eps"); raise UNSOLVABLE ())
1.346 +            | @{const_name If} =>
1.347 +              do_robust_set_operation (range_type T) accum
1.348 +              |>> curry3 MFun bool_M (A Gen)
1.349 +            | @{const_name Pair} => do_pair_constr T accum
1.350 +            | @{const_name fst} => do_nth_pair_sel 0 T accum
1.351 +            | @{const_name snd} => do_nth_pair_sel 1 T accum
1.352 +            | @{const_name Id} =>
1.353 +              (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
1.354 +            | @{const_name converse} =>
1.355 +              let
1.356 +                val x = Unsynchronized.inc max_fresh
1.357 +                fun mtype_for_set T =
1.358 +                  MFun (mtype_for (domain_type T), V x, bool_M)
1.359 +                val ab_set_M = domain_type T |> mtype_for_set
1.360 +                val ba_set_M = range_type T |> mtype_for_set
1.361 +              in (MFun (ab_set_M, A Gen, ba_set_M), accum) end
1.362 +            | @{const_name trancl} => do_fragile_set_operation T accum
1.363 +            | @{const_name rel_comp} =>
1.364 +              let
1.365 +                val x = Unsynchronized.inc max_fresh
1.366 +                fun mtype_for_set T =
1.367 +                  MFun (mtype_for (domain_type T), V x, bool_M)
1.368 +                val bc_set_M = domain_type T |> mtype_for_set
1.369 +                val ab_set_M = domain_type (range_type T) |> mtype_for_set
1.370 +                val ac_set_M = nth_range_type 2 T |> mtype_for_set
1.371 +              in
1.372 +                (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
1.373 +                 accum)
1.374 +              end
1.375 +            | @{const_name image} =>
1.376 +              let
1.377 +                val a_M = mtype_for (domain_type (domain_type T))
1.378 +                val b_M = mtype_for (range_type (domain_type T))
1.379 +              in
1.380 +                (MFun (MFun (a_M, A Gen, b_M), A Gen,
1.381 +                       MFun (plus_set_mtype_for_dom a_M, A Gen,
1.382 +                             plus_set_mtype_for_dom b_M)), accum)
1.383 +              end
1.384 +            | @{const_name finite} =>
1.385 +              let val M1 = mtype_for (domain_type (domain_type T)) in
1.386 +                (MFun (plus_set_mtype_for_dom M1, A Gen, bool_M), accum)
1.387 +              end
1.388 +            | @{const_name Sigma} =>
1.389 +              let
1.390 +                val x = Unsynchronized.inc max_fresh
1.391 +                fun mtype_for_set T =
1.392 +                  MFun (mtype_for (domain_type T), V x, bool_M)
1.393 +                val a_set_T = domain_type T
1.394 +                val a_M = mtype_for (domain_type a_set_T)
1.395 +                val b_set_M =
1.396 +                  mtype_for_set (range_type (domain_type (range_type T)))
1.397 +                val a_set_M = mtype_for_set a_set_T
1.398 +                val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
1.399 +                val ab_set_M = mtype_for_set (nth_range_type 2 T)
1.400 +              in
1.401 +                (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
1.402 +                 accum)
1.403 +              end
1.404              | _ =>
1.405 -              if not (could_exist_alpha_subtype alpha_T T) then
1.406 -                (mtype_for T, accum)
1.407 -              else case s of
1.408 -                @{const_name all} => do_all T accum
1.409 -              | @{const_name "=="} => do_equals T accum
1.410 -              | @{const_name All} => do_all T accum
1.411 -              | @{const_name Ex} =>
1.412 -                let val set_T = domain_type T in
1.413 -                  do_term (Abs (Name.uu, set_T,
1.414 -                                @{const Not} \$ (HOLogic.mk_eq
1.415 -                                    (Abs (Name.uu, domain_type set_T,
1.416 -                                          @{const False}),
1.417 -                                     Bound 0)))) accum
1.418 -                  |>> mtype_of_mterm
1.419 -                end
1.420 -              | @{const_name HOL.eq} => do_equals T accum
1.421 -              | @{const_name The} =>
1.422 -                (trace_msg (K "*** The"); raise UNSOLVABLE ())
1.423 -              | @{const_name Eps} =>
1.424 -                (trace_msg (K "*** Eps"); raise UNSOLVABLE ())
1.425 -              | @{const_name If} =>
1.426 -                do_robust_set_operation (range_type T) accum
1.427 -                |>> curry3 MFun bool_M (A Gen)
1.428 -              | @{const_name Pair} => do_pair_constr T accum
1.429 -              | @{const_name fst} => do_nth_pair_sel 0 T accum
1.430 -              | @{const_name snd} => do_nth_pair_sel 1 T accum
1.431 -              | @{const_name Id} =>
1.432 -                (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
1.433 -              | @{const_name converse} =>
1.434 -                let
1.435 -                  val x = Unsynchronized.inc max_fresh
1.436 -                  fun mtype_for_set T =
1.437 -                    MFun (mtype_for (domain_type T), V x, bool_M)
1.438 -                  val ab_set_M = domain_type T |> mtype_for_set
1.439 -                  val ba_set_M = range_type T |> mtype_for_set
1.440 -                in (MFun (ab_set_M, A Gen, ba_set_M), accum) end
1.441 -              | @{const_name trancl} => do_fragile_set_operation T accum
1.442 -              | @{const_name rel_comp} =>
1.443 +              if s = @{const_name safe_The} then
1.444                  let
1.445 -                  val x = Unsynchronized.inc max_fresh
1.446 -                  fun mtype_for_set T =
1.447 -                    MFun (mtype_for (domain_type T), V x, bool_M)
1.448 -                  val bc_set_M = domain_type T |> mtype_for_set
1.449 -                  val ab_set_M = domain_type (range_type T) |> mtype_for_set
1.450 -                  val ac_set_M = nth_range_type 2 T |> mtype_for_set
1.451 -                in
1.452 -                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
1.453 -                   accum)
1.454 -                end
1.455 -              | @{const_name image} =>
1.456 -                let
1.457 -                  val a_M = mtype_for (domain_type (domain_type T))
1.458 -                  val b_M = mtype_for (range_type (domain_type T))
1.459 -                in
1.460 -                  (MFun (MFun (a_M, A Gen, b_M), A Gen,
1.461 -                         MFun (plus_set_mtype_for_dom a_M, A Gen,
1.462 -                               plus_set_mtype_for_dom b_M)), accum)
1.463 -                end
1.464 -              | @{const_name finite} =>
1.465 -                let val M1 = mtype_for (domain_type (domain_type T)) in
1.466 -                  (MFun (plus_set_mtype_for_dom M1, A Gen, bool_M), accum)
1.467 -                end
1.468 -              | @{const_name Sigma} =>
1.469 -                let
1.470 -                  val x = Unsynchronized.inc max_fresh
1.471 -                  fun mtype_for_set T =
1.472 -                    MFun (mtype_for (domain_type T), V x, bool_M)
1.473 -                  val a_set_T = domain_type T
1.474 -                  val a_M = mtype_for (domain_type a_set_T)
1.475 -                  val b_set_M =
1.476 -                    mtype_for_set (range_type (domain_type (range_type T)))
1.477 -                  val a_set_M = mtype_for_set a_set_T
1.478 -                  val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
1.479 -                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
1.480 -                in
1.481 -                  (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
1.482 -                   accum)
1.483 -                end
1.484 -              | _ =>
1.485 -                if s = @{const_name safe_The} then
1.486 -                  let
1.487 -                    val a_set_M = mtype_for (domain_type T)
1.488 -                    val a_M = dest_MFun a_set_M |> #1
1.489 -                  in (MFun (a_set_M, A Gen, a_M), accum) end
1.490 -                else if s = @{const_name ord_class.less_eq} andalso
1.491 -                        is_set_type (domain_type T) then
1.492 -                  do_fragile_set_operation T accum
1.493 -                else if is_sel s then
1.494 -                  (mtype_for_sel mdata x, accum)
1.495 -                else if is_constr ctxt stds x then
1.496 -                  (mtype_for_constr mdata x, accum)
1.497 -                else if is_built_in_const thy stds x then
1.498 -                  (fresh_mtype_for_type mdata true T, accum)
1.499 -                else
1.500 -                  let val M = mtype_for T in
1.501 -                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
1.502 -                          bound_frame = bound_frame, frees = frees,
1.503 -                          consts = (x, M) :: consts}, cset))
1.504 -                  end) |>> curry MRaw t
1.505 +                  val a_set_M = mtype_for (domain_type T)
1.506 +                  val a_M = dest_MFun a_set_M |> #1
1.507 +                in (MFun (a_set_M, A Gen, a_M), accum) end
1.508 +              else if s = @{const_name ord_class.less_eq} andalso
1.509 +                      is_set_type (domain_type T) then
1.510 +                do_fragile_set_operation T accum
1.511 +              else if is_sel s then
1.512 +                (mtype_for_sel mdata x, accum)
1.513 +              else if is_constr ctxt stds x then
1.514 +                (mtype_for_constr mdata x, accum)
1.515 +              else if is_built_in_const thy stds x then
1.516 +                (fresh_mtype_for_type mdata true T, accum)
1.517 +              else
1.518 +                let val M = mtype_for T in
1.519 +                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
1.520 +                        bound_frame = bound_frame, frees = frees,
1.521 +                        consts = (x, M) :: consts}, cset))
1.522 +                end)
1.523 +           |>> curry MRaw t
1.524 +           ||> apsnd (add_comp_frame Gen Eq bound_frame)
1.525           | Free (x as (_, T)) =>
1.526             (case AList.lookup (op =) frees x of
1.527                SOME M => (M, accum)
1.528 @@ -812,9 +845,12 @@
1.529                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
1.530                        bound_frame = bound_frame, frees = (x, M) :: frees,
1.531                        consts = consts}, cset))
1.532 -              end) |>> curry MRaw t
1.533 +              end)
1.534 +           |>> curry MRaw t ||> apsnd (add_comp_frame Gen Eq bound_frame)
1.535           | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
1.536 -         | Bound j => (MRaw (t, nth bound_Ms j), accum)
1.537 +         | Bound j =>
1.538 +           (MRaw (t, nth bound_Ms j),
1.539 +            accum ||> add_bound_frame (length bound_Ts - j - 1) bound_frame)
1.540           | Abs (s, T, t') =>
1.541             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
1.542                SOME t' =>
1.543 @@ -843,6 +879,18 @@
1.544                          val (m', accum) =
1.545                            do_term t' (accum |>> push_bound aa T M)
1.546                        in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
1.547 +         | (t0 as @{const implies}) \$ t1 \$ t2 =>
1.548 +           let
1.549 +             val frame1 = fresh_imp_frame mdata Minus bound_frame
1.550 +             val frame2 = fresh_imp_frame mdata Plus bound_frame
1.551 +             val (m0, accum) = accum |> do_term t0
1.552 +             val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
1.553 +             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
1.554 +           in
1.555 +             (MApp (MApp (m0, m1), m2),
1.556 +              accum |>> set_frame bound_frame
1.557 +                    ||> add_imp_frames bound_frame frame1 frame2)
1.558 +           end
1.559           | (t0 as Const (@{const_name All}, _))
1.560             \$ Abs (s', T', (t10 as @{const HOL.implies})
1.561                            \$ (t11 \$ Bound 0) \$ t12) =>
1.562 @@ -1071,7 +1119,7 @@
1.563                                  Syntax.string_of_typ ctxt alpha_T)
1.564      val mdata as {max_fresh, constr_mcache, ...} =
1.565        initial_mdata hol_ctxt binarize no_harmless alpha_T
1.566 -    val accum = (initial_gamma, ([], [], []))
1.567 +    val accum = (initial_gamma, ([], []))
1.568      val (nondef_ms, accum) =
1.569        ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
1.570                    |> fold (amass (consider_nondefinitional_axiom mdata))
```