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