src/HOL/Tools/Nitpick/nitpick_mono.ML
author blanchet
Tue, 09 Mar 2010 09:25:23 +0100
changeset 35665 ff2bf50505ab
parent 35386 45a4e19d3ebd
child 35671 ed2c3830d881
permissions -rw-r--r--
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33852
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_mono.ML
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
     3
    Copyright   2009, 2010
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     4
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
     5
Monotonicity inference for higher-order logic.
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     8
signature NITPICK_MONO =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
    10
  type hol_context = Nitpick_HOL.hol_context
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    11
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    12
  val formulas_monotonic :
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
    13
    hol_context -> bool -> typ -> term list * term list -> bool
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    14
  val finitize_funs :
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    15
    hol_context -> bool -> (typ option * bool option) list -> typ
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    16
    -> term list * term list -> term list * term list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    19
structure Nitpick_Mono : NITPICK_MONO =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    21
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    22
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    23
open Nitpick_HOL
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    24
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
type var = int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
    27
datatype sign = Plus | Minus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
datatype sign_atom = S of sign | V of var
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    30
type literal = var * sign
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    31
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    32
datatype mtyp =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    33
  MAlpha |
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    34
  MFun of mtyp * sign_atom * mtyp |
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    35
  MPair of mtyp * mtyp |
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    36
  MType of string * mtyp list |
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    37
  MRec of string * typ list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    38
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    39
datatype mterm =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
    40
  MRaw of term * mtyp |
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    41
  MAbs of string * typ * mtyp * sign_atom * mterm |
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    42
  MApp of mterm * mterm
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    43
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    44
type mdata =
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
    45
  {hol_ctxt: hol_context,
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35079
diff changeset
    46
   binarize: bool,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
   alpha_T: typ,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    48
   no_harmless: bool,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
   max_fresh: int Unsynchronized.ref,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    50
   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    51
   constr_mcache: (styp * mtyp) list Unsynchronized.ref}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    52
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    53
exception MTYPE of string * mtyp list * typ list
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    54
exception MTERM of string * mterm list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    55
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    56
(* string -> unit *)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
    57
fun print_g (_ : string) = ()
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    58
(* val print_g = tracing *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    59
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
(* var -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    61
val string_for_var = signed_string_of_int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    62
(* string -> var list -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    63
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    64
  | string_for_vars sep xs = space_implode sep (map string_for_var xs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    65
fun subscript_string_for_vars sep xs =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    66
  if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    67
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
(* sign -> string *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
    69
fun string_for_sign Plus = "+"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
    70
  | string_for_sign Minus = "-"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    71
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    72
(* sign -> sign -> sign *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
    73
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    74
(* sign -> sign *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
    75
val negate = xor Minus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    76
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    77
(* sign_atom -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    78
fun string_for_sign_atom (S sn) = string_for_sign sn
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    79
  | string_for_sign_atom (V x) = string_for_var x
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    80
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    81
(* literal -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    82
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    83
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    84
val bool_M = MType (@{type_name bool}, [])
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
    85
val dummy_M = MType (nitpick_prefix ^ "dummy", [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    86
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    87
(* mtyp -> bool *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    88
fun is_MRec (MRec _) = true
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    89
  | is_MRec _ = false
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    90
(* mtyp -> mtyp * sign_atom * mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    91
fun dest_MFun (MFun z) = z
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
    92
  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    94
val no_prec = 100
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    95
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    96
(* mtyp -> int *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    97
fun precedence_of_mtype (MFun _) = 1
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    98
  | precedence_of_mtype (MPair _) = 2
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
    99
  | precedence_of_mtype _ = no_prec
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   100
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   101
(* mtyp -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   102
val string_for_mtype =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   103
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   104
    (* int -> mtyp -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   105
    fun aux outer_prec M =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
      let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   107
        val prec = precedence_of_mtype M
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   108
        val need_parens = (prec < outer_prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   110
        (if need_parens then "(" else "") ^
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   111
        (if M = dummy_M then
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   112
           "_"
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   113
         else case M of
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   114
             MAlpha => "\<alpha>"
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   115
           | MFun (M1, a, M2) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   116
             aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   117
             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   118
           | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   119
           | MType (s, []) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   120
             if s = @{type_name prop} orelse s = @{type_name bool} then "o"
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   121
             else s
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   122
           | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   123
           | MRec (s, _) => "[" ^ s ^ "]") ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   124
        (if need_parens then ")" else "")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   125
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   126
  in aux 0 end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   127
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   128
(* mtyp -> mtyp list *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   129
fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   130
  | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   131
  | flatten_mtype M = [M]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   132
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   133
(* mterm -> bool *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   134
fun precedence_of_mterm (MRaw _) = no_prec
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   135
  | precedence_of_mterm (MAbs _) = 1
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   136
  | precedence_of_mterm (MApp _) = 2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   138
(* Proof.context -> mterm -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   139
fun string_for_mterm ctxt =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   140
  let
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   141
    (* mtype -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   142
    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   143
    (* int -> mterm -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   144
    fun aux outer_prec m =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   145
      let
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   146
        val prec = precedence_of_mterm m
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   147
        val need_parens = (prec < outer_prec)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   148
      in
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   149
        (if need_parens then "(" else "") ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   150
        (case m of
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   151
           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   152
         | MAbs (s, _, M, a, m) =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   153
           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   154
           string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   155
         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   156
        (if need_parens then ")" else "")
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   157
      end
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   158
  in aux 0 end
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   159
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   160
(* mterm -> mtyp *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   161
fun mtype_of_mterm (MRaw (_, M)) = M
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   162
  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   163
  | mtype_of_mterm (MApp (m1, _)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   164
    case mtype_of_mterm m1 of
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   165
      MFun (_, _, M12) => M12
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   166
    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   167
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   168
(* mterm -> mterm * mterm list *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   169
fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   170
  | strip_mcomb m = (m, [])
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   171
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   172
(* hol_context -> bool -> bool -> typ -> mdata *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   173
fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35079
diff changeset
   174
  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   175
    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   176
    datatype_mcache = Unsynchronized.ref [],
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   177
    constr_mcache = Unsynchronized.ref []} : mdata)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
(* typ -> typ -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34123
diff changeset
   181
    T = alpha_T orelse (not (is_fp_iterator_type T) andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34123
diff changeset
   182
                        exists (could_exist_alpha_subtype alpha_T) Ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   183
  | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   184
(* theory -> typ -> typ -> bool *)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   185
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   186
    could_exist_alpha_subtype alpha_T T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   187
  | could_exist_alpha_sub_mtype thy alpha_T T =
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   188
    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   189
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   190
(* mtyp -> bool *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   191
fun exists_alpha_sub_mtype MAlpha = true
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   192
  | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   193
    exists exists_alpha_sub_mtype [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   194
  | exists_alpha_sub_mtype (MPair (M1, M2)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   195
    exists exists_alpha_sub_mtype [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   196
  | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   197
  | exists_alpha_sub_mtype (MRec _) = true
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   198
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   199
(* mtyp -> bool *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   200
fun exists_alpha_sub_mtype_fresh MAlpha = true
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   201
  | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   202
  | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   203
    exists_alpha_sub_mtype_fresh M2
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   204
  | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   205
    exists exists_alpha_sub_mtype_fresh [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   206
  | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   207
    exists exists_alpha_sub_mtype_fresh Ms
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   208
  | exists_alpha_sub_mtype_fresh (MRec _) = true
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   209
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   210
(* string * typ list -> mtyp list -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   211
fun constr_mtype_for_binders z Ms =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   212
  fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   213
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   214
(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   215
fun repair_mtype _ _ MAlpha = MAlpha
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   216
  | repair_mtype cache seen (MFun (M1, a, M2)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   217
    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   218
  | repair_mtype cache seen (MPair Mp) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   219
    MPair (pairself (repair_mtype cache seen) Mp)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   220
  | repair_mtype cache seen (MType (s, Ms)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   221
    MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   222
  | repair_mtype cache seen (MRec (z as (s, _))) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
    case AList.lookup (op =) cache z |> the of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   224
      MRec _ => MType (s, [])
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   225
    | M => if member (op =) seen M then MType (s, [])
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   226
           else repair_mtype cache (M :: seen) M
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   228
(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   229
fun repair_datatype_mcache cache =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   230
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   231
    (* (string * typ list) * mtyp -> unit *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   232
    fun repair_one (z, M) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   233
      Unsynchronized.change cache
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   234
          (AList.update (op =) (z, repair_mtype (!cache) [] M))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   235
  in List.app repair_one (rev (!cache)) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   236
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   237
(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   238
fun repair_constr_mcache dtype_cache constr_mcache =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   240
    (* styp * mtyp -> unit *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   241
    fun repair_one (x, M) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   242
      Unsynchronized.change constr_mcache
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   243
          (AList.update (op =) (x, repair_mtype dtype_cache [] M))
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   244
  in List.app repair_one (!constr_mcache) end
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   245
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   246
(* typ -> bool *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   247
fun is_fin_fun_supported_type @{typ prop} = true
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   248
  | is_fin_fun_supported_type @{typ bool} = true
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   249
  | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   250
  | is_fin_fun_supported_type _ = false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   251
(* typ -> typ -> term -> term option *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   252
fun fin_fun_body _ _ (t as @{term False}) = SOME t
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   253
  | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   254
  | fin_fun_body dom_T ran_T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   255
                 ((t0 as Const (@{const_name If}, _))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   256
                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   257
                  $ t2 $ t3) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   258
    (if loose_bvar1 (t1', 0) then
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   259
       NONE
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   260
     else case fin_fun_body dom_T ran_T t3 of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   261
       NONE => NONE
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   262
     | SOME t3 =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   263
       SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   264
                $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   265
  | fin_fun_body _ _ _ = NONE
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   266
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   267
(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   268
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   269
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   270
    val M1 = fresh_mtype_for_type mdata T1
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   271
    val M2 = fresh_mtype_for_type mdata T2
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   272
    val a = if is_fin_fun_supported_type (body_type T2) andalso
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   273
               exists_alpha_sub_mtype_fresh M1 then
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   274
              V (Unsynchronized.inc max_fresh)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   275
            else
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   276
              S Minus
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   277
  in (M1, a, M2) end
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   278
(* mdata -> typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   279
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   280
                                    datatype_mcache, constr_mcache, ...}) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   281
  let
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   282
    (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   283
    fun do_type T =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   284
      if T = alpha_T then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   285
        MAlpha
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
      else case T of
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   287
        Type (@{type_name fun}, [T1, T2]) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   288
        MFun (fresh_mfun_for_fun_type mdata T1 T2)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   289
      | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
      | Type (z as (s, _)) =>
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   291
        if could_exist_alpha_sub_mtype thy alpha_T T then
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   292
          case AList.lookup (op =) (!datatype_mcache) z of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   293
            SOME M => M
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   294
          | NONE =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   295
            let
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   296
              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
35219
15a5f213ef5b fix bug in Nitpick's monotonicity code w.r.t. binary integers
blanchet
parents: 35190
diff changeset
   297
              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   298
              val (all_Ms, constr_Ms) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   299
                fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   300
                             let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   301
                               val binder_Ms = map do_type (binder_types T')
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   302
                               val new_Ms = filter exists_alpha_sub_mtype_fresh
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   303
                                                   binder_Ms
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   304
                               val constr_M = constr_mtype_for_binders z
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   305
                                                                       binder_Ms
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   306
                             in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   307
                               (union (op =) new_Ms all_Ms,
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   308
                                constr_M :: constr_Ms)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
                             end)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   310
                         xs ([], [])
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   311
              val M = MType (s, all_Ms)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   312
              val _ = Unsynchronized.change datatype_mcache
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   313
                          (AList.update (op =) (z, M))
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   314
              val _ = Unsynchronized.change constr_mcache
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   315
                          (append (xs ~~ constr_Ms))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   316
            in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   317
              if forall (not o is_MRec o snd) (!datatype_mcache) then
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   318
                (repair_datatype_mcache datatype_mcache;
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   319
                 repair_constr_mcache (!datatype_mcache) constr_mcache;
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   320
                 AList.lookup (op =) (!datatype_mcache) z |> the)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   321
              else
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   322
                M
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   323
            end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   324
        else
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   325
          MType (s, [])
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   326
      | _ => MType (Refute.string_of_typ T, [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   327
  in do_type end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   329
(* mtyp -> mtyp list *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   330
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   331
  | prodM_factors M = [M]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   332
(* mtyp -> mtyp list * mtyp *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   333
fun curried_strip_mtype (MFun (M1, _, M2)) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   334
    curried_strip_mtype M2 |>> append (prodM_factors M1)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   335
  | curried_strip_mtype M = ([], M)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   336
(* string -> mtyp -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   337
fun sel_mtype_from_constr_mtype s M =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   338
  let val (arg_Ms, dataM) = curried_strip_mtype M in
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   339
    MFun (dataM, S Minus,
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   340
          case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   341
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   342
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   343
(* mdata -> styp -> mtyp *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   344
fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   345
                                ...}) (x as (_, T)) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   346
  if could_exist_alpha_sub_mtype thy alpha_T T then
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   347
    case AList.lookup (op =) (!constr_mcache) x of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   348
      SOME M => M
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   349
    | NONE => if T = alpha_T then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   350
                let val M = fresh_mtype_for_type mdata T in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   351
                  (Unsynchronized.change constr_mcache (cons (x, M)); M)
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   352
                end
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   353
              else
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   354
                (fresh_mtype_for_type mdata (body_type T);
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   355
                 AList.lookup (op =) (!constr_mcache) x |> the)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   356
  else
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   357
    fresh_mtype_for_type mdata T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   358
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35079
diff changeset
   359
  x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   360
    |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   361
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   362
(* literal list -> sign_atom -> sign_atom *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   363
fun resolve_sign_atom lits (V x) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   364
    x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   365
  | resolve_sign_atom _ a = a
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   366
(* literal list -> mtyp -> mtyp *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   367
fun resolve_mtype lits =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   368
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   369
    (* mtyp -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   370
    fun aux MAlpha = MAlpha
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   371
      | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   372
      | aux (MPair Mp) = MPair (pairself aux Mp)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   373
      | aux (MType (s, Ms)) = MType (s, map aux Ms)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   374
      | aux (MRec z) = MRec z
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   375
  in aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   376
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   377
datatype comp_op = Eq | Leq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   378
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   379
type comp = sign_atom * sign_atom * comp_op * var list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   380
type sign_expr = literal list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   381
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   382
datatype constraint_set =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   383
  UnsolvableCSet |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   384
  CSet of literal list * comp list * sign_expr list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   385
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   386
(* comp_op -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   387
fun string_for_comp_op Eq = "="
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   388
  | string_for_comp_op Leq = "\<le>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   389
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   390
(* sign_expr -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   391
fun string_for_sign_expr [] = "\<bot>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   392
  | string_for_sign_expr lits =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   393
    space_implode " \<or> " (map string_for_literal lits)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   394
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   395
(* constraint_set *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   396
val slack = CSet ([], [], [])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   397
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   398
(* literal -> literal list option -> literal list option *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   399
fun do_literal _ NONE = NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   400
  | do_literal (x, sn) (SOME lits) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   401
    case AList.lookup (op =) lits x of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   402
      SOME sn' => if sn = sn' then SOME lits else NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
    | NONE => SOME ((x, sn) :: lits)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   404
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   405
(* comp_op -> var list -> sign_atom -> sign_atom -> literal list * comp list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   406
   -> (literal list * comp list) option *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   407
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   408
    (case (a1, a2) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   409
       (S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   410
     | (V x1, S sn2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   411
       Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   412
     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   413
     | _ => do_sign_atom_comp Eq [] a2 a1 accum)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   414
  | do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   415
    (case (a1, a2) of
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   416
       (_, S Minus) => SOME accum
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   417
     | (S Plus, _) => SOME accum
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   418
     | (S Minus, S Plus) => NONE
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   419
     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   420
     | _ => do_sign_atom_comp Eq [] a1 a2 accum)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   421
  | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   422
    SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   423
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   424
(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   425
   -> (literal list * comp list) option *)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   426
fun do_mtype_comp _ _ _ _ NONE = NONE
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   427
  | do_mtype_comp _ _ MAlpha MAlpha accum = accum
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   428
  | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   429
                  (SOME accum) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   430
     accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   431
           |> do_mtype_comp Eq xs M12 M22
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   432
  | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   433
                  (SOME accum) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   434
    (if exists_alpha_sub_mtype M11 then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   435
       accum |> do_sign_atom_comp Leq xs a1 a2
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   436
             |> do_mtype_comp Leq xs M21 M11
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
             |> (case a2 of
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   438
                   S Minus => I
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   439
                 | S Plus => do_mtype_comp Leq xs M11 M21
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   440
                 | V x => do_mtype_comp Leq (x :: xs) M11 M21)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
     else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
       SOME accum)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   443
    |> do_mtype_comp Leq xs M12 M22
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   444
  | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   445
                  accum =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   446
    (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
     handle Library.UnequalLengths =>
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   448
            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   449
  | do_mtype_comp _ _ (MType _) (MType _) accum =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   450
    accum (* no need to compare them thanks to the cache *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   451
  | do_mtype_comp cmp _ M1 M2 _ =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   452
    raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   453
                 [M1, M2], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   454
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   455
(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   456
fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   457
  | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   458
    (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   459
              " " ^ string_for_mtype M2);
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   460
     case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   461
       NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
     | SOME (lits, comps) => CSet (lits, comps, sexps))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   463
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   464
(* mtyp -> mtyp -> constraint_set -> constraint_set *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   465
val add_mtypes_equal = add_mtype_comp Eq
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   466
val add_is_sub_mtype = add_mtype_comp Leq
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   467
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   468
(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   469
   -> (literal list * sign_expr list) option *)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   470
fun do_notin_mtype_fv _ _ _ NONE = NONE
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   471
  | do_notin_mtype_fv Minus _ MAlpha accum = accum
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   472
  | do_notin_mtype_fv Plus [] MAlpha _ = NONE
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   473
  | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
    SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   475
  | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
    SOME (lits, insert (op =) sexp sexps)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   477
  | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   478
    accum |> (if sn' = Plus andalso sn = Plus then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   479
                do_notin_mtype_fv Plus sexp M1
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   480
              else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   481
                I)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   482
          |> (if sn' = Minus orelse sn = Plus then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   483
                do_notin_mtype_fv Minus sexp M1
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   484
              else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   485
                I)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   486
          |> do_notin_mtype_fv sn sexp M2
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   487
  | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   488
    accum |> (case do_literal (x, Minus) (SOME sexp) of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   489
                NONE => I
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   490
              | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   491
          |> do_notin_mtype_fv Minus sexp M1
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   492
          |> do_notin_mtype_fv Plus sexp M2
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   493
  | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   494
    accum |> (case do_literal (x, Plus) (SOME sexp) of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   495
                NONE => I
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   496
              | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   497
          |> do_notin_mtype_fv Minus sexp M2
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   498
  | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   499
    accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   500
  | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   501
    accum |> fold (do_notin_mtype_fv sn sexp) Ms
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   502
  | do_notin_mtype_fv _ _ M _ =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   503
    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   504
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   505
(* sign -> mtyp -> constraint_set -> constraint_set *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   506
fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   507
  | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   508
    (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   509
              (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   510
     case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   511
       NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
     | SOME (lits, sexps) => CSet (lits, comps, sexps))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   514
(* mtyp -> constraint_set -> constraint_set *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   515
val add_mtype_is_concrete = add_notin_mtype_fv Minus
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   516
val add_mtype_is_complete = add_notin_mtype_fv Plus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   517
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   518
val bool_from_minus = true
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   519
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   520
(* sign -> bool *)
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   521
fun bool_from_sign Plus = not bool_from_minus
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   522
  | bool_from_sign Minus = bool_from_minus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
(* bool -> sign *)
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   524
fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   525
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   526
(* literal -> PropLogic.prop_formula *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   527
fun prop_for_literal (x, sn) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
  (not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
(* sign_atom -> PropLogic.prop_formula *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   530
fun prop_for_sign_atom_eq (S sn', sn) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
    if sn = sn' then PropLogic.True else PropLogic.False
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
  | prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
(* sign_expr -> PropLogic.prop_formula *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
(* var list -> sign -> PropLogic.prop_formula *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
fun prop_for_exists_eq xs sn =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
  PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   538
(* comp -> PropLogic.prop_formula *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
fun prop_for_comp (a1, a2, Eq, []) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
    PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
                    prop_for_comp (a2, a1, Leq, []))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
  | prop_for_comp (a1, a2, Leq, []) =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   543
    PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   544
                   prop_for_sign_atom_eq (a2, Minus))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
  | prop_for_comp (a1, a2, cmp, xs) =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   546
    PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   548
(* var -> (int -> bool option) -> literal list -> literal list *)
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   549
fun literals_from_assignments max_var assigns lits =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   550
  fold (fn x => fn accum =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
           if AList.defined (op =) lits x then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
             accum
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   553
           else case assigns x of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
             SOME b => (x, sign_from_bool b) :: accum
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   555
           | NONE => accum) (max_var downto 1) lits
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
(* comp -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   558
fun string_for_comp (a1, a2, cmp, xs) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   559
  string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
(* literal list -> comp list -> sign_expr list -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
fun print_problem lits comps sexps =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   564
  print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   565
                                         map string_for_comp comps @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   566
                                         map string_for_sign_expr sexps))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   567
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
(* literal list -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   569
fun print_solution lits =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   570
  let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   571
    print_g ("*** Solution:\n" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   572
             "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   573
             "-: " ^ commas (map (string_for_var o fst) neg))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   574
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   575
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35280
diff changeset
   576
(* var -> constraint_set -> literal list option *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   577
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   578
  | solve max_var (CSet (lits, comps, sexps)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   579
    let
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   580
      (* (int -> bool option) -> literal list option *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   581
      fun do_assigns assigns =
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   582
        SOME (literals_from_assignments max_var assigns lits
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   583
              |> tap print_solution)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   584
      val _ = print_problem lits comps sexps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
      val prop = PropLogic.all (map prop_for_literal lits @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
                                map prop_for_comp comps @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
                                map prop_for_sign_expr sexps)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   588
      val default_val = bool_from_sign Minus
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   589
    in
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   590
      if PropLogic.eval (K default_val) prop then
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   591
        do_assigns (K (SOME default_val))
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   592
      else
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   593
        let
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   594
          (* use the first ML solver (to avoid startup overhead) *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   595
          val solvers = !SatSolver.solvers
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   596
                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   597
        in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   598
          case snd (hd solvers) prop of
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   599
            SatSolver.SATISFIABLE assigns => do_assigns assigns
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   600
          | _ => NONE
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   601
        end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   604
type mtype_schema = mtyp * constraint_set
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   605
type mtype_context =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   606
  {bound_Ts: typ list,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   607
   bound_Ms: mtyp list,
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   608
   frees: (styp * mtyp) list,
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   609
   consts: (styp * mtyp) list}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   610
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   611
type accumulator = mtype_context * constraint_set
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   612
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   613
val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   614
val unsolvable_accum = (initial_gamma, UnsolvableCSet)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   616
(* typ -> mtyp -> mtype_context -> mtype_context *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   617
fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   618
  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   619
   consts = consts}
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   620
(* mtype_context -> mtype_context *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   621
fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   622
  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   623
   consts = consts}
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   624
  handle List.Empty => initial_gamma (* FIXME: needed? *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   625
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   626
(* mdata -> term -> accumulator -> mterm * accumulator *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   627
fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   628
                                          def_table, ...},
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   629
                             alpha_T, max_fresh, ...}) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   630
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   631
    (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   632
    val mtype_for = fresh_mtype_for_type mdata
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   633
    (* mtyp -> mtyp *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   634
    fun plus_set_mtype_for_dom M =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   635
      MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   636
    (* typ -> accumulator -> mterm * accumulator *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   637
    fun do_all T (gamma, cset) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   638
      let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   639
        val abs_M = mtype_for (domain_type (domain_type T))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   640
        val body_M = mtype_for (body_type T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   641
      in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   642
        (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   643
         (gamma, cset |> add_mtype_is_complete abs_M))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   644
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   645
    fun do_equals T (gamma, cset) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   646
      let val M = mtype_for (domain_type T) in
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   647
        (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   648
                                 mtype_for (nth_range_type 2 T))),
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   649
         (gamma, cset |> add_mtype_is_concrete M))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   650
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
    fun do_robust_set_operation T (gamma, cset) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
        val set_T = domain_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   654
        val M1 = mtype_for set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   655
        val M2 = mtype_for set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   656
        val M3 = mtype_for set_T
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
      in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   658
        (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   659
         (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   660
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   661
    fun do_fragile_set_operation T (gamma, cset) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   662
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   663
        val set_T = domain_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   664
        val set_M = mtype_for set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   665
        (* typ -> mtyp *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   666
        fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   667
            if T = set_T then set_M
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   668
            else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   669
          | custom_mtype_for T = mtype_for T
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   670
      in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   671
        (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   672
      end
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   673
    (* typ -> accumulator -> mtyp * accumulator *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   674
    fun do_pair_constr T accum =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   675
      case mtype_for (nth_range_type 2 T) of
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   676
        M as MPair (a_M, b_M) =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   677
        (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   678
      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   679
    (* int -> typ -> accumulator -> mtyp * accumulator *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
    fun do_nth_pair_sel n T =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   681
      case mtype_for (domain_type T) of
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   682
        M as MPair (a_M, b_M) =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   683
        pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   684
      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   685
    (* mtyp * accumulator *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   686
    val mtype_unsolvable = (dummy_M, unsolvable_accum)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   687
    (* term -> mterm * accumulator *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   688
    fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   689
    (* term -> string -> typ -> term -> term -> term -> accumulator
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   690
       -> mterm * accumulator *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   691
    fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   692
      let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   693
        val abs_M = mtype_for abs_T
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   694
        val (bound_m, accum) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   695
          accum |>> push_bound abs_T abs_M |> do_term bound_t
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   696
        val expected_bound_M = plus_set_mtype_for_dom abs_M
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   697
        val (body_m, accum) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   698
          accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   699
                |> do_term body_t ||> apfst pop_bound
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   700
        val bound_M = mtype_of_mterm bound_m
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   701
        val (M1, a, M2) = dest_MFun bound_M
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   702
      in
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   703
        (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   704
               MAbs (abs_s, abs_T, M1, a,
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   705
                     MApp (MApp (MRaw (connective_t,
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   706
                                       mtype_for (fastype_of connective_t)),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   707
                                 MApp (bound_m, MRaw (Bound 0, M1))),
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   708
                           body_m))), accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   709
      end
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   710
    (* term -> accumulator -> mterm * accumulator *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   711
    and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   712
      | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   713
                             cset)) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   714
        (case t of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   715
           Const (x as (s, T)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   716
           (case AList.lookup (op =) consts x of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   717
              SOME M => (M, accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   718
            | NONE =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   719
              if not (could_exist_alpha_subtype alpha_T T) then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   720
                (mtype_for T, accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
              else case s of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   722
                @{const_name all} => do_all T accum
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   723
              | @{const_name "=="} => do_equals T accum
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   724
              | @{const_name All} => do_all T accum
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   725
              | @{const_name Ex} =>
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   726
                let val set_T = domain_type T in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   727
                  do_term (Abs (Name.uu, set_T,
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   728
                                @{const Not} $ (HOLogic.mk_eq
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   729
                                    (Abs (Name.uu, domain_type set_T,
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   730
                                          @{const False}),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   731
                                     Bound 0)))) accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   732
                  |>> mtype_of_mterm
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   733
                end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
              | @{const_name "op ="} => do_equals T accum
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   735
              | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   736
              | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
              | @{const_name If} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   738
                do_robust_set_operation (range_type T) accum
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   739
                |>> curry3 MFun bool_M (S Minus)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   740
              | @{const_name Pair} => do_pair_constr T accum
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   741
              | @{const_name fst} => do_nth_pair_sel 0 T accum
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   742
              | @{const_name snd} => do_nth_pair_sel 1 T accum 
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   743
              | @{const_name Id} =>
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   744
                (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   745
              | @{const_name insert} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   746
                let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   747
                  val set_T = domain_type (range_type T)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   748
                  val M1 = mtype_for (domain_type set_T)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   749
                  val M1' = plus_set_mtype_for_dom M1
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   750
                  val M2 = mtype_for set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   751
                  val M3 = mtype_for set_T
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   752
                in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   753
                  (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   754
                   (gamma, cset |> add_mtype_is_concrete M1
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   755
                                |> add_is_sub_mtype M1' M3
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   756
                                |> add_is_sub_mtype M2 M3))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   758
              | @{const_name converse} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   759
                let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   760
                  val x = Unsynchronized.inc max_fresh
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   761
                  (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   762
                  fun mtype_for_set T =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   763
                    MFun (mtype_for (domain_type T), V x, bool_M)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   764
                  val ab_set_M = domain_type T |> mtype_for_set
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   765
                  val ba_set_M = range_type T |> mtype_for_set
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   766
                in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   767
              | @{const_name trancl} => do_fragile_set_operation T accum
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   768
              | @{const_name rtrancl} =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   769
                (print_g "*** rtrancl"; mtype_unsolvable)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   770
              | @{const_name finite} =>
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   771
                if is_finite_type hol_ctxt T then
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   772
                  let val M1 = mtype_for (domain_type (domain_type T)) in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   773
                    (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   774
                  end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   775
                else
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   776
                  (print_g "*** finite"; mtype_unsolvable)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   777
              | @{const_name rel_comp} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
                let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   779
                  val x = Unsynchronized.inc max_fresh
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   780
                  (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   781
                  fun mtype_for_set T =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   782
                    MFun (mtype_for (domain_type T), V x, bool_M)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   783
                  val bc_set_M = domain_type T |> mtype_for_set
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   784
                  val ab_set_M = domain_type (range_type T) |> mtype_for_set
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   785
                  val ac_set_M = nth_range_type 2 T |> mtype_for_set
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   786
                in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   787
                  (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   788
                   accum)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   790
              | @{const_name image} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   791
                let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   792
                  val a_M = mtype_for (domain_type (domain_type T))
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   793
                  val b_M = mtype_for (range_type (domain_type T))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   794
                in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   795
                  (MFun (MFun (a_M, S Minus, b_M), S Minus,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   796
                         MFun (plus_set_mtype_for_dom a_M, S Minus,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   797
                               plus_set_mtype_for_dom b_M)), accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   798
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   799
              | @{const_name Sigma} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   800
                let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   801
                  val x = Unsynchronized.inc max_fresh
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   802
                  (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   803
                  fun mtype_for_set T =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   804
                    MFun (mtype_for (domain_type T), V x, bool_M)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   805
                  val a_set_T = domain_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   806
                  val a_M = mtype_for (domain_type a_set_T)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   807
                  val b_set_M = mtype_for_set (range_type (domain_type
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   808
                                                               (range_type T)))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   809
                  val a_set_M = mtype_for_set a_set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   810
                  val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   811
                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   812
                in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   813
                  (MFun (a_set_M, S Minus,
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   814
                         MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   815
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   816
              | @{const_name Tha} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   817
                let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   818
                  val a_M = mtype_for (domain_type (domain_type T))
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   819
                  val a_set_M = plus_set_mtype_for_dom a_M
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   820
                in (MFun (a_set_M, S Minus, a_M), accum) end
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   821
              | _ =>
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   822
                if s = @{const_name minus_class.minus} andalso
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   823
                   is_set_type (domain_type T) then
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   824
                  let
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   825
                    val set_T = domain_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   826
                    val left_set_M = mtype_for set_T
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   827
                    val right_set_M = mtype_for set_T
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   828
                  in
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   829
                    (MFun (left_set_M, S Minus,
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   830
                           MFun (right_set_M, S Minus, left_set_M)),
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   831
                     (gamma, cset |> add_mtype_is_concrete right_set_M
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   832
                                  |> add_is_sub_mtype right_set_M left_set_M))
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   833
                  end
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   834
                else if s = @{const_name ord_class.less_eq} andalso
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   835
                        is_set_type (domain_type T) then
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   836
                  do_fragile_set_operation T accum
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   837
                else if (s = @{const_name semilattice_inf_class.inf} orelse
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   838
                         s = @{const_name semilattice_sup_class.sup}) andalso
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   839
                        is_set_type (domain_type T) then
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   840
                  do_robust_set_operation T accum
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   841
                else if is_sel s then
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   842
                  (mtype_for_sel mdata x, accum)
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   843
                else if is_constr thy stds x then
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   844
                  (mtype_for_constr mdata x, accum)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   845
                else if is_built_in_const thy stds fast_descrs x andalso
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   846
                        s <> @{const_name is_unknown} andalso
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   847
                        s <> @{const_name unknown} then
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   848
                  (* the "unknown" part is a hack *)
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   849
                  case def_of_const thy def_table x of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   850
                    SOME t' => do_term t' accum |>> mtype_of_mterm
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   851
                  | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35219
diff changeset
   852
                else
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   853
                  let val M = mtype_for T in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   854
                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   855
                          frees = frees, consts = (x, M) :: consts}, cset))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   856
                  end) |>> curry MRaw t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   857
         | Free (x as (_, T)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   858
           (case AList.lookup (op =) frees x of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   859
              SOME M => (M, accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   860
            | NONE =>
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   861
              let val M = mtype_for T in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   862
                (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   863
                      frees = (x, M) :: frees, consts = consts}, cset))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   864
              end) |>> curry MRaw t
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   865
         | Var _ => (print_g "*** Var"; mterm_unsolvable t)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   866
         | Bound j => (MRaw (t, nth bound_Ms j), accum)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   867
         | Abs (s, T, t') =>
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   868
           (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   869
              SOME t' =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   870
              let
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   871
                val M = mtype_for T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   872
                val a = V (Unsynchronized.inc max_fresh)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   873
                val (m', accum) = do_term t' (accum |>> push_bound T M)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   874
              in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   875
            | NONE =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   876
              ((case t' of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   877
                  t1' $ Bound 0 =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   878
                  if not (loose_bvar1 (t1', 0)) then
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   879
                    do_term (incr_boundvars ~1 t1') accum
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   880
                  else
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   881
                    raise SAME ()
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   882
                | _ => raise SAME ())
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   883
               handle SAME () =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   884
                      let
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   885
                        val M = mtype_for T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   886
                        val (m', accum) = do_term t' (accum |>> push_bound T M)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   887
                      in
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   888
                        (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   889
                      end))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   890
         | (t0 as Const (@{const_name All}, _))
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   891
           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   892
           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   893
         | (t0 as Const (@{const_name Ex}, _))
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   894
           $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   895
           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   896
         | Const (@{const_name Let}, _) $ t1 $ t2 =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   897
           do_term (betapply (t2, t1)) accum
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   898
         | t1 $ t2 =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   899
           let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   900
             val (m1, accum) = do_term t1 accum
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   901
             val (m2, accum) = do_term t2 accum
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   902
           in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   903
             case accum of
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   904
               (_, UnsolvableCSet) => mterm_unsolvable t
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   905
             | _ =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   906
               let
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   907
                 val T11 = domain_type (fastype_of1 (bound_Ts, t1))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   908
                 val T2 = fastype_of1 (bound_Ts, t2)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   909
                 val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   910
                 val M2 = mtype_of_mterm m2
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   911
               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   912
           end)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   913
        |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   914
                                      string_for_mterm ctxt m))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
  in do_term end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   916
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   917
(*
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   918
    accum |> (case a of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   919
                S Minus => accum 
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   920
              | S Plus => unsolvable_accum
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   921
              | V x => do_literal (x, Minus) lits)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   922
*)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   923
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   924
(* int -> mtyp -> accumulator -> accumulator *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   925
fun force_minus_funs 0 _ = I
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   926
  | force_minus_funs n (M as MFun (M1, _, M2)) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   927
    add_mtypes_equal M (MFun (M1, S Minus, M2))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   928
    #> force_minus_funs (n - 1) M2
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   929
  | force_minus_funs _ M =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   930
    raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   931
(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   932
fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   933
  let
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   934
    val (m1, accum) = consider_term mdata t1 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   935
    val (m2, accum) = consider_term mdata t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   936
    val M1 = mtype_of_mterm m1
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   937
    val M2 = mtype_of_mterm m2
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   938
    val accum = accum ||> add_mtypes_equal M1 M2
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   939
    val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   940
    val m = MApp (MApp (MRaw (Const x,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   941
                MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   942
  in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   943
    (m, if def then
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   944
          let val (head_m, arg_ms) = strip_mcomb m1 in
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   945
            accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   946
          end
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   947
        else
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   948
          accum)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   949
  end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   950
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   951
(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   952
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   953
  let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   954
    (* typ -> mtyp *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   955
    val mtype_for = fresh_mtype_for_type mdata
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   956
    (* term -> accumulator -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   957
    val do_term = consider_term mdata
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   958
    (* sign -> term -> accumulator -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   959
    fun do_formula _ t (_, UnsolvableCSet) =
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   960
        (MRaw (t, dummy_M), unsolvable_accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   961
      | do_formula sn t accum =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   962
        let
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   963
          (* styp -> string -> typ -> term -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   964
          fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   965
            let
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   966
              val abs_M = mtype_for abs_T
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34936
diff changeset
   967
              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   968
              val (body_m, accum) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   969
                accum ||> side_cond ? add_mtype_is_complete abs_M
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   970
                      |>> push_bound abs_T abs_M |> do_formula sn body_t
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   971
              val body_M = mtype_of_mterm body_m
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   972
            in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   973
              (MApp (MRaw (Const quant_x,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   974
                           MFun (MFun (abs_M, S Minus, body_M), S Minus,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   975
                                 body_M)),
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   976
                     MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   977
               accum |>> pop_bound)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   978
            end
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   979
          (* styp -> term -> term -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   980
          fun do_equals x t1 t2 =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   981
            case sn of
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   982
              Plus => do_term t accum
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   983
            | Minus => consider_general_equals mdata false x t1 t2 accum
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   984
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   985
          case t of
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   986
            Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   987
            do_quantifier x s1 T1 t1
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   988
          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   989
          | @{const Trueprop} $ t1 =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   990
            let val (m1, accum) = do_formula sn t1 accum in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   991
              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   992
                     m1), accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   993
            end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   994
          | @{const Not} $ t1 =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   995
            let val (m1, accum) = do_formula (negate sn) t1 accum in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   996
              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   997
               accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   998
            end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   999
          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1000
            do_quantifier x s1 T1 t1
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1001
          | Const (x0 as (s0 as @{const_name Ex}, T0))
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1002
            $ (t1 as Abs (s1, T1, t1')) =>
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1003
            (case sn of
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1004
               Plus => do_quantifier x0 s1 T1 t1'
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1005
             | Minus =>
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1006
               (* FIXME: Move elsewhere *)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1007
               do_term (@{const Not}
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1008
                        $ (HOLogic.eq_const (domain_type T0) $ t1
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1009
                           $ Abs (Name.uu, T1, @{const False}))) accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1010
          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1011
            do_equals x t1 t2
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1012
          | (t0 as Const (s0, _)) $ t1 $ t2 =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1013
            if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1014
               s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1015
              let
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1016
                val impl = (s0 = @{const_name "==>"} orelse
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1017
                           s0 = @{const_name "op -->"})
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1018
                val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1019
                val (m2, accum) = do_formula sn t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1020
              in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1021
                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1022
                 accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1023
              end 
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1024
            else
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1025
              do_term t accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1026
          | _ => do_term t accum
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1027
        end
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1028
        |> tap (fn (m, _) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1029
                   print_g ("\<Gamma> \<turnstile> " ^
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1030
                            string_for_mterm ctxt m ^ " : o\<^sup>" ^
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1031
                            string_for_sign sn))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1032
  in do_formula end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1033
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1034
(* The harmless axiom optimization below is somewhat too aggressive in the face
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1035
   of (rather peculiar) user-defined axioms. *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1036
val harmless_consts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1037
  [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1038
val bounteous_consts = [@{const_name bisim}]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1039
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1040
(* mdata -> term -> bool *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1041
fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1042
  | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1043
    Term.add_consts t []
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1044
    |> filter_out (is_built_in_const thy stds fast_descrs)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1045
    |> (forall (member (op =) harmless_consts o original_name o fst) orf
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1046
        exists (member (op =) bounteous_consts o fst))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1047
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1048
(* mdata -> term -> accumulator -> mterm * accumulator *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1049
fun consider_nondefinitional_axiom mdata t =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1050
  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1051
  else consider_general_formula mdata Plus t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1052
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1053
(* mdata -> term -> accumulator -> mterm * accumulator *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1054
fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1055
  if not (is_constr_pattern_formula thy t) then
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1056
    consider_nondefinitional_axiom mdata t
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1057
  else if is_harmless_axiom mdata t then
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1058
    pair (MRaw (t, dummy_M))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1059
  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1060
    let
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1061
      (* typ -> mtyp *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1062
      val mtype_for = fresh_mtype_for_type mdata
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1063
      (* term -> accumulator -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1064
      val do_term = consider_term mdata
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1065
      (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1066
      fun do_all quant_t abs_s abs_T body_t accum =
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1067
        let
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1068
          val abs_M = mtype_for abs_T
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1069
          val (body_m, accum) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1070
            accum |>> push_bound abs_T abs_M |> do_formula body_t
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1071
          val body_M = mtype_of_mterm body_m
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1072
        in
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1073
          (MApp (MRaw (quant_t,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1074
                       MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1075
                 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1076
           accum |>> pop_bound)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1077
        end
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1078
      (* term -> term -> term -> accumulator -> mterm * accumulator *)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1079
      and do_conjunction t0 t1 t2 accum =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1080
        let
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1081
          val (m1, accum) = do_formula t1 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1082
          val (m2, accum) = do_formula t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1083
        in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1084
          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1085
        end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1086
      and do_implies t0 t1 t2 accum =
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1087
        let
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1088
          val (m1, accum) = do_term t1 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1089
          val (m2, accum) = do_formula t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1090
        in
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1091
          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1092
        end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1093
      (* term -> accumulator -> accumulator *)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1094
      and do_formula t (_, UnsolvableCSet) =
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1095
          (MRaw (t, dummy_M), unsolvable_accum)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1096
        | do_formula t accum =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1097
          case t of
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1098
            (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1099
            do_all t0 s1 T1 t1 accum
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1100
          | @{const Trueprop} $ t1 =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1101
            let val (m1, accum) = do_formula t1 accum in
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1102
              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1103
                     m1), accum)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1104
            end
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1105
          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1106
            consider_general_equals mdata true x t1 t2 accum
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1107
          | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1108
          | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1109
            do_conjunction t0 t1 t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1110
          | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1111
            do_all t0 s0 T1 t1 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1112
          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1113
            consider_general_equals mdata true x t1 t2 accum
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1114
          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1115
          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1116
          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1117
                             \do_formula", [t])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1118
    in do_formula t end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1119
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1120
(* Proof.context -> literal list -> term -> mtyp -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1121
fun string_for_mtype_of_term ctxt lits t M =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1122
  Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1123
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1124
(* theory -> literal list -> mtype_context -> unit *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1125
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1126
  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1127
  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1128
  |> cat_lines |> print_g
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1129
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1130
(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1131
fun amass f t (ms, accum) =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1132
  let val (m, accum) = f t accum in (m :: ms, accum) end
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1133
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1134
(* string -> bool -> hol_context -> bool -> typ -> term list * term list
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1135
   -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1136
fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1137
          (nondef_ts, def_ts) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1138
  let
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1139
    val _ = print_g ("****** " ^ which ^ " analysis: " ^
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
  1140
                     string_for_mtype MAlpha ^ " is " ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1141
                     Syntax.string_of_typ ctxt alpha_T)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1142
    val mdata as {max_fresh, constr_mcache, ...} =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1143
      initial_mdata hol_ctxt binarize no_harmless alpha_T
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1144
    val accum = (initial_gamma, slack)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1145
    val (nondef_ms, accum) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1146
      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1147
                  |> fold (amass (consider_nondefinitional_axiom mdata))
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1148
                          (tl nondef_ts)
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
  1149
    val (def_ms, (gamma, cset)) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1150
      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1151
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1152
    case solve (!max_fresh) cset of
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1153
      SOME lits => (print_mtype_context ctxt lits gamma;
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1154
                    SOME (lits, (nondef_ms, def_ms), !constr_mcache))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1155
    | _ => NONE
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1156
  end
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1157
  handle MTYPE (loc, Ms, Ts) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1158
         raise BAD (loc, commas (map string_for_mtype Ms @
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1159
                                 map (Syntax.string_of_typ ctxt) Ts))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1160
       | MTERM (loc, ms) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1161
         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1162
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1163
(* hol_context -> bool -> typ -> term list * term list -> bool *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1164
val formulas_monotonic = is_some oooo infer "Monotonicity" false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1165
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1166
(* typ -> typ -> styp *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1167
fun fin_fun_constr T1 T2 =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1168
  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1169
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1170
(* hol_context -> bool -> (typ option * bool option) list -> typ
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1171
   -> term list * term list -> term list * term list *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1172
fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1173
                  binarize finitizes alpha_T tsp =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1174
  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1175
    SOME (lits, msp, constr_mtypes) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1176
    let
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1177
      (* typ -> sign_atom -> bool *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1178
      fun should_finitize T a =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1179
        case triple_lookup (type_match thy) finitizes T of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1180
          SOME (SOME false) => false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1181
        | _ => resolve_sign_atom lits a = S Plus
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1182
      (* typ -> mtyp -> typ *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1183
      fun type_from_mtype T M =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1184
        case (M, T) of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1185
          (MAlpha, _) => T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1186
        | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1187
          Type (if should_finitize T a then @{type_name fin_fun}
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1188
                else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1189
        | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1190
          Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1191
        | (MType _, _) => T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1192
        | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1193
                            [M], [T])
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1194
      (* styp -> styp *)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1195
      fun finitize_constr (x as (s, T)) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1196
        (s, case AList.lookup (op =) constr_mtypes x of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1197
              SOME M => type_from_mtype T M
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1198
            | NONE => T)
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386