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