# HG changeset patch # User webertj # Date 1167865950 -3600 # Node ID acfb13e8819e28ba43fceadc4a7b990d9a250410 # Parent 7b9c2f6b45f509ace348c165bf54e83cf494f0f8 constants are unfolded, universal quantifiers are stripped, some minor changes diff -r 7b9c2f6b45f5 -r acfb13e8819e src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Jan 03 22:59:30 2007 +0100 +++ b/src/HOL/Tools/refute.ML Thu Jan 04 00:12:30 2007 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/refute.ML ID: $Id$ Author: Tjark Weber - Copyright 2003-2005 + Copyright 2003-2007 Finite model generation for HOL formulas, using a SAT solver. *) @@ -382,25 +382,337 @@ fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = (* replace a 'DtTFree' variable by the associated type *) - (the o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a) + (Option.valOf o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a) | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = Type (s, map (typ_of_dtyp descr typ_assoc) ds) | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = let - val (s, ds, _) = (the o AList.lookup (op =) descr) i + val (s, ds, _) = (Option.valOf o AList.lookup (op =) descr) i in Type (s, map (typ_of_dtyp descr typ_assoc) ds) end; (* ------------------------------------------------------------------------- *) -(* collect_axioms: collects (monomorphic, universally quantified versions *) -(* of) all HOL axioms that are relevant w.r.t 't' *) +(* close_form: universal closure over schematic variables in 't' *) +(* ------------------------------------------------------------------------- *) + + (* Term.term -> Term.term *) + + fun close_form t = + let + (* (Term.indexname * Term.typ) list *) + val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) + in + Library.foldl + (fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) + (t, vars) + end; + +(* ------------------------------------------------------------------------- *) +(* monomorphic_term: applies a type substitution 'typeSubs' for all type *) +(* variables in a term 't' *) +(* ------------------------------------------------------------------------- *) + + (* Type.tyenv -> Term.term -> Term.term *) + + fun monomorphic_term typeSubs t = + map_types (map_type_tvar + (fn v => + case Type.lookup (typeSubs, v) of + NONE => + (* schematic type variable not instantiated *) + raise REFUTE ("monomorphic_term", + "no substitution for type variable " ^ fst (fst v) ^ + " in term " ^ Display.raw_string_of_term t) + | SOME typ => + typ)) t; + +(* ------------------------------------------------------------------------- *) +(* specialize_type: given a constant 's' of type 'T', which is a subterm of *) +(* 't', where 't' has a (possibly) more general type, the *) +(* schematic type variables in 't' are instantiated to *) +(* match the type 'T' (may raise Type.TYPE_MATCH) *) +(* ------------------------------------------------------------------------- *) + + (* theory -> (string * Term.typ) -> Term.term -> Term.term *) + + fun specialize_type thy (s, T) t = + let + fun find_typeSubs (Const (s', T')) = + if s=s' then + SOME (Sign.typ_match thy (T', T) Vartab.empty) + handle Type.TYPE_MATCH => NONE + else + NONE + | find_typeSubs (Free _) = NONE + | find_typeSubs (Var _) = NONE + | find_typeSubs (Bound _) = NONE + | find_typeSubs (Abs (_, _, body)) = find_typeSubs body + | find_typeSubs (t1 $ t2) = + (case find_typeSubs t1 of SOME x => SOME x + | NONE => find_typeSubs t2) + in + case find_typeSubs t of + SOME typeSubs => + monomorphic_term typeSubs t + | NONE => + (* no match found - perhaps due to sort constraints *) + raise Type.TYPE_MATCH + end; + +(* ------------------------------------------------------------------------- *) +(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *) +(* denotes membership to an axiomatic type class *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string * Term.typ -> bool *) + + fun is_const_of_class thy (s, T) = + let + val class_const_names = map Logic.const_of_class (Sign.all_classes thy) + in + (* I'm not quite sure if checking the name 's' is sufficient, *) + (* or if we should also check the type 'T'. *) + s mem_string class_const_names + end; + +(* ------------------------------------------------------------------------- *) +(* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor *) +(* of an inductive datatype in 'thy' *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string * Term.typ -> bool *) + + fun is_IDT_constructor thy (s, T) = + (case body_type T of + Type (s', _) => + (case DatatypePackage.get_datatype_constrs thy s' of + SOME constrs => + List.exists (fn (cname, cty) => + cname = s andalso Sign.typ_instance thy (T, cty)) constrs + | NONE => + false) + | _ => + false); + +(* ------------------------------------------------------------------------- *) +(* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion *) +(* operator of an inductive datatype in 'thy' *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string * Term.typ -> bool *) + + fun is_IDT_recursor thy (s, T) = + let + val rec_names = Symtab.fold (append o #rec_names o snd) + (DatatypePackage.get_datatypes thy) [] + in + (* I'm not quite sure if checking the name 's' is sufficient, *) + (* or if we should also check the type 'T'. *) + s mem_string rec_names + end; + +(* ------------------------------------------------------------------------- *) +(* get_def: looks up the definition of a constant, as created by "constdefs" *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string * Term.typ -> (string * Term.term) option *) + + fun get_def thy (s, T) = + let + (* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) + fun norm_rhs eqn = + let + fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) + | lambda v t = raise TERM ("lambda", [v, t]) + val (lhs, rhs) = Logic.dest_equals eqn + val (_, args) = Term.strip_comb lhs + in + fold lambda (rev args) rhs + end + (* (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 + val (s', T') = Term.dest_Const c + in + if s=s' then + let + val typeSubs = Sign.typ_match thy (T', T) Vartab.empty + val ax' = monomorphic_term typeSubs ax + val rhs = norm_rhs ax' + in + SOME (axname, rhs) + end + else + get_def_ax axioms + end handle ERROR _ => get_def_ax axioms + | TERM _ => get_def_ax axioms + | Type.TYPE_MATCH => get_def_ax axioms) + in + get_def_ax (Theory.all_axioms_of thy) + end; + +(* ------------------------------------------------------------------------- *) +(* get_typedef: looks up the definition of a type, as created by "typedef" *) +(* ------------------------------------------------------------------------- *) + + (* theory -> (string * Term.typ) -> (string * Term.term) option *) + + 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'="Typedef.type_definition" then + SOME T' + else + NONE + | type_of_type_definition (Free _) = NONE + | type_of_type_definition (Var _) = NONE + | type_of_type_definition (Bound _) = NONE + | type_of_type_definition (Abs (_, _, body)) = + type_of_type_definition body + | type_of_type_definition (t1 $ t2) = + (case type_of_type_definition t1 of + SOME x => SOME x + | NONE => type_of_type_definition t2) + in + case type_of_type_definition ax of + SOME T' => + let + val T'' = (domain_type o domain_type) T' + val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty + in + SOME (axname, monomorphic_term typeSubs ax) + end + | NONE => + get_typedef_ax axioms + end handle ERROR _ => get_typedef_ax axioms + | MATCH => get_typedef_ax axioms + | Type.TYPE_MATCH => get_typedef_ax axioms) + in + get_typedef_ax (Theory.all_axioms_of thy) + end; + +(* ------------------------------------------------------------------------- *) +(* get_classdef: looks up the defining axiom for an axiomatic type class, as *) +(* created by the "axclass" command *) +(* ------------------------------------------------------------------------- *) + + (* theory -> string -> (string * Term.term) option *) + + fun get_classdef thy class = + let + val axname = class ^ "_class_def" + in + Option.map (pair axname) + (AList.lookup (op =) (Theory.all_axioms_of thy) axname) + end; + +(* ------------------------------------------------------------------------- *) +(* unfold_defs: unfolds all defined constants in a term 't', beta-eta *) +(* normalizes the result term; certain constants are not *) +(* unfolded (cf. 'collect_axioms' and the various interpreters *) +(* below): if the interpretation respects a definition anyway, *) +(* that definition does not need to be unfolded *) +(* ------------------------------------------------------------------------- *) + + (* theory -> Term.term -> Term.term *) + + (* Note: we could intertwine unfolding of constants and beta-(eta-) *) + (* normalization; this would save some unfolding for terms where *) + (* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *) + (* 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 ("all", _) => t + | Const ("==", _) => t + | Const ("==>", _) => t + | Const ("TYPE", _) => t (* axiomatic type classes *) + (* HOL *) + | Const ("Trueprop", _) => t + | Const ("Not", _) => t + | (* redundant, since 'True' is also an IDT constructor *) + Const ("True", _) => t + | (* redundant, since 'False' is also an IDT constructor *) + Const ("False", _) => t + | Const ("arbitrary", _) => t + | Const ("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 + (* sets *) + | Const ("Collect", _) => t + | Const ("op :", _) => t + (* other optimizations *) + | Const ("Finite_Set.card", _) => t + | Const ("Finite_Set.Finites", _) => t + | Const ("Orderings.less", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t + | Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t + | Const ("List.op @", _) => t + | Const ("Lfp.lfp", _) => t + | Const ("Gfp.gfp", _) => t + | Const ("fst", _) => t + | Const ("snd", _) => t + (* simply-typed lambda calculus *) + | Const (s, T) => + (if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then + t (* do not unfold IDT constructors/recursors *) + (* unfold the constant if there is a defining equation *) + else case get_def thy (s, T) of + SOME (axname, rhs) => + (* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) + (* occurs on the right-hand side of the equation, i.e. in *) + (* 'rhs', we must not use this equation to unfold, because *) + (* that would loop. Here would be the right place to *) + (* check this. However, getting this really right seems *) + (* difficult because the user may state arbitrary axioms, *) + (* which could interact with overloading to create loops. *) + ((*immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs) + | NONE => t) + | Free _ => t + | Var _ => t + | Bound _ => t + | Abs (s, T, body) => Abs (s, T, unfold_loop body) + | t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) + val result = Envir.beta_eta_contract (unfold_loop t) + in + result + end; + +(* ------------------------------------------------------------------------- *) +(* collect_axioms: collects (monomorphic, universally quantified, unfolded *) +(* versions of) all HOL axioms that are relevant w.r.t 't' *) (* ------------------------------------------------------------------------- *) (* Note: to make the collection of axioms more easily extensible, this *) (* function could be based on user-supplied "axiom collectors", *) (* similar to 'interpret'/interpreters or 'print'/printers *) + (* Note: currently we use "inverse" functions to the definitional *) + (* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) + (* "typedef", "constdefs". A more general approach could consider *) + (* *every* axiom of the theory and collect it if it has a constant/ *) + (* type/typeclass in common with the term 't'. *) + (* theory -> Term.term -> Term.term list *) (* Which axioms are "relevant" for a particular term/type goes hand in *) @@ -408,109 +720,60 @@ (* way below): if the interpretation respects an axiom anyway, the axiom *) (* does not need to be added as a constraint here. *) - (* When an axiom is added as relevant, further axioms may need to be *) - (* added as well (e.g. when a constant is defined in terms of other *) - (* constants). To avoid infinite recursion (which should not happen for *) - (* constants anyway, but it could happen for "typedef"-related axioms, *) - (* since they contain the type again), we use an accumulator 'axs' and *) - (* add a relevant axiom only if it is not in 'axs' yet. *) + (* To avoid collecting the same axiom multiple times, we use an *) + (* accumulator 'axs' which contains all axioms collected so far. *) fun collect_axioms thy t = let val _ = immediate_output "Adding axioms..." (* (string * Term.term) list *) - val axioms = Theory.all_axioms_of thy; - (* string list *) - val rec_names = Symtab.fold (append o #rec_names o snd) - (DatatypePackage.get_datatypes thy) []; - (* string list *) - val const_of_class_names = map Logic.const_of_class (Sign.all_classes thy) - (* given a constant 's' of type 'T', which is a subterm of 't', where *) - (* 't' has a (possibly) more general type, the schematic type *) - (* variables in 't' are instantiated to match the type 'T' (may raise *) - (* Type.TYPE_MATCH) *) - (* (string * Term.typ) * Term.term -> Term.term *) - fun specialize_type ((s, T), t) = + val axioms = Theory.all_axioms_of thy + (* string * Term.term -> Term.term list -> Term.term list *) + fun collect_this_axiom (axname, ax) axs = let - fun find_typeSubs (Const (s', T')) = - (if s=s' then - SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE - else - NONE) - | find_typeSubs (Free _) = NONE - | find_typeSubs (Var _) = NONE - | find_typeSubs (Bound _) = NONE - | find_typeSubs (Abs (_, _, body)) = find_typeSubs body - | find_typeSubs (t1 $ t2) = (case find_typeSubs t1 of SOME x => SOME x | NONE => find_typeSubs t2) - val typeSubs = (case find_typeSubs t of - SOME x => x - | NONE => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *)) + val ax' = unfold_defs thy ax in - map_types - (map_type_tvar - (fn v => - case Type.lookup (typeSubs, v) of - NONE => - (* schematic type variable not instantiated *) - raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")") - | SOME typ => - typ)) - t + if member (op aconv) axs ax' then + axs + else ( + immediate_output (" " ^ axname); + collect_term_axioms (ax' :: axs, ax') + ) end - (* applies a type substitution 'typeSubs' for all type variables in a *) - (* term 't' *) - (* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *) - fun monomorphic_term typeSubs t = - map_types (map_type_tvar - (fn v => - case Type.lookup (typeSubs, v) of - NONE => - (* schematic type variable not instantiated *) - error "" - | SOME typ => - typ)) t (* Term.term list * Term.typ -> Term.term list *) - fun collect_sort_axioms (axs, T) = - let - (* collect the axioms for a single 'class' (but not for its superclasses) *) - (* Term.term list * string -> Term.term list *) - fun collect_class_axioms (axs, class) = - let - (* obtain the axioms generated by the "axclass" command *) - (* (string * Term.term) list *) - val class_axioms = List.filter (fn (s, _) => String.isPrefix (Logic.const_of_class class ^ ".axioms_") s) axioms - (* replace the one schematic type variable in each axiom by the actual type 'T' *) - (* (string * Term.term) list *) - val monomorphic_class_axioms = map (fn (axname, ax) => - let - val (idx, S) = (case term_tvars ax of - [is] => is - | _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable")) - in - (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) - end) class_axioms - (* Term.term list * (string * Term.term) list -> Term.term list *) - fun collect_axiom (axs, (axname, ax)) = - if member (op aconv) axs ax then - axs - else ( - immediate_output (" " ^ axname); - collect_term_axioms (ax :: axs, ax) - ) - in - Library.foldl collect_axiom (axs, monomorphic_class_axioms) - end - (* string list *) - val sort = (case T of - TFree (_, sort) => sort - | TVar (_, sort) => sort - | _ => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable")) - (* obtain all superclasses of classes in 'sort' *) - (* string list *) - val superclasses = distinct (op =) (sort @ maps (Sign.super_classes thy) sort) - in - Library.foldl collect_class_axioms (axs, superclasses) - end + and collect_sort_axioms (axs, T) = + let + (* string list *) + val sort = (case T of + TFree (_, sort) => sort + | TVar (_, sort) => sort + | _ => raise REFUTE ("collect_axioms", "type " ^ + Sign.string_of_typ thy T ^ " is not a variable")) + (* obtain axioms for all superclasses *) + val superclasses = sort @ (maps (Sign.super_classes thy) sort) + (* merely an optimization, because 'collect_this_axiom' disallows *) + (* duplicate axioms anyway: *) + val superclasses = distinct (op =) superclasses + val class_axioms = maps (fn class => map (fn ax => + ("<" ^ class ^ ">", Thm.prop_of ax)) + (#axioms (AxClass.get_definition thy class) handle ERROR _ => [])) + superclasses + (* replace the (at most one) schematic type variable in each axiom *) + (* by the actual type 'T' *) + val monomorphic_class_axioms = map (fn (axname, ax) => + (case Term.term_tvars ax of + [] => + (axname, ax) + | [(idx, S)] => + (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) + | _ => + raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ + Sign.string_of_term thy ax ^ + ") contains more than one type variable"))) + class_axioms + in + fold collect_this_axiom monomorphic_class_axioms axs + end (* Term.term list * Term.typ -> Term.term list *) and collect_type_axioms (axs, T) = case T of @@ -520,58 +783,18 @@ | Type ("set", [T1]) => collect_type_axioms (axs, T1) | Type ("itself", [T1]) => collect_type_axioms (axs, T1) (* axiomatic type classes *) | Type (s, Ts) => - let - (* look up the definition of a type, as created by "typedef" *) - (* (string * Term.term) list -> (string * Term.term) option *) - fun get_typedefn [] = - NONE - | get_typedefn ((axname,ax)::axms) = - (let - (* Term.term -> Term.typ option *) - fun type_of_type_definition (Const (s', T')) = - if s'="Typedef.type_definition" then - SOME T' - else - NONE - | type_of_type_definition (Free _) = NONE - | type_of_type_definition (Var _) = NONE - | type_of_type_definition (Bound _) = NONE - | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body - | type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of SOME x => SOME x | NONE => type_of_type_definition t2) - in - case type_of_type_definition ax of - SOME T' => - let - val T'' = (domain_type o domain_type) T' - val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty - in - SOME (axname, monomorphic_term typeSubs ax) - end - | NONE => - get_typedefn axms - end - handle ERROR _ => get_typedefn axms - | MATCH => get_typedefn axms - | Type.TYPE_MATCH => get_typedefn axms) - in - case DatatypePackage.get_datatype thy s of - SOME info => (* inductive datatype *) - (* only collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts) + (case DatatypePackage.get_datatype thy s of + SOME info => (* inductive datatype *) + (* only collect relevant type axioms for the argument types *) + Library.foldl collect_type_axioms (axs, Ts) + | NONE => + (case get_typedef thy T of + SOME (axname, ax) => + collect_this_axiom (axname, ax) axs | NONE => - (case get_typedefn axioms of - SOME (axname, ax) => - if member (op aconv) axs ax then - (* only collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts) - else - (immediate_output (" " ^ axname); - collect_term_axioms (ax :: axs, ax)) - | NONE => - (* unspecified type, perhaps introduced with 'typedecl' *) - (* at least collect relevant type axioms for the argument types *) - Library.foldl collect_type_axioms (axs, Ts)) - end + (* unspecified type, perhaps introduced with "typedecl" *) + (* at least collect relevant type axioms for the argument types *) + Library.foldl collect_type_axioms (axs, Ts))) | TFree _ => collect_sort_axioms (axs, T) (* axiomatic type classes *) | TVar _ => collect_sort_axioms (axs, T) (* axiomatic type classes *) (* Term.term list * Term.term -> Term.term list *) @@ -590,27 +813,18 @@ | Const ("arbitrary", T) => collect_type_axioms (axs, T) | Const ("The", T) => let - val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial") + val ax = specialize_type thy ("The", T) ((Option.valOf o AList.lookup (op =) axioms) "HOL.the_eq_trivial") in - if member (op aconv) axs ax then - collect_type_axioms (axs, T) - else - (immediate_output " HOL.the_eq_trivial"; - collect_term_axioms (ax :: axs, ax)) + collect_this_axiom ("HOL.the_eq_trivial", ax) axs end | Const ("Hilbert_Choice.Eps", T) => let - val ax = specialize_type (("Hilbert_Choice.Eps", T), - (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI") + val ax = specialize_type thy ("Hilbert_Choice.Eps", T) ((Option.valOf o AList.lookup (op =) axioms) "Hilbert_Choice.someI") in - if member (op aconv) axs ax then - collect_type_axioms (axs, T) - else - (immediate_output " Hilbert_Choice.someI"; - collect_term_axioms (ax :: axs, ax)) + collect_this_axiom ("Hilbert_Choice.someI", ax) axs end - | Const ("All", _) $ t1 => collect_term_axioms (axs, t1) - | Const ("Ex", _) $ t1 => collect_term_axioms (axs, t1) + | 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 @@ -632,116 +846,36 @@ | Const ("snd", T) => collect_type_axioms (axs, T) (* simply-typed lambda calculus *) | Const (s, T) => - let - (* look up the definition of a constant, as created by "constdefs" *) - (* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *) - fun get_defn [] = - NONE - | get_defn ((axname, ax)::axms) = - (let - val (lhs, _) = Logic.dest_equals ax (* equations only *) - val c = head_of lhs - val (s', T') = dest_Const c - in - if s=s' then - let - val typeSubs = Sign.typ_match thy (T', T) Vartab.empty - in - SOME (axname, monomorphic_term typeSubs ax) - end - else - get_defn axms - end - handle ERROR _ => get_defn axms - | TERM _ => get_defn axms - | Type.TYPE_MATCH => get_defn axms) - (* axiomatic type classes *) - (* unit -> bool *) - fun is_const_of_class () = - (* I'm not quite sure if checking the name 's' is sufficient, *) - (* or if we should also check the type 'T' *) - s mem const_of_class_names - (* inductive data types *) - (* unit -> bool *) - fun is_IDT_constructor () = - (case body_type T of - Type (s', _) => - (case DatatypePackage.get_datatype_constrs thy s' of - SOME constrs => - Library.exists (fn (cname, cty) => - cname = s andalso Sign.typ_instance thy (T, cty)) - constrs - | NONE => - false) - | _ => - false) - (* unit -> bool *) - fun is_IDT_recursor () = - (* I'm not quite sure if checking the name 's' is sufficient, *) - (* or if we should also check the type 'T' *) - member (op =) rec_names s - in - if is_const_of_class () then - (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *) - (* the introduction rule "class.intro" as axioms *) + if is_const_of_class thy (s, T) then + (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) + (* and the class definition *) let val class = Logic.class_of_const s val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) - (* Term.term option *) - val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE) - val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) - (AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE) - val axs' = (case ofclass_ax of NONE => axs | SOME ax => if member (op aconv) axs ax then - (* collect relevant type axioms *) - collect_type_axioms (axs, T) - else - (immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax); - collect_term_axioms (ax :: axs, ax))) - val axs'' = (case intro_ax of NONE => axs' | SOME ax => if member (op aconv) axs' ax then - (* collect relevant type axioms *) - collect_type_axioms (axs', T) - else - (immediate_output (" " ^ s ^ ".intro"); - collect_term_axioms (ax :: axs', ax))) + val ax_in = SOME (specialize_type thy (s, T) inclass) + (* type match may fail due to sort constraints *) + handle Type.TYPE_MATCH => NONE + val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax)) ax_in + val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) in - axs'' + collect_type_axioms (fold collect_this_axiom + (map_filter I [ax_1, ax_2]) axs, T) end - else if is_IDT_constructor () then - (* only collect relevant type axioms *) - collect_type_axioms (axs, T) - else if is_IDT_recursor () then + else if is_IDT_constructor thy (s, T) + orelse is_IDT_recursor thy (s, T) then (* only collect relevant type axioms *) collect_type_axioms (axs, T) - else ( - case get_defn axioms of - SOME (axname, ax) => - if member (op aconv) axs ax then - (* collect relevant type axioms *) - collect_type_axioms (axs, T) - else - (immediate_output (" " ^ axname); - collect_term_axioms (ax :: axs, ax)) - | NONE => - (* collect relevant type axioms *) - collect_type_axioms (axs, T) - ) - end - | Free (_, T) => collect_type_axioms (axs, T) - | Var (_, T) => collect_type_axioms (axs, T) - | Bound i => axs - | Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body) - | t1 $ t2 => collect_term_axioms (collect_term_axioms (axs, t1), t2) - (* universal closure over schematic variables *) - (* Term.term -> Term.term *) - fun close_form t = - let - (* (Term.indexname * Term.typ) list *) - val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t)) - in - Library.foldl - (fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x, i), T), t'))) - (t, vars) - end + else + (* other constants should have been unfolded, with some *) + (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) + (* typedefs, or type-class related constants *) + (* only collect relevant type axioms *) + collect_type_axioms (axs, T) + | Free (_, T) => collect_type_axioms (axs, T) + | Var (_, T) => collect_type_axioms (axs, T) + | Bound i => axs + | Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body) + | t1 $ t2 => collect_term_axioms (collect_term_axioms (axs, t1), t2) (* Term.term list *) val result = map close_form (collect_term_axioms ([], t)) val _ = writeln " ...done." @@ -776,7 +910,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index + val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = (if Library.exists (fn d => @@ -930,11 +1064,12 @@ (* unit -> unit *) fun wrapper () = let - (* Term.term list *) - val axioms = collect_axioms thy t + val u = unfold_defs thy t + val _ = writeln ("Unfolded term: " ^ Sign.string_of_term (sign_of thy) u) + val axioms = collect_axioms thy u (* Term.typ list *) - val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms) - val _ = writeln ("Ground types: " + val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], u :: axioms) + val _ = writeln ("Ground types: " ^ (if null types then "none." else commas (map (Sign.string_of_typ (sign_of thy)) types))) (* we can only consider fragments of recursive IDTs, so we issue a *) @@ -947,7 +1082,7 @@ let val index = #index info val descr = #descr info - val (_, _, constrs) = (the o AList.lookup (op =) descr) index + val (_, _, constrs) = (Option.valOf o AList.lookup (op =) descr) index in (* recursive datatype? *) Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs @@ -963,19 +1098,19 @@ val init_model = (universe, []) val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True} val _ = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") - (* translate 't' and all axioms *) + (* translate 'u' and all axioms *) val ((model, args), intrs) = foldl_map (fn ((m, a), t') => let val (i, m', a') = interpret thy m a t' in (* set 'def_eq' to 'true' *) ((m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'}), i) - end) ((init_model, init_args), t :: axioms) - (* make 't' either true or false, and make all axioms true, and *) + end) ((init_model, init_args), u :: axioms) + (* make 'u' either true or false, and make all axioms true, and *) (* add the well-formedness side condition *) - val fm_t = (if negate then toFalse else toTrue) (hd intrs) + val fm_u = (if negate then toFalse else toTrue) (hd intrs) val fm_ax = PropLogic.all (map toTrue (tl intrs)) - val fm = PropLogic.all [#wellformed args, fm_ax, fm_t] + val fm = PropLogic.all [#wellformed args, fm_ax, fm_u] in immediate_output " invoking SAT solver..."; (case SatSolver.invoke_solver satsolver fm of @@ -1317,10 +1452,11 @@ fun eta_expand t i = let - val Ts = binder_types (fastype_of t) + val Ts = Term.binder_types (Term.fastype_of t) + val t' = Term.incr_boundvars i t in - foldr (fn (T, t) => Abs ("", T, t)) - (list_comb (t, map Bound (i-1 downto 0))) (Library.take (i, Ts)) + foldr (fn (T, term) => Abs ("", T, term)) + (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i)) end; (* ------------------------------------------------------------------------- *) @@ -1377,7 +1513,7 @@ (* unit -> (interpretation * model * arguments) option *) fun interpret_groundtype () = let - val size = (if T = Term.propT then 2 else (the o AList.lookup (op =) typs) T) (* the model MUST specify a size for ground types *) + val size = (if T = Term.propT then 2 else (Option.valOf o AList.lookup (op =) typs) T) (* the model MUST specify a size for ground types *) val next = next_idx+size val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) (* prop_formula list *) @@ -1473,12 +1609,13 @@ fun Pure_interpreter thy model args t = case t of - Const ("all", _) $ t1 => (* in the meta-logic, 'all' MUST be followed by an argument term *) + Const ("all", _) $ t1 => let val (i, m, a) = interpret thy model args t1 in case i of Node xs => + (* 3-valued logic *) let val fmTrue = PropLogic.all (map toTrue xs) val fmFalse = PropLogic.exists (map toFalse xs) @@ -1488,6 +1625,8 @@ | _ => raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function") end + | Const ("all", _) => + SOME (interpret thy model args (eta_expand t 1)) | Const ("==", _) $ t1 $ t2 => let val (i1, m1, a1) = interpret thy model args t1 @@ -1496,8 +1635,24 @@ (* we use either 'make_def_equality' or 'make_equality' *) SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end - | Const ("==>", _) => (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *) - SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) + | Const ("==", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("==", _) => + SOME (interpret thy model args (eta_expand t 2)) + | Const ("==>", _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret thy model args t1 + val (i2, m2, a2) = interpret thy m1 a1 t2 + val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) + val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const ("==>", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("==>", _) => + SOME (interpret thy model args (eta_expand t 2)) | _ => NONE; (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) @@ -1506,8 +1661,7 @@ (* ------------------------------------------------------------------------- *) (* Providing interpretations directly is more efficient than unfolding the *) (* logical constants. In HOL however, logical constants can themselves be *) - (* arguments. "All" and "Ex" are then translated just like any other *) - (* constant, with the relevant axiom being added by 'collect_axioms'. *) + (* arguments. They are then translated using eta-expansion. *) (* ------------------------------------------------------------------------- *) case t of Const ("Trueprop", _) => @@ -1518,15 +1672,13 @@ SOME (TT, model, args) | Const ("False", _) => (* redundant, since 'False' is also an IDT constructor *) SOME (FF, model, args) - | Const ("All", _) $ t1 => - (* if "All" occurs without an argument (i.e. as argument to a higher-order *) - (* function or predicate), it is handled by the 'stlc_interpreter' (i.e. *) - (* by unfolding its definition) *) + | Const ("All", _) $ t1 => (* similar to "all" (Pure) *) let val (i, m, a) = interpret thy model args t1 in case i of Node xs => + (* 3-valued logic *) let val fmTrue = PropLogic.all (map toTrue xs) val fmFalse = PropLogic.exists (map toFalse xs) @@ -1536,15 +1688,15 @@ | _ => raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function") end + | Const ("All", _) => + SOME (interpret thy model args (eta_expand t 1)) | Const ("Ex", _) $ t1 => - (* if "Ex" occurs without an argument (i.e. as argument to a higher-order *) - (* function or predicate), it is handled by the 'stlc_interpreter' (i.e. *) - (* by unfolding its definition) *) let val (i, m, a) = interpret thy model args t1 in case i of Node xs => + (* 3-valued logic *) let val fmTrue = PropLogic.exists (map toTrue xs) val fmFalse = PropLogic.all (map toFalse xs) @@ -1554,7 +1706,9 @@ | _ => raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function") end - | Const ("op =", _) $ t1 $ t2 => + | Const ("Ex", _) => + SOME (interpret thy model args (eta_expand t 1)) + | Const ("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 @@ -1579,6 +1733,8 @@ SOME (interpret thy model args (eta_expand t 1)) | Const ("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 => (* 3-valued logic *) @@ -1594,8 +1750,10 @@ SOME (interpret thy model args (eta_expand t 1)) | Const ("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 => + | Const ("op -->", _) $ t1 $ t2 => (* similar to "==>" (Pure) *) (* 3-valued logic *) let val (i1, m1, a1) = interpret thy model args t1 @@ -1605,9 +1763,13 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end + | Const ("op -->", _) $ t1 => + SOME (interpret thy model args (eta_expand t 1)) | Const ("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 [TT, TT]], model, args) *) - SOME (interpret thy model args (eta_expand t 2)) | _ => NONE; (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) @@ -1679,7 +1841,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index + val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = (if Library.exists (fn d => @@ -1747,7 +1909,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index + val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index val typ_assoc = dtyps ~~ Ts' (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = (if Library.exists (fn d => @@ -1925,8 +2087,8 @@ let val index = #index info val descr = #descr info - val (dtname, dtyps, _) = (the o AList.lookup (op =) descr) index - (* number of all constructors, including those of different *) + val (dtname, dtyps, _) = (Option.valOf o AList.lookup (op =) descr) index + (* number of all constructors, including those of ({({(a0, True)}, False), ({(a0, False)}, False)}, True)different *) (* (mutually recursive) datatypes within the same descriptor 'descr' *) val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr) val params_count = length params @@ -2016,7 +2178,7 @@ SOME args => (n, args) | NONE => get_cargs_rec (n+1, xs)) in - get_cargs_rec (0, (the o AList.lookup (op =) mc_intrs) idx) + get_cargs_rec (0, (Option.valOf o AList.lookup (op =) mc_intrs) idx) end (* returns the number of constructors in datatypes that occur in *) (* the descriptor 'descr' before the datatype given by 'idx' *) @@ -2036,7 +2198,7 @@ (* where 'idx' gives the datatype and 'elem' the element of it *) (* int -> int -> interpretation *) fun compute_array_entry idx elem = - case Array.sub ((the o AList.lookup (op =) INTRS) idx, elem) of + case Array.sub ((Option.valOf o AList.lookup (op =) INTRS) idx, elem) of SOME result => (* simply return the previously computed result *) result @@ -2054,7 +2216,7 @@ (* select the correct subtree of the parameter corresponding to constructor 'c' *) val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args) (* find the indices of the constructor's recursive arguments *) - val (_, _, constrs) = (the o AList.lookup (op =) descr) idx + val (_, _, constrs) = (Option.valOf o AList.lookup (op =) descr) idx val constr_args = (snd o List.nth) (constrs, c) val rec_args = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args) val rec_args' = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args @@ -2062,7 +2224,7 @@ val result = foldl (fn ((idx, elem), intr) => interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args' (* update 'INTRS' *) - val _ = Array.update ((the o AList.lookup (op =) INTRS) idx, elem, SOME result) + val _ = Array.update ((Option.valOf o AList.lookup (op =) INTRS) idx, elem, SOME result) in result end @@ -2081,13 +2243,13 @@ in modifyi_loop 0 end - val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((the o AList.lookup (op =) INTRS) index) + val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((Option.valOf o AList.lookup (op =) INTRS) index) (* 'a Array.array -> 'a list *) fun toList arr = Array.foldr op:: [] arr in (* return the part of 'INTRS' that corresponds to the current datatype *) - SOME ((Node o map the o toList o the o AList.lookup (op =) INTRS) index, model', args') + SOME ((Node o map Option.valOf o toList o Option.valOf o AList.lookup (op =) INTRS) index, model', args') end end else @@ -2576,7 +2738,7 @@ val (typs, _) = model val index = #index info val descr = #descr info - val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index + val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = (if Library.exists (fn d => diff -r 7b9c2f6b45f5 -r acfb13e8819e src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Wed Jan 03 22:59:30 2007 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Thu Jan 04 00:12:30 2007 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/ex/Refute_Examples.thy ID: $Id$ Author: Tjark Weber - Copyright 2003-2005 + Copyright 2003-2007 *) (* See 'HOL/Refute.thy' for help. *) @@ -24,6 +24,8 @@ refute [satsolver="dpll"] 2 -- {* ... and specify a subgoal at the same time *} oops +(******************************************************************************) + section {* Examples and Test Cases *} subsection {* Propositional logic *} @@ -65,6 +67,8 @@ refute oops +(******************************************************************************) + subsection {* Predicate logic *} lemma "P x y z" @@ -79,6 +83,8 @@ refute oops +(******************************************************************************) + subsection {* Equality *} lemma "P = True" @@ -111,6 +117,8 @@ refute oops +(******************************************************************************) + subsection {* First-Order Logic *} lemma "\x. P x" @@ -203,6 +211,8 @@ refute oops +(******************************************************************************) + subsection {* Higher-Order Logic *} lemma "\P. P" @@ -227,15 +237,15 @@ refute oops -lemma "P All" +lemma "x \ All" refute oops -lemma "P Ex" +lemma "x \ Ex" refute oops -lemma "P Ex1" +lemma "x \ Ex1" refute oops @@ -302,6 +312,8 @@ apply (fast intro: ext) done +(******************************************************************************) + subsection {* Meta-logic *} lemma "!!x. P x" @@ -320,6 +332,20 @@ refute oops +lemma "(x == all) \ False" + refute +oops + +lemma "(x == (op ==)) \ False" + refute +oops + +lemma "(x == (op \)) \ False" + refute +oops + +(******************************************************************************) + subsection {* Schematic variables *} lemma "?P" @@ -332,6 +358,8 @@ apply auto done +(******************************************************************************) + subsection {* Abstractions *} lemma "(\x. x) = (\x. y)" @@ -347,6 +375,8 @@ apply simp done +(******************************************************************************) + subsection {* Sets *} lemma "P (A::'a set)" @@ -390,6 +420,8 @@ refute oops +(******************************************************************************) + subsection {* arbitrary *} lemma "arbitrary" @@ -408,6 +440,8 @@ refute oops +(******************************************************************************) + subsection {* The *} lemma "The P" @@ -430,6 +464,8 @@ refute oops +(******************************************************************************) + subsection {* Eps *} lemma "Eps P" @@ -968,11 +1004,11 @@ refute oops -lemma "a @ [] = b @ []" +lemma "xs @ [] = ys @ []" refute oops -lemma "a @ b = b @ a" +lemma "xs @ ys = ys @ xs" refute oops @@ -1000,7 +1036,7 @@ refute oops -text {* The axiom of this type class does not contain any type variables, but is internally converted into one that does: *} +text {* The axiom of this type class does not contain any type variables: *} axclass classB classB_ax: "P | ~ P"