# HG changeset patch # User blanchet # Date 1233767407 -3600 # Node ID d201a838d0f7e16e7570899c97b0594483f3067f # Parent 67266b31cd46a15180a70007e215c18b703f1bb8 Make some Refute functions public so I can use them in Nitpick, use @{const_name} antiquotation whenever possible (some, like Lfp.lfp had been renamed since Tjark wrote Refute), and removed some "set"-related code that is no longer relevant in Isabelle2008. There's still some "set" code that needs to be ported; see TODO in the file. diff -r 67266b31cd46 -r d201a838d0f7 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Feb 04 11:32:35 2009 +0000 +++ b/src/HOL/Tools/refute.ML Wed Feb 04 18:10:07 2009 +0100 @@ -57,6 +57,23 @@ val setup : theory -> theory +(* ------------------------------------------------------------------------- *) +(* Additional functions used by Nitpick (to be factored out) *) +(* ------------------------------------------------------------------------- *) + + val close_form : Term.term -> Term.term + val get_classdef : theory -> string -> (string * Term.term) option + val get_def : theory -> string * Term.typ -> (string * Term.term) option + val get_typedef : theory -> Term.typ -> (string * Term.term) option + val is_IDT_constructor : theory -> string * Term.typ -> bool + val is_IDT_recursor : theory -> string * Term.typ -> bool + val is_const_of_class: theory -> string * Term.typ -> bool + val monomorphic_term : Type.tyenv -> Term.term -> Term.term + val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term + val string_of_typ : Term.typ -> string + val typ_of_dtyp : + DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp + -> Term.typ end; (* signature REFUTE *) structure Refute : REFUTE = @@ -577,7 +594,7 @@ (* get_typedef: looks up the definition of a type, as created by "typedef" *) (* ------------------------------------------------------------------------- *) - (* theory -> (string * Term.typ) -> (string * Term.term) option *) + (* theory -> Term.typ -> (string * Term.term) option *) fun get_typedef thy T = let @@ -655,33 +672,32 @@ fun unfold_loop t = case t of (* Pure *) - Const ("all", _) => t - | Const ("==", _) => t - | Const ("==>", _) => t - | Const ("TYPE", _) => t (* axiomatic type classes *) + Const (@{const_name all}, _) => t + | Const (@{const_name "=="}, _) => t + | Const (@{const_name "==>"}, _) => t + | Const (@{const_name TYPE}, _) => t (* axiomatic type classes *) (* HOL *) - | Const ("Trueprop", _) => t - | Const ("Not", _) => t + | Const (@{const_name Trueprop}, _) => t + | Const (@{const_name Not}, _) => t | (* redundant, since 'True' is also an IDT constructor *) - Const ("True", _) => t + Const (@{const_name True}, _) => t | (* redundant, since 'False' is also an IDT constructor *) - Const ("False", _) => t - | Const (@{const_name undefined}, _) => t - | Const ("The", _) => t + Const (@{const_name False}, _) => t + | Const (@{const_name undefined}, _) => t + | Const (@{const_name The}, _) => t | Const ("Hilbert_Choice.Eps", _) => t - | Const ("All", _) => t - | Const ("Ex", _) => t - | Const ("op =", _) => t - | Const ("op &", _) => t - | Const ("op |", _) => t - | Const ("op -->", _) => t + | Const (@{const_name All}, _) => t + | Const (@{const_name Ex}, _) => t + | Const (@{const_name "op ="}, _) => t + | Const (@{const_name "op &"}, _) => t + | Const (@{const_name "op |"}, _) => t + | Const (@{const_name "op -->"}, _) => t (* sets *) - | Const ("Collect", _) => t - | Const ("op :", _) => t + | Const (@{const_name Collect}, _) => t + | Const (@{const_name "op :"}, _) => t (* other optimizations *) - | Const ("Finite_Set.card", _) => t - | Const ("Finite_Set.Finites", _) => t - | Const ("Finite_Set.finite", _) => t + | Const ("Finite_Set.card", _) => t + | Const ("Finite_Set.finite", _) => t | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []), @@ -690,11 +706,11 @@ Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const ("List.append", _) => t - | Const ("Lfp.lfp", _) => t - | Const ("Gfp.gfp", _) => t - | Const ("fst", _) => t - | Const ("snd", _) => t + | Const ("List.append", _) => t + | Const (@{const_name lfp}, _) => t + | Const (@{const_name gfp}, _) => t + | Const ("Product_Type.fst", _) => t + | Const ("Product_Type.snd", _) => t (* simply-typed lambda calculus *) | Const (s, T) => (if is_IDT_constructor thy (s, T) @@ -805,7 +821,6 @@ Type ("prop", []) => axs | Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2) - | Type ("set", [T1]) => collect_type_axioms (axs, T1) (* axiomatic type classes *) | Type ("itself", [T1]) => collect_type_axioms (axs, T1) | Type (s, Ts) => @@ -829,22 +844,22 @@ and collect_term_axioms (axs, t) = case t of (* Pure *) - Const ("all", _) => axs - | Const ("==", _) => axs - | Const ("==>", _) => axs + Const (@{const_name all}, _) => axs + | Const (@{const_name "=="}, _) => axs + | Const (@{const_name "==>"}, _) => axs (* axiomatic type classes *) - | Const ("TYPE", T) => collect_type_axioms (axs, T) + | Const (@{const_name TYPE}, T) => collect_type_axioms (axs, T) (* HOL *) - | Const ("Trueprop", _) => axs - | Const ("Not", _) => axs + | Const (@{const_name Trueprop}, _) => axs + | Const (@{const_name Not}, _) => axs (* redundant, since 'True' is also an IDT constructor *) - | Const ("True", _) => axs + | Const (@{const_name True}, _) => axs (* redundant, since 'False' is also an IDT constructor *) - | Const ("False", _) => axs - | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T) - | Const ("The", T) => + | Const (@{const_name False}, _) => axs + | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T) + | Const (@{const_name The}, T) => let - val ax = specialize_type thy ("The", T) + val ax = specialize_type thy (@{const_name The}, T) (the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) in collect_this_axiom ("HOL.the_eq_trivial", ax) axs @@ -856,19 +871,18 @@ in collect_this_axiom ("Hilbert_Choice.someI", ax) axs end - | Const ("All", T) => collect_type_axioms (axs, T) - | Const ("Ex", T) => collect_type_axioms (axs, T) - | Const ("op =", T) => collect_type_axioms (axs, T) - | Const ("op &", _) => axs - | Const ("op |", _) => axs - | Const ("op -->", _) => axs + | Const (@{const_name All}, T) => collect_type_axioms (axs, T) + | Const (@{const_name Ex}, T) => collect_type_axioms (axs, T) + | Const (@{const_name "op ="}, T) => collect_type_axioms (axs, T) + | Const (@{const_name "op &"}, _) => axs + | Const (@{const_name "op |"}, _) => axs + | Const (@{const_name "op -->"}, _) => axs (* sets *) - | Const ("Collect", T) => collect_type_axioms (axs, T) - | Const ("op :", T) => collect_type_axioms (axs, T) + | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T) + | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T) (* other optimizations *) - | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) - | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T) - | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T) + | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T) + | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T) | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T) @@ -881,13 +895,13 @@ | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) - | Const ("List.append", T) => collect_type_axioms (axs, T) - | Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) - | Const ("Gfp.gfp", T) => collect_type_axioms (axs, T) - | Const ("fst", T) => collect_type_axioms (axs, T) - | Const ("snd", T) => collect_type_axioms (axs, T) + | Const ("List.append", T) => collect_type_axioms (axs, T) + | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T) + | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T) + | Const ("Product_Type.fst", T) => collect_type_axioms (axs, T) + | Const ("Product_Type.snd", T) => collect_type_axioms (axs, T) (* simply-typed lambda calculus *) - | Const (s, T) => + | Const (s, T) => if is_const_of_class thy (s, T) then (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) (* and the class definition *) @@ -943,7 +957,6 @@ (case T of Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) | Type ("prop", []) => acc - | Type ("set", [T1]) => collect_types T1 acc | Type (s, Ts) => (case DatatypePackage.get_datatype thy s of SOME info => (* inductive datatype *) @@ -1303,18 +1316,18 @@ (* interpretation which includes values for the (formerly) *) (* quantified variables. *) (* maps !!x1...xn. !xk...xm. t to t *) - fun strip_all_body (Const ("all", _) $ Abs (_, _, t)) = strip_all_body t - | strip_all_body (Const ("Trueprop", _) $ t) = strip_all_body t - | strip_all_body (Const ("All", _) $ Abs (_, _, t)) = strip_all_body t - | strip_all_body t = t + fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = strip_all_body t + | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = strip_all_body t + | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = strip_all_body t + | strip_all_body t = t (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) - fun strip_all_vars (Const ("all", _) $ Abs (a, T, t)) = + fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t - | strip_all_vars (Const ("Trueprop", _) $ t) = + | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = strip_all_vars t - | strip_all_vars (Const ("All", _) $ Abs (a, T, t)) = + | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t - | strip_all_vars t = + | strip_all_vars t = [] : (string * typ) list val strip_t = strip_all_body ex_closure val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) @@ -1764,7 +1777,7 @@ fun Pure_interpreter thy model args t = case t of - Const ("all", _) $ t1 => + Const (@{const_name all}, _) $ t1 => let val (i, m, a) = interpret thy model args t1 in @@ -1781,9 +1794,9 @@ raise REFUTE ("Pure_interpreter", "\"all\" is followed by a non-function") end - | Const ("all", _) => + | Const (@{const_name all}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const ("==", _) $ t1 $ t2 => + | Const (@{const_name "=="}, _) $ t1 $ t2 => let val (i1, m1, a1) = interpret thy model args t1 val (i2, m2, a2) = interpret thy m1 a1 t2 @@ -1792,11 +1805,11 @@ SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end - | Const ("==", _) $ t1 => + | Const (@{const_name "=="}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("==", _) => + | Const (@{const_name "=="}, _) => SOME (interpret thy model args (eta_expand t 2)) - | Const ("==>", _) $ t1 $ t2 => + | Const (@{const_name "==>"}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1806,9 +1819,9 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const ("==>", _) $ t1 => + | Const (@{const_name "==>"}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("==>", _) => + | Const (@{const_name "==>"}, _) => SOME (interpret thy model args (eta_expand t 2)) | _ => NONE; @@ -1820,17 +1833,17 @@ (* logical constants. In HOL however, logical constants can themselves be *) (* arguments. They are then translated using eta-expansion. *) case t of - Const ("Trueprop", _) => + Const (@{const_name Trueprop}, _) => SOME (Node [TT, FF], model, args) - | Const ("Not", _) => + | Const (@{const_name Not}, _) => SOME (Node [FF, TT], model, args) (* redundant, since 'True' is also an IDT constructor *) - | Const ("True", _) => + | Const (@{const_name True}, _) => SOME (TT, model, args) (* redundant, since 'False' is also an IDT constructor *) - | Const ("False", _) => + | Const (@{const_name False}, _) => SOME (FF, model, args) - | Const ("All", _) $ t1 => (* similar to "all" (Pure) *) + | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) let val (i, m, a) = interpret thy model args t1 in @@ -1847,9 +1860,9 @@ raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function") end - | Const ("All", _) => + | Const (@{const_name All}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const ("Ex", _) $ t1 => + | Const (@{const_name Ex}, _) $ t1 => let val (i, m, a) = interpret thy model args t1 in @@ -1866,20 +1879,20 @@ raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function") end - | Const ("Ex", _) => + | Const (@{const_name Ex}, _) => SOME (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) $ t1 $ t2 => (* similar to "==" (Pure) *) + | Const (@{const_name "op ="}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) let val (i1, m1, a1) = interpret thy model args t1 val (i2, m2, a2) = interpret thy m1 a1 t2 in SOME (make_equality (i1, i2), m2, a2) end - | Const ("op =", _) $ t1 => + | Const (@{const_name "op ="}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("op =", _) => + | Const (@{const_name "op ="}, _) => SOME (interpret thy model args (eta_expand t 2)) - | Const ("op &", _) $ t1 $ t2 => + | Const (@{const_name "op &"}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1889,14 +1902,14 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const ("op &", _) $ t1 => + | Const (@{const_name "op &"}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("op &", _) => + | Const (@{const_name "op &"}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False & undef": *) (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) - | Const ("op |", _) $ t1 $ t2 => + | Const (@{const_name "op |"}, _) $ t1 $ t2 => (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1906,14 +1919,14 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const ("op |", _) $ t1 => + | Const (@{const_name "op |"}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("op |", _) => + | Const (@{const_name "op |"}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "True | undef": *) (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) - | Const ("op -->", _) $ t1 $ t2 => (* similar to "==>" (Pure) *) + | Const (@{const_name "op -->"}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1923,9 +1936,9 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const ("op -->", _) $ t1 => + | Const (@{const_name "op -->"}, _) $ t1 => SOME (interpret thy model args (eta_expand t 1)) - | Const ("op -->", _) => + | Const (@{const_name "op -->"}, _) => SOME (interpret thy model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False --> undef": *) @@ -1935,56 +1948,6 @@ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - fun set_interpreter thy model args t = - (* "T set" is isomorphic to "T --> bool" *) - let - val (typs, terms) = model - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Free (x, Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Var ((x, i), Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Const (s, Type ("set", [T])) => - let - val (intr, _, args') = - interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - (* 'Collect' == identity *) - | Const ("Collect", _) $ t1 => - SOME (interpret thy model args t1) - | Const ("Collect", _) => - SOME (interpret thy model args (eta_expand t 1)) - (* 'op :' == application *) - | Const ("op :", _) $ t1 $ t2 => - SOME (interpret thy model args (t2 $ t1)) - | Const ("op :", _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) - | Const ("op :", _) => - SOME (interpret thy model args (eta_expand t 2)) - | _ => NONE) - end; - - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* interprets variables and constants whose type is an IDT (this is *) (* relatively easy and merely requires us to compute the size of the IDT); *) (* constructors of IDTs however are properly interpreted by *) @@ -2120,9 +2083,9 @@ val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT (* Term.term *) - val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_empty_set = Const (@{const_name "{}"}, HOLogic_setT) val HOLogic_insert = - Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) in (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *) map (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) @@ -2688,6 +2651,8 @@ | _ => (* head of term is not a constant *) NONE; + (* TODO: Fix all occurrences of Type ("set", _). *) + (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) @@ -2738,26 +2703,6 @@ (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) - (* only an optimization: 'Finites' could in principle be interpreted with *) - (* interpreters available already (using its definition), but the code *) - (* below is more efficient *) - - fun Finite_Set_Finites_interpreter thy model args t = - case t of - Const ("Finite_Set.Finites", Type ("set", [Type ("set", [T])])) => - let - val size_of_set = size_of_type thy model (Type ("set", [T])) - in - (* we only consider finite models anyway, hence EVERY set is in *) - (* "Finites" *) - SOME (Node (replicate size_of_set TT), model, args) - end - | _ => - NONE; - - (* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'finite' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) @@ -2995,9 +2940,9 @@ (* interpreters available already (using its definition), but the code *) (* below is more efficient *) - fun Lfp_lfp_interpreter thy model args t = + fun lfp_interpreter thy model args t = case t of - Const ("Lfp.lfp", Type ("fun", [Type ("fun", + Const (@{const_name lfp}, Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => let val size_elem = size_of_type thy model T @@ -3014,14 +2959,14 @@ List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) | is_subset (_, _) = - raise REFUTE ("Lfp_lfp_interpreter", + 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_lfp_interpreter", + raise REFUTE ("lfp_interpreter", "intersection: interpretation for set is not a node") (* interpretation -> interpretaion *) fun lfp (Node resultsets) = @@ -3031,7 +2976,7 @@ else acc) i_univ (i_sets ~~ resultsets) | lfp _ = - raise REFUTE ("Lfp_lfp_interpreter", + raise REFUTE ("lfp_interpreter", "lfp: interpretation for function is not a node") in SOME (Node (map lfp i_funs), model, args) @@ -3046,9 +2991,9 @@ (* interpreters available already (using its definition), but the code *) (* below is more efficient *) - fun Gfp_gfp_interpreter thy model args t = + fun gfp_interpreter thy model args t = case t of - Const ("Gfp.gfp", Type ("fun", [Type ("fun", + Const (@{const_name gfp}, Type ("fun", [Type ("fun", [Type ("set", [T]), Type ("set", [_])]), Type ("set", [_])])) => let nonfix union (* because "union" is used below *) val size_elem = size_of_type thy model T @@ -3065,14 +3010,14 @@ List.all (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) | is_subset (_, _) = - raise REFUTE ("Gfp_gfp_interpreter", + 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_gfp_interpreter", + raise REFUTE ("gfp_interpreter", "union: interpretation for set is not a node") (* interpretation -> interpretaion *) fun gfp (Node resultsets) = @@ -3082,7 +3027,7 @@ else acc) i_univ (i_sets ~~ resultsets) | gfp _ = - raise REFUTE ("Gfp_gfp_interpreter", + raise REFUTE ("gfp_interpreter", "gfp: interpretation for function is not a node") in SOME (Node (map gfp i_funs), model, args) @@ -3099,7 +3044,7 @@ fun Product_Type_fst_interpreter thy model args t = case t of - Const ("fst", Type ("fun", [Type ("*", [T, U]), _])) => + Const ("Product_Type.fst", Type ("fun", [Type ("*", [T, U]), _])) => let val constants_T = make_constants thy model T val size_U = size_of_type thy model U @@ -3119,7 +3064,7 @@ fun Product_Type_snd_interpreter thy model args t = case t of - Const ("snd", Type ("fun", [Type ("*", [T, U]), _])) => + Const ("Product_Type.snd", Type ("fun", [Type ("*", [T, U]), _])) => let val size_T = size_of_type thy model T val constants_U = make_constants thy model U @@ -3175,9 +3120,9 @@ val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT (* Term.term *) - val HOLogic_empty_set = Const ("{}", HOLogic_setT) + val HOLogic_empty_set = Const (@{const_name "{}"}, HOLogic_setT) val HOLogic_insert = - Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) in SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set pairs) @@ -3209,45 +3154,6 @@ (* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> Term.term option *) - fun set_printer thy model T intr assignment = - (case T of - Type ("set", [T1]) => - let - (* create all constants of type 'T1' *) - val constants = make_constants thy 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 PropLogic.eval assignment fmTrue then - SOME (print thy model T1 arg assignment) - else (* if PropLogic.eval assignment fmFalse then *) - 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 ("{}", HOLogic_setT1) - val HOLogic_insert = - Const ("insert", T1 --> HOLogic_setT1 --> HOLogic_setT1) - in - SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) - (HOLogic_empty_set, elements)) - end - | _ => - NONE); - - (* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term option *) - fun IDT_printer thy model T intr assignment = (case T of Type (s, Ts) => @@ -3359,24 +3265,21 @@ add_interpreter "stlc" stlc_interpreter #> add_interpreter "Pure" Pure_interpreter #> add_interpreter "HOLogic" HOLogic_interpreter #> - add_interpreter "set" set_interpreter #> add_interpreter "IDT" IDT_interpreter #> add_interpreter "IDT_constructor" IDT_constructor_interpreter #> add_interpreter "IDT_recursion" IDT_recursion_interpreter #> add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> - add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #> add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> add_interpreter "Nat_HOL.times" Nat_times_interpreter #> add_interpreter "List.append" List_append_interpreter #> - add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #> - add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #> + add_interpreter "lfp" lfp_interpreter #> + add_interpreter "gfp" gfp_interpreter #> add_interpreter "fst" Product_Type_fst_interpreter #> add_interpreter "snd" Product_Type_snd_interpreter #> add_printer "stlc" stlc_printer #> - add_printer "set" set_printer #> add_printer "IDT" IDT_printer; end (* structure Refute *)