src/HOL/Library/refute.ML

 
 datatype 'a tree =
     Leaf of 'a
   | Node of ('a tree) list;
 
-(* ('a -> 'b) -> 'a tree -> 'b tree *)
-
 fun tree_map f tr =
   case tr of
     Leaf x  => Leaf (f x)
   | Node xs => Node (map (tree_map f) xs);
-
-(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
-
-fun tree_foldl f =
-  let
-    fun itl (e, Leaf x)  = f(e,x)
-      | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs)
-  in
-    itl
-  end;
-
-(* 'a tree * 'b tree -> ('a * 'b) tree *)
 
 fun tree_pair (t1, t2) =
   case t1 of
     Leaf x =>
       (case t2 of

 (*      returns a record that can be passed to 'find_model'.                 *)
 (* ------------------------------------------------------------------------- *)
 
 fun actual_params ctxt override =
   let
-    (* (string * string) list * string -> bool *)
     fun read_bool (parms, name) =
       case AList.lookup (op =) parms name of
         SOME "true" => true
       | SOME "false" => false
       | SOME s => error ("parameter " ^ quote name ^
           " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
       | NONE   => error ("parameter " ^ quote name ^
           " must be assigned a value")
-    (* (string * string) list * string -> int *)
     fun read_int (parms, name) =
       case AList.lookup (op =) parms name of
         SOME s =>
           (case Int.fromString s of
             SOME i => i
           | NONE   => error ("parameter " ^ quote name ^
             " (value is " ^ quote s ^ ") must be an integer value"))
       | NONE => error ("parameter " ^ quote name ^
           " must be assigned a value")
-    (* (string * string) list * string -> string *)
     fun read_string (parms, name) =
       case AList.lookup (op =) parms name of
         SOME s => s
       | NONE => error ("parameter " ^ quote name ^
         " must be assigned a value")
     (* 'override' first, defaults last: *)
-    (* (string * string) list *)
     val allparams = override @ get_default_params ctxt
-    (* int *)
     val minsize = read_int (allparams, "minsize")
     val maxsize = read_int (allparams, "maxsize")
     val maxvars = read_int (allparams, "maxvars")
     val maxtime = read_int (allparams, "maxtime")
-    (* string *)
     val satsolver = read_string (allparams, "satsolver")
     val no_assms = read_bool (allparams, "no_assms")
     val expect = the_default "" (AList.lookup (op =) allparams "expect")
     (* all remaining parameters of the form "string=int" are collected in *)
     (* 'sizes'                                                            *)

 (* get_def: looks up the definition of a constant                            *)
 (* ------------------------------------------------------------------------- *)
 
 fun get_def thy (s, T) =
   let
-    (* (string * Term.term) list -> (string * Term.term) option *)
     fun get_def_ax [] = NONE
       | get_def_ax ((axname, ax) :: axioms) =
           (let
             val (lhs, _) = Logic.dest_equals ax  (* equations only *)
             val c        = Term.head_of lhs

 (* get_typedef: looks up the definition of a type, as created by "typedef"   *)
 (* ------------------------------------------------------------------------- *)
 
 fun get_typedef thy T =
   let
-    (* (string * Term.term) list -> (string * Term.term) option *)
     fun get_typedef_ax [] = NONE
       | get_typedef_ax ((axname, ax) :: axioms) =
           (let
-            (* Term.term -> Term.typ option *)
             fun type_of_type_definition (Const (s', T')) =
                   if s'= @{const_name type_definition} then
                     SOME T'
                   else
                     NONE

 (*       the other hand, this would cause additional work for terms where *)
 (*       constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3').  *)
 
 fun unfold_defs thy t =
   let
-    (* Term.term -> Term.term *)
     fun unfold_loop t =
       case t of
       (* Pure *)
         Const (@{const_name all}, _) => t
       | Const (@{const_name "=="}, _) => t

 (*                look up the size of a type in 'sizes'.  Parameterized      *)
 (*                types with different parameters (e.g. "'a list" vs. "bool  *)
 (*                list") are identified.                                     *)
 (* ------------------------------------------------------------------------- *)
 
-(* Term.typ -> string *)
-
 fun string_of_typ (Type (s, _))     = s
   | string_of_typ (TFree (s, _))    = s
   | string_of_typ (TVar ((s,_), _)) = s;
 
 (* ------------------------------------------------------------------------- *)
 (* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
 (*                 'minsize' to every type for which no size is specified in *)
 (*                 'sizes'                                                   *)
 (* ------------------------------------------------------------------------- *)
-
-(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
 
 fun first_universe xs sizes minsize =
   let
     fun size_of_typ T =
       case AList.lookup (op =) sizes (string_of_typ T) of

 (*                types), where the minimal size of a type is given by       *)
 (*                'minsize', the maximal size is given by 'maxsize', and a   *)
 (*                type may have a fixed size given in 'sizes'                *)
 (* ------------------------------------------------------------------------- *)
 
-(* (Term.typ * int) list -> (string * int) list -> int -> int ->
-  (Term.typ * int) list option *)
-
 fun next_universe xs sizes minsize maxsize =
   let
     (* creates the "first" list of length 'len', where the sum of all list *)
     (* elements is 'sum', and the length of the list is 'len'              *)
-    (* int -> int -> int -> int list option *)
     fun make_first _ 0 sum =
           if sum = 0 then
             SOME []
           else
             NONE

             Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0)
           else
             Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
     (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
     (* all list elements x (unless 'max'<0)                                *)
-    (* int -> int -> int -> int list -> int list option *)
     fun next _ _ _ [] =
           NONE
       | next max len sum [x] =
           (* we've reached the last list element, so there's no shift possible *)
           make_first max (len+1) (sum+x+1)  (* increment 'sum' by 1 *)

 (* ------------------------------------------------------------------------- *)
 (* toTrue: converts the interpretation of a Boolean value to a propositional *)
 (*         formula that is true iff the interpretation denotes "true"        *)
 (* ------------------------------------------------------------------------- *)
 
-(* interpretation -> prop_formula *)
-
 fun toTrue (Leaf [fm, _]) = fm
   | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
 
 (* ------------------------------------------------------------------------- *)
 (* toFalse: converts the interpretation of a Boolean value to a              *)
 (*          propositional formula that is true iff the interpretation        *)
 (*          denotes "false"                                                  *)
 (* ------------------------------------------------------------------------- *)
-
-(* interpretation -> prop_formula *)
 
 fun toFalse (Leaf [_, fm]) = fm
   | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
 
 (* ------------------------------------------------------------------------- *)

 fun find_model ctxt
     {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
     assm_ts t negate =
   let
     val thy = Proof_Context.theory_of ctxt
-    (* string -> string *)
     fun check_expect outcome_code =
       if expect = "" orelse outcome_code = expect then outcome_code
       else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
-    (* unit -> string *)
     fun wrapper () =
       let
         val timer = Timer.startRealTimer ()
         val t =
           if no_assms then t
           else if negate then Logic.list_implies (assm_ts, t)
           else Logic.mk_conjunction_list (t :: assm_ts)
         val u = unfold_defs thy t
         val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
         val axioms = collect_axioms ctxt u
-        (* Term.typ list *)
         val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
         val _ = tracing ("Ground types: "
           ^ (if null types then "none."
              else commas (map (Syntax.string_of_typ ctxt) types)))
         (* we can only consider fragments of recursive IDTs, so we issue a  *)

           if maybe_spurious then
             warning ("Term contains a recursive datatype; "
               ^ "countermodel(s) may be spurious!")
           else
             ()
-        (* (Term.typ * int) list -> string *)
         fun find_model_loop universe =
           let
             val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
             val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
                     orelse raise TimeLimit.TimeOut

 (* ------------------------------------------------------------------------- *)
 
 fun make_constants ctxt model T =
   let
     (* returns a list with all unit vectors of length n *)
-    (* int -> interpretation list *)
     fun unit_vectors n =
       let
         (* returns the k-th unit vector of length n *)
-        (* int * int -> interpretation *)
         fun unit_vector (k, n) =
           Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
-        (* int -> interpretation list *)
         fun unit_vectors_loop k =
           if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1)
       in
         unit_vectors_loop 1
       end
     (* returns a list of lists, each one consisting of n (possibly *)
     (* identical) elements from 'xs'                               *)
-    (* int -> 'a list -> 'a list list *)
     fun pick_all 1 xs = map single xs
       | pick_all n xs =
           let val rec_pick = pick_all (n - 1) xs in
             maps (fn x => map (cons x) rec_pick) xs
           end
     (* returns all constant interpretations that have the same tree *)
     (* structure as the interpretation argument                     *)
-    (* interpretation -> interpretation list *)
     fun make_constants_intr (Leaf xs) = unit_vectors (length xs)
       | make_constants_intr (Node xs) = map Node (pick_all (length xs)
           (make_constants_intr (hd xs)))
     (* obtain the interpretation for a variable of type 'T' *)
     val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,

 
 (* ------------------------------------------------------------------------- *)
 (* TT/FF: interpretations that denote "true" or "false", respectively        *)
 (* ------------------------------------------------------------------------- *)
 
-(* interpretation *)
-
 val TT = Leaf [True, False];
 
 val FF = Leaf [False, True];
 
 (* ------------------------------------------------------------------------- *)

 (* in the size of T.  Therefore comparing the interpretations 'i1' and    *)
 (* 'i2' directly is more efficient than constructing the interpretation   *)
 (* for equality on T first, and "applying" this interpretation to 'i1'    *)
 (* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)
 
-(* interpretation * interpretation -> interpretation *)
-
 fun make_equality (i1, i2) =
   let
-    (* interpretation * interpretation -> prop_formula *)
     fun equal (i1, i2) =
       (case i1 of
         Leaf xs =>
           (case i2 of
             Leaf ys => Prop_Logic.dot_product (xs, ys)  (* defined and equal *)

       | Node xs =>
           (case i2 of
             Leaf _  => raise REFUTE ("make_equality",
             "first interpretation is higher")
           | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
-    (* interpretation * interpretation -> prop_formula *)
     fun not_equal (i1, i2) =
       (case i1 of
         Leaf xs =>
           (case i2 of
             (* defined and not equal *)

 (* different from 'make_equality': two undefined interpretations are         *)
 (* considered equal, while a defined interpretation is considered not equal  *)
 (* to an undefined interpretation.                                           *)
 (* ------------------------------------------------------------------------- *)
 
-(* interpretation * interpretation -> interpretation *)
-
 fun make_def_equality (i1, i2) =
   let
-    (* interpretation * interpretation -> prop_formula *)
     fun equal (i1, i2) =
       (case i1 of
         Leaf xs =>
           (case i2 of
             (* defined and equal, or both undefined *)

       | Node xs =>
           (case i2 of
             Leaf _  => raise REFUTE ("make_def_equality",
             "first interpretation is higher")
           | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
-    (* interpretation *)
     val eq = equal (i1, i2)
   in
     Leaf [eq, SNot eq]
   end;
 

 (* interpretation_apply: returns an interpretation that denotes the result   *)
 (*                       of applying the function denoted by 'i1' to the     *)
 (*                       argument denoted by 'i2'                            *)
 (* ------------------------------------------------------------------------- *)
 
-(* interpretation * interpretation -> interpretation *)
-
 fun interpretation_apply (i1, i2) =
   let
-    (* interpretation * interpretation -> interpretation *)
     fun interpretation_disjunction (tr1,tr2) =
       tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys))
         (tree_pair (tr1,tr2))
-    (* prop_formula * interpretation -> interpretation *)
     fun prop_formula_times_interpretation (fm,tr) =
       tree_map (map (fn x => SAnd (fm,x))) tr
-    (* prop_formula list * interpretation list -> interpretation *)
     fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
           prop_formula_times_interpretation (fm,tr)
       | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
           interpretation_disjunction (prop_formula_times_interpretation (fm,tr),
             prop_formula_list_dot_product_interpretation_list (fms,trees))
       | prop_formula_list_dot_product_interpretation_list (_,_) =
           raise REFUTE ("interpretation_apply", "empty list (in dot product)")
     (* returns a list of lists, each one consisting of one element from each *)
     (* element of 'xss'                                                      *)
-    (* 'a list list -> 'a list list *)
     fun pick_all [xs] = map single xs
       | pick_all (xs::xss) =
           let val rec_pick = pick_all xss in
             maps (fn x => map (cons x) rec_pick) xs
           end
       | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
-    (* interpretation -> prop_formula list *)
     fun interpretation_to_prop_formula_list (Leaf xs) = xs
       | interpretation_to_prop_formula_list (Node trees) =
           map Prop_Logic.all (pick_all
             (map interpretation_to_prop_formula_list trees))
   in

 
 (* ------------------------------------------------------------------------- *)
 (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
 (* ------------------------------------------------------------------------- *)
 
-(* Term.term -> int -> Term.term *)
-
 fun eta_expand t i =
   let
     val Ts = Term.binder_types (Term.fastype_of t)
     val t' = Term.incr_boundvars i t
   in

 
 fun stlc_interpreter ctxt model args t =
   let
     val (typs, terms) = model
     val {maxvars, def_eq, next_idx, bounds, wellformed} = args
-    (* Term.typ -> (interpretation * model * arguments) option *)
     fun interpret_groundterm T =
       let
-        (* unit -> (interpretation * model * arguments) option *)
         fun interpret_groundtype () =
           let
             (* the model must specify a size for ground types *)
             val size =
               if T = Term.propT then 2
               else the (AList.lookup (op =) typs T)
             val next = next_idx + size
             (* check if 'maxvars' is large enough *)
             val _ = (if next - 1 > maxvars andalso maxvars > 0 then
               raise MAXVARS_EXCEEDED else ())
-            (* prop_formula list *)
             val fms  = map BoolVar (next_idx upto (next_idx + size - 1))
-            (* interpretation *)
             val intr = Leaf fms
-            (* prop_formula list -> prop_formula *)
             fun one_of_two_false [] = True
               | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
                   SOr (SNot x, SNot x')) xs), one_of_two_false xs)
-            (* prop_formula *)
             val wf = one_of_two_false fms
           in
             (* extend the model, increase 'next_idx', add well-formedness *)
             (* condition                                                  *)
             SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars,

               (* interpretation for 'T2', which are then combined into a single *)
               (* new interpretation                                             *)
               (* make fresh copies, with different variable indices *)
               (* 'idx': next variable index                         *)
               (* 'n'  : number of copies                            *)
-              (* int -> int -> (int * interpretation list * prop_formula *)
               fun make_copies idx 0 = (idx, [], True)
                 | make_copies idx n =
                     let
                       val (copy, _, new_args) = interpret ctxt (typs, [])
                         {maxvars = maxvars, def_eq = false, next_idx = idx,

 
 fun IDT_interpreter ctxt model args t =
   let
     val thy = Proof_Context.theory_of ctxt
     val (typs, terms) = model
-    (* Term.typ -> (interpretation * model * arguments) option *)
     fun interpret_term (Type (s, Ts)) =
           (case Datatype.get_info thy s of
             SOME info =>  (* inductive datatype *)
               let
-                (* int option -- only recursive IDTs have an associated depth *)
+                (* only recursive IDTs have an associated depth *)
                 val depth = AList.lookup (op =) typs (Type (s, Ts))
                 (* sanity check: depth must be at least 0 *)
                 val _ =
                   (case depth of SOME n =>
                     if n < 0 then

                     val next_idx = #next_idx args
                     val next     = next_idx+size
                     (* check if 'maxvars' is large enough *)
                     val _        = (if next-1 > #maxvars args andalso
                       #maxvars args > 0 then raise MAXVARS_EXCEEDED else ())
-                    (* prop_formula list *)
                     val fms      = map BoolVar (next_idx upto (next_idx+size-1))
-                    (* interpretation *)
                     val intr     = Leaf fms
-                    (* prop_formula list -> prop_formula *)
                     fun one_of_two_false [] = True
                       | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
                           SOr (SNot x, SNot x')) xs), one_of_two_false xs)
-                    (* prop_formula *)
                     val wf = one_of_two_false fms
                   in
                     (* extend the model, increase 'next_idx', add well-formedness *)
                     (* condition                                                  *)
                     SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args,

     val thy = Proof_Context.theory_of ctxt
     (* returns a list of canonical representations for terms of the type 'T' *)
     (* It would be nice if we could just use 'print' for this, but 'print'   *)
     (* for IDTs calls 'IDT_constructor_interpreter' again, and this could    *)
     (* lead to infinite recursion when we have (mutually) recursive IDTs.    *)
-    (* (Term.typ * int) list -> Term.typ -> Term.term list *)
     fun canonical_terms typs T =
           (case T of
             Type ("fun", [T1, T2]) =>
             (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *)
             (* least not for 'T2'                                               *)
             let
               (* returns a list of lists, each one consisting of n (possibly *)
               (* identical) elements from 'xs'                               *)
-              (* int -> 'a list -> 'a list list *)
               fun pick_all 1 xs = map single xs
                 | pick_all n xs =
                     let val rec_pick = pick_all (n-1) xs in
                       maps (fn x => map (cons x) rec_pick) xs
                     end

               val functions = map (curry (op ~~) terms1)
                 (pick_all (length terms1) terms2)
               (* [["(x1, y1)", ..., "(xn, y1)"], ..., *)
               (*   ["(x1, ym)", ..., "(xn, ym)"]]     *)
               val pairss = map (map HOLogic.mk_prod) functions
-              (* Term.typ *)
               val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
               val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
-              (* Term.term *)
               val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
               val HOLogic_insert    =
                 Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
             in
               (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)

                         [] =>
                           (* 'Const (s, T)' is not a constructor of this datatype *)
                           NONE
                       | (_, ctypes)::_ =>
                           let
-                            (* int option -- only /recursive/ IDTs have an associated *)
-                            (*               depth                                    *)
+                            (* only /recursive/ IDTs have an associated depth *)
                             val depth = AList.lookup (op =) typs (Type (s', Ts'))
                             (* this should never happen: at depth 0, this IDT fragment *)
                             (* is definitely empty, and in this case we don't need to  *)
                             (* interpret its constructors                              *)
                             val _ = (case depth of SOME 0 =>

                                   else
                                     raise REFUTE ("IDT_constructor_interpreter",
                                       "offset >= total")
                               | make_constr (d::ds) offset =
                                   let
-                                    (* Term.typ *)
                                     val dT = typ_of_dtyp descr typ_assoc d
                                     (* compute canonical term representations for all   *)
                                     (* elements of the type 'd' (with the reduced depth *)
                                     (* for the IDT)                                     *)
                                     val terms' = canonical_terms typs' dT

                                           | search (_::_) [] =
                                               raise REFUTE ("IDT_constructor_interpreter",
                                                 "element order not preserved")
                                           | search [] _ = ()
                                       in search terms' terms end
-                                    (* int * interpretation list *)
                                     val (intrs, new_offset) =
                                       fold_map (fn t_elem => fn off =>
                                         (* if 't_elem' existed at the previous depth,    *)
                                         (* proceed recursively, otherwise map the entire *)
                                         (* subtree to "undefined"                        *)

                       (* Since the order on datatype elements is given by an     *)
                       (* order on constructors (and then by the order on         *)
                       (* argument tuples), we can simply copy corresponding      *)
                       (* subtrees from 'p_intrs', in the order in which they are *)
                       (* given.                                                  *)
-                      (* interpretation * interpretation -> interpretation list *)
                       fun ci_pi (Leaf xs, pi) =
                             (* if the constructor does not match the arguments to a *)
                             (* defined element of the IDT, the corresponding value  *)
                             (* of the parameter must be ignored                     *)
                             if List.exists (equal True) xs then [pi] else []
                         | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys)
                         | ci_pi (Node _, Leaf _) =
                             raise REFUTE ("IDT_recursion_interpreter",
                               "constructor takes more arguments than the " ^
                                 "associated parameter")
-                      (* (int * interpretation list) list *)
                       val rec_operators = map (fn (idx, c_p_intrs) =>
                         (idx, maps ci_pi c_p_intrs)) mc_p_intrs
                       (* sanity check: every recursion operator must provide as  *)
                       (*               many values as the corresponding datatype *)
                       (*               has elements                              *)

                       (* (recursively obtained) interpretations for recursive    *)
                       (* constructor arguments.  To do so more efficiently, we   *)
                       (* copy 'rec_operators' into arrays first.  Each Boolean   *)
                       (* indicates whether the recursive arguments have been     *)
                       (* considered already.                                     *)
-                      (* (int * (bool * interpretation) Array.array) list *)
                       val REC_OPERATORS = map (fn (idx, intrs) =>
                         (idx, Array.fromList (map (pair false) intrs)))
                         rec_operators
                       (* takes an interpretation, and if some leaf of this     *)
                       (* interpretation is the 'elem'-th element of the type,  *)
                       (* the indices of the arguments leading to this leaf are *)
                       (* returned                                              *)
-                      (* interpretation -> int -> int list option *)
                       fun get_args (Leaf xs) elem =
                             if find_index (fn x => x = True) xs = elem then
                               SOME []
                             else
                               NONE
                         | get_args (Node xs) elem =
                             let
-                              (* interpretation list * int -> int list option *)
                               fun search ([], _) =
                                 NONE
                                 | search (x::xs, n) =
                                 (case get_args x elem of
                                   SOME result => SOME (n::result)

                               search (xs, 0)
                             end
                       (* returns the index of the constructor and indices for *)
                       (* its arguments that generate the 'elem'-th element of *)
                       (* the datatype given by 'idx'                          *)
-                      (* int -> int -> int * int list *)
                       fun get_cargs idx elem =
                         let
-                          (* int * interpretation list -> int * int list *)
                           fun get_cargs_rec (_, []) =
                                 raise REFUTE ("IDT_recursion_interpreter",
                                   "no matching constructor found for datatype element")
                             | get_cargs_rec (n, x::xs) =
                                 (case get_args x elem of

                           get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
                         end
                       (* computes one entry in 'REC_OPERATORS', and recursively *)
                       (* all entries needed for it, where 'idx' gives the       *)
                       (* datatype and 'elem' the element of it                  *)
-                      (* int -> int -> interpretation *)
                       fun compute_array_entry idx elem =
                         let
                           val arr = the (AList.lookup (op =) REC_OPERATORS idx)
                           val (flag, intr) = Array.sub (arr, elem)
                         in

                             intr
                           else
                             (* we have to apply 'intr' to interpretations for all *)
                             (* recursive arguments                                *)
                             let
-                              (* int * int list *)
                               val (c, args) = get_cargs idx elem
                               (* find the indices of the constructor's /recursive/ *)
                               (* arguments                                         *)
                               val (_, _, constrs) = the (AList.lookup (op =) descr idx)
                               val (_, dtyps) = nth constrs c

                       val _ =
                           if idt_size <> size_of_type ctxt (typs, []) IDT then
                             raise REFUTE ("IDT_recursion_interpreter",
                               "unexpected size of IDT (wrong type associated?)")
                           else ()
-                      (* interpretation *)
                       val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
                     in
                       SOME (rec_op, model', args')
                     end
                 end

 fun Finite_Set_card_interpreter ctxt model args t =
   case t of
     Const (@{const_name Finite_Set.card},
         Type ("fun", [Type (@{type_name set}, [T]), @{typ nat}])) =>
       let
-        (* interpretation -> int *)
         fun number_of_elements (Node xs) =
             fold (fn x => fn n =>
               if x = TT then
                 n + 1
               else if x = FF then

               raise REFUTE ("Finite_Set_card_interpreter",
                 "interpretation for set type is a leaf")
         val size_of_nat = size_of_type ctxt model (@{typ nat})
         (* takes an interpretation for a set and returns an interpretation *)
         (* for a 'nat' denoting the set's cardinality                      *)
-        (* interpretation -> interpretation *)
         fun card i =
           let
             val n = number_of_elements i
           in
             if n < size_of_nat then

         Type ("fun", [@{typ nat}, @{typ bool}])])) =>
       let
         val size_of_nat = size_of_type ctxt model (@{typ nat})
         (* the 'n'-th nat is not less than the first 'n' nats, while it *)
         (* is less than the remaining 'size_of_nat - n' nats            *)
-        (* int -> interpretation *)
         fun less n = Node ((replicate n FF) @ (replicate (size_of_nat - n) TT))
       in
         SOME (Node (map less (1 upto size_of_nat)), model, args)
       end
   | _ => NONE;

   case t of
     Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
       let
         val size_of_nat = size_of_type ctxt model (@{typ nat})
-        (* int -> int -> interpretation *)
         fun plus m n =
           let
             val element = m + n
           in
             if element > size_of_nat - 1 then

   case t of
     Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
       let
         val size_of_nat = size_of_type ctxt model (@{typ nat})
-        (* int -> int -> interpretation *)
         fun minus m n =
           let
             val element = Int.max (m-n, 0)
           in
             Leaf ((replicate element False) @ True ::

   case t of
     Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
       let
         val size_of_nat = size_of_type ctxt model (@{typ nat})
-        (* nat -> nat -> interpretation *)
         fun mult m n =
           let
             val element = m * n
           in
             if element > size_of_nat - 1 then

         val size_elem = size_of_type ctxt model T
         val size_list = size_of_type ctxt model (Type ("List.list", [T]))
         (* maximal length of lists; 0 if we only consider the empty list *)
         val list_length =
           let
-            (* int -> int -> int -> int *)
             fun list_length_acc len lists total =
               if lists = total then
                 len
               else if lists < total then
                 list_length_acc (len+1) (lists*size_elem) (total-lists)

           end) elements ([], 0)
         (* we also need the reverse association (from length/offset to *)
         (* index)                                                      *)
         val lenoff'_lists = map Library.swap lenoff_lists
         (* returns the interpretation for "(list no. m) @ (list no. n)" *)
-        (* nat -> nat -> interpretation *)
         fun append m n =
           let
             val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
             val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
             val len_elem = len_m + len_n

         val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
         (* all functions that map sets to sets *)
         val i_funs = make_constants ctxt model (Type ("fun",
           [HOLogic.mk_setT T, HOLogic.mk_setT T]))
         (* "lfp(f) == Inter({u. f(u) <= u})" *)
-        (* interpretation * interpretation -> bool *)
         fun is_subset (Node subs, Node sups) =
               forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
           | is_subset (_, _) =
               raise REFUTE ("lfp_interpreter",
                 "is_subset: interpretation for set is not a node")
-        (* interpretation * interpretation -> interpretation *)
         fun intersection (Node xs, Node ys) =
               Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF)
                 (xs ~~ ys))
           | intersection (_, _) =
               raise REFUTE ("lfp_interpreter",
                 "intersection: interpretation for set is not a node")
-        (* interpretation -> interpretaion *)
         fun lfp (Node resultsets) =
               fold (fn (set, resultset) => fn acc =>
                 if is_subset (resultset, set) then
                   intersection (acc, set)
                 else

         val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
         (* all functions that map sets to sets *)
         val i_funs = make_constants ctxt model (Type ("fun",
           [HOLogic.mk_setT T, HOLogic.mk_setT T]))
         (* "gfp(f) == Union({u. u <= f(u)})" *)
-        (* interpretation * interpretation -> bool *)
         fun is_subset (Node subs, Node sups) =
               forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
                 (subs ~~ sups)
           | is_subset (_, _) =
               raise REFUTE ("gfp_interpreter",
                 "is_subset: interpretation for set is not a node")
-        (* interpretation * interpretation -> interpretation *)
         fun union (Node xs, Node ys) =
               Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF)
                    (xs ~~ ys))
           | union (_, _) =
               raise REFUTE ("gfp_interpreter",
                 "union: interpretation for set is not a node")
-        (* interpretation -> interpretaion *)
         fun gfp (Node resultsets) =
               fold (fn (set, resultset) => fn acc =>
                 if is_subset (set, resultset) then
                   union (acc, set)
                 else

 (* PRINTERS                                                                  *)
 (* ------------------------------------------------------------------------- *)
 
 fun stlc_printer ctxt model T intr assignment =
   let
-    (* string -> string *)
     val strip_leading_quote = perhaps (try (unprefix "'"))
-    (* Term.typ -> string *)
     fun string_of_typ (Type (s, _)) = s
       | string_of_typ (TFree (x, _)) = strip_leading_quote x
       | string_of_typ (TVar ((x,i), _)) =
           strip_leading_quote x ^ string_of_int i
-    (* interpretation -> int *)
     fun index_from_interpretation (Leaf xs) =
           find_index (Prop_Logic.eval assignment) xs
       | index_from_interpretation _ =
           raise REFUTE ("stlc_printer",
             "interpretation for ground type is not a leaf")

     case T of
       Type ("fun", [T1, T2]) =>
         let
           (* create all constants of type 'T1' *)
           val constants = make_constants ctxt model T1
-          (* interpretation list *)
           val results =
             (case intr of
               Node xs => xs
             | _ => raise REFUTE ("stlc_printer",
               "interpretation for function type is a leaf"))

           val pairs = map (fn (arg, result) =>
             HOLogic.mk_prod
               (print ctxt model T1 arg assignment,
                print ctxt model T2 result assignment))
             (constants ~~ results)
-          (* Term.typ *)
           val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
           val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
-          (* Term.term *)
           val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
           val HOLogic_insert    =
             Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
         in
           SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)

   (case T of
     Type (@{type_name set}, [T1]) =>
     let
       (* create all constants of type 'T1' *)
       val constants = make_constants ctxt model T1
-      (* interpretation list *)
       val results = (case intr of
           Node xs => xs
         | _       => raise REFUTE ("set_printer",
           "interpretation for set type is a leaf"))
-      (* Term.term list *)
       val elements = List.mapPartial (fn (arg, result) =>
         case result of
           Leaf [fmTrue, (* fmFalse *) _] =>
           if Prop_Logic.eval assignment fmTrue then
             SOME (print ctxt model T1 arg assignment)

             NONE
         | _ =>
           raise REFUTE ("set_printer",
             "illegal interpretation for a Boolean value"))
         (constants ~~ results)
-      (* Term.typ *)
       val HOLogic_setT1     = HOLogic.mk_setT T1
-      (* Term.term *)
       val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT1)
       val HOLogic_insert    =
         Const (@{const_name insert}, T1 --> HOLogic_setT1 --> HOLogic_setT1)
     in
       SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc)

                     let
                       val cTerm      = Const (cname,
                         map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts))
                       val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0,
                         def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
-                      (* interpretation -> int list option *)
                       fun get_args (Leaf xs) =
                             if find_index (fn x => x = True) xs = element then
                               SOME []
                             else
                               NONE
                         | get_args (Node xs) =
                             let
-                              (* interpretation * int -> int list option *)
                               fun search ([], _) =
                                 NONE
                                 | search (x::xs, n) =
                                 (case get_args x of
                                   SOME result => SOME (n::result)