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