more work on frames in the new monotonicity calculus
authorblanchet
Mon Dec 06 13:26:23 2010 +0100 (2010-12-06)
changeset 409943bdb8df0daf0
parent 40993 52ee2a187cdb
child 40995 3cae30b60577
more work on frames in the new monotonicity calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     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.125  val add_mtypes_equal = add_mtype_comp Eq
   1.126  val add_is_sub_mtype = add_mtype_comp Leq
   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.203  val add_mtype_is_concrete = add_notin_mtype_fv Minus
   1.204  val add_mtype_is_complete = add_notin_mtype_fv Plus
   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))