support for recursion over mutually recursive IDTs
authorwebertj
Mon Apr 18 17:20:49 2005 +0200 (2005-04-18)
changeset 157678ed9fcc004fe
parent 15766 b08feb003f3c
child 15768 a167d50eadbb
support for recursion over mutually recursive IDTs
src/HOL/Tools/refute.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Apr 18 15:54:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Apr 18 17:20:49 2005 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4  			 parameters = Symtab.merge (op=) (pa1, pa2)};
     1.5  		fun print sg {interpreters, printers, parameters} =
     1.6  			Pretty.writeln (Pretty.chunks
     1.7 -				[Pretty.strs ("default parameters:" :: List.concat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
     1.8 +				[Pretty.strs ("default parameters:" :: List.concat (map (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
     1.9  				 Pretty.strs ("interpreters:" :: map fst interpreters),
    1.10  				 Pretty.strs ("printers:" :: map fst printers)]);
    1.11  	end;
    1.12 @@ -624,6 +624,7 @@
    1.13  			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.14  			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.15  			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.16 +			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
    1.17  			(* simply-typed lambda calculus *)
    1.18  			| Const (s, T)                    =>
    1.19  				let
    1.20 @@ -896,8 +897,8 @@
    1.21  
    1.22  	(* interpretation -> prop_formula *)
    1.23  
    1.24 -	fun toTrue (Leaf [fm,_]) = fm
    1.25 -	  | toTrue _             = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
    1.26 +	fun toTrue (Leaf [fm, _]) = fm
    1.27 +	  | toTrue _              = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
    1.28  
    1.29  (* ------------------------------------------------------------------------- *)
    1.30  (* toFalse: converts the interpretation of a Boolean value to a              *)
    1.31 @@ -907,8 +908,8 @@
    1.32  
    1.33  	(* interpretation -> prop_formula *)
    1.34  
    1.35 -	fun toFalse (Leaf [_,fm]) = fm
    1.36 -	  | toFalse _             = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
    1.37 +	fun toFalse (Leaf [_, fm]) = fm
    1.38 +	  | toFalse _              = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
    1.39  
    1.40  (* ------------------------------------------------------------------------- *)
    1.41  (* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)
    1.42 @@ -1607,7 +1608,7 @@
    1.43  				in
    1.44  					SOME (intr, (typs, (t, intr)::terms), args')
    1.45  				end
    1.46 -			| Var ((x,i), Type ("set", [T])) =>
    1.47 +			| Var ((x, i), Type ("set", [T])) =>
    1.48  				let
    1.49  					val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
    1.50  				in
    1.51 @@ -1896,27 +1897,33 @@
    1.52  					result  (* just keep 'result' *)
    1.53  				| NONE =>
    1.54  					if s mem (#rec_names info) then
    1.55 -						(* okay, we do have a recursion operator of the datatype given by 'info' *)
    1.56 +						(* we do have a recursion operator of the datatype given by 'info', *)
    1.57 +						(* or of a mutually recursive datatype                              *)
    1.58  						let
    1.59 -							val index               = #index info
    1.60 -							val descr               = #descr info
    1.61 -							val (_, dtyps, constrs) = (valOf o assoc) (descr, index)
    1.62 -							(* the total number of constructors, including those of different    *)
    1.63 -							(* (mutually recursive) datatypes within the same descriptor 'descr' *)
    1.64 -							val constrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr)
    1.65 -							val params_count  = length params
    1.66 +							val index              = #index info
    1.67 +							val descr              = #descr info
    1.68 +							val (dtname, dtyps, _) = (valOf o assoc) (descr, index)
    1.69 +							(* number of all constructors, including those of different           *)
    1.70 +							(* (mutually recursive) datatypes within the same descriptor 'descr'  *)
    1.71 +							val mconstrs_count     = sum (map (fn (_, (_, _, cs)) => length cs) descr)
    1.72 +							val params_count       = length params
    1.73 +							(* the type of a recursion operator: [T1, ..., Tn, IDT] ---> Tresult *)
    1.74 +							val IDT = List.nth (binder_types T, mconstrs_count)
    1.75  						in
    1.76 -							if constrs_count < params_count then
    1.77 +							if (fst o dest_Type) IDT <> dtname then
    1.78 +								(* recursion operator of a mutually recursive datatype *)
    1.79 +								NONE
    1.80 +							else if mconstrs_count < params_count then
    1.81  								(* too many actual parameters; for now we'll use the *)
    1.82  								(* 'stlc_interpreter' to strip off one application   *)
    1.83  								NONE
    1.84 -							else if constrs_count > params_count then
    1.85 +							else if mconstrs_count > params_count then
    1.86  								(* too few actual parameters; we use eta expansion            *)
    1.87  								(* Note that the resulting expansion of lambda abstractions   *)
    1.88  								(* by the 'stlc_interpreter' may be rather slow (depending on *)
    1.89  								(* the argument types and the size of the IDT, of course).    *)
    1.90 -								SOME (interpret thy model args (eta_expand t (constrs_count - params_count)))
    1.91 -							else  (* constrs_count = params_count *)
    1.92 +								SOME (interpret thy model args (eta_expand t (mconstrs_count - params_count)))
    1.93 +							else  (* mconstrs_count = params_count *)
    1.94  								let
    1.95  									(* interpret each parameter separately *)
    1.96  									val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) =>
    1.97 @@ -1925,23 +1932,37 @@
    1.98  										in
    1.99  											((m', a'), i)
   1.100  										end) ((model, args), params)
   1.101 -									val (typs, terms) = model'
   1.102 -									(* the type of a recursion operator: [T1, ..., Tn, IDT] ---> Tresult *)
   1.103 -									val IDT       = List.nth (binder_types T, constrs_count)
   1.104 +									val (typs, _) = model'
   1.105  									val typ_assoc = dtyps ~~ (snd o dest_Type) IDT
   1.106 -									(* interpret each constructor of the datatype *)
   1.107 -									(* TODO: we probably need to interpret every constructor in the descriptor, *)
   1.108 -									(*       possibly for typs' instead of typs                                 *)
   1.109 -									val c_intrs = map (#1 o interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True})
   1.110 -										(map (fn (cname, cargs) => Const (cname, map (typ_of_dtyp descr typ_assoc) cargs ---> IDT)) constrs)
   1.111 +									(* interpret each constructor in the descriptor (including *)
   1.112 +									(* those of mutually recursive datatypes)                  *)
   1.113 +									(* (int * interpretation list) list *)
   1.114 +									val mc_intrs = map (fn (idx, (_, _, cs)) =>
   1.115 +										let
   1.116 +											val c_return_typ = typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec idx)
   1.117 +										in
   1.118 +											(idx, map (fn (cname, cargs) =>
   1.119 +												(#1 o interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True})
   1.120 +													(Const (cname, map (typ_of_dtyp descr typ_assoc) cargs ---> c_return_typ))) cs)
   1.121 +										end) descr
   1.122 +									val _ = writeln (makestring index)
   1.123 +									val _ = writeln (makestring descr)
   1.124 +									val _ = writeln (makestring mc_intrs)
   1.125  									(* the recursion operator is a function that maps every element of *)
   1.126 -									(* the inductive datatype to an element of the result type         *)
   1.127 -									val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", IDT))
   1.128 -									val size      = size_of_type i
   1.129 -									val INTRS     = Array.array (size, Leaf [])  (* the initial value 'Leaf []' does not matter; it will be overwritten *)
   1.130 -									(* takes an interpretation, and if some leaf of this interpretation *)
   1.131 -									(* is the 'elem'-th element of the datatype, the indices of the     *)
   1.132 -									(* arguments leading to this leaf are returned                      *)
   1.133 +									(* the inductive datatype (and of mutually recursive types) to an  *)
   1.134 +									(* element of some result type                                     *)
   1.135 +									(* (int * interpretation option Array.array) list *)
   1.136 +									val INTRS = map (fn (idx, _) =>
   1.137 +										let
   1.138 +											val T         = typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec idx)
   1.139 +											val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.140 +											val size      = size_of_type i
   1.141 +										in
   1.142 +											(idx, Array.array (size, NONE))
   1.143 +										end) descr
   1.144 +									(* takes an interpretation, and if some leaf of this interpretation   *)
   1.145 +									(* is the 'elem'-th element of the type, the indices of the arguments *)
   1.146 +									(* leading to this leaf are returned                                  *)
   1.147  									(* interpretation -> int -> int list option *)
   1.148  									fun get_args (Leaf xs) elem =
   1.149  										if find_index_eq True xs = elem then
   1.150 @@ -1962,27 +1983,46 @@
   1.151  										end
   1.152  									(* returns the index of the constructor and indices for its      *)
   1.153  									(* arguments that generate the 'elem'-th element of the datatype *)
   1.154 -									(* int -> int * int list *)
   1.155 -									fun get_cargs elem =
   1.156 +									(* given by 'idx'                                                *)
   1.157 +									(* int -> int -> int * int list *)
   1.158 +									fun get_cargs idx elem =
   1.159  										let
   1.160  											(* int * interpretation list -> int * int list *)
   1.161  											fun get_cargs_rec (_, []) =
   1.162 -												raise REFUTE ("IDT_recursion_interpreter", "no matching constructor found for element " ^ string_of_int elem)
   1.163 +												raise REFUTE ("IDT_recursion_interpreter", "no matching constructor found for element " ^ string_of_int elem ^ " in datatype " ^ Sign.string_of_typ (sign_of thy) IDT ^ " (datatype index " ^ string_of_int idx ^ ")")
   1.164  											  | get_cargs_rec (n, x::xs) =
   1.165  												(case get_args x elem of
   1.166  												  SOME args => (n, args)
   1.167  												| NONE      => get_cargs_rec (n+1, xs))
   1.168  										in
   1.169 -											get_cargs_rec (0, c_intrs)
   1.170 +											get_cargs_rec (0, (valOf o assoc) (mc_intrs, idx))
   1.171  										end
   1.172 -									(* int -> unit *)
   1.173 -									fun compute_loop elem =
   1.174 -										if elem=size then
   1.175 -											()
   1.176 -										else  (* elem < size *)
   1.177 +									(* returns the number of constructors in datatypes that occur in *)
   1.178 +									(* the descriptor 'descr' before the datatype given by 'idx'     *)
   1.179 +									fun get_coffset idx =
   1.180 +										let
   1.181 +											fun get_coffset_acc _ [] =
   1.182 +												raise REFUTE ("IDT_recursion_interpreter", "index " ^ string_of_int idx ^ " not found in descriptor")
   1.183 +											  | get_coffset_acc sum ((i, (_, _, cs))::descr') =
   1.184 +												if i=idx then
   1.185 +													sum
   1.186 +												else
   1.187 +													get_coffset_acc (sum + length cs) descr'
   1.188 +										in
   1.189 +											get_coffset_acc 0 descr
   1.190 +										end
   1.191 +									(* computes one entry in INTRS, and recursively all entries needed for it, *)
   1.192 +									(* where 'idx' gives the datatype and 'elem' the element of it             *)
   1.193 +									(* int -> int -> interpretation *)
   1.194 +									fun compute_array_entry idx elem =
   1.195 +										case Array.sub ((valOf o assoc) (INTRS, idx), elem) of
   1.196 +										  SOME result =>
   1.197 +											(* simply return the previously computed result *)
   1.198 +											result
   1.199 +										| NONE =>
   1.200  											let
   1.201  												(* int * int list *)
   1.202 -												val (c, args) = get_cargs elem
   1.203 +												val (c, args) = get_cargs idx elem
   1.204  												(* interpretation * int list -> interpretation *)
   1.205  												fun select_subtree (tr, []) =
   1.206  													tr  (* return the whole tree *)
   1.207 @@ -1991,22 +2031,40 @@
   1.208  												  | select_subtree (Node tr, x::xs) =
   1.209  													select_subtree (List.nth (tr, x), xs)
   1.210  												(* select the correct subtree of the parameter corresponding to constructor 'c' *)
   1.211 -												val p_intr = select_subtree (List.nth (p_intrs, c), args)
   1.212 -												(* find the indices of recursive arguments *)
   1.213 -												val rec_args = map snd (List.filter (DatatypeAux.is_rec_type o fst) ((snd (List.nth (constrs, c))) ~~ args))
   1.214 +												val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args)
   1.215 +												(* find the indices of the constructor's recursive arguments *)
   1.216 +												val (_, _, constrs) = (valOf o assoc) (descr, idx)
   1.217 +												val constr_args     = (snd o List.nth) (constrs, c)
   1.218 +												val rec_args        = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)
   1.219 +												val rec_args'       = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args
   1.220  												(* apply 'p_intr' to recursively computed results *)
   1.221 -												val rec_p_intr = Library.foldl (fn (i, n) => interpretation_apply (i, Array.sub (INTRS, n))) (p_intr, rec_args)
   1.222 +												val result = foldl (fn ((idx, elem), intr) =>
   1.223 +													interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args'
   1.224  												(* update 'INTRS' *)
   1.225 -												val _ = Array.update (INTRS, elem, rec_p_intr)
   1.226 +												val _ = Array.update ((valOf o assoc) (INTRS, idx), elem, SOME result)
   1.227  											in
   1.228 -												compute_loop (elem+1)
   1.229 +												result
   1.230  											end
   1.231 +									(* compute all entries in INTRS for the current datatype (given by 'index') *)
   1.232 +									val size = (Array.length o valOf o assoc) (INTRS, index)
   1.233 +									(* int -> unit *)
   1.234 +									fun compute_loop elem =
   1.235 +										if elem=size then
   1.236 +											(* terminate *)
   1.237 +											()
   1.238 +										else (  (* elem < size *)
   1.239 +											compute_array_entry index elem;
   1.240 +											compute_loop (elem+1)
   1.241 +										)
   1.242  									val _ = compute_loop 0
   1.243 +									val _ = Array.modifyi ... ((valOf o assoc) (INTRS, index))
   1.244  									(* 'a Array.array -> 'a list *)
   1.245  									fun toList arr =
   1.246  										Array.foldr op:: [] arr
   1.247 +									val _ = writeln (makestring INTRS)
   1.248  								in
   1.249 -									SOME (Node (toList INTRS), model', args')
   1.250 +									(* return the part of 'INTRS' that corresponds to the current datatype *)
   1.251 +									SOME ((Node o (map valOf) o toList o valOf o assoc) (INTRS, index), model', args')
   1.252  								end
   1.253  						end
   1.254  					else
   1.255 @@ -2111,7 +2169,8 @@
   1.256  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   1.257  				val size_nat      = size_of_type i_nat
   1.258  				(* int -> int -> interpretation *)
   1.259 -				fun plus m n = let
   1.260 +				fun plus m n =
   1.261 +					let
   1.262  						val element = (m+n)+1
   1.263  					in
   1.264  						if element > size_nat then
   1.265 @@ -2138,7 +2197,8 @@
   1.266  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   1.267  				val size_nat      = size_of_type i_nat
   1.268  				(* int -> int -> interpretation *)
   1.269 -				fun minus m n = let
   1.270 +				fun minus m n =
   1.271 +					let
   1.272  						val element = Int.max (m-n, 0) + 1
   1.273  					in
   1.274  						Leaf ((replicate (element-1) False) @ True :: (replicate (size_nat - element) False))
   1.275 @@ -2162,7 +2222,8 @@
   1.276  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
   1.277  				val size_nat      = size_of_type i_nat
   1.278  				(* nat -> nat -> interpretation *)
   1.279 -				fun mult m n = let
   1.280 +				fun mult m n =
   1.281 +					let
   1.282  						val element = (m*n)+1
   1.283  					in
   1.284  						if element > size_nat then
   1.285 @@ -2176,6 +2237,53 @@
   1.286  		| _ =>
   1.287  			NONE;
   1.288  
   1.289 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.290 +
   1.291 +	(* only an optimization: 'op @' could in principle be interpreted with    *)
   1.292 +	(* interpreters available already (using its definition), but the code    *)
   1.293 +	(* below is more efficient                                                *)
   1.294 +
   1.295 +	fun List_append_interpreter thy model args t =
   1.296 +		case t of
   1.297 +		  Const ("List.op @", Type ("fun", [Type ("List.list", [T]), Type ("fun", [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
   1.298 +			let
   1.299 +				val (i_elem, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.300 +				val size_elem      = size_of_type i_elem
   1.301 +				val (i_list, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("List.list", [T])))
   1.302 +				val size_list      = size_of_type i_list
   1.303 +				(* power (a, b) computes a^b, for a>=0, b>=0 *)
   1.304 +				(* int * int -> int *)
   1.305 +				fun power (a, 0) = 1
   1.306 +				  | power (a, 1) = a
   1.307 +				  | power (a, b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
   1.308 +				(* log (a, b) computes floor(log_a(b)), i.e. the largest integer x s.t. a^x <= b, for a>=2, b>=1 *)
   1.309 +				(* int * int -> int *)
   1.310 +				fun log (a, b) =
   1.311 +					let
   1.312 +						fun logloop (ax, x) =
   1.313 +							if ax > b then x-1 else logloop (a * ax, x+1)
   1.314 +					in
   1.315 +						logloop (1, 0)
   1.316 +					end
   1.317 +				(* nat -> nat -> interpretation *)
   1.318 +				fun append m n =
   1.319 +					let
   1.320 +						(* The following formula depends on the order in which lists are *)
   1.321 +						(* enumerated by the 'IDT_constructor_interpreter'.  It took me  *)
   1.322 +						(* a while to come up with this formula.                         *)
   1.323 +						val element = n + m * (if size_elem = 1 then 1 else power (size_elem, log (size_elem, n+1))) + 1
   1.324 +					in
   1.325 +						if element > size_list then
   1.326 +							Leaf (replicate size_list False)
   1.327 +						else
   1.328 +							Leaf ((replicate (element-1) False) @ True :: (replicate (size_list - element) False))
   1.329 +					end
   1.330 +			in
   1.331 +				SOME (Node (map (fn m => Node (map (append m) (0 upto size_list-1))) (0 upto size_list-1)), model, args)
   1.332 +			end
   1.333 +		| _ =>
   1.334 +			NONE;
   1.335 +
   1.336  
   1.337  (* ------------------------------------------------------------------------- *)
   1.338  (* PRINTERS                                                                  *)
   1.339 @@ -2413,6 +2521,7 @@
   1.340  		 add_interpreter "Nat.op +" Nat_plus_interpreter,
   1.341  		 add_interpreter "Nat.op -" Nat_minus_interpreter,
   1.342  		 add_interpreter "Nat.op *" Nat_mult_interpreter,
   1.343 +		 add_interpreter "List.op @" List_append_interpreter,
   1.344  		 add_printer "stlc" stlc_printer,
   1.345  		 add_printer "set"  set_printer,
   1.346  		 add_printer "IDT"  IDT_printer];
     2.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Apr 18 15:54:23 2005 +0200
     2.2 +++ b/src/HOL/ex/Refute_Examples.thy	Mon Apr 18 17:20:49 2005 +0200
     2.3 @@ -161,7 +161,8 @@
     2.4  oops
     2.5  
     2.6  lemma "\<forall>a b c d e f. a=b | a=c | a=d | a=e | a=f | b=c | b=d | b=e | b=f | c=d | c=e | c=f | d=e | d=f | e=f"
     2.7 -  refute
     2.8 +  refute  -- {* quantification causes an expansion of the formula; the
     2.9 +                previous version with free variables is refuted much faster *}
    2.10  oops
    2.11  
    2.12  text {* "Every reflexive and symmetric relation is transitive." *}
    2.13 @@ -451,6 +452,8 @@
    2.14    apply (auto simp add: someI)
    2.15  done
    2.16  
    2.17 +(******************************************************************************)
    2.18 +
    2.19  subsection {* Subtypes (typedef), typedecl *}
    2.20  
    2.21  text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
    2.22 @@ -471,16 +474,16 @@
    2.23    refute
    2.24  oops
    2.25  
    2.26 +(******************************************************************************)
    2.27 +
    2.28  subsection {* Inductive datatypes *}
    2.29  
    2.30 -text {* This is necessary because with quick\_and\_dirty set, the datatype
    2.31 -package does not generate certain axioms for recursion operators.  Without
    2.32 -these axioms, refute may find spurious countermodels. *}
    2.33 +text {* With quick\_and\_dirty set, the datatype package does not generate
    2.34 +  certain axioms for recursion operators.  Without these axioms, refute may
    2.35 +  find spurious countermodels. *}
    2.36  
    2.37  ML {* reset quick_and_dirty; *}
    2.38  
    2.39 -(*TODO*) ML {* set show_consts; set show_types; *}
    2.40 -
    2.41  subsubsection {* unit *}
    2.42  
    2.43  lemma "P (x::unit)"
    2.44 @@ -777,11 +780,11 @@
    2.45  oops
    2.46  
    2.47  lemma "P (aexp_bexp_rec_2 number ite equal x)"
    2.48 -  (*TODO refute*)
    2.49 +  refute
    2.50  oops
    2.51  
    2.52  lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
    2.53 -  (*TODO: refute*)
    2.54 +  refute
    2.55  oops
    2.56  
    2.57  subsubsection {* Other datatype examples *}
    2.58 @@ -800,7 +803,11 @@
    2.59    refute
    2.60  oops
    2.61  
    2.62 -lemma "P (Trie_rec tr x)"
    2.63 +lemma "P (Trie_rec_1 a b c x)"
    2.64 +  refute
    2.65 +oops
    2.66 +
    2.67 +lemma "P (Trie_rec_2 a b c x)"
    2.68    refute
    2.69  oops
    2.70  
    2.71 @@ -840,14 +847,106 @@
    2.72    refute
    2.73  oops
    2.74  
    2.75 -subsubsection {* Examples involving certain functions *}
    2.76 +text {* Taken from "Inductive datatypes in HOL", p.8: *}
    2.77 +
    2.78 +datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
    2.79 +datatype 'c U = E "('c, 'c U) T"
    2.80 +
    2.81 +lemma "P (x::'c U)"
    2.82 +  refute
    2.83 +oops
    2.84 +
    2.85 +lemma "\<forall>x::'c U. P x"
    2.86 +  refute
    2.87 +oops
    2.88 +
    2.89 +lemma "P (E (C (\<lambda>a. True)))"
    2.90 +  refute
    2.91 +oops
    2.92 +
    2.93 +lemma "P (U_rec_1 e f g h i x)"
    2.94 +  refute
    2.95 +oops
    2.96 +
    2.97 +lemma "P (U_rec_2 e f g h i x)"
    2.98 +  refute
    2.99 +oops
   2.100 +
   2.101 +lemma "P (U_rec_3 e f g h i x)"
   2.102 +  refute
   2.103 +oops
   2.104 +
   2.105 +(******************************************************************************)
   2.106 +
   2.107 +subsection {* Records *}
   2.108 +
   2.109 +(*TODO: make use of pair types, rather than typedef, for record types*)
   2.110 +
   2.111 +record ('a, 'b) point =
   2.112 +  xpos :: 'a
   2.113 +  ypos :: 'b
   2.114 +
   2.115 +lemma "(x::('a, 'b) point) = y"
   2.116 +  refute
   2.117 +oops
   2.118 +
   2.119 +record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
   2.120 +  ext :: 'c
   2.121 +
   2.122 +lemma "(x::('a, 'b, 'c) extpoint) = y"
   2.123 +  refute
   2.124 +oops
   2.125 +
   2.126 +(******************************************************************************)
   2.127 +
   2.128 +subsection {* Inductively defined sets *}
   2.129 +
   2.130 +(*TODO: can we implement lfp/gfp more efficiently? *)
   2.131 +
   2.132 +consts
   2.133 +  arbitrarySet :: "'a set"
   2.134 +inductive arbitrarySet
   2.135 +intros
   2.136 +  "arbitrary : arbitrarySet"
   2.137 +
   2.138 +lemma "x : arbitrarySet"
   2.139 +  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
   2.140 +oops
   2.141 +
   2.142 +consts
   2.143 +  evenCard :: "'a set set"
   2.144 +inductive evenCard
   2.145 +intros
   2.146 +  "{} : evenCard"
   2.147 +  "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
   2.148 +
   2.149 +lemma "S : evenCard"
   2.150 +  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
   2.151 +oops
   2.152 +
   2.153 +consts
   2.154 +  even :: "nat set"
   2.155 +  odd  :: "nat set"
   2.156 +inductive even odd
   2.157 +intros
   2.158 +  "0 : even"
   2.159 +  "n : even \<Longrightarrow> Suc n : odd"
   2.160 +  "n : odd \<Longrightarrow> Suc n : even"
   2.161 +
   2.162 +lemma "n : odd"
   2.163 +  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
   2.164 +oops
   2.165 +
   2.166 +(******************************************************************************)
   2.167 +
   2.168 +subsection {* Examples involving special functions *}
   2.169  
   2.170  lemma "card x = 0"
   2.171    refute
   2.172  oops
   2.173  
   2.174 -lemma "P nat_rec"
   2.175 -  refute
   2.176 +lemma "finite x"
   2.177 +  refute  -- {* no finite countermodel exists *}
   2.178  oops
   2.179  
   2.180  lemma "(x::nat) + y = 0"
   2.181 @@ -874,18 +973,14 @@
   2.182    refute
   2.183  oops
   2.184  
   2.185 -lemma "P (xs::'a list)"
   2.186 -  refute ["List.list"=4, "'a"=2]
   2.187 +lemma "a @ b = b @ a"
   2.188 +  refute
   2.189  oops
   2.190  
   2.191 -lemma "a @ b = b @ a"
   2.192 -  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
   2.193 -oops
   2.194 +(******************************************************************************)
   2.195  
   2.196  subsection {* Axiomatic type classes and overloading *}
   2.197  
   2.198 -ML {* set show_consts; set show_types; set show_sorts; *}
   2.199 -
   2.200  text {* A type class without axioms: *}
   2.201  
   2.202  axclass classA