src/HOL/Library/refute.ML
changeset 55507 5f27fb2110e0
parent 55411 27de2c976d90
child 55891 d1a9b07783ab
     1.1 --- a/src/HOL/Library/refute.ML	Sat Feb 15 18:48:43 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sat Feb 15 21:09:48 2014 +0100
     1.3 @@ -102,25 +102,11 @@
     1.4      Leaf of 'a
     1.5    | Node of ('a tree) list;
     1.6  
     1.7 -(* ('a -> 'b) -> 'a tree -> 'b tree *)
     1.8 -
     1.9  fun tree_map f tr =
    1.10    case tr of
    1.11      Leaf x  => Leaf (f x)
    1.12    | Node xs => Node (map (tree_map f) xs);
    1.13  
    1.14 -(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
    1.15 -
    1.16 -fun tree_foldl f =
    1.17 -  let
    1.18 -    fun itl (e, Leaf x)  = f(e,x)
    1.19 -      | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs)
    1.20 -  in
    1.21 -    itl
    1.22 -  end;
    1.23 -
    1.24 -(* 'a tree * 'b tree -> ('a * 'b) tree *)
    1.25 -
    1.26  fun tree_pair (t1, t2) =
    1.27    case t1 of
    1.28      Leaf x =>
    1.29 @@ -335,7 +321,6 @@
    1.30  
    1.31  fun actual_params ctxt override =
    1.32    let
    1.33 -    (* (string * string) list * string -> bool *)
    1.34      fun read_bool (parms, name) =
    1.35        case AList.lookup (op =) parms name of
    1.36          SOME "true" => true
    1.37 @@ -344,7 +329,6 @@
    1.38            " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
    1.39        | NONE   => error ("parameter " ^ quote name ^
    1.40            " must be assigned a value")
    1.41 -    (* (string * string) list * string -> int *)
    1.42      fun read_int (parms, name) =
    1.43        case AList.lookup (op =) parms name of
    1.44          SOME s =>
    1.45 @@ -354,21 +338,17 @@
    1.46              " (value is " ^ quote s ^ ") must be an integer value"))
    1.47        | NONE => error ("parameter " ^ quote name ^
    1.48            " must be assigned a value")
    1.49 -    (* (string * string) list * string -> string *)
    1.50      fun read_string (parms, name) =
    1.51        case AList.lookup (op =) parms name of
    1.52          SOME s => s
    1.53        | NONE => error ("parameter " ^ quote name ^
    1.54          " must be assigned a value")
    1.55      (* 'override' first, defaults last: *)
    1.56 -    (* (string * string) list *)
    1.57      val allparams = override @ get_default_params ctxt
    1.58 -    (* int *)
    1.59      val minsize = read_int (allparams, "minsize")
    1.60      val maxsize = read_int (allparams, "maxsize")
    1.61      val maxvars = read_int (allparams, "maxvars")
    1.62      val maxtime = read_int (allparams, "maxtime")
    1.63 -    (* string *)
    1.64      val satsolver = read_string (allparams, "satsolver")
    1.65      val no_assms = read_bool (allparams, "no_assms")
    1.66      val expect = the_default "" (AList.lookup (op =) allparams "expect")
    1.67 @@ -461,7 +441,6 @@
    1.68  
    1.69  fun get_def thy (s, T) =
    1.70    let
    1.71 -    (* (string * Term.term) list -> (string * Term.term) option *)
    1.72      fun get_def_ax [] = NONE
    1.73        | get_def_ax ((axname, ax) :: axioms) =
    1.74            (let
    1.75 @@ -492,11 +471,9 @@
    1.76  
    1.77  fun get_typedef thy T =
    1.78    let
    1.79 -    (* (string * Term.term) list -> (string * Term.term) option *)
    1.80      fun get_typedef_ax [] = NONE
    1.81        | get_typedef_ax ((axname, ax) :: axioms) =
    1.82            (let
    1.83 -            (* Term.term -> Term.typ option *)
    1.84              fun type_of_type_definition (Const (s', T')) =
    1.85                    if s'= @{const_name type_definition} then
    1.86                      SOME T'
    1.87 @@ -557,7 +534,6 @@
    1.88  
    1.89  fun unfold_defs thy t =
    1.90    let
    1.91 -    (* Term.term -> Term.term *)
    1.92      fun unfold_loop t =
    1.93        case t of
    1.94        (* Pure *)
    1.95 @@ -907,8 +883,6 @@
    1.96  (*                list") are identified.                                     *)
    1.97  (* ------------------------------------------------------------------------- *)
    1.98  
    1.99 -(* Term.typ -> string *)
   1.100 -
   1.101  fun string_of_typ (Type (s, _))     = s
   1.102    | string_of_typ (TFree (s, _))    = s
   1.103    | string_of_typ (TVar ((s,_), _)) = s;
   1.104 @@ -919,8 +893,6 @@
   1.105  (*                 'sizes'                                                   *)
   1.106  (* ------------------------------------------------------------------------- *)
   1.107  
   1.108 -(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
   1.109 -
   1.110  fun first_universe xs sizes minsize =
   1.111    let
   1.112      fun size_of_typ T =
   1.113 @@ -938,14 +910,10 @@
   1.114  (*                type may have a fixed size given in 'sizes'                *)
   1.115  (* ------------------------------------------------------------------------- *)
   1.116  
   1.117 -(* (Term.typ * int) list -> (string * int) list -> int -> int ->
   1.118 -  (Term.typ * int) list option *)
   1.119 -
   1.120  fun next_universe xs sizes minsize maxsize =
   1.121    let
   1.122      (* creates the "first" list of length 'len', where the sum of all list *)
   1.123      (* elements is 'sum', and the length of the list is 'len'              *)
   1.124 -    (* int -> int -> int -> int list option *)
   1.125      fun make_first _ 0 sum =
   1.126            if sum = 0 then
   1.127              SOME []
   1.128 @@ -958,7 +926,6 @@
   1.129              Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
   1.130      (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   1.131      (* all list elements x (unless 'max'<0)                                *)
   1.132 -    (* int -> int -> int -> int list -> int list option *)
   1.133      fun next _ _ _ [] =
   1.134            NONE
   1.135        | next max len sum [x] =
   1.136 @@ -994,8 +961,6 @@
   1.137  (*         formula that is true iff the interpretation denotes "true"        *)
   1.138  (* ------------------------------------------------------------------------- *)
   1.139  
   1.140 -(* interpretation -> prop_formula *)
   1.141 -
   1.142  fun toTrue (Leaf [fm, _]) = fm
   1.143    | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
   1.144  
   1.145 @@ -1005,8 +970,6 @@
   1.146  (*          denotes "false"                                                  *)
   1.147  (* ------------------------------------------------------------------------- *)
   1.148  
   1.149 -(* interpretation -> prop_formula *)
   1.150 -
   1.151  fun toFalse (Leaf [_, fm]) = fm
   1.152    | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
   1.153  
   1.154 @@ -1025,11 +988,9 @@
   1.155      assm_ts t negate =
   1.156    let
   1.157      val thy = Proof_Context.theory_of ctxt
   1.158 -    (* string -> string *)
   1.159      fun check_expect outcome_code =
   1.160        if expect = "" orelse outcome_code = expect then outcome_code
   1.161        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   1.162 -    (* unit -> string *)
   1.163      fun wrapper () =
   1.164        let
   1.165          val timer = Timer.startRealTimer ()
   1.166 @@ -1040,7 +1001,6 @@
   1.167          val u = unfold_defs thy t
   1.168          val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
   1.169          val axioms = collect_axioms ctxt u
   1.170 -        (* Term.typ list *)
   1.171          val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
   1.172          val _ = tracing ("Ground types: "
   1.173            ^ (if null types then "none."
   1.174 @@ -1069,7 +1029,6 @@
   1.175                ^ "countermodel(s) may be spurious!")
   1.176            else
   1.177              ()
   1.178 -        (* (Term.typ * int) list -> string *)
   1.179          fun find_model_loop universe =
   1.180            let
   1.181              val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
   1.182 @@ -1271,14 +1230,11 @@
   1.183  fun make_constants ctxt model T =
   1.184    let
   1.185      (* returns a list with all unit vectors of length n *)
   1.186 -    (* int -> interpretation list *)
   1.187      fun unit_vectors n =
   1.188        let
   1.189          (* returns the k-th unit vector of length n *)
   1.190 -        (* int * int -> interpretation *)
   1.191          fun unit_vector (k, n) =
   1.192            Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   1.193 -        (* int -> interpretation list *)
   1.194          fun unit_vectors_loop k =
   1.195            if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1)
   1.196        in
   1.197 @@ -1286,7 +1242,6 @@
   1.198        end
   1.199      (* returns a list of lists, each one consisting of n (possibly *)
   1.200      (* identical) elements from 'xs'                               *)
   1.201 -    (* int -> 'a list -> 'a list list *)
   1.202      fun pick_all 1 xs = map single xs
   1.203        | pick_all n xs =
   1.204            let val rec_pick = pick_all (n - 1) xs in
   1.205 @@ -1294,7 +1249,6 @@
   1.206            end
   1.207      (* returns all constant interpretations that have the same tree *)
   1.208      (* structure as the interpretation argument                     *)
   1.209 -    (* interpretation -> interpretation list *)
   1.210      fun make_constants_intr (Leaf xs) = unit_vectors (length xs)
   1.211        | make_constants_intr (Node xs) = map Node (pick_all (length xs)
   1.212            (make_constants_intr (hd xs)))
   1.213 @@ -1335,8 +1289,6 @@
   1.214  (* TT/FF: interpretations that denote "true" or "false", respectively        *)
   1.215  (* ------------------------------------------------------------------------- *)
   1.216  
   1.217 -(* interpretation *)
   1.218 -
   1.219  val TT = Leaf [True, False];
   1.220  
   1.221  val FF = Leaf [False, True];
   1.222 @@ -1359,11 +1311,8 @@
   1.223  (* for equality on T first, and "applying" this interpretation to 'i1'    *)
   1.224  (* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)
   1.225  
   1.226 -(* interpretation * interpretation -> interpretation *)
   1.227 -
   1.228  fun make_equality (i1, i2) =
   1.229    let
   1.230 -    (* interpretation * interpretation -> prop_formula *)
   1.231      fun equal (i1, i2) =
   1.232        (case i1 of
   1.233          Leaf xs =>
   1.234 @@ -1376,7 +1325,6 @@
   1.235              Leaf _  => raise REFUTE ("make_equality",
   1.236              "first interpretation is higher")
   1.237            | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
   1.238 -    (* interpretation * interpretation -> prop_formula *)
   1.239      fun not_equal (i1, i2) =
   1.240        (case i1 of
   1.241          Leaf xs =>
   1.242 @@ -1407,11 +1355,8 @@
   1.243  (* to an undefined interpretation.                                           *)
   1.244  (* ------------------------------------------------------------------------- *)
   1.245  
   1.246 -(* interpretation * interpretation -> interpretation *)
   1.247 -
   1.248  fun make_def_equality (i1, i2) =
   1.249    let
   1.250 -    (* interpretation * interpretation -> prop_formula *)
   1.251      fun equal (i1, i2) =
   1.252        (case i1 of
   1.253          Leaf xs =>
   1.254 @@ -1426,7 +1371,6 @@
   1.255              Leaf _  => raise REFUTE ("make_def_equality",
   1.256              "first interpretation is higher")
   1.257            | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
   1.258 -    (* interpretation *)
   1.259      val eq = equal (i1, i2)
   1.260    in
   1.261      Leaf [eq, SNot eq]
   1.262 @@ -1438,18 +1382,13 @@
   1.263  (*                       argument denoted by 'i2'                            *)
   1.264  (* ------------------------------------------------------------------------- *)
   1.265  
   1.266 -(* interpretation * interpretation -> interpretation *)
   1.267 -
   1.268  fun interpretation_apply (i1, i2) =
   1.269    let
   1.270 -    (* interpretation * interpretation -> interpretation *)
   1.271      fun interpretation_disjunction (tr1,tr2) =
   1.272        tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys))
   1.273          (tree_pair (tr1,tr2))
   1.274 -    (* prop_formula * interpretation -> interpretation *)
   1.275      fun prop_formula_times_interpretation (fm,tr) =
   1.276        tree_map (map (fn x => SAnd (fm,x))) tr
   1.277 -    (* prop_formula list * interpretation list -> interpretation *)
   1.278      fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
   1.279            prop_formula_times_interpretation (fm,tr)
   1.280        | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
   1.281 @@ -1459,14 +1398,12 @@
   1.282            raise REFUTE ("interpretation_apply", "empty list (in dot product)")
   1.283      (* returns a list of lists, each one consisting of one element from each *)
   1.284      (* element of 'xss'                                                      *)
   1.285 -    (* 'a list list -> 'a list list *)
   1.286      fun pick_all [xs] = map single xs
   1.287        | pick_all (xs::xss) =
   1.288            let val rec_pick = pick_all xss in
   1.289              maps (fn x => map (cons x) rec_pick) xs
   1.290            end
   1.291        | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
   1.292 -    (* interpretation -> prop_formula list *)
   1.293      fun interpretation_to_prop_formula_list (Leaf xs) = xs
   1.294        | interpretation_to_prop_formula_list (Node trees) =
   1.295            map Prop_Logic.all (pick_all
   1.296 @@ -1484,8 +1421,6 @@
   1.297  (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
   1.298  (* ------------------------------------------------------------------------- *)
   1.299  
   1.300 -(* Term.term -> int -> Term.term *)
   1.301 -
   1.302  fun eta_expand t i =
   1.303    let
   1.304      val Ts = Term.binder_types (Term.fastype_of t)
   1.305 @@ -1520,10 +1455,8 @@
   1.306    let
   1.307      val (typs, terms) = model
   1.308      val {maxvars, def_eq, next_idx, bounds, wellformed} = args
   1.309 -    (* Term.typ -> (interpretation * model * arguments) option *)
   1.310      fun interpret_groundterm T =
   1.311        let
   1.312 -        (* unit -> (interpretation * model * arguments) option *)
   1.313          fun interpret_groundtype () =
   1.314            let
   1.315              (* the model must specify a size for ground types *)
   1.316 @@ -1534,15 +1467,11 @@
   1.317              (* check if 'maxvars' is large enough *)
   1.318              val _ = (if next - 1 > maxvars andalso maxvars > 0 then
   1.319                raise MAXVARS_EXCEEDED else ())
   1.320 -            (* prop_formula list *)
   1.321              val fms  = map BoolVar (next_idx upto (next_idx + size - 1))
   1.322 -            (* interpretation *)
   1.323              val intr = Leaf fms
   1.324 -            (* prop_formula list -> prop_formula *)
   1.325              fun one_of_two_false [] = True
   1.326                | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
   1.327                    SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   1.328 -            (* prop_formula *)
   1.329              val wf = one_of_two_false fms
   1.330            in
   1.331              (* extend the model, increase 'next_idx', add well-formedness *)
   1.332 @@ -1561,7 +1490,6 @@
   1.333                (* make fresh copies, with different variable indices *)
   1.334                (* 'idx': next variable index                         *)
   1.335                (* 'n'  : number of copies                            *)
   1.336 -              (* int -> int -> (int * interpretation list * prop_formula *)
   1.337                fun make_copies idx 0 = (idx, [], True)
   1.338                  | make_copies idx n =
   1.339                      let
   1.340 @@ -1807,12 +1735,11 @@
   1.341    let
   1.342      val thy = Proof_Context.theory_of ctxt
   1.343      val (typs, terms) = model
   1.344 -    (* Term.typ -> (interpretation * model * arguments) option *)
   1.345      fun interpret_term (Type (s, Ts)) =
   1.346            (case Datatype.get_info thy s of
   1.347              SOME info =>  (* inductive datatype *)
   1.348                let
   1.349 -                (* int option -- only recursive IDTs have an associated depth *)
   1.350 +                (* only recursive IDTs have an associated depth *)
   1.351                  val depth = AList.lookup (op =) typs (Type (s, Ts))
   1.352                  (* sanity check: depth must be at least 0 *)
   1.353                  val _ =
   1.354 @@ -1853,15 +1780,11 @@
   1.355                      (* check if 'maxvars' is large enough *)
   1.356                      val _        = (if next-1 > #maxvars args andalso
   1.357                        #maxvars args > 0 then raise MAXVARS_EXCEEDED else ())
   1.358 -                    (* prop_formula list *)
   1.359                      val fms      = map BoolVar (next_idx upto (next_idx+size-1))
   1.360 -                    (* interpretation *)
   1.361                      val intr     = Leaf fms
   1.362 -                    (* prop_formula list -> prop_formula *)
   1.363                      fun one_of_two_false [] = True
   1.364                        | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
   1.365                            SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   1.366 -                    (* prop_formula *)
   1.367                      val wf = one_of_two_false fms
   1.368                    in
   1.369                      (* extend the model, increase 'next_idx', add well-formedness *)
   1.370 @@ -1903,7 +1826,6 @@
   1.371      (* It would be nice if we could just use 'print' for this, but 'print'   *)
   1.372      (* for IDTs calls 'IDT_constructor_interpreter' again, and this could    *)
   1.373      (* lead to infinite recursion when we have (mutually) recursive IDTs.    *)
   1.374 -    (* (Term.typ * int) list -> Term.typ -> Term.term list *)
   1.375      fun canonical_terms typs T =
   1.376            (case T of
   1.377              Type ("fun", [T1, T2]) =>
   1.378 @@ -1912,7 +1834,6 @@
   1.379              let
   1.380                (* returns a list of lists, each one consisting of n (possibly *)
   1.381                (* identical) elements from 'xs'                               *)
   1.382 -              (* int -> 'a list -> 'a list list *)
   1.383                fun pick_all 1 xs = map single xs
   1.384                  | pick_all n xs =
   1.385                      let val rec_pick = pick_all (n-1) xs in
   1.386 @@ -1929,10 +1850,8 @@
   1.387                (* [["(x1, y1)", ..., "(xn, y1)"], ..., *)
   1.388                (*   ["(x1, ym)", ..., "(xn, ym)"]]     *)
   1.389                val pairss = map (map HOLogic.mk_prod) functions
   1.390 -              (* Term.typ *)
   1.391                val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
   1.392                val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
   1.393 -              (* Term.term *)
   1.394                val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
   1.395                val HOLogic_insert    =
   1.396                  Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   1.397 @@ -2037,8 +1956,7 @@
   1.398                            NONE
   1.399                        | (_, ctypes)::_ =>
   1.400                            let
   1.401 -                            (* int option -- only /recursive/ IDTs have an associated *)
   1.402 -                            (*               depth                                    *)
   1.403 +                            (* only /recursive/ IDTs have an associated depth *)
   1.404                              val depth = AList.lookup (op =) typs (Type (s', Ts'))
   1.405                              (* this should never happen: at depth 0, this IDT fragment *)
   1.406                              (* is definitely empty, and in this case we don't need to  *)
   1.407 @@ -2083,7 +2001,6 @@
   1.408                                        "offset >= total")
   1.409                                | make_constr (d::ds) offset =
   1.410                                    let
   1.411 -                                    (* Term.typ *)
   1.412                                      val dT = typ_of_dtyp descr typ_assoc d
   1.413                                      (* compute canonical term representations for all   *)
   1.414                                      (* elements of the type 'd' (with the reduced depth *)
   1.415 @@ -2131,7 +2048,6 @@
   1.416                                                  "element order not preserved")
   1.417                                            | search [] _ = ()
   1.418                                        in search terms' terms end
   1.419 -                                    (* int * interpretation list *)
   1.420                                      val (intrs, new_offset) =
   1.421                                        fold_map (fn t_elem => fn off =>
   1.422                                          (* if 't_elem' existed at the previous depth,    *)
   1.423 @@ -2333,7 +2249,6 @@
   1.424                        (* argument tuples), we can simply copy corresponding      *)
   1.425                        (* subtrees from 'p_intrs', in the order in which they are *)
   1.426                        (* given.                                                  *)
   1.427 -                      (* interpretation * interpretation -> interpretation list *)
   1.428                        fun ci_pi (Leaf xs, pi) =
   1.429                              (* if the constructor does not match the arguments to a *)
   1.430                              (* defined element of the IDT, the corresponding value  *)
   1.431 @@ -2344,7 +2259,6 @@
   1.432                              raise REFUTE ("IDT_recursion_interpreter",
   1.433                                "constructor takes more arguments than the " ^
   1.434                                  "associated parameter")
   1.435 -                      (* (int * interpretation list) list *)
   1.436                        val rec_operators = map (fn (idx, c_p_intrs) =>
   1.437                          (idx, maps ci_pi c_p_intrs)) mc_p_intrs
   1.438                        (* sanity check: every recursion operator must provide as  *)
   1.439 @@ -2368,7 +2282,6 @@
   1.440                        (* copy 'rec_operators' into arrays first.  Each Boolean   *)
   1.441                        (* indicates whether the recursive arguments have been     *)
   1.442                        (* considered already.                                     *)
   1.443 -                      (* (int * (bool * interpretation) Array.array) list *)
   1.444                        val REC_OPERATORS = map (fn (idx, intrs) =>
   1.445                          (idx, Array.fromList (map (pair false) intrs)))
   1.446                          rec_operators
   1.447 @@ -2376,7 +2289,6 @@
   1.448                        (* interpretation is the 'elem'-th element of the type,  *)
   1.449                        (* the indices of the arguments leading to this leaf are *)
   1.450                        (* returned                                              *)
   1.451 -                      (* interpretation -> int -> int list option *)
   1.452                        fun get_args (Leaf xs) elem =
   1.453                              if find_index (fn x => x = True) xs = elem then
   1.454                                SOME []
   1.455 @@ -2384,7 +2296,6 @@
   1.456                                NONE
   1.457                          | get_args (Node xs) elem =
   1.458                              let
   1.459 -                              (* interpretation list * int -> int list option *)
   1.460                                fun search ([], _) =
   1.461                                  NONE
   1.462                                  | search (x::xs, n) =
   1.463 @@ -2397,10 +2308,8 @@
   1.464                        (* returns the index of the constructor and indices for *)
   1.465                        (* its arguments that generate the 'elem'-th element of *)
   1.466                        (* the datatype given by 'idx'                          *)
   1.467 -                      (* int -> int -> int * int list *)
   1.468                        fun get_cargs idx elem =
   1.469                          let
   1.470 -                          (* int * interpretation list -> int * int list *)
   1.471                            fun get_cargs_rec (_, []) =
   1.472                                  raise REFUTE ("IDT_recursion_interpreter",
   1.473                                    "no matching constructor found for datatype element")
   1.474 @@ -2414,7 +2323,6 @@
   1.475                        (* computes one entry in 'REC_OPERATORS', and recursively *)
   1.476                        (* all entries needed for it, where 'idx' gives the       *)
   1.477                        (* datatype and 'elem' the element of it                  *)
   1.478 -                      (* int -> int -> interpretation *)
   1.479                        fun compute_array_entry idx elem =
   1.480                          let
   1.481                            val arr = the (AList.lookup (op =) REC_OPERATORS idx)
   1.482 @@ -2427,7 +2335,6 @@
   1.483                              (* we have to apply 'intr' to interpretations for all *)
   1.484                              (* recursive arguments                                *)
   1.485                              let
   1.486 -                              (* int * int list *)
   1.487                                val (c, args) = get_cargs idx elem
   1.488                                (* find the indices of the constructor's /recursive/ *)
   1.489                                (* arguments                                         *)
   1.490 @@ -2485,7 +2392,6 @@
   1.491                              raise REFUTE ("IDT_recursion_interpreter",
   1.492                                "unexpected size of IDT (wrong type associated?)")
   1.493                            else ()
   1.494 -                      (* interpretation *)
   1.495                        val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
   1.496                      in
   1.497                        SOME (rec_op, model', args')
   1.498 @@ -2553,7 +2459,6 @@
   1.499      Const (@{const_name Finite_Set.card},
   1.500          Type ("fun", [Type (@{type_name set}, [T]), @{typ nat}])) =>
   1.501        let
   1.502 -        (* interpretation -> int *)
   1.503          fun number_of_elements (Node xs) =
   1.504              fold (fn x => fn n =>
   1.505                if x = TT then
   1.506 @@ -2570,7 +2475,6 @@
   1.507          val size_of_nat = size_of_type ctxt model (@{typ nat})
   1.508          (* takes an interpretation for a set and returns an interpretation *)
   1.509          (* for a 'nat' denoting the set's cardinality                      *)
   1.510 -        (* interpretation -> interpretation *)
   1.511          fun card i =
   1.512            let
   1.513              val n = number_of_elements i
   1.514 @@ -2621,7 +2525,6 @@
   1.515          val size_of_nat = size_of_type ctxt model (@{typ nat})
   1.516          (* the 'n'-th nat is not less than the first 'n' nats, while it *)
   1.517          (* is less than the remaining 'size_of_nat - n' nats            *)
   1.518 -        (* int -> interpretation *)
   1.519          fun less n = Node ((replicate n FF) @ (replicate (size_of_nat - n) TT))
   1.520        in
   1.521          SOME (Node (map less (1 upto size_of_nat)), model, args)
   1.522 @@ -2638,7 +2541,6 @@
   1.523          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.524        let
   1.525          val size_of_nat = size_of_type ctxt model (@{typ nat})
   1.526 -        (* int -> int -> interpretation *)
   1.527          fun plus m n =
   1.528            let
   1.529              val element = m + n
   1.530 @@ -2665,7 +2567,6 @@
   1.531          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.532        let
   1.533          val size_of_nat = size_of_type ctxt model (@{typ nat})
   1.534 -        (* int -> int -> interpretation *)
   1.535          fun minus m n =
   1.536            let
   1.537              val element = Int.max (m-n, 0)
   1.538 @@ -2689,7 +2590,6 @@
   1.539          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.540        let
   1.541          val size_of_nat = size_of_type ctxt model (@{typ nat})
   1.542 -        (* nat -> nat -> interpretation *)
   1.543          fun mult m n =
   1.544            let
   1.545              val element = m * n
   1.546 @@ -2720,7 +2620,6 @@
   1.547          (* maximal length of lists; 0 if we only consider the empty list *)
   1.548          val list_length =
   1.549            let
   1.550 -            (* int -> int -> int -> int *)
   1.551              fun list_length_acc len lists total =
   1.552                if lists = total then
   1.553                  len
   1.554 @@ -2775,7 +2674,6 @@
   1.555          (* index)                                                      *)
   1.556          val lenoff'_lists = map Library.swap lenoff_lists
   1.557          (* returns the interpretation for "(list no. m) @ (list no. n)" *)
   1.558 -        (* nat -> nat -> interpretation *)
   1.559          fun append m n =
   1.560            let
   1.561              val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
   1.562 @@ -2817,20 +2715,17 @@
   1.563          val i_funs = make_constants ctxt model (Type ("fun",
   1.564            [HOLogic.mk_setT T, HOLogic.mk_setT T]))
   1.565          (* "lfp(f) == Inter({u. f(u) <= u})" *)
   1.566 -        (* interpretation * interpretation -> bool *)
   1.567          fun is_subset (Node subs, Node sups) =
   1.568                forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
   1.569            | is_subset (_, _) =
   1.570                raise REFUTE ("lfp_interpreter",
   1.571                  "is_subset: interpretation for set is not a node")
   1.572 -        (* interpretation * interpretation -> interpretation *)
   1.573          fun intersection (Node xs, Node ys) =
   1.574                Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF)
   1.575                  (xs ~~ ys))
   1.576            | intersection (_, _) =
   1.577                raise REFUTE ("lfp_interpreter",
   1.578                  "intersection: interpretation for set is not a node")
   1.579 -        (* interpretation -> interpretaion *)
   1.580          fun lfp (Node resultsets) =
   1.581                fold (fn (set, resultset) => fn acc =>
   1.582                  if is_subset (resultset, set) then
   1.583 @@ -2865,21 +2760,18 @@
   1.584          val i_funs = make_constants ctxt model (Type ("fun",
   1.585            [HOLogic.mk_setT T, HOLogic.mk_setT T]))
   1.586          (* "gfp(f) == Union({u. u <= f(u)})" *)
   1.587 -        (* interpretation * interpretation -> bool *)
   1.588          fun is_subset (Node subs, Node sups) =
   1.589                forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
   1.590                  (subs ~~ sups)
   1.591            | is_subset (_, _) =
   1.592                raise REFUTE ("gfp_interpreter",
   1.593                  "is_subset: interpretation for set is not a node")
   1.594 -        (* interpretation * interpretation -> interpretation *)
   1.595          fun union (Node xs, Node ys) =
   1.596                Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF)
   1.597                     (xs ~~ ys))
   1.598            | union (_, _) =
   1.599                raise REFUTE ("gfp_interpreter",
   1.600                  "union: interpretation for set is not a node")
   1.601 -        (* interpretation -> interpretaion *)
   1.602          fun gfp (Node resultsets) =
   1.603                fold (fn (set, resultset) => fn acc =>
   1.604                  if is_subset (set, resultset) then
   1.605 @@ -2931,14 +2823,11 @@
   1.606  
   1.607  fun stlc_printer ctxt model T intr assignment =
   1.608    let
   1.609 -    (* string -> string *)
   1.610      val strip_leading_quote = perhaps (try (unprefix "'"))
   1.611 -    (* Term.typ -> string *)
   1.612      fun string_of_typ (Type (s, _)) = s
   1.613        | string_of_typ (TFree (x, _)) = strip_leading_quote x
   1.614        | string_of_typ (TVar ((x,i), _)) =
   1.615            strip_leading_quote x ^ string_of_int i
   1.616 -    (* interpretation -> int *)
   1.617      fun index_from_interpretation (Leaf xs) =
   1.618            find_index (Prop_Logic.eval assignment) xs
   1.619        | index_from_interpretation _ =
   1.620 @@ -2950,7 +2839,6 @@
   1.621          let
   1.622            (* create all constants of type 'T1' *)
   1.623            val constants = make_constants ctxt model T1
   1.624 -          (* interpretation list *)
   1.625            val results =
   1.626              (case intr of
   1.627                Node xs => xs
   1.628 @@ -2962,10 +2850,8 @@
   1.629                (print ctxt model T1 arg assignment,
   1.630                 print ctxt model T2 result assignment))
   1.631              (constants ~~ results)
   1.632 -          (* Term.typ *)
   1.633            val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
   1.634            val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
   1.635 -          (* Term.term *)
   1.636            val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
   1.637            val HOLogic_insert    =
   1.638              Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   1.639 @@ -3005,12 +2891,10 @@
   1.640      let
   1.641        (* create all constants of type 'T1' *)
   1.642        val constants = make_constants ctxt model T1
   1.643 -      (* interpretation list *)
   1.644        val results = (case intr of
   1.645            Node xs => xs
   1.646          | _       => raise REFUTE ("set_printer",
   1.647            "interpretation for set type is a leaf"))
   1.648 -      (* Term.term list *)
   1.649        val elements = List.mapPartial (fn (arg, result) =>
   1.650          case result of
   1.651            Leaf [fmTrue, (* fmFalse *) _] =>
   1.652 @@ -3022,9 +2906,7 @@
   1.653            raise REFUTE ("set_printer",
   1.654              "illegal interpretation for a Boolean value"))
   1.655          (constants ~~ results)
   1.656 -      (* Term.typ *)
   1.657        val HOLogic_setT1     = HOLogic.mk_setT T1
   1.658 -      (* Term.term *)
   1.659        val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT1)
   1.660        val HOLogic_insert    =
   1.661          Const (@{const_name insert}, T1 --> HOLogic_setT1 --> HOLogic_setT1)
   1.662 @@ -3078,7 +2960,6 @@
   1.663                          map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts))
   1.664                        val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0,
   1.665                          def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
   1.666 -                      (* interpretation -> int list option *)
   1.667                        fun get_args (Leaf xs) =
   1.668                              if find_index (fn x => x = True) xs = element then
   1.669                                SOME []
   1.670 @@ -3086,7 +2967,6 @@
   1.671                                NONE
   1.672                          | get_args (Node xs) =
   1.673                              let
   1.674 -                              (* interpretation * int -> int list option *)
   1.675                                fun search ([], _) =
   1.676                                  NONE
   1.677                                  | search (x::xs, n) =