--- a/src/HOL/Library/refute.ML Sat Feb 15 18:48:43 2014 +0100
+++ b/src/HOL/Library/refute.ML Sat Feb 15 21:09:48 2014 +0100
@@ -102,25 +102,11 @@
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 =>
@@ -335,7 +321,6 @@
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
@@ -344,7 +329,6 @@
" (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 =>
@@ -354,21 +338,17 @@
" (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")
@@ -461,7 +441,6 @@
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
@@ -492,11 +471,9 @@
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'
@@ -557,7 +534,6 @@
fun unfold_defs thy t =
let
- (* Term.term -> Term.term *)
fun unfold_loop t =
case t of
(* Pure *)
@@ -907,8 +883,6 @@
(* 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;
@@ -919,8 +893,6 @@
(* 'sizes' *)
(* ------------------------------------------------------------------------- *)
-(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
-
fun first_universe xs sizes minsize =
let
fun size_of_typ T =
@@ -938,14 +910,10 @@
(* 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 []
@@ -958,7 +926,6 @@
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] =
@@ -994,8 +961,6 @@
(* 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");
@@ -1005,8 +970,6 @@
(* denotes "false" *)
(* ------------------------------------------------------------------------- *)
-(* interpretation -> prop_formula *)
-
fun toFalse (Leaf [_, fm]) = fm
| toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
@@ -1025,11 +988,9 @@
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 ()
@@ -1040,7 +1001,6 @@
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."
@@ -1069,7 +1029,6 @@
^ "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)
@@ -1271,14 +1230,11 @@
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
@@ -1286,7 +1242,6 @@
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
@@ -1294,7 +1249,6 @@
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)))
@@ -1335,8 +1289,6 @@
(* TT/FF: interpretations that denote "true" or "false", respectively *)
(* ------------------------------------------------------------------------- *)
-(* interpretation *)
-
val TT = Leaf [True, False];
val FF = Leaf [False, True];
@@ -1359,11 +1311,8 @@
(* 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 =>
@@ -1376,7 +1325,6 @@
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 =>
@@ -1407,11 +1355,8 @@
(* 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 =>
@@ -1426,7 +1371,6 @@
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]
@@ -1438,18 +1382,13 @@
(* 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) =
@@ -1459,14 +1398,12 @@
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
@@ -1484,8 +1421,6 @@
(* 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)
@@ -1520,10 +1455,8 @@
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 *)
@@ -1534,15 +1467,11 @@
(* 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 *)
@@ -1561,7 +1490,6 @@
(* 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
@@ -1807,12 +1735,11 @@
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 _ =
@@ -1853,15 +1780,11 @@
(* 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 *)
@@ -1903,7 +1826,6 @@
(* 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]) =>
@@ -1912,7 +1834,6 @@
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
@@ -1929,10 +1850,8 @@
(* [["(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)
@@ -2037,8 +1956,7 @@
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 *)
@@ -2083,7 +2001,6 @@
"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 *)
@@ -2131,7 +2048,6 @@
"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, *)
@@ -2333,7 +2249,6 @@
(* 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 *)
@@ -2344,7 +2259,6 @@
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 *)
@@ -2368,7 +2282,6 @@
(* 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
@@ -2376,7 +2289,6 @@
(* 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 []
@@ -2384,7 +2296,6 @@
NONE
| get_args (Node xs) elem =
let
- (* interpretation list * int -> int list option *)
fun search ([], _) =
NONE
| search (x::xs, n) =
@@ -2397,10 +2308,8 @@
(* 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")
@@ -2414,7 +2323,6 @@
(* 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)
@@ -2427,7 +2335,6 @@
(* 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 *)
@@ -2485,7 +2392,6 @@
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')
@@ -2553,7 +2459,6 @@
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
@@ -2570,7 +2475,6 @@
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
@@ -2621,7 +2525,6 @@
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)
@@ -2638,7 +2541,6 @@
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
@@ -2665,7 +2567,6 @@
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)
@@ -2689,7 +2590,6 @@
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
@@ -2720,7 +2620,6 @@
(* 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
@@ -2775,7 +2674,6 @@
(* 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)
@@ -2817,20 +2715,17 @@
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
@@ -2865,21 +2760,18 @@
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
@@ -2931,14 +2823,11 @@
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 _ =
@@ -2950,7 +2839,6 @@
let
(* create all constants of type 'T1' *)
val constants = make_constants ctxt model T1
- (* interpretation list *)
val results =
(case intr of
Node xs => xs
@@ -2962,10 +2850,8 @@
(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)
@@ -3005,12 +2891,10 @@
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 *) _] =>
@@ -3022,9 +2906,7 @@
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)
@@ -3078,7 +2960,6 @@
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 []
@@ -3086,7 +2967,6 @@
NONE
| get_args (Node xs) =
let
- (* interpretation * int -> int list option *)
fun search ([], _) =
NONE
| search (x::xs, n) =