src/HOL/Tools/refute.ML
changeset 16050 828fc32f390f
parent 15794 5de27a5fc5ed
child 16073 794b37d08a2e
     1.1 --- a/src/HOL/Tools/refute.ML	Mon May 23 16:57:02 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon May 23 17:17:06 2005 +0200
     1.3 @@ -625,6 +625,8 @@
     1.4  			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
     1.5  			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
     1.6  			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
     1.7 +			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
     1.8 +			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
     1.9  			(* simply-typed lambda calculus *)
    1.10  			| Const (s, T)                    =>
    1.11  				let
    1.12 @@ -2284,6 +2286,98 @@
    1.13  		| _ =>
    1.14  			NONE;
    1.15  
    1.16 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.17 +
    1.18 +	(* only an optimization: 'lfp' could in principle be interpreted with     *)
    1.19 +	(* interpreters available already (using its definition), but the code    *)
    1.20 +	(* below is more efficient                                                *)
    1.21 +
    1.22 +	fun Lfp_lfp_interpreter thy model args t =
    1.23 +		case t of
    1.24 +		  Const ("Lfp.lfp", Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) =>
    1.25 +			let
    1.26 +				val (i_elem, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.27 +				val size_elem      = size_of_type i_elem
    1.28 +				(* the universe (i.e. the set that contains every element) *)
    1.29 +				val i_univ         = Node (replicate size_elem TT)
    1.30 +				(* all sets with elements from type 'T' *)
    1.31 +				val (i_set, _, _)  = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
    1.32 +				val i_sets         = make_constants i_set
    1.33 +				(* all functions that map sets to sets *)
    1.34 +				val (i_fun, _, _)  = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("fun", [Type ("set", [T]), Type ("set", [T])])))
    1.35 +				val i_funs         = make_constants i_fun
    1.36 +				(* "lfp(f) == Inter({u. f(u) <= u})" *)
    1.37 +				(* interpretation * interpretation -> bool *)
    1.38 +				fun is_subset (Node subs, Node sups) =
    1.39 +					List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
    1.40 +				  | is_subset (_, _) =
    1.41 +					raise REFUTE ("Lfp_lfp_interpreter", "is_subset: interpretation for set is not a node")
    1.42 +				(* interpretation * interpretation -> interpretation *)
    1.43 +				fun intersection (Node xs, Node ys) =
    1.44 +					Node (map (fn (x, y) => if (x = TT) andalso (y = TT) then TT else FF) (xs ~~ ys))
    1.45 +				  | intersection (_, _) =
    1.46 +					raise REFUTE ("Lfp_lfp_interpreter", "intersection: interpretation for set is not a node")
    1.47 +				(* interpretation -> interpretaion *)
    1.48 +				fun lfp (Node resultsets) =
    1.49 +					foldl (fn ((set, resultset), acc) =>
    1.50 +						if is_subset (resultset, set) then
    1.51 +							intersection (acc, set)
    1.52 +						else
    1.53 +							acc) i_univ (i_sets ~~ resultsets)
    1.54 +				  | lfp _ =
    1.55 +						raise REFUTE ("Lfp_lfp_interpreter", "lfp: interpretation for function is not a node")
    1.56 +			in
    1.57 +				SOME (Node (map lfp i_funs), model, args)
    1.58 +			end
    1.59 +		| _ =>
    1.60 +			NONE;
    1.61 +
    1.62 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.63 +
    1.64 +	(* only an optimization: 'gfp' could in principle be interpreted with     *)
    1.65 +	(* interpreters available already (using its definition), but the code    *)
    1.66 +	(* below is more efficient                                                *)
    1.67 +
    1.68 +	fun Gfp_gfp_interpreter thy model args t =
    1.69 +		case t of
    1.70 +		  Const ("Gfp.gfp", Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) =>
    1.71 +			let
    1.72 +				val (i_elem, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.73 +				val size_elem      = size_of_type i_elem
    1.74 +				(* the universe (i.e. the set that contains every element) *)
    1.75 +				val i_univ         = Node (replicate size_elem TT)
    1.76 +				(* all sets with elements from type 'T' *)
    1.77 +				val (i_set, _, _)  = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
    1.78 +				val i_sets         = make_constants i_set
    1.79 +				(* all functions that map sets to sets *)
    1.80 +				val (i_fun, _, _)  = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("fun", [Type ("set", [T]), Type ("set", [T])])))
    1.81 +				val i_funs         = make_constants i_fun
    1.82 +				(* "gfp(f) == Union({u. u <= f(u)})" *)
    1.83 +				(* interpretation * interpretation -> bool *)
    1.84 +				fun is_subset (Node subs, Node sups) =
    1.85 +					List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
    1.86 +				  | is_subset (_, _) =
    1.87 +					raise REFUTE ("Gfp_gfp_interpreter", "is_subset: interpretation for set is not a node")
    1.88 +				(* interpretation * interpretation -> interpretation *)
    1.89 +				fun union (Node xs, Node ys) =
    1.90 +					Node (map (fn (x, y) => if (x = TT) orelse (y = TT) then TT else FF) (xs ~~ ys))
    1.91 +				  | union (_, _) =
    1.92 +					raise REFUTE ("Lfp_lfp_interpreter", "union: interpretation for set is not a node")
    1.93 +				(* interpretation -> interpretaion *)
    1.94 +				fun gfp (Node resultsets) =
    1.95 +					foldl (fn ((set, resultset), acc) =>
    1.96 +						if is_subset (set, resultset) then
    1.97 +							union (acc, set)
    1.98 +						else
    1.99 +							acc) i_univ (i_sets ~~ resultsets)
   1.100 +				  | gfp _ =
   1.101 +						raise REFUTE ("Gfp_gfp_interpreter", "gfp: interpretation for function is not a node")
   1.102 +			in
   1.103 +				SOME (Node (map gfp i_funs), model, args)
   1.104 +			end
   1.105 +		| _ =>
   1.106 +			NONE;
   1.107 +
   1.108  
   1.109  (* ------------------------------------------------------------------------- *)
   1.110  (* PRINTERS                                                                  *)
   1.111 @@ -2522,6 +2616,8 @@
   1.112  		 add_interpreter "Nat.op -" Nat_minus_interpreter,
   1.113  		 add_interpreter "Nat.op *" Nat_mult_interpreter,
   1.114  		 add_interpreter "List.op @" List_append_interpreter,
   1.115 +		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter,
   1.116 +		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter,
   1.117  		 add_printer "stlc" stlc_printer,
   1.118  		 add_printer "set"  set_printer,
   1.119  		 add_printer "IDT"  IDT_printer];