# HG changeset patch # User wenzelm # Date 1294440366 -3600 # Node ID 73981e95b30b53446d84cde8a9f712e934f0745f # Parent 79ec1ddf49dfa2362d1fc8ac1c21d9885f57cbba# Parent 3bb2f035203f269052523c834df0e98af7581d32 merged diff -r 79ec1ddf49df -r 73981e95b30b Admin/CHECKLIST --- a/Admin/CHECKLIST Fri Jan 07 18:10:43 2011 +0100 +++ b/Admin/CHECKLIST Fri Jan 07 23:46:06 2011 +0100 @@ -3,7 +3,7 @@ - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj; -- test Proof General 3.7.1.1, 4.0; +- test Proof General 3.7.1.1/4.0 xor 4.1; - test Scala wrapper; @@ -17,6 +17,8 @@ - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS; +- check Admin/contributed_components; + - diff NEWS wrt. last official release, which is read-only; - update https://isabelle.in.tum.de/repos/website; diff -r 79ec1ddf49df -r 73981e95b30b Admin/contributed_components --- a/Admin/contributed_components Fri Jan 07 18:10:43 2011 +0100 +++ b/Admin/contributed_components Fri Jan 07 23:46:06 2011 +0100 @@ -1,9 +1,8 @@ #contributed components contrib/cvc3-2.2 contrib/e-1.2 -contrib/jedit-4.3.2 contrib/kodkodi-1.2.16 contrib/spass-3.7 -contrib/scala-2.8.0.RC5 +contrib/scala-2.8.1.final contrib/vampire-1.0 contrib/z3-2.15 diff -r 79ec1ddf49df -r 73981e95b30b COPYRIGHT --- a/COPYRIGHT Fri Jan 07 18:10:43 2011 +0100 +++ b/COPYRIGHT Fri Jan 07 23:46:06 2011 +0100 @@ -1,8 +1,9 @@ ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. -Copyright (c) 2010, - University of Cambridge and - Technische Universitaet Muenchen. +Copyright (c) 2011, + University of Cambridge, + Technische Universitaet Muenchen, + and contributors. All rights reserved. diff -r 79ec1ddf49df -r 73981e95b30b lib/scripts/unsymbolize --- a/lib/scripts/unsymbolize Fri Jan 07 18:10:43 2011 +0100 +++ b/lib/scripts/unsymbolize Fri Jan 07 23:46:06 2011 +0100 @@ -46,13 +46,13 @@ my $result = $_; if ($text ne $result) { - print STDERR "fixing $file\n"; + print STDERR "fixing $file\n"; if (! -f "$file~~") { - rename $file, "$file~~" || die $!; + rename $file, "$file~~" || die $!; } - open (FILE, "> $file") || die $!; - print FILE $result; - close FILE || die $!; + open (FILE, "> $file") || die $!; + print FILE $result; + close FILE || die $!; } } diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Fri Jan 07 23:46:06 2011 +0100 @@ -4,6 +4,8 @@ Derivation of the proof rules and, most importantly, the VCG tactic. *) +(* FIXME structure Hoare: HOARE *) + (*** The tactics ***) (*****************************************************************************) @@ -13,7 +15,7 @@ (** working on at the moment of the call **) (*****************************************************************************) -local open HOLogic in +local (** maps (%x1 ... xn. t) to [x1,...,xn] **) fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t @@ -26,14 +28,17 @@ (** abstraction of body over a tuple formed from a list of free variables. Types are also built **) -fun mk_abstupleC [] body = absfree ("x", unitT, body) +fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT, body) | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v in if w=[] then absfree (n, T, body) else let val z = mk_abstupleC w body; val T2 = case z of Abs(_,T,_) => T | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T; - in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT) - $ absfree (n, T, z) end end; + in + Const (@{const_name prod_case}, + (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT) + $ absfree (n, T, z) + end end; (** maps [x1,...,xn] to (x1,...,xn) and types**) fun mk_bodyC [] = HOLogic.unit @@ -43,22 +48,23 @@ val T2 = case z of Free(_, T) => T | Const (@{const_name Pair}, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T; - in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) $ x $ z end; + in Const (@{const_name Pair}, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end; (** maps a subgoal of the form: VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) fun get_vars c = let val d = Logic.strip_assums_concl c; - val Const _ $ pre $ _ $ _ = dest_Trueprop d; + val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d; in mk_vars pre end; fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm - in Collect_const t $ trm end; + in HOLogic.Collect_const t $ trm end; -fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT); +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> HOLogic.boolT); +in fun Mset ctxt prop = let @@ -66,11 +72,11 @@ val vars = get_vars prop; val varsT = fastype_of (mk_bodyC vars); - val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> boolT) $ mk_bodyC vars)); - val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> boolT) $ Bound 0)); + val big_Collect = mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars)); + val small_Collect = mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0)); val MsetT = fastype_of big_Collect; - fun Mset_incl t = mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t); + fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t); val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect); val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1); in (vars, th) end; diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 07 23:46:06 2011 +0100 @@ -130,7 +130,7 @@ relevance_fudge relevance_override facts hyp_ts concl_t |> map (fst o fst) val (found_facts, lost_facts) = - List.concat proofs |> sort_distinct string_ord + flat proofs |> sort_distinct string_ord |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |> List.partition (curry (op <=) 0 o fst) |>> sort (prod_ord int_ord string_ord) ||> map snd diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Jan 07 23:46:06 2011 +0100 @@ -53,7 +53,7 @@ text {* qdelete(A, [A|L], L). qdelete(X, [A|Z], [A|R]) :- - qdelete(X, Z, R). + qdelete(X, Z, R). *} inductive qdelete :: "int => int list => int list => bool" @@ -64,9 +64,9 @@ text {* qperm([], []). qperm([X|Y], K) :- - qdelete(U, [X|Y], Z), - K = [U|V], - qperm(Z, V). + qdelete(U, [X|Y], Z), + K = [U|V], + qperm(Z, V). *} inductive qperm :: "int list => int list => bool" @@ -77,8 +77,8 @@ text {* safe([]). safe([N|L]) :- - nodiag(N, 1, L), - safe(L). + nodiag(N, 1, L), + safe(L). *} inductive safe :: "int list => bool" @@ -88,8 +88,8 @@ text {* queen(Data, Out) :- - qperm(Data, Out), - safe(Out) + qperm(Data, Out), + safe(Out) *} inductive queen :: "int list => int list => bool" @@ -113,36 +113,36 @@ text {* d(U + V, X, DU + DV) :- - cut, - d(U, X, DU), - d(V, X, DV). + cut, + d(U, X, DU), + d(V, X, DV). d(U - V, X, DU - DV) :- - cut, - d(U, X, DU), - d(V, X, DV). + cut, + d(U, X, DU), + d(V, X, DV). d(U * V, X, DU * V + U * DV) :- - cut, - d(U, X, DU), - d(V, X, DV). + cut, + d(U, X, DU), + d(V, X, DV). d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :- - cut, - d(U, X, DU), - d(V, X, DV). + cut, + d(U, X, DU), + d(V, X, DV). d(^(U, N), X, DU * num(N) * ^(U, N1)) :- - cut, - N1 is N - 1, - d(U, X, DU). + cut, + N1 is N - 1, + d(U, X, DU). d(-U, X, -DU) :- - cut, - d(U, X, DU). + cut, + d(U, X, DU). d(exp(U), X, exp(U) * DU) :- - cut, - d(U, X, DU). + cut, + d(U, X, DU). d(log(U), X, DU / U) :- - cut, - d(U, X, DU). + cut, + d(U, X, DU). d(x, X, num(1)) :- - cut. + cut. d(num(_), _, num(0)). *} @@ -162,16 +162,16 @@ text {* ops8(E) :- - d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E). + d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E). divide10(E) :- - d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E). + d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E). log10(E) :- - d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E). + d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E). times10(E) :- - d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E) + d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E) *} inductive ops8 :: "expr => bool" diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Quotient.thy Fri Jan 07 23:46:06 2011 +0100 @@ -667,6 +667,7 @@ text {* Auxiliary data for the quotient package *} use "Tools/Quotient/quotient_info.ML" +setup Quotient_Info.setup declare [[map "fun" = (map_fun, fun_rel)]] diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/ATP/scripts/spass --- a/src/HOL/Tools/ATP/scripts/spass Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/ATP/scripts/spass Fri Jan 07 23:46:06 2011 +0100 @@ -8,12 +8,12 @@ options=${@:1:$(($#-1))} name=${@:$(($#)):1} -$SPASS_HOME/tptp2dfg $name $name.fof.dfg -$SPASS_HOME/SPASS -Flotter $name.fof.dfg \ +"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg +"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \ | sed 's/description({$/description({*/' \ > $name.cnf.dfg rm -f $name.fof.dfg cat $name.cnf.dfg -$SPASS_HOME/SPASS $options $name.cnf.dfg \ +"$SPASS_HOME/SPASS" $options $name.cnf.dfg \ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' rm -f $name.cnf.dfg diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Qelim/qelim.ML Fri Jan 07 23:46:06 2011 +0100 @@ -6,30 +6,28 @@ signature QELIM = sig - val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a - -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv - val standard_qelim_conv: (cterm list -> conv) -> (cterm list -> conv) - -> (cterm list -> conv) -> conv + val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a -> + ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv + val standard_qelim_conv: (cterm list -> conv) -> (cterm list -> conv) -> + (cterm list -> conv) -> conv end; structure Qelim: QELIM = struct -open Conv; - val all_not_ex = mk_meta_eq @{thm "all_not_ex"}; fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv = let fun conv env p = case (term_of p) of - Const(s,T)$_$_ => + Const(s,T)$_$_ => if domain_type T = HOLogic.boolT andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj}, @{const_name HOL.implies}, @{const_name HOL.eq}] s - then binop_conv (conv env) p + then Conv.binop_conv (conv env) p else atcv env p - | Const(@{const_name Not},_)$_ => arg_conv (conv env) p + | Const(@{const_name Not},_)$_ => Conv.arg_conv (conv env) p | Const(@{const_name Ex},_)$Abs(s,_,_) => let val (e,p0) = Thm.dest_comb p diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 23:46:06 2011 +0100 @@ -19,9 +19,6 @@ structure Quotient_Def: QUOTIENT_DEF = struct -open Quotient_Info; -open Quotient_Term; - (** Interface and Syntax Setup **) (* The ML-interface for a quotient definition takes @@ -34,75 +31,76 @@ It stores the qconst_info in the qconsts data slot. - Restriction: At the moment the left- and right-hand - side of the definition must be a constant. + Restriction: At the moment the left- and right-hand + side of the definition must be a constant. *) -fun error_msg bind str = -let - val name = Binding.name_of bind - val pos = Position.str_of (Binding.pos_of bind) -in - error ("Head of quotient_definition " ^ - quote str ^ " differs from declaration " ^ name ^ pos) -end +fun error_msg bind str = + let + val name = Binding.name_of bind + val pos = Position.str_of (Binding.pos_of bind) + in + error ("Head of quotient_definition " ^ + quote str ^ " differs from declaration " ^ name ^ pos) + end fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = -let - val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." - val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" - val _ = if is_Const rhs then () else warning "The definiens is not a constant" - - fun sanity_test NONE _ = true - | sanity_test (SOME bind) str = - if Name.of_binding bind = str then true - else error_msg bind str + let + val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." + val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" + val _ = if is_Const rhs then () else warning "The definiens is not a constant" - val _ = sanity_test optbind lhs_str + fun sanity_test NONE _ = true + | sanity_test (SOME bind) str = + if Name.of_binding bind = str then true + else error_msg bind str + + val _ = sanity_test optbind lhs_str - val qconst_bname = Binding.name lhs_str - val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs - val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) - val (_, prop') = Local_Defs.cert_def lthy prop - val (_, newrhs) = Local_Defs.abs_def prop' + val qconst_bname = Binding.name lhs_str + val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs + val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) + val (_, prop') = Local_Defs.cert_def lthy prop + val (_, newrhs) = Local_Defs.abs_def prop' - val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy + val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy - (* data storage *) - val qconst_data = {qconst = trm, rconst = rhs, def = thm} + (* data storage *) + val qconst_data = {qconst = trm, rconst = rhs, def = thm} - fun qcinfo phi = transform_qconsts phi qconst_data - fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) - val lthy'' = Local_Theory.declaration true - (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' -in - (qconst_data, lthy'') -end + fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data + fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) + val lthy'' = + Local_Theory.declaration true + (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' + in + (qconst_data, lthy'') + end fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = -let - val lhs = Syntax.read_term lthy lhs_str - val rhs = Syntax.read_term lthy rhs_str - val lthy' = Variable.declare_term lhs lthy - val lthy'' = Variable.declare_term rhs lthy' -in - quotient_def (decl, (attr, (lhs, rhs))) lthy'' -end + let + val lhs = Syntax.read_term lthy lhs_str + val rhs = Syntax.read_term lthy rhs_str + val lthy' = Variable.declare_term lhs lthy + val lthy'' = Variable.declare_term rhs lthy' + in + quotient_def (decl, (attr, (lhs, rhs))) lthy'' + end (* a wrapper for automatically lifting a raw constant *) fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt = -let - val rty = fastype_of rconst - val qty = derive_qtyp ctxt qtys rty - val lhs = Free (qconst_name, qty) -in - quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt -end + let + val rty = fastype_of rconst + val qty = Quotient_Term.derive_qtyp ctxt qtys rty + val lhs = Free (qconst_name, qty) + in + quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt + end (* parser and command *) val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where" val quotdef_parser = - Scan.optional quotdef_decl (NONE, NoSyn) -- + Scan.optional quotdef_decl (NONE, NoSyn) -- Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term)) val _ = diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 23:46:06 2011 +0100 @@ -4,13 +4,15 @@ Data slots for the quotient package. *) +(* FIXME odd names/signatures of data access operations *) + signature QUOTIENT_INFO = sig exception NotFound (* FIXME complicates signatures unnecessarily *) type maps_info = {mapfun: string, relmap: string} val maps_defined: theory -> string -> bool - (* FIXME functions called "lookup" must return option, not raise exception *) + (* FIXME functions called "lookup" must return option, not raise exception! *) val maps_lookup: theory -> string -> maps_info (* raises NotFound *) val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context @@ -42,13 +44,13 @@ val id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute + val setup: theory -> theory end; - structure Quotient_Info: QUOTIENT_INFO = struct -exception NotFound +exception NotFound (* FIXME odd OCaml-ism!? *) (** data containers **) @@ -68,9 +70,9 @@ Symtab.defined (MapsData.get thy) s fun maps_lookup thy s = - case (Symtab.lookup (MapsData.get thy) s) of + (case Symtab.lookup (MapsData.get thy) s of SOME map_fun => map_fun - | NONE => raise NotFound + | NONE => raise NotFound) fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo) (* FIXME *) @@ -80,17 +82,17 @@ (* attribute to be used in declare statements *) fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = -let - val thy = ProofContext.theory_of ctxt - val tyname = Sign.intern_type thy tystr - val mapname = Sign.intern_const thy mapstr - val relname = Sign.intern_const thy relstr + let + val thy = ProofContext.theory_of ctxt + val tyname = Sign.intern_type thy tystr + val mapname = Sign.intern_const thy mapstr + val relname = Sign.intern_const thy relstr - fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) - val _ = List.app sanity_check [mapname, relname] -in - maps_attribute_aux tyname {mapfun = mapname, relmap = relname} -end + fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) + val _ = List.app sanity_check [mapname, relname] + in + maps_attribute_aux tyname {mapfun = mapname, relmap = relname} + end val maps_attr_parser = Args.context -- Scan.lift @@ -98,25 +100,21 @@ (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," -- Args.name --| Parse.$$$ ")")) -val _ = Context.>> (Context.map_theory - (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) - "declaration of map information")) - fun print_mapsinfo ctxt = -let - fun prt_map (ty_name, {mapfun, relmap}) = - Pretty.block (Library.separate (Pretty.brk 2) - (map Pretty.str - ["type:", ty_name, - "map:", mapfun, - "relation map:", relmap])) -in - MapsData.get (ProofContext.theory_of ctxt) - |> Symtab.dest - |> map (prt_map) - |> Pretty.big_list "maps for type constructors:" - |> Pretty.writeln -end + let + fun prt_map (ty_name, {mapfun, relmap}) = + Pretty.block (separate (Pretty.brk 2) + (map Pretty.str + ["type:", ty_name, + "map:", mapfun, + "relation map:", relmap])) + in + MapsData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map (prt_map) + |> Pretty.big_list "maps for type constructors:" + |> Pretty.writeln + end (* info about quotient types *) @@ -150,24 +148,24 @@ map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) fun print_quotinfo ctxt = -let - fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = - Pretty.block (Library.separate (Pretty.brk 2) - [Pretty.str "quotient type:", - Syntax.pretty_typ ctxt qtyp, - Pretty.str "raw type:", - Syntax.pretty_typ ctxt rtyp, - Pretty.str "relation:", - Syntax.pretty_term ctxt equiv_rel, - Pretty.str "equiv. thm:", - Syntax.pretty_term ctxt (prop_of equiv_thm)]) -in - QuotData.get (ProofContext.theory_of ctxt) - |> Symtab.dest - |> map (prt_quot o snd) - |> Pretty.big_list "quotients:" - |> Pretty.writeln -end + let + fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = + Pretty.block (separate (Pretty.brk 2) + [Pretty.str "quotient type:", + Syntax.pretty_typ ctxt qtyp, + Pretty.str "raw type:", + Syntax.pretty_typ ctxt rtyp, + Pretty.str "relation:", + Syntax.pretty_term ctxt equiv_rel, + Pretty.str "equiv. thm:", + Syntax.pretty_term ctxt (prop_of equiv_thm)]) + in + QuotData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map (prt_quot o snd) + |> Pretty.big_list "quotients:" + |> Pretty.writeln + end (* info about quotient constants *) @@ -207,32 +205,32 @@ name = name' andalso Sign.typ_instance thy (qty, qty') end in - case Symtab.lookup (QConstsData.get thy) name of + (case Symtab.lookup (QConstsData.get thy) name of NONE => raise NotFound | SOME l => - (case (find_first matches l) of - SOME x => x - | NONE => raise NotFound) + (case find_first matches l of + SOME x => x + | NONE => raise NotFound)) end fun print_qconstinfo ctxt = -let - fun prt_qconst {qconst, rconst, def} = - Pretty.block (separate (Pretty.brk 1) - [Syntax.pretty_term ctxt qconst, - Pretty.str ":=", - Syntax.pretty_term ctxt rconst, - Pretty.str "as", - Syntax.pretty_term ctxt (prop_of def)]) -in - QConstsData.get (ProofContext.theory_of ctxt) - |> Symtab.dest - |> map snd - |> flat - |> map prt_qconst - |> Pretty.big_list "quotient constants:" - |> Pretty.writeln -end + let + fun prt_qconst {qconst, rconst, def} = + Pretty.block (separate (Pretty.brk 1) + [Syntax.pretty_term ctxt qconst, + Pretty.str ":=", + Syntax.pretty_term ctxt rconst, + Pretty.str "as", + Syntax.pretty_term ctxt (prop_of def)]) + in + QConstsData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map snd + |> flat + |> map prt_qconst + |> Pretty.big_list "quotient constants:" + |> Pretty.writeln + end (* equivalence relation theorems *) structure EquivRules = Named_Thms @@ -283,25 +281,32 @@ val quotient_rules_get = QuotientRules.get val quotient_rules_add = QuotientRules.add -(* setup of the theorem lists *) + +(* theory setup *) -val _ = Context.>> (Context.map_theory - (EquivRules.setup #> - RspRules.setup #> - PrsRules.setup #> - IdSimps.setup #> - QuotientRules.setup)) +val setup = + Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + "declaration of map information" #> + EquivRules.setup #> + RspRules.setup #> + PrsRules.setup #> + IdSimps.setup #> + QuotientRules.setup + -(* setup of the printing commands *) +(* outer syntax commands *) + +val _ = + Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag + (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of))) -fun improper_command (pp_fn, cmd_name, descr_str) = - Outer_Syntax.improper_command cmd_name descr_str - Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) +val _ = + Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag + (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) -val _ = map improper_command - [(print_mapsinfo, "print_quotmaps", "print out all map functions"), - (print_quotinfo, "print_quotients", "print out all quotients"), - (print_qconstinfo, "print_quotconsts", "print out all quotient constants")] +val _ = + Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag + (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) end; (* structure *) diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 23:46:06 2011 +0100 @@ -11,10 +11,10 @@ val injection_tac: Proof.context -> int -> tactic val all_injection_tac: Proof.context -> int -> tactic val clean_tac: Proof.context -> int -> tactic - + val descend_procedure_tac: Proof.context -> thm list -> int -> tactic val descend_tac: Proof.context -> thm list -> int -> tactic - + val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic @@ -25,10 +25,6 @@ structure Quotient_Tacs: QUOTIENT_TACS = struct -open Quotient_Info; -open Quotient_Term; - - (** various helper fuctions **) (* Since HOL_basic_ss is too "big" for us, we *) @@ -42,12 +38,12 @@ fun OF1 thm1 thm2 = thm2 RS thm1 fun atomize_thm thm = -let - val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) - val thm'' = Object_Logic.atomize (cprop_of thm') -in - @{thm equal_elim_rule1} OF [thm'', thm'] -end + let + val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *) + val thm'' = Object_Logic.atomize (cprop_of thm') + in + @{thm equal_elim_rule1} OF [thm'', thm'] + end @@ -56,7 +52,7 @@ (** solvers for equivp and quotient assumptions **) fun equiv_tac ctxt = - REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) + REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt)) fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac @@ -64,7 +60,7 @@ fun quotient_tac ctxt = (REPEAT_ALL_NEW (FIRST' [rtac @{thm identity_quotient}, - resolve_tac (quotient_rules_get ctxt)])) + resolve_tac (Quotient_Info.quotient_rules_get ctxt)])) fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) val quotient_solver = @@ -83,14 +79,14 @@ (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) fun get_match_inst thy pat trm = -let - val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) - val tenv = Vartab.dest (Envir.term_env env) - val tyenv = Vartab.dest (Envir.type_env env) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end + let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) + in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) + end (* Calculates the instantiations for the lemmas: @@ -101,35 +97,35 @@ theorem applies and return NONE if it doesn't. *) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = -let - val thy = ProofContext.theory_of ctxt - fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) - val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] - val trm_inst = map (SOME o cterm_of thy) [R2, R1] -in - case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of - NONE => NONE - | SOME thm' => - (case try (get_match_inst thy (get_lhs thm')) redex of - NONE => NONE - | SOME inst2 => try (Drule.instantiate inst2) thm') -end + let + val thy = ProofContext.theory_of ctxt + fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) + val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] + val trm_inst = map (SOME o cterm_of thy) [R2, R1] + in + (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of + NONE => NONE + | SOME thm' => + (case try (get_match_inst thy (get_lhs thm')) redex of + NONE => NONE + | SOME inst2 => try (Drule.instantiate inst2) thm')) + end fun ball_bex_range_simproc ss redex = -let - val ctxt = Simplifier.the_context ss -in - case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + let + val ctxt = Simplifier.the_context ss + in + case redex of + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 - | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 - | _ => NONE -end + | _ => NONE + end (* Regularize works as follows: @@ -152,32 +148,34 @@ fun reflp_get ctxt = map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE - handle THM _ => NONE) (equiv_rules_get ctxt) + handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt) val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} -fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt) +fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt) fun regularize_tac ctxt = -let - val thy = ProofContext.theory_of ctxt - val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} - val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} - val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) - val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] - addSolver equiv_solver addSolver quotient_solver - val eq_eqvs = eq_imp_rel_get ctxt -in - simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' - [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, - resolve_tac (Inductive.get_monos ctxt), - resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simpset]) -end + let + val thy = ProofContext.theory_of ctxt + val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} + val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} + val simproc = + Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) + val simpset = + mk_minimal_ss ctxt + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + addsimprocs [simproc] + addSolver equiv_solver addSolver quotient_solver + val eq_eqvs = eq_imp_rel_get ctxt + in + simp_tac simpset THEN' + REPEAT_ALL_NEW (CHANGED o FIRST' + [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, + resolve_tac (Inductive.get_monos ctxt), + resolve_tac @{thms ball_all_comm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) + end @@ -187,52 +185,52 @@ is an application, it returns the function and the argument. *) fun find_qt_asm asms = -let - fun find_fun trm = - case trm of - (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true - | _ => false -in - case find_first find_fun asms of - SOME (_ $ (_ $ (f $ a))) => SOME (f, a) - | _ => NONE -end + let + fun find_fun trm = + (case trm of + (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true + | _ => false) + in + (case find_first find_fun asms of + SOME (_ $ (_ $ (f $ a))) => SOME (f, a) + | _ => NONE) + end fun quot_true_simple_conv ctxt fnctn ctrm = - case (term_of ctrm) of + case term_of ctrm of (Const (@{const_name Quot_True}, _) $ x) => - let - val fx = fnctn x; - val thy = ProofContext.theory_of ctxt; - val cx = cterm_of thy x; - val cfx = cterm_of thy fx; - val cxt = ctyp_of thy (fastype_of x); - val cfxt = ctyp_of thy (fastype_of fx); - val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp} - in - Conv.rewr_conv thm ctrm - end + let + val fx = fnctn x; + val thy = ProofContext.theory_of ctxt; + val cx = cterm_of thy x; + val cfx = cterm_of thy fx; + val cxt = ctyp_of thy (fastype_of x); + val cfxt = ctyp_of thy (fastype_of fx); + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp} + in + Conv.rewr_conv thm ctrm + end fun quot_true_conv ctxt fnctn ctrm = - case (term_of ctrm) of + (case term_of ctrm of (Const (@{const_name Quot_True}, _) $ _) => quot_true_simple_conv ctxt fnctn ctrm | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm - | _ => Conv.all_conv ctrm + | _ => Conv.all_conv ctrm) fun quot_true_tac ctxt fnctn = - CONVERSION + CONVERSION ((Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) + (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) fun dest_comb (f $ a) = (f, a) fun dest_bcomb ((_ $ l) $ r) = (l, r) fun unlam t = - case t of - (Abs a) => snd (Term.dest_abs a) - | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) + (case t of + Abs a => snd (Term.dest_abs a) + | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))) val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl @@ -242,53 +240,53 @@ *) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => - let - val bare_concl = HOLogic.dest_Trueprop (term_of concl) - val qt_asm = find_qt_asm (map term_of asms) - in - case (bare_concl, qt_asm) of - (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => - if fastype_of qt_fun = fastype_of f - then no_tac - else - let - val ty_x = fastype_of x - val ty_b = fastype_of qt_arg - val ty_f = range_type (fastype_of f) - val thy = ProofContext.theory_of context - val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] - val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val inst_thm = Drule.instantiate' ty_inst - ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} - in - (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1 - end - | _ => no_tac - end) + let + val bare_concl = HOLogic.dest_Trueprop (term_of concl) + val qt_asm = find_qt_asm (map term_of asms) + in + case (bare_concl, qt_asm) of + (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => + if fastype_of qt_fun = fastype_of f + then no_tac + else + let + val ty_x = fastype_of x + val ty_b = fastype_of qt_arg + val ty_f = range_type (fastype_of f) + val thy = ProofContext.theory_of context + val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val inst_thm = Drule.instantiate' ty_inst + ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + in + (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1 + end + | _ => no_tac + end) (* Instantiates and applies 'equals_rsp'. Since the theorem is complex we rely on instantiation to tell us if it applies *) fun equals_rsp_tac R ctxt = -let - val thy = ProofContext.theory_of ctxt -in - case try (cterm_of thy) R of (* There can be loose bounds in R *) - SOME ctm => - let - val ty = domain_type (fastype_of R) - in - case try (Drule.instantiate' [SOME (ctyp_of thy ty)] - [SOME (cterm_of thy R)]) @{thm equals_rsp} of - SOME thm => rtac thm THEN' quotient_tac ctxt - | NONE => K no_tac - end - | _ => K no_tac -end + let + val thy = ProofContext.theory_of ctxt + in + case try (cterm_of thy) R of (* There can be loose bounds in R *) + SOME ctm => + let + val ty = domain_type (fastype_of R) + in + case try (Drule.instantiate' [SOME (ctyp_of thy ty)] + [SOME (cterm_of thy R)]) @{thm equals_rsp} of + SOME thm => rtac thm THEN' quotient_tac ctxt + | NONE => K no_tac + end + | _ => K no_tac + end fun rep_abs_rsp_tac ctxt = SUBGOAL (fn (goal, i) => - case (try bare_concl goal) of + (case try bare_concl goal of SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac | SOME (rel $ _ $ (rep $ (abs $ _))) => let @@ -303,7 +301,7 @@ | NONE => no_tac) | NONE => no_tac end - | _ => no_tac) + | _ => no_tac)) @@ -329,67 +327,66 @@ - reflexivity of the relation *) fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => -(case (bare_concl goal) of - (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) - (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) - => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam + (case bare_concl goal of + (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) + (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) + => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam - (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) -| (Const (@{const_name HOL.eq},_) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} + (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) + | (Const (@{const_name HOL.eq},_) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} - (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam + (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) + | (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam - (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) -| Const (@{const_name HOL.eq},_) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} + (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) + | Const (@{const_name HOL.eq},_) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} - (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam + (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) + | (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) - => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt + | (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) + => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt -| (_ $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] + | (_ $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] -| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) => - (rtac @{thm refl} ORELSE' - (equals_rsp_tac R ctxt THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) + | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) => + (rtac @{thm refl} ORELSE' + (equals_rsp_tac R ctxt THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) - (* reflexivity of operators arising from Cong_tac *) -| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl} + (* reflexivity of operators arising from Cong_tac *) + | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl} - (* respectfulness of constants; in particular of a simple relation *) -| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) - => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt + (* respectfulness of constants; in particular of a simple relation *) + | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) + => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt - (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) - (* observe map_fun *) -| _ $ _ $ _ - => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) - ORELSE' rep_abs_rsp_tac ctxt + (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) + (* observe map_fun *) + | _ $ _ $ _ + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + ORELSE' rep_abs_rsp_tac ctxt -| _ => K no_tac -) i) + | _ => K no_tac) i) fun injection_step_tac ctxt rel_refl = - FIRST' [ + FIRST' [ injection_match_tac ctxt, (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) @@ -412,11 +409,11 @@ resolve_tac rel_refl] fun injection_tac ctxt = -let - val rel_refl = reflp_get ctxt -in - injection_step_tac ctxt rel_refl -end + let + val rel_refl = reflp_get ctxt + in + injection_step_tac ctxt rel_refl + end fun all_injection_tac ctxt = REPEAT_ALL_NEW (injection_tac ctxt) @@ -427,46 +424,48 @@ (* expands all map_funs, except in front of the (bound) variables listed in xs *) fun map_fun_simple_conv xs ctrm = - case (term_of ctrm) of + (case term_of ctrm of ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) => if member (op=) xs h then Conv.all_conv ctrm else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm - | _ => Conv.all_conv ctrm + | _ => Conv.all_conv ctrm) fun map_fun_conv xs ctxt ctrm = - case (term_of ctrm) of - _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv - map_fun_simple_conv xs) ctrm - | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm - | _ => Conv.all_conv ctrm + (case term_of ctrm of + _ $ _ => + (Conv.comb_conv (map_fun_conv xs ctxt) then_conv + map_fun_simple_conv xs) ctrm + | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm) fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt) (* custom matching functions *) fun mk_abs u i t = - if incr_boundvars i u aconv t then Bound i else - case t of - t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2 - | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') - | Bound j => if i = j then error "make_inst" else t - | _ => t + if incr_boundvars i u aconv t then Bound i + else + case t of + t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2 + | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t fun make_inst lhs t = -let - val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; - val _ $ (Abs (_, _, (_ $ g))) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end + let + val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; + val _ $ (Abs (_, _, (_ $ g))) = t; + in + (f, Abs ("x", T, mk_abs u 0 g)) + end fun make_inst_id lhs t = -let - val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; - val _ $ (Abs (_, _, g)) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end + let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; + in + (f, Abs ("x", T, mk_abs u 0 g)) + end (* Simplifies a redex using the 'lambda_prs' theorem. First instantiates the types and known subterms. @@ -476,7 +475,7 @@ make_inst_id is used *) fun lambda_prs_simple_conv ctxt ctrm = - case (term_of ctrm) of + (case term_of ctrm of (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) => let val thy = ProofContext.theory_of ctxt @@ -495,7 +494,7 @@ in Conv.rewr_conv thm4 ctrm end - | _ => Conv.all_conv ctrm + | _ => Conv.all_conv ctrm) fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) @@ -523,25 +522,27 @@ 4. test for refl *) fun clean_tac lthy = -let - val defs = map (Thm.symmetric o #def) (qconsts_dest lthy) - val prs = prs_rules_get lthy - val ids = id_simps_get lthy - val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs + let + val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy) + val prs = Quotient_Info.prs_rules_get lthy + val ids = Quotient_Info.id_simps_get lthy + val thms = + @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs - val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver -in - EVERY' [map_fun_tac lthy, - lambda_prs_tac lthy, - simp_tac ss, - TRY o rtac refl] -end + val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver + in + EVERY' [ + map_fun_tac lthy, + lambda_prs_tac lthy, + simp_tac ss, + TRY o rtac refl] + end (* Tactic for Generalising Free Variables in a Goal *) fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms) @@ -588,31 +589,31 @@ by (simp add: Quot_True_def)} fun lift_match_error ctxt msg rtrm qtrm = -let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, - "", "does not match with original theorem", rtrm_str] -in - error msg -end + let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, + "", "does not match with original theorem", rtrm_str] + in + error msg + end fun procedure_inst ctxt rtrm qtrm = -let - val thy = ProofContext.theory_of ctxt - val rtrm' = HOLogic.dest_Trueprop rtrm - val qtrm' = HOLogic.dest_Trueprop qtrm - val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') - handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm - val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') - handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm -in - Drule.instantiate' [] - [SOME (cterm_of thy rtrm'), - SOME (cterm_of thy reg_goal), - NONE, - SOME (cterm_of thy inj_goal)] lifting_procedure_thm -end + let + val thy = ProofContext.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm') + handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm + val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm') + handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm + in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + NONE, + SOME (cterm_of thy inj_goal)] lifting_procedure_thm + end (* Since we use Ball and Bex during the lifting and descending, @@ -625,34 +626,34 @@ (** descending as tactic **) fun descend_procedure_tac ctxt simps = -let - val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds) -in - full_simp_tac ss - THEN' Object_Logic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' SUBGOAL (fn (goal, i) => - let - val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) - val rtrm = derive_rtrm ctxt qtys goal - val rule = procedure_inst ctxt rtrm goal - in - rtac rule i - end) -end + let + val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds) + in + full_simp_tac ss + THEN' Object_Logic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' SUBGOAL (fn (goal, i) => + let + val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) + val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal + val rule = procedure_inst ctxt rtrm goal + in + rtac rule i + end) + end fun descend_tac ctxt simps = -let - val mk_tac_raw = - descend_procedure_tac ctxt simps - THEN' RANGE - [Object_Logic.rulify_tac THEN' (K all_tac), - regularize_tac ctxt, - all_injection_tac ctxt, - clean_tac ctxt] -in - Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw -end + let + val mk_tac_raw = + descend_procedure_tac ctxt simps + THEN' RANGE + [Object_Logic.rulify_tac THEN' (K all_tac), + regularize_tac ctxt, + all_injection_tac ctxt, + clean_tac ctxt] + in + Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw + end (** lifting as a tactic **) @@ -660,29 +661,29 @@ (* the tactic leaves three subgoals to be proved *) fun lift_procedure_tac ctxt simps rthm = -let - val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds) -in - full_simp_tac ss - THEN' Object_Logic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' SUBGOAL (fn (goal, i) => - let - (* full_atomize_tac contracts eta redexes, - so we do it also in the original theorem *) - val rthm' = - rthm |> full_simplify ss - |> Drule.eta_contraction_rule - |> Thm.forall_intr_frees - |> atomize_thm + let + val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds) + in + full_simp_tac ss + THEN' Object_Logic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' SUBGOAL (fn (goal, i) => + let + (* full_atomize_tac contracts eta redexes, + so we do it also in the original theorem *) + val rthm' = + rthm |> full_simplify ss + |> Drule.eta_contraction_rule + |> Thm.forall_intr_frees + |> atomize_thm - val rule = procedure_inst ctxt (prop_of rthm') goal - in - (rtac rule THEN' rtac rthm') i - end) -end + val rule = procedure_inst ctxt (prop_of rthm') goal + in + (rtac rule THEN' rtac rthm') i + end) + end -fun lift_single_tac ctxt simps rthm = +fun lift_single_tac ctxt simps rthm = lift_procedure_tac ctxt simps rthm THEN' RANGE [ regularize_tac ctxt, @@ -690,26 +691,26 @@ clean_tac ctxt ] fun lift_tac ctxt simps rthms = - Goal.conjunction_tac + Goal.conjunction_tac THEN' RANGE (map (lift_single_tac ctxt simps) rthms) (* automated lifting with pre-simplification of the theorems; for internal usage *) fun lifted ctxt qtys simps rthm = -let - val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt - val goal = derive_qtrm ctxt' qtys (prop_of rthm') -in - Goal.prove ctxt' [] [] goal - (K (HEADGOAL (lift_single_tac ctxt' simps rthm'))) - |> singleton (ProofContext.export ctxt' ctxt) -end + let + val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt + val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm') + in + Goal.prove ctxt' [] [] goal + (K (HEADGOAL (lift_single_tac ctxt' simps rthm'))) + |> singleton (ProofContext.export ctxt' ctxt) + end (* lifting as an attribute *) -val lifted_attrib = Thm.rule_attribute (fn context => +val lifted_attrib = Thm.rule_attribute (fn context => let val ctxt = Context.proof_of context val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt) diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 23:46:06 2011 +0100 @@ -35,8 +35,6 @@ structure Quotient_Term: QUOTIENT_TERM = struct -open Quotient_Info; - exception LIFT_MATCH of string @@ -65,13 +63,13 @@ | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 fun get_mapfun ctxt s = -let - val thy = ProofContext.theory_of ctxt - val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => - raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") -in - Const (mapfun, dummyT) -end + let + val thy = ProofContext.theory_of ctxt + val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") + in + Const (mapfun, dummyT) + end (* makes a Free out of a TVar *) fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) @@ -85,74 +83,74 @@ it produces: %a b. prod_map (map a) b *) fun mk_mapfun ctxt vs rty = -let - val vs' = map mk_Free vs + let + val vs' = map mk_Free vs - fun mk_mapfun_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => mk_identity rty - | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) - | _ => raise LIFT_MATCH "mk_mapfun (default)" -in - fold_rev Term.lambda vs' (mk_mapfun_aux rty) -end + fun mk_mapfun_aux rty = + case rty of + TVar _ => mk_Free rty + | Type (_, []) => mk_identity rty + | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) + | _ => raise LIFT_MATCH "mk_mapfun (default)" + in + fold_rev Term.lambda vs' (mk_mapfun_aux rty) + end (* looks up the (varified) rty and qty for a quotient definition *) fun get_rty_qty ctxt s = -let - val thy = ProofContext.theory_of ctxt - val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => - raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") -in - (#rtyp qdata, #qtyp qdata) -end + let + val thy = ProofContext.theory_of ctxt + val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound => + raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") + in + (#rtyp qdata, #qtyp qdata) + end (* takes two type-environments and looks up in both of them the variable v, which must be listed in the environment *) fun double_lookup rtyenv qtyenv v = -let - val v' = fst (dest_TVar v) -in - (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) -end + let + val v' = fst (dest_TVar v) + in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) + end (* matches a type pattern with a type *) fun match ctxt err ty_pat ty = -let - val thy = ProofContext.theory_of ctxt -in - Sign.typ_match thy (ty_pat, ty) Vartab.empty - handle Type.TYPE_MATCH => err ctxt ty_pat ty -end + let + val thy = ProofContext.theory_of ctxt + in + Sign.typ_match thy (ty_pat, ty) Vartab.empty + handle Type.TYPE_MATCH => err ctxt ty_pat ty + end (* produces the rep or abs constant for a qty *) fun absrep_const flag ctxt qty_str = -let - val qty_name = Long_Name.base_name qty_str - val qualifier = Long_Name.qualifier qty_str -in - case flag of - AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT) - | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT) -end + let + val qty_name = Long_Name.base_name qty_str + val qualifier = Long_Name.qualifier qty_str + in + case flag of + AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT) + | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT) + end (* Lets Nitpick represent elements of quotient types as elements of the raw type *) fun absrep_const_chk flag ctxt qty_str = Syntax.check_term ctxt (absrep_const flag ctxt qty_str) fun absrep_match_err ctxt ty_pat ty = -let - val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty -in - raise LIFT_MATCH (space_implode " " - ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) -end + let + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat + val ty_str = Syntax.string_of_typ ctxt ty + in + raise LIFT_MATCH (space_implode " " + ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) + end (** generation of an aggregate absrep function **) @@ -213,29 +211,29 @@ | (Type (s, tys), Type (s', tys')) => if s = s' then - let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') - in - list_comb (get_mapfun ctxt s, args) - end + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + in + list_comb (get_mapfun ctxt s, args) + end else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt absrep_match_err rty_pat rty - val qtyenv = match ctxt absrep_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (absrep_fun flag ctxt) args_aux - in - if forall is_identity args - then absrep_const flag ctxt s' - else - let - val map_fun = mk_mapfun ctxt vs rty_pat - val result = list_comb (map_fun, args) - in - mk_fun_compose flag (absrep_const flag ctxt s', result) - end - end + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt absrep_match_err rty_pat rty + val qtyenv = match ctxt absrep_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (absrep_fun flag ctxt) args_aux + in + if forall is_identity args + then absrep_const flag ctxt s' + else + let + val map_fun = mk_mapfun ctxt vs rty_pat + val result = list_comb (map_fun, args) + in + mk_fun_compose flag (absrep_const flag ctxt s', result) + end + end | (TFree x, TFree x') => if x = x' then mk_identity rty @@ -259,13 +257,13 @@ (* instantiates TVars so that the term is of type ty *) fun force_typ ctxt trm ty = -let - val thy = ProofContext.theory_of ctxt - val trm_ty = fastype_of trm - val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty -in - map_types (Envir.subst_type ty_inst) trm -end + let + val thy = ProofContext.theory_of ctxt + val trm_ty = fastype_of trm + val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty + in + map_types (Envir.subst_type ty_inst) trm + end fun is_eq (Const (@{const_name HOL.eq}, _)) = true | is_eq _ = false @@ -274,44 +272,44 @@ Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 fun get_relmap ctxt s = -let - val thy = ProofContext.theory_of ctxt - val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => - raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") -in - Const (relmap, dummyT) -end + let + val thy = ProofContext.theory_of ctxt + val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") + in + Const (relmap, dummyT) + end fun mk_relmap ctxt vs rty = -let - val vs' = map (mk_Free) vs + let + val vs' = map (mk_Free) vs - fun mk_relmap_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => HOLogic.eq_const rty - | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) - | _ => raise LIFT_MATCH ("mk_relmap (default)") -in - fold_rev Term.lambda vs' (mk_relmap_aux rty) -end + fun mk_relmap_aux rty = + case rty of + TVar _ => mk_Free rty + | Type (_, []) => HOLogic.eq_const rty + | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) + | _ => raise LIFT_MATCH ("mk_relmap (default)") + in + fold_rev Term.lambda vs' (mk_relmap_aux rty) + end fun get_equiv_rel ctxt s = -let - val thy = ProofContext.theory_of ctxt -in - #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => - raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") -end + let + val thy = ProofContext.theory_of ctxt + in + #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound => + raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") + end fun equiv_match_err ctxt ty_pat ty = -let - val ty_pat_str = Syntax.string_of_typ ctxt ty_pat - val ty_str = Syntax.string_of_typ ctxt ty -in - raise LIFT_MATCH (space_implode " " - ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) -end + let + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat + val ty_str = Syntax.string_of_typ ctxt ty + in + raise LIFT_MATCH (space_implode " " + ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) + end (* builds the aggregate equivalence relation that will be the argument of Respects @@ -322,34 +320,34 @@ else case (rty, qty) of (Type (s, tys), Type (s', tys')) => - if s = s' - then - let - val args = map (equiv_relation ctxt) (tys ~~ tys') - in - list_comb (get_relmap ctxt s, args) - end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt equiv_match_err rty_pat rty - val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (equiv_relation ctxt) args_aux - val eqv_rel = get_equiv_rel ctxt s' - val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) - in - if forall is_eq args - then eqv_rel' - else - let - val rel_map = mk_relmap ctxt vs rty_pat - val result = list_comb (rel_map, args) - in - mk_rel_compose (result, eqv_rel') - end - end - | _ => HOLogic.eq_const rty + if s = s' + then + let + val args = map (equiv_relation ctxt) (tys ~~ tys') + in + list_comb (get_relmap ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt equiv_match_err rty_pat rty + val qtyenv = match ctxt equiv_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (equiv_relation ctxt) args_aux + val eqv_rel = get_equiv_rel ctxt s' + val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) + in + if forall is_eq args + then eqv_rel' + else + let + val rel_map = mk_relmap ctxt vs rty_pat + val result = list_comb (rel_map, args) + in + mk_rel_compose (result, eqv_rel') + end + end + | _ => HOLogic.eq_const rty fun equiv_relation_chk ctxt (rty, qty) = equiv_relation ctxt (rty, qty) @@ -414,14 +412,14 @@ | _ => f (trm1, trm2) fun term_mismatch str ctxt t1 t2 = -let - val t1_str = Syntax.string_of_term ctxt t1 - val t2_str = Syntax.string_of_term ctxt t2 - val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) - val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) -in - raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) -end + let + val t1_str = Syntax.string_of_term ctxt t1 + val t2_str = Syntax.string_of_term ctxt t2 + val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) + val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) + in + raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) + end (* the major type of All and Ex quantifiers *) fun qnt_typ ty = domain_type (domain_type ty) @@ -429,17 +427,18 @@ (* Checks that two types match, for example: rty -> rty matches qty -> qty *) fun matches_typ thy rT qT = - if rT = qT then true else - case (rT, qT) of - (Type (rs, rtys), Type (qs, qtys)) => - if rs = qs then - if length rtys <> length qtys then false else - forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) - else - (case quotdata_lookup_raw thy qs of - SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) - | NONE => false) - | _ => false + if rT = qT then true + else + (case (rT, qT) of + (Type (rs, rtys), Type (qs, qtys)) => + if rs = qs then + if length rtys <> length qtys then false + else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) + else + (case Quotient_Info.quotdata_lookup_raw thy qs of + SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) + | NONE => false) + | _ => false) (* produces a regularized version of rtrm @@ -452,124 +451,124 @@ fun regularize_trm ctxt (rtrm, qtrm) = case (rtrm, qtrm) of (Abs (x, ty, t), Abs (_, ty', t')) => - let - val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) - in - if ty = ty' then subtrm - else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm - end + let + val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) + in + if ty = ty' then subtrm + else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm + end | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => - let - val subtrm = regularize_trm ctxt (t, t') - val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') - in - if resrel <> needres - then term_mismatch "regularize (Babs)" ctxt resrel needres - else mk_babs $ resrel $ subtrm - end + let + val subtrm = regularize_trm ctxt (t, t') + val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') + in + if resrel <> needres + then term_mismatch "regularize (Babs)" ctxt resrel needres + else mk_babs $ resrel $ subtrm + end | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name All}, ty) $ subtrm - else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name All}, ty) $ subtrm + else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm - else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm + else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end | (Const (@{const_name Ex1}, ty) $ (Abs (_, _, (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $ (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), Const (@{const_name Ex1}, ty') $ t') => - let - val t_ = incr_boundvars (~1) t - val subtrm = apply_subt (regularize_trm ctxt) (t_, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex1)" ctxt resrel needrel - else mk_bex1_rel $ resrel $ subtrm - end + let + val t_ = incr_boundvars (~1) t + val subtrm = apply_subt (regularize_trm ctxt) (t_, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex1)" ctxt resrel needrel + else mk_bex1_rel $ resrel $ subtrm + end | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - in - if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm - else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm + else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, Const (@{const_name All}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Ball)" ctxt resrel needrel - else mk_ball $ (mk_resp $ resrel) $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Ball)" ctxt resrel needrel + else mk_ball $ (mk_resp $ resrel) $ subtrm + end | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, Const (@{const_name Ex}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex)" ctxt resrel needrel - else mk_bex $ (mk_resp $ resrel) $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex)" ctxt resrel needrel + else mk_bex $ (mk_resp $ resrel) $ subtrm + end | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm ctxt) (t, t') - val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') - in - if resrel <> needrel - then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel - else mk_bex1_rel $ resrel $ subtrm - end + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel + else mk_bex1_rel $ resrel $ subtrm + end | (* equalities need to be replaced by appropriate equivalence relations *) (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) => - if ty = ty' then rtrm - else equiv_relation ctxt (domain_type ty, domain_type ty') + if ty = ty' then rtrm + else equiv_relation ctxt (domain_type ty, domain_type ty') | (* in this case we just check whether the given equivalence relation is correct *) (rel, Const (@{const_name HOL.eq}, ty')) => - let - val rel_ty = fastype_of rel - val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') - in - if rel' aconv rel then rtrm - else term_mismatch "regularize (relation mismatch)" ctxt rel rel' - end + let + val rel_ty = fastype_of rel + val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') + in + if rel' aconv rel then rtrm + else term_mismatch "regularize (relation mismatch)" ctxt rel rel' + end | (_, Const _) => - let - val thy = ProofContext.theory_of ctxt - fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' - | same_const _ _ = false - in - if same_const rtrm qtrm then rtrm - else - let - val rtrm' = #rconst (qconsts_lookup thy qtrm) - handle Quotient_Info.NotFound => + let + val thy = ProofContext.theory_of ctxt + fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' + | same_const _ _ = false + in + if same_const rtrm qtrm then rtrm + else + let + val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm) + handle Quotient_Info.NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm - in - if Pattern.matches thy (rtrm', rtrm) - then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm - end - end + in + if Pattern.matches thy (rtrm', rtrm) + then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm + end + end | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => @@ -583,16 +582,16 @@ regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') | (Bound i, Bound i') => - if i = i' then rtrm - else raise (LIFT_MATCH "regularize (bounds mismatch)") + if i = i' then rtrm + else raise (LIFT_MATCH "regularize (bounds mismatch)") | _ => - let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm - in - raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) - end + let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + in + raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) + end fun regularize_trm_chk ctxt (rtrm, qtrm) = regularize_trm ctxt (rtrm, qtrm) @@ -635,12 +634,12 @@ absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) fun inj_repabs_err ctxt msg rtrm qtrm = -let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm -in - raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) -end + let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + in + raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) + end (* bound variables need to be treated properly, @@ -717,8 +716,8 @@ NONE => matches tail | SOME inst => Envir.subst_type inst qty in - matches ty_subst - end + matches ty_subst + end | _ => rty fun subst_trm ctxt ty_subst trm_subst rtrm = @@ -728,7 +727,7 @@ | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty) | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty) | Bound i => Bound i - | Const (a, ty) => + | Const (a, ty) => let val thy = ProofContext.theory_of ctxt @@ -742,43 +741,43 @@ end (* generate type and term substitutions out of the - qtypes involved in a quotient; the direction flag - indicates in which direction the substitutions work: - + qtypes involved in a quotient; the direction flag + indicates in which direction the substitutions work: + true: quotient -> raw false: raw -> quotient *) fun mk_ty_subst qtys direction ctxt = -let - val thy = ProofContext.theory_of ctxt -in - quotdata_dest ctxt - |> map (fn x => (#rtyp x, #qtyp x)) - |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) - |> map (if direction then swap else I) -end + let + val thy = ProofContext.theory_of ctxt + in + Quotient_Info.quotdata_dest ctxt + |> map (fn x => (#rtyp x, #qtyp x)) + |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) + |> map (if direction then swap else I) + end fun mk_trm_subst qtys direction ctxt = -let - val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) - fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 + let + val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) + fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 - val const_substs = - qconsts_dest ctxt - |> map (fn x => (#rconst x, #qconst x)) - |> map (if direction then swap else I) + val const_substs = + Quotient_Info.qconsts_dest ctxt + |> map (fn x => (#rconst x, #qconst x)) + |> map (if direction then swap else I) - val rel_substs = - quotdata_dest ctxt - |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) - |> map (if direction then swap else I) -in - filter proper (const_substs @ rel_substs) -end + val rel_substs = + Quotient_Info.quotdata_dest ctxt + |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) + |> map (if direction then swap else I) + in + filter proper (const_substs @ rel_substs) + end (* derives a qtyp and qtrm out of a rtyp and rtrm, - respectively + respectively *) fun derive_qtyp ctxt qtys rty = subst_typ ctxt (mk_ty_subst qtys false ctxt) rty @@ -787,7 +786,7 @@ subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm (* derives a rtyp and rtrm out of a qtyp and qtrm, - respectively + respectively *) fun derive_rtyp ctxt qtys qty = subst_typ ctxt (mk_ty_subst qtys true ctxt) qty diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 23:46:06 2011 +0100 @@ -20,16 +20,15 @@ structure Quotient_Type: QUOTIENT_TYPE = struct -open Quotient_Info; +(* wrappers for define, note, Attrib.internal and theorem_i *) (* FIXME !? *) -(* wrappers for define, note, Attrib.internal and theorem_i *) fun define (name, mx, rhs) lthy = -let - val ((rhs, (_ , thm)), lthy') = - Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy -in - ((rhs, thm), lthy') -end + let + val ((rhs, (_ , thm)), lthy') = + Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy + in + ((rhs, thm), lthy') + end fun note (name, thm, attrs) lthy = Local_Theory.note ((name, attrs), [thm]) lthy |> snd @@ -38,12 +37,12 @@ fun intern_attr at = Attrib.internal (K at) fun theorem after_qed goals ctxt = -let - val goals' = map (rpair []) goals - fun after_qed' thms = after_qed (the_single thms) -in - Proof.theorem NONE after_qed' [goals'] ctxt -end + let + val goals' = map (rpair []) goals + fun after_qed' thms = after_qed (the_single thms) + in + Proof.theorem NONE after_qed' [goals'] ctxt + end @@ -54,178 +53,182 @@ (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) fun typedef_term rel rty lthy = -let - val [x, c] = - [("x", rty), ("c", HOLogic.mk_setT rty)] - |> Variable.variant_frees lthy [rel] - |> map Free -in - lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) -end + let + val [x, c] = + [("x", rty), ("c", HOLogic.mk_setT rty)] + |> Variable.variant_frees lthy [rel] + |> map Free + in + lambda c (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) + end (* makes the new type definitions and proves non-emptyness *) fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = -let - val typedef_tac = - EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) -in -(* FIXME: purely local typedef causes at the moment - problems with type variables - - Typedef.add_typedef false NONE (qty_name, vs, mx) - (typedef_term rel rty lthy) NONE typedef_tac lthy -*) -(* FIXME should really use local typedef here *) - Local_Theory.background_theory_result + let + val typedef_tac = + EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) + in + (* FIXME: purely local typedef causes at the moment + problems with type variables + + Typedef.add_typedef false NONE (qty_name, vs, mx) + (typedef_term rel rty lthy) NONE typedef_tac lthy + *) + (* FIXME should really use local typedef here *) + Local_Theory.background_theory_result (Typedef.add_typedef_global false NONE (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac) lthy -end + end (* tactic to prove the quot_type theorem for the new type *) fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) = -let - val rep_thm = #Rep typedef_info RS mem_def1 - val rep_inv = #Rep_inverse typedef_info - val abs_inv = #Abs_inverse typedef_info - val rep_inj = #Rep_inject typedef_info -in - (rtac @{thm quot_type.intro} THEN' RANGE [ - rtac equiv_thm, - rtac rep_thm, - rtac rep_inv, - rtac abs_inv THEN' rtac mem_def2 THEN' atac, - rtac rep_inj]) 1 -end + let + val rep_thm = #Rep typedef_info RS mem_def1 + val rep_inv = #Rep_inverse typedef_info + val abs_inv = #Abs_inverse typedef_info + val rep_inj = #Rep_inject typedef_info + in + (rtac @{thm quot_type.intro} THEN' RANGE [ + rtac equiv_thm, + rtac rep_thm, + rtac rep_inv, + rtac abs_inv THEN' rtac mem_def2 THEN' atac, + rtac rep_inj]) 1 + end (* proves the quot_type theorem for the new type *) fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = -let - val quot_type_const = Const (@{const_name "quot_type"}, dummyT) - val goal = - HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) - |> Syntax.check_term lthy -in - Goal.prove lthy [] [] goal - (K (typedef_quot_type_tac equiv_thm typedef_info)) -end + let + val quot_type_const = Const (@{const_name "quot_type"}, dummyT) + val goal = + HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) + |> Syntax.check_term lthy + in + Goal.prove lthy [] [] goal + (K (typedef_quot_type_tac equiv_thm typedef_info)) + end (* main function for constructing a quotient type *) fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = -let - val part_equiv = - if partial - then equiv_thm - else equiv_thm RS @{thm equivp_implies_part_equivp} + let + val part_equiv = + if partial + then equiv_thm + else equiv_thm RS @{thm equivp_implies_part_equivp} - (* generates the typedef *) - val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy + (* generates the typedef *) + val ((qty_full_name, typedef_info), lthy1) = + typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy - (* abs and rep functions from the typedef *) - val Abs_ty = #abs_type (#1 typedef_info) - val Rep_ty = #rep_type (#1 typedef_info) - val Abs_name = #Abs_name (#1 typedef_info) - val Rep_name = #Rep_name (#1 typedef_info) - val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) - val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) + (* abs and rep functions from the typedef *) + val Abs_ty = #abs_type (#1 typedef_info) + val Rep_ty = #rep_type (#1 typedef_info) + val Abs_name = #Abs_name (#1 typedef_info) + val Rep_name = #Rep_name (#1 typedef_info) + val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) + val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) - (* more useful abs and rep definitions *) - val abs_const = Const (@{const_name "quot_type.abs"}, dummyT ) - val rep_const = Const (@{const_name "quot_type.rep"}, dummyT ) - val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) - val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) - val abs_name = Binding.prefix_name "abs_" qty_name - val rep_name = Binding.prefix_name "rep_" qty_name + (* more useful abs and rep definitions *) + val abs_const = Const (@{const_name "quot_type.abs"}, dummyT ) + val rep_const = Const (@{const_name "quot_type.rep"}, dummyT ) + val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) + val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) + val abs_name = Binding.prefix_name "abs_" qty_name + val rep_name = Binding.prefix_name "rep_" qty_name - val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 - val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 + val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 + val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 - (* quot_type theorem *) - val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 + (* quot_type theorem *) + val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 - (* quotient theorem *) - val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name - val quotient_thm = - (quot_thm RS @{thm quot_type.Quotient}) - |> fold_rule [abs_def, rep_def] + (* quotient theorem *) + val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name + val quotient_thm = + (quot_thm RS @{thm quot_type.Quotient}) + |> fold_rule [abs_def, rep_def] + + (* name equivalence theorem *) + val equiv_thm_name = Binding.suffix_name "_equivp" qty_name - (* name equivalence theorem *) - val equiv_thm_name = Binding.suffix_name "_equivp" qty_name + (* storing the quotdata *) + val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} - (* storing the quotdata *) - val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} - - fun qinfo phi = transform_quotdata phi quotdata + fun qinfo phi = Quotient_Info.transform_quotdata phi quotdata - val lthy4 = lthy3 - |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) - |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) - |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) -in - (quotdata, lthy4) -end + val lthy4 = lthy3 + |> Local_Theory.declaration true + (fn phi => Quotient_Info.quotdata_update_gen qty_full_name (qinfo phi)) + |> note + (equiv_thm_name, equiv_thm, + if partial then [] else [intern_attr Quotient_Info.equiv_rules_add]) + |> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add]) + in + (quotdata, lthy4) + end (* sanity checks for the quotient type specifications *) fun sanity_check ((vs, qty_name, _), (rty, rel, _)) = -let - val rty_tfreesT = map fst (Term.add_tfreesT rty []) - val rel_tfrees = map fst (Term.add_tfrees rel []) - val rel_frees = map fst (Term.add_frees rel []) - val rel_vars = Term.add_vars rel [] - val rel_tvars = Term.add_tvars rel [] - val qty_str = Binding.str_of qty_name ^ ": " + let + val rty_tfreesT = map fst (Term.add_tfreesT rty []) + val rel_tfrees = map fst (Term.add_tfrees rel []) + val rel_frees = map fst (Term.add_frees rel []) + val rel_vars = Term.add_vars rel [] + val rel_tvars = Term.add_tvars rel [] + val qty_str = Binding.str_of qty_name ^ ": " - val illegal_rel_vars = - if null rel_vars andalso null rel_tvars then [] - else [qty_str ^ "illegal schematic variable(s) in the relation."] + val illegal_rel_vars = + if null rel_vars andalso null rel_tvars then [] + else [qty_str ^ "illegal schematic variable(s) in the relation."] - val dup_vs = - (case duplicates (op =) vs of - [] => [] - | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) + val dup_vs = + (case duplicates (op =) vs of + [] => [] + | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) - val extra_rty_tfrees = - (case subtract (op =) vs rty_tfreesT of - [] => [] - | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) + val extra_rty_tfrees = + (case subtract (op =) vs rty_tfreesT of + [] => [] + | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) - val extra_rel_tfrees = - (case subtract (op =) vs rel_tfrees of - [] => [] - | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) + val extra_rel_tfrees = + (case subtract (op =) vs rel_tfrees of + [] => [] + | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) - val illegal_rel_frees = - (case rel_frees of - [] => [] - | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) + val illegal_rel_frees = + (case rel_frees of + [] => [] + | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) - val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees -in - if null errs then () else error (cat_lines errs) -end + val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees + in + if null errs then () else error (cat_lines errs) + end (* check for existence of map functions *) fun map_check ctxt (_, (rty, _, _)) = -let - val thy = ProofContext.theory_of ctxt + let + val thy = ProofContext.theory_of ctxt - fun map_check_aux rty warns = - case rty of - Type (_, []) => warns - | Type (s, _) => if maps_defined thy s then warns else s::warns - | _ => warns + fun map_check_aux rty warns = + case rty of + Type (_, []) => warns + | Type (s, _) => if Quotient_Info.maps_defined thy s then warns else s::warns + | _ => warns - val warns = map_check_aux rty [] -in - if null warns then () - else warning ("No map function defined for " ^ commas warns ^ - ". This will cause problems later on.") -end + val warns = map_check_aux rty [] + in + if null warns then () + else warning ("No map function defined for " ^ commas warns ^ + ". This will cause problems later on.") + end @@ -246,48 +249,48 @@ *) fun quotient_type quot_list lthy = -let - (* sanity check *) - val _ = List.app sanity_check quot_list - val _ = List.app (map_check lthy) quot_list + let + (* sanity check *) + val _ = List.app sanity_check quot_list + val _ = List.app (map_check lthy) quot_list - fun mk_goal (rty, rel, partial) = - let - val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} - val const = - if partial then @{const_name part_equivp} else @{const_name equivp} + fun mk_goal (rty, rel, partial) = + let + val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} + val const = + if partial then @{const_name part_equivp} else @{const_name equivp} + in + HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) + end + + val goals = map (mk_goal o snd) quot_list + + fun after_qed thms lthy = + fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd in - HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) + theorem after_qed goals lthy end - val goals = map (mk_goal o snd) quot_list - - fun after_qed thms lthy = - fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd -in - theorem after_qed goals lthy -end - fun quotient_type_cmd specs lthy = -let - fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy = let - val rty = Syntax.read_typ lthy rty_str - val lthy1 = Variable.declare_typ rty lthy - val rel = - Syntax.parse_term lthy1 rel_str - |> Type.constraint (rty --> rty --> @{typ bool}) - |> Syntax.check_term lthy1 - val lthy2 = Variable.declare_term rel lthy1 + fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy = + let + val rty = Syntax.read_typ lthy rty_str + val lthy1 = Variable.declare_typ rty lthy + val rel = + Syntax.parse_term lthy1 rel_str + |> Type.constraint (rty --> rty --> @{typ bool}) + |> Syntax.check_term lthy1 + val lthy2 = Variable.declare_term rel lthy1 + in + (((vs, qty_name, mx), (rty, rel, partial)), lthy2) + end + + val (spec', lthy') = fold_map parse_spec specs lthy in - (((vs, qty_name, mx), (rty, rel, partial)), lthy2) + quotient_type spec' lthy' end - val (spec', lthy') = fold_map parse_spec specs lthy -in - quotient_type spec' lthy' -end - val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false val quotspec_parser = @@ -299,8 +302,8 @@ val _ = Keyword.keyword "/" val _ = - Outer_Syntax.local_theory_to_proof "quotient_type" - "quotient type definitions (require equivalence proofs)" - Keyword.thy_goal (quotspec_parser >> quotient_type_cmd) + Outer_Syntax.local_theory_to_proof "quotient_type" + "quotient type definitions (require equivalence proofs)" + Keyword.thy_goal (quotspec_parser >> quotient_type_cmd) end; (* structure *) diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Fri Jan 07 23:46:06 2011 +0100 @@ -34,20 +34,20 @@ signature CNF = sig - val is_atom: term -> bool - val is_literal: term -> bool - val is_clause: term -> bool - val clause_is_trivial: term -> bool + val is_atom: term -> bool + val is_literal: term -> bool + val is_clause: term -> bool + val clause_is_trivial: term -> bool - val clause2raw_thm: thm -> thm + val clause2raw_thm: thm -> thm - val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) + val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) - val make_cnf_thm: theory -> term -> thm - val make_cnfx_thm: theory -> term -> thm - val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *) - val cnfx_rewrite_tac: Proof.context -> int -> tactic - (* converts all prems of a subgoal to (almost) definitional CNF *) + val make_cnf_thm: theory -> term -> thm + val make_cnfx_thm: theory -> term -> thm + val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *) + val cnfx_rewrite_tac: Proof.context -> int -> tactic + (* converts all prems of a subgoal to (almost) definitional CNF *) end; structure cnf : CNF = @@ -93,39 +93,35 @@ val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto}; -fun is_atom (Const (@{const_name False}, _)) = false - | is_atom (Const (@{const_name True}, _)) = false - | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false - | is_atom (Const (@{const_name Not}, _) $ _) = false - | is_atom _ = true; +fun is_atom (Const (@{const_name False}, _)) = false + | is_atom (Const (@{const_name True}, _)) = false + | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false + | is_atom (Const (@{const_name Not}, _) $ _) = false + | is_atom _ = true; fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x - | is_literal x = is_atom x; + | is_literal x = is_atom x; fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y - | is_clause x = is_literal x; + | is_clause x = is_literal x; (* ------------------------------------------------------------------------- *) (* clause_is_trivial: a clause is trivially true if it contains both an atom *) (* and the atom's negation *) (* ------------------------------------------------------------------------- *) -(* Term.term -> bool *) - fun clause_is_trivial c = - let - (* Term.term -> Term.term *) - fun dual (Const (@{const_name Not}, _) $ x) = x - | dual x = HOLogic.Not $ x - (* Term.term list -> bool *) - fun has_duals [] = false - | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs - in - has_duals (HOLogic.disjuncts c) - end; + let + fun dual (Const (@{const_name Not}, _) $ x) = x + | dual x = HOLogic.Not $ x + fun has_duals [] = false + | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs + in + has_duals (HOLogic.disjuncts c) + end; (* ------------------------------------------------------------------------- *) (* clause2raw_thm: translates a clause into a raw clause, i.e. *) @@ -135,41 +131,39 @@ (* where each xi' is the negation normal form of ~xi *) (* ------------------------------------------------------------------------- *) -(* Thm.thm -> Thm.thm *) - fun clause2raw_thm clause = -let - (* eliminates negated disjunctions from the i-th premise, possibly *) - (* adding new premises, then continues with the (i+1)-th premise *) - (* int -> Thm.thm -> Thm.thm *) - fun not_disj_to_prem i thm = - if i > nprems_of thm then - thm - else - not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) - (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) - (* becomes "[..., A1, ..., An] |- B" *) - (* Thm.thm -> Thm.thm *) - fun prems_to_hyps thm = - fold (fn cprem => fn thm' => - Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm -in - (* [...] |- ~(x1 | ... | xn) ==> False *) - (clause2raw_notE OF [clause]) - (* [...] |- ~x1 ==> ... ==> ~xn ==> False *) - |> not_disj_to_prem 1 - (* [...] |- x1' ==> ... ==> xn' ==> False *) - |> Seq.hd o TRYALL (rtac clause2raw_not_not) - (* [..., x1', ..., xn'] |- False *) - |> prems_to_hyps -end; + let + (* eliminates negated disjunctions from the i-th premise, possibly *) + (* adding new premises, then continues with the (i+1)-th premise *) + (* int -> Thm.thm -> Thm.thm *) + fun not_disj_to_prem i thm = + if i > nprems_of thm then + thm + else + not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) + (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) + (* becomes "[..., A1, ..., An] |- B" *) + (* Thm.thm -> Thm.thm *) + fun prems_to_hyps thm = + fold (fn cprem => fn thm' => + Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm + in + (* [...] |- ~(x1 | ... | xn) ==> False *) + (clause2raw_notE OF [clause]) + (* [...] |- ~x1 ==> ... ==> ~xn ==> False *) + |> not_disj_to_prem 1 + (* [...] |- x1' ==> ... ==> xn' ==> False *) + |> Seq.hd o TRYALL (rtac clause2raw_not_not) + (* [..., x1', ..., xn'] |- False *) + |> prems_to_hyps + end; (* ------------------------------------------------------------------------- *) (* inst_thm: instantiates a theorem with a list of terms *) (* ------------------------------------------------------------------------- *) fun inst_thm thy ts thm = - instantiate' [] (map (SOME o cterm_of thy) ts) thm; + instantiate' [] (map (SOME o cterm_of thy) ts) thm; (* ------------------------------------------------------------------------- *) (* Naive CNF transformation *) @@ -182,80 +176,81 @@ (* eliminated (possibly causing an exponential blowup) *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy y - in - conj_cong OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy y + in + conj_cong OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy y - in - disj_cong OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy y + in + disj_cong OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy y - in - make_nnf_imp OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy y + in + make_nnf_imp OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ x) - val thm3 = make_nnf_thm thy y - val thm4 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_iff OF [thm1, thm2, thm3, thm4] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ x) + val thm3 = make_nnf_thm thy y + val thm4 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_iff OF [thm1, thm2, thm3, thm4] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) = - make_nnf_not_false + make_nnf_not_false | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) = - make_nnf_not_true + make_nnf_not_true | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_conj OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_conj OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_disj OF [thm1, thm2] - end - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_imp OF [thm1, thm2] - end - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ x) - val thm3 = make_nnf_thm thy y - val thm4 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_iff OF [thm1, thm2, thm3, thm4] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_disj OF [thm1, thm2] + end + | make_nnf_thm thy + (Const (@{const_name Not}, _) $ + (Const (@{const_name HOL.implies}, _) $ x $ y)) = + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_imp OF [thm1, thm2] + end + | make_nnf_thm thy + (Const (@{const_name Not}, _) $ + (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) = + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ x) + val thm3 = make_nnf_thm thy y + val thm4 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_iff OF [thm1, thm2, thm3, thm4] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) = - let - val thm1 = make_nnf_thm thy x - in - make_nnf_not_not OF [thm1] - end - | make_nnf_thm thy t = - inst_thm thy [t] iff_refl; + let + val thm1 = make_nnf_thm thy x + in + make_nnf_not_not OF [thm1] + end + | make_nnf_thm thy t = inst_thm thy [t] iff_refl; (* ------------------------------------------------------------------------- *) (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) @@ -277,51 +272,50 @@ (* Theory.theory -> Term.term -> Thm.thm *) fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = simp_True_False_thm thy x - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - in - if x' = HOLogic.false_const then - simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) - else - let - val thm2 = simp_True_False_thm thy y - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - in - if x' = HOLogic.true_const then - simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) - else if y' = HOLogic.false_const then - simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) - else if y' = HOLogic.true_const then - simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) - else - conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) - end - end + let + val thm1 = simp_True_False_thm thy x + val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + in + if x' = HOLogic.false_const then + simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) + else + let + val thm2 = simp_True_False_thm thy y + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + in + if x' = HOLogic.true_const then + simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) + else if y' = HOLogic.false_const then + simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) + else if y' = HOLogic.true_const then + simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) + else + conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) + end + end | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - val thm1 = simp_True_False_thm thy x - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - in - if x' = HOLogic.true_const then - simp_TF_disj_True_l OF [thm1] (* (x | y) = True *) - else - let - val thm2 = simp_True_False_thm thy y - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - in - if x' = HOLogic.false_const then - simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *) - else if y' = HOLogic.true_const then - simp_TF_disj_True_r OF [thm2] (* (x | y) = True *) - else if y' = HOLogic.false_const then - simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *) - else - disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - end - end - | simp_True_False_thm thy t = - inst_thm thy [t] iff_refl; (* t = t *) + let + val thm1 = simp_True_False_thm thy x + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + in + if x' = HOLogic.true_const then + simp_TF_disj_True_l OF [thm1] (* (x | y) = True *) + else + let + val thm2 = simp_True_False_thm thy y + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + in + if x' = HOLogic.false_const then + simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *) + else if y' = HOLogic.true_const then + simp_TF_disj_True_r OF [thm2] (* (x | y) = True *) + else if y' = HOLogic.false_const then + simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *) + else + disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + end + end + | simp_True_False_thm thy t = inst_thm thy [t] iff_refl; (* t = t *) (* ------------------------------------------------------------------------- *) (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) @@ -329,58 +323,54 @@ (* in the length of the term. *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_cnf_thm thy t = -let - (* Term.term -> Thm.thm *) - fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = make_cnf_thm_from_nnf x - val thm2 = make_cnf_thm_from_nnf y - in - conj_cong OF [thm1, thm2] - end - | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *) - fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = - let - val thm1 = make_cnf_disj_thm x1 y' - val thm2 = make_cnf_disj_thm x2 y' - in - make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) - end - | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = - let - val thm1 = make_cnf_disj_thm x' y1 - val thm2 = make_cnf_disj_thm x' y2 - in - make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) - end - | make_cnf_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) - val thm1 = make_cnf_thm_from_nnf x - val thm2 = make_cnf_thm_from_nnf y - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - in - iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] - end - | make_cnf_thm_from_nnf t = - inst_thm thy [t] iff_refl - (* convert 't' to NNF first *) - val nnf_thm = make_nnf_thm thy t - val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm - (* then simplify wrt. True/False (this should preserve NNF) *) - val simp_thm = simp_True_False_thm thy nnf - val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm - (* finally, convert to CNF (this should preserve the simplification) *) - val cnf_thm = make_cnf_thm_from_nnf simp -in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] -end; + let + fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = + let + val thm1 = make_cnf_thm_from_nnf x + val thm2 = make_cnf_thm_from_nnf y + in + conj_cong OF [thm1, thm2] + end + | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = + let + (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *) + fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = + let + val thm1 = make_cnf_disj_thm x1 y' + val thm2 = make_cnf_disj_thm x2 y' + in + make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) + end + | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = + let + val thm1 = make_cnf_disj_thm x' y1 + val thm2 = make_cnf_disj_thm x' y2 + in + make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) + end + | make_cnf_disj_thm x' y' = + inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + val thm1 = make_cnf_thm_from_nnf x + val thm2 = make_cnf_thm_from_nnf y + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + in + iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] + end + | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl + (* convert 't' to NNF first *) + val nnf_thm = make_nnf_thm thy t + val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm + (* then simplify wrt. True/False (this should preserve NNF) *) + val simp_thm = simp_True_False_thm thy nnf + val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm + (* finally, convert to CNF (this should preserve the simplification) *) + val cnf_thm = make_cnf_thm_from_nnf simp + in + iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] + end; (* ------------------------------------------------------------------------- *) (* CNF transformation by introducing new literals *) @@ -396,106 +386,107 @@ (* in the case of nested equivalences. *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_cnfx_thm thy t = -let - val var_id = Unsynchronized.ref 0 (* properly initialized below *) - fun new_free () = - Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) - fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = - let - val thm1 = make_cnfx_thm_from_nnf x - val thm2 = make_cnfx_thm_from_nnf y - in - conj_cong OF [thm1, thm2] - end - | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = - if is_clause x andalso is_clause y then - inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl - else if is_literal y orelse is_literal x then let - (* produces a theorem "(x' | y') = t'", where x', y', and t' are *) - (* almost in CNF, and x' or y' is a literal *) - fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = - let - val thm1 = make_cnfx_disj_thm x1 y' - val thm2 = make_cnfx_disj_thm x2 y' - in - make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) - end - | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = - let - val thm1 = make_cnfx_disj_thm x' y1 - val thm2 = make_cnfx_disj_thm x' y2 - in - make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) - end - | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' = - let - val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *) - val var = new_free () - val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) - end - | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') = - let - val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *) - val var = new_free () - val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) - end - | make_cnfx_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) - val thm1 = make_cnfx_thm_from_nnf x - val thm2 = make_cnfx_thm_from_nnf y - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - in - iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] - end else let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) - val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *) - val var = new_free () - val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) - val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] - end - | make_cnfx_thm_from_nnf t = - inst_thm thy [t] iff_refl - (* convert 't' to NNF first *) - val nnf_thm = make_nnf_thm thy t - val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm - (* then simplify wrt. True/False (this should preserve NNF) *) - val simp_thm = simp_True_False_thm thy nnf - val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm - (* initialize var_id, in case the term already contains variables of the form "cnfx_" *) - val _ = (var_id := fold (fn free => fn max => - let - val (name, _) = dest_Free free - val idx = if String.isPrefix "cnfx_" name then - (Int.fromString o String.extract) (name, String.size "cnfx_", NONE) - else - NONE - in - Int.max (max, the_default 0 idx) - end) (OldTerm.term_frees simp) 0) - (* finally, convert to definitional CNF (this should preserve the simplification) *) - val cnfx_thm = make_cnfx_thm_from_nnf simp -in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] -end; + let + val var_id = Unsynchronized.ref 0 (* properly initialized below *) + fun new_free () = + Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) + fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = + let + val thm1 = make_cnfx_thm_from_nnf x + val thm2 = make_cnfx_thm_from_nnf y + in + conj_cong OF [thm1, thm2] + end + | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = + if is_clause x andalso is_clause y then + inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl + else if is_literal y orelse is_literal x then + let + (* produces a theorem "(x' | y') = t'", where x', y', and t' are *) + (* almost in CNF, and x' or y' is a literal *) + fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = + let + val thm1 = make_cnfx_disj_thm x1 y' + val thm2 = make_cnfx_disj_thm x2 y' + in + make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) + end + | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = + let + val thm1 = make_cnfx_disj_thm x' y1 + val thm2 = make_cnfx_disj_thm x' y2 + in + make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) + end + | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' = + let + val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *) + val var = new_free () + val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) + end + | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') = + let + val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *) + val var = new_free () + val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) + end + | make_cnfx_disj_thm x' y' = + inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + val thm1 = make_cnfx_thm_from_nnf x + val thm2 = make_cnfx_thm_from_nnf y + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + in + iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] + end + else + let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) + val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *) + val var = new_free () + val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) + val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] + end + | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl + (* convert 't' to NNF first *) + val nnf_thm = make_nnf_thm thy t + val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm + (* then simplify wrt. True/False (this should preserve NNF) *) + val simp_thm = simp_True_False_thm thy nnf + val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm + (* initialize var_id, in case the term already contains variables of the form "cnfx_" *) + val _ = (var_id := fold (fn free => fn max => + let + val (name, _) = dest_Free free + val idx = + if String.isPrefix "cnfx_" name then + (Int.fromString o String.extract) (name, String.size "cnfx_", NONE) + else + NONE + in + Int.max (max, the_default 0 idx) + end) (OldTerm.term_frees simp) 0) + (* finally, convert to definitional CNF (this should preserve the simplification) *) + val cnfx_thm = make_cnfx_thm_from_nnf simp + in + iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] + end; (* ------------------------------------------------------------------------- *) (* Tactics *) @@ -506,7 +497,7 @@ (* ------------------------------------------------------------------------- *) fun weakening_tac i = - dtac weakening_thm i THEN atac (i+1); + dtac weakening_thm i THEN atac (i+1); (* ------------------------------------------------------------------------- *) (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -515,22 +506,22 @@ (* ------------------------------------------------------------------------- *) fun cnf_rewrite_tac ctxt i = - (* cut the CNF formulas as new premises *) - Subgoal.FOCUS (fn {prems, ...} => - let - val thy = ProofContext.theory_of ctxt - val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems - val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) - in - cut_facts_tac cut_thms 1 - end) ctxt i - (* remove the original premises *) - THEN SELECT_GOAL (fn thm => - let - val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) - in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm - end) i; + (* cut the CNF formulas as new premises *) + Subgoal.FOCUS (fn {prems, ...} => + let + val thy = ProofContext.theory_of ctxt + val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems + val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) + in + cut_facts_tac cut_thms 1 + end) ctxt i + (* remove the original premises *) + THEN SELECT_GOAL (fn thm => + let + val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) + in + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + end) i; (* ------------------------------------------------------------------------- *) (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -538,21 +529,21 @@ (* ------------------------------------------------------------------------- *) fun cnfx_rewrite_tac ctxt i = - (* cut the CNF formulas as new premises *) - Subgoal.FOCUS (fn {prems, ...} => - let - val thy = ProofContext.theory_of ctxt; - val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems - val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) - in - cut_facts_tac cut_thms 1 - end) ctxt i - (* remove the original premises *) - THEN SELECT_GOAL (fn thm => - let - val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) - in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm - end) i; + (* cut the CNF formulas as new premises *) + Subgoal.FOCUS (fn {prems, ...} => + let + val thy = ProofContext.theory_of ctxt; + val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems + val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) + in + cut_facts_tac cut_thms 1 + end) ctxt i + (* remove the original premises *) + THEN SELECT_GOAL (fn thm => + let + val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) + in + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + end) i; -end; (* of structure *) +end; diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/groebner.ML Fri Jan 07 23:46:06 2011 +0100 @@ -4,12 +4,12 @@ signature GROEBNER = sig - val ring_and_ideal_conv : + val ring_and_ideal_conv: {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list, vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> conv -> conv -> - {ring_conv : conv, + {ring_conv : conv, simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, poly_eq_ss: simpset, unwind_conv : conv} @@ -22,8 +22,6 @@ structure Groebner : GROEBNER = struct -open Conv Drule Thm; - fun is_comb ct = (case Thm.term_of ct of _ $ _ => true @@ -281,12 +279,12 @@ [] => basis | (l,(p1,p2))::opairs => let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2)) - in + in if null sp orelse criterion2 basis (l,(p1,p2)) opairs then grobner_basis basis opairs else if constant_poly sp then grobner_basis (sph::basis) [] - else - let + else + let val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph))) basis val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) @@ -391,13 +389,14 @@ fun refute_disj rfn tm = case term_of tm of Const(@{const_name HOL.disj},_)$l$r => - compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE)) + Drule.compose_single + (refute_disj rfn (Thm.dest_arg tm), 2, + Drule.compose_single (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE)) | _ => rfn tm ; val notnotD = @{thm notnotD}; -fun mk_binop ct x y = capply (capply ct x) y +fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y -val mk_comb = capply; fun is_neg t = case term_of t of (Const(@{const_name Not},_)$p) => true @@ -424,8 +423,9 @@ val strip_exists = let fun h (acc, t) = - case (term_of t) of - Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc)) + case term_of t of + Const (@{const_name Ex}, _) $ Abs (x, T, p) => + h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc)) | _ => (acc,t) in fn t => h ([],t) end; @@ -451,12 +451,12 @@ val cTrp = @{cterm "Trueprop"}; val cConj = @{cterm HOL.conj}; val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"}); -val assume_Trueprop = mk_comb cTrp #> assume; +val assume_Trueprop = Thm.capply cTrp #> Thm.assume; val list_mk_conj = list_mk_binop cConj; val conjs = list_dest_binop cConj; -val mk_neg = mk_comb cNot; +val mk_neg = Thm.capply cNot; -fun striplist dest = +fun striplist dest = let fun h acc x = case try dest x of SOME (a,b) => h (h acc b) a @@ -466,7 +466,7 @@ val eq_commute = mk_meta_eq @{thm eq_commute}; -fun sym_conv eq = +fun sym_conv eq = let val (l,r) = Thm.dest_binop eq in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute end; @@ -481,10 +481,10 @@ val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ; -fun mk_conj_tab th = - let fun h acc th = +fun mk_conj_tab th = + let fun h acc th = case prop_of th of - @{term "Trueprop"}$(@{term HOL.conj}$p$q) => + @{term "Trueprop"}$(@{term HOL.conj}$p$q) => h (h acc (th RS conjunct2)) (th RS conjunct1) | @{term "Trueprop"}$p => (p,th)::acc in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end; @@ -492,85 +492,87 @@ fun is_conj (@{term HOL.conj}$_$_) = true | is_conj _ = false; -fun prove_conj tab cjs = - case cjs of +fun prove_conj tab cjs = + case cjs of [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs]; -fun conj_ac_rule eq = - let +fun conj_ac_rule eq = + let val (l,r) = Thm.dest_equals eq - val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l)) - val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r)) + val ctabl = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} l)) + val ctabr = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} r)) fun tabl c = the (Termtab.lookup ctabl (term_of c)) fun tabr c = the (Termtab.lookup ctabr (term_of c)) val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI} - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end; + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; (* END FIXME.*) - (* Conversion for the equivalence of existential statements where + (* Conversion for the equivalence of existential statements where EX quantifiers are rearranged differently *) - fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex} + fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex} fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t) -fun choose v th th' = case concl_of th of - @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => +fun choose v th th' = case concl_of th of + @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => let val p = (funpow 2 Thm.dest_arg o cprop_of) th val T = (hd o Thm.dest_ctyp o ctyp_of_term) p - val th0 = fconv_rule (Thm.beta_conversion true) + val th0 = Conv.fconv_rule (Thm.beta_conversion true) (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) - val pv = (Thm.rhs_of o Thm.beta_conversion true) + val pv = (Thm.rhs_of o Thm.beta_conversion true) (Thm.capply @{cterm Trueprop} (Thm.capply p v)) - val th1 = forall_intr v (implies_intr pv th') - in implies_elim (implies_elim th0 th) th1 end -| _ => error "" + val th1 = Thm.forall_intr v (Thm.implies_intr pv th') + in Thm.implies_elim (Thm.implies_elim th0 th) th1 end +| _ => error "" (* FIXME ? *) -fun simple_choose v th = - choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th +fun simple_choose v th = + choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) + ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th - fun mkexi v th = - let + fun mkexi v th = + let val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th)) - in implies_elim - (fconv_rule (Thm.beta_conversion true) (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI})) + in Thm.implies_elim + (Conv.fconv_rule (Thm.beta_conversion true) + (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI})) th end - fun ex_eq_conv t = - let + fun ex_eq_conv t = + let val (p0,q0) = Thm.dest_binop t - val (vs',P) = strip_exists p0 - val (vs,_) = strip_exists q0 - val th = assume (Thm.capply @{cterm Trueprop} P) - val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th)) - val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th)) + val (vs',P) = strip_exists p0 + val (vs,_) = strip_exists q0 + val th = Thm.assume (Thm.capply @{cterm Trueprop} P) + val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th)) + val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th)) val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1 val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1 - in implies_elim (implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2 + in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2 |> mk_meta_eq end; - fun getname v = case term_of v of + fun getname v = case term_of v of Free(s,_) => s | Var ((s,_),_) => s | _ => "x" fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t) - fun mk_exists v th = arg_cong_rule (ext (ctyp_of_term v)) + fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v)) (Thm.abstract_rule (getname v) v th) - val simp_ex_conv = + val simp_ex_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)}) fun frees t = Thm.add_cterm_frees t []; fun free_in v t = member op aconvc (frees t) v; val vsubst = let - fun vsubst (t,v) tm = + fun vsubst (t,v) tm = (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t) in fold vsubst end; @@ -578,37 +580,37 @@ (** main **) fun ring_and_ideal_conv - {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal} dest_const mk_const ring_eq_conv ring_normalize_conv = let val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; val [ring_add_tm, ring_mul_tm, ring_pow_tm] = - map dest_fun2 [add_pat, mul_pat, pow_pat]; + map Thm.dest_fun2 [add_pat, mul_pat, pow_pat]; val (ring_sub_tm, ring_neg_tm) = (case r_ops of - [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat) + [sub_pat, neg_pat] => (Thm.dest_fun2 sub_pat, Thm.dest_fun neg_pat) |_ => (@{cterm "True"}, @{cterm "True"})); val (field_div_tm, field_inv_tm) = (case f_ops of - [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat) + [div_pat, inv_pat] => (Thm.dest_fun2 div_pat, Thm.dest_fun inv_pat) | _ => (@{cterm "True"}, @{cterm "True"})); val [idom_thm, neq_thm] = idom; - val [idl_sub, idl_add0] = + val [idl_sub, idl_add0] = if length ideal = 2 then ideal else [eq_commute, eq_commute] fun ring_dest_neg t = - let val (l,r) = dest_comb t - in if Term.could_unify(term_of l,term_of ring_neg_tm) then r + let val (l,r) = Thm.dest_comb t + in if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t]) end - val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm); + val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm); fun field_dest_inv t = - let val (l,r) = dest_comb t in - if Term.could_unify(term_of l, term_of field_inv_tm) then r + let val (l,r) = Thm.dest_comb t in + if Term.could_unify(term_of l, term_of field_inv_tm) then r else raise CTERM ("field_dest_inv", [t]) end val ring_dest_add = dest_binary ring_add_tm; @@ -623,21 +625,21 @@ val ring_mk_pow = mk_binop ring_pow_tm ; fun grobvars tm acc = if can dest_const tm then acc - else if can ring_dest_neg tm then grobvars (dest_arg tm) acc - else if can ring_dest_pow tm then grobvars (dest_arg1 tm) acc + else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc + else if can ring_dest_pow tm then grobvars (Thm.dest_arg1 tm) acc else if can ring_dest_add tm orelse can ring_dest_sub tm orelse can ring_dest_mul tm - then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc) + then grobvars (Thm.dest_arg1 tm) (grobvars (Thm.dest_arg tm) acc) else if can field_dest_inv tm then - let val gvs = grobvars (dest_arg tm) [] + let val gvs = grobvars (Thm.dest_arg tm) [] in if null gvs then acc else tm::acc end else if can field_dest_div tm then - let val lvs = grobvars (dest_arg1 tm) acc - val gvs = grobvars (dest_arg tm) [] + let val lvs = grobvars (Thm.dest_arg1 tm) acc + val gvs = grobvars (Thm.dest_arg tm) [] in if null gvs then lvs else tm::acc - end + end else tm::acc ; fun grobify_term vars tm = @@ -652,7 +654,7 @@ handle CTERM _ => ( (grob_inv(grobify_term vars (field_dest_inv tm))) - handle CTERM _ => + handle CTERM _ => ((let val (l,r) = ring_dest_add tm in grob_add (grobify_term vars l) (grobify_term vars r) end) @@ -673,7 +675,7 @@ in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r) end) handle CTERM _ => error "grobify_term: unknown or invalid term"))))))))); -val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2; +val eq_tm = idom_thm |> concl |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_fun2; val dest_eq = dest_binary eq_tm; fun grobify_equation vars tm = @@ -684,9 +686,9 @@ fun grobify_equations tm = let val cjs = conjs tm - val rawvars = fold_rev (fn eq => fn a => - grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs [] - val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y)) + val rawvars = + fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs [] + val vars = sort (fn (x, y) => Term_Ord.term_ord (term_of x, term_of y)) (distinct (op aconvc) rawvars) in (vars,map (grobify_equation vars) cjs) end; @@ -708,26 +710,26 @@ (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0)))); val neq_01 = prove_nz (rat_1); fun neq_rule n th = [prove_nz n, th] MRS neq_thm; -fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1); +fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1); fun refute tm = if tm aconvc false_tm then assume_Trueprop tm else ((let val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm)) - val nths = filter (is_eq o dest_arg o concl) nths0 + val nths = filter (is_eq o Thm.dest_arg o concl) nths0 val eths = filter (is_eq o concl) eths0 in if null eths then let val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths - val th2 = Conv.fconv_rule - ((arg_conv #> arg_conv) - (binop_conv ring_normalize_conv)) th1 - val conc = th2 |> concl |> dest_arg + val th2 = + Conv.fconv_rule + ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1 + val conc = th2 |> concl |> Thm.dest_arg val (l,r) = conc |> dest_eq - in implies_intr (mk_comb cTrp tm) - (equal_elim (arg_cong_rule cTrp (eqF_intr th2)) - (reflexive l |> mk_object_eq)) + in Thm.implies_intr (Thm.capply cTrp tm) + (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2)) + (Thm.reflexive l |> mk_object_eq)) end else let @@ -741,9 +743,10 @@ let val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths val (vars,pol::pols) = - grobify_equations(list_mk_conj(dest_arg(concl nth)::map concl eths)) + grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths)) val (deg,l,cert) = grobner_strong vars pols pol - val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth + val th1 = + Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01 in (vars,l,cert,th2) end) @@ -753,27 +756,30 @@ val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg fun thm_fn pols = - if null pols then reflexive(mk_const rat_0) else + if null pols then Thm.reflexive(mk_const rat_0) else end_itlist mk_add - (map (fn (i,p) => arg_cong_rule (mk_comb ring_mul_tm p) + (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p) (nth eths i |> mk_meta_eq)) pols) val th1 = thm_fn herts_pos val th2 = thm_fn herts_neg - val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth - val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv) - (neq_rule l th3) - val (l,r) = dest_eq(dest_arg(concl th4)) - in implies_intr (mk_comb cTrp tm) - (equal_elim (arg_cong_rule cTrp (eqF_intr th4)) - (reflexive l |> mk_object_eq)) + val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth + val th4 = + Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv) + (neq_rule l th3) + val (l,r) = dest_eq(Thm.dest_arg(concl th4)) + in Thm.implies_intr (Thm.capply cTrp tm) + (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4)) + (Thm.reflexive l |> mk_object_eq)) end - end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm])) + end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm])) fun ring tm = let fun mk_forall x p = - mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p) - val avs = add_cterm_frees tm [] + Thm.capply + (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) + @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p) + val avs = Thm.add_cterm_frees tm [] val P' = fold mk_forall avs tm val th1 = initial_conv(mk_neg P') val (evs,bod) = strip_exists(concl th1) in @@ -784,10 +790,10 @@ val boda = concl th1a val th2a = refute_disj refute boda val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans - val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse) - val th3 = equal_elim - (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym]) - (th2 |> cprop_of)) th2 + val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse) + val th3 = + Thm.equal_elim + (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym]) (th2 |> cprop_of)) th2 in specl avs ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) end @@ -803,18 +809,18 @@ (length pols) end -fun poly_eq_conv t = +fun poly_eq_conv t = let val (a,b) = Thm.dest_binop t - in fconv_rule (arg_conv (arg1_conv ring_normalize_conv)) + in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv)) (instantiate' [] [SOME a, SOME b] idl_sub) end - val poly_eq_simproc = - let - fun proc phi ss t = + val poly_eq_simproc = + let + fun proc phi ss t = let val th = poly_eq_conv t in if Thm.is_reflexive th then NONE else SOME th end - in make_simproc {lhss = [Thm.lhs_of idl_sub], + in make_simproc {lhss = [Thm.lhs_of idl_sub], name = "poly_eq_simproc", proc = proc, identifier = []} end; val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms} @@ -822,79 +828,80 @@ local fun is_defined v t = - let - val mons = striplist(dest_binary ring_add_tm) t - in member (op aconvc) mons v andalso - forall (fn m => v aconvc m + let + val mons = striplist(dest_binary ring_add_tm) t + in member (op aconvc) mons v andalso + forall (fn m => v aconvc m orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons end fun isolate_variable vars tm = - let + let val th = poly_eq_conv tm val th' = (sym_conv then_conv poly_eq_conv) tm - val (v,th1) = + val (v,th1) = case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of SOME v => (v,th') - | NONE => (the (find_first + | NONE => (the (find_first (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th) - val th2 = transitive th1 - (instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] + val th2 = Thm.transitive th1 + (instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] idl_add0) - in fconv_rule(funpow 2 arg_conv ring_normalize_conv) th2 + in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2 end in fun unwind_polys_conv tm = - let + let val (vars,bod) = strip_exists tm val cjs = striplist (dest_binary @{cterm HOL.conj}) bod - val th1 = (the (get_first (try (isolate_variable vars)) cjs) + val th1 = (the (get_first (try (isolate_variable vars)) cjs) handle Option => raise CTERM ("unwind_polys_conv",[tm])) val eq = Thm.lhs_of th1 val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs)) val th2 = conj_ac_rule (mk_eq bod bod') - val th3 = transitive th2 - (Drule.binop_cong_rule @{cterm HOL.conj} th1 - (reflexive (Thm.dest_arg (Thm.rhs_of th2)))) + val th3 = + Thm.transitive th2 + (Drule.binop_cong_rule @{cterm HOL.conj} th1 + (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2)))) val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3)) val vars' = (remove op aconvc v vars) @ [v] - val th4 = fconv_rule (arg_conv simp_ex_conv) (mk_exists v th3) + val th4 = Conv.fconv_rule (Conv.arg_conv simp_ex_conv) (mk_exists v th3) val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4))) - in transitive th5 (fold mk_exists (remove op aconvc v vars) th4) + in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4) end; end local fun scrub_var v m = - let - val ps = striplist ring_dest_mul m + let + val ps = striplist ring_dest_mul m val ps' = remove op aconvc v ps in if null ps' then one_tm else fold1 ring_mk_mul ps' end fun find_multipliers v mons = - let - val mons1 = filter (fn m => free_in v m) mons - val mons2 = map (scrub_var v) mons1 + let + val mons1 = filter (fn m => free_in v m) mons + val mons2 = map (scrub_var v) mons1 in if null mons2 then zero_tm else fold1 ring_mk_add mons2 end fun isolate_monomials vars tm = - let + let val (cmons,vmons) = List.partition (fn m => null (inter (op aconvc) vars (frees m))) (striplist ring_dest_add tm) val cofactors = map (fn v => find_multipliers v vmons) vars val cnc = if null cmons then zero_tm else Thm.capply ring_neg_tm - (list_mk_binop ring_add_tm cmons) + (list_mk_binop ring_add_tm cmons) in (cofactors,cnc) end; fun isolate_variables evs ps eq = - let + let val vars = filter (fn v => free_in v eq) evs val (qs,p) = isolate_monomials vars eq - val rs = ideal (qs @ ps) p + val rs = ideal (qs @ ps) p (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t)) in (eq, take (length qs) rs ~~ vars) end; @@ -902,7 +909,7 @@ in fun solve_idealism evs ps eqs = if null evs then [] else - let + let val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the val evs' = subtract op aconvc evs (map snd cfs) val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs) @@ -911,7 +918,7 @@ end; -in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, +in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv} end; @@ -920,32 +927,32 @@ (case term_of tm of Const (@{const_name HOL.eq}, T) $ _ $ _ => if domain_type T = HOLogic.boolT then find_args bounds tm - else dest_arg tm - | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm) - | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm) - | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm) + else Thm.dest_arg tm + | Const (@{const_name Not}, _) $ _ => find_term bounds (Thm.dest_arg tm) + | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm) + | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm) | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm | @{term "op ==>"} $_$_ => find_args bounds tm | Const("op ==",_)$_$_ => find_args bounds tm - | @{term Trueprop}$_ => find_term bounds (dest_arg tm) + | @{term Trueprop}$_ => find_term bounds (Thm.dest_arg tm) | _ => raise TERM ("find_term", [])) and find_args bounds tm = let val (t, u) = Thm.dest_binop tm in (find_term bounds t handle TERM _ => find_term bounds u) end and find_body bounds b = - let val (_, b') = dest_abs (SOME (Name.bound bounds)) b + let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b in find_term (bounds + 1) b' end; -fun get_ring_ideal_convs ctxt form = +fun get_ring_ideal_convs ctxt form = case try (find_term 0) form of NONE => NONE | SOME tm => (case Semiring_Normalizer.match ctxt tm of NONE => NONE - | SOME (res as (theory, {is_const, dest_const, + | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => SOME (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) @@ -953,10 +960,10 @@ fun ring_solve ctxt form = (case try (find_term 0 (* FIXME !? *)) form of - NONE => reflexive form + NONE => Thm.reflexive form | SOME tm => (case Semiring_Normalizer.match ctxt tm of - NONE => reflexive form + NONE => Thm.reflexive form | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => #ring_conv (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) @@ -971,7 +978,7 @@ THEN' CSUBGOAL (fn (p, i) => rtac (let val form = Object_Logic.dest_judgment p in case get_ring_ideal_convs ctxt form of - NONE => reflexive form + NONE => Thm.reflexive form | SOME thy => #ring_conv thy form end) i handle TERM _ => no_tac @@ -984,42 +991,42 @@ | _=> raise CTERM ("ideal_tac - lhs",[t]) fun exitac NONE = no_tac | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1 -in -fun ideal_tac add_ths del_ths ctxt = +in +fun ideal_tac add_ths del_ths ctxt = presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => case get_ring_ideal_convs ctxt p of NONE => no_tac - | SOME thy => + | SOME thy => let fun poly_exists_tac {asms = asms, concl = concl, prems = prems, - params = params, context = ctxt, schematics = scs} = + params = params, context = ctxt, schematics = scs} = let val (evs,bod) = strip_exists (Thm.dest_arg concl) - val ps = map_filter (try (lhs o Thm.dest_arg)) asms - val cfs = (map swap o #multi_ideal thy evs ps) + val ps = map_filter (try (lhs o Thm.dest_arg)) asms + val cfs = (map swap o #multi_ideal thy evs ps) (map Thm.dest_arg1 (conjuncts bod)) val ws = map (exitac o AList.lookup op aconvc cfs) evs - in EVERY (rev ws) THEN Method.insert_tac prems 1 + in EVERY (rev ws) THEN Method.insert_tac prems 1 THEN ring_tac add_ths del_ths ctxt 1 end - in - clarify_tac @{claset} i - THEN Object_Logic.full_atomize_tac i - THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i - THEN clarify_tac @{claset} i + in + clarify_tac @{claset} i + THEN Object_Logic.full_atomize_tac i + THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i + THEN clarify_tac @{claset} i THEN (REPEAT (CONVERSION (#unwind_conv thy) i)) THEN SUBPROOF poly_exists_tac ctxt i end handle TERM _ => no_tac | CTERM _ => no_tac - | THM _ => no_tac); + | THM _ => no_tac); end; -fun algebra_tac add_ths del_ths ctxt i = +fun algebra_tac add_ths del_ths ctxt i = ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i - + local fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () @@ -1030,7 +1037,7 @@ in -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- +val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- (Scan.optional (keyword delN |-- thms) [])) >> (fn (add_ths, del_ths) => fn ctxt => SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Jan 07 23:46:06 2011 +0100 @@ -17,8 +17,6 @@ structure Inductive_Codegen : INDUCTIVE_CODEGEN = struct -open Codegen; - (**** theory data ****) fun merge_rules tabs = @@ -89,14 +87,14 @@ | SOME ({names, ...}, {intrs, raw_induct, ...}) => SOME (names, Codegen.thyname_of_const thy s, length (Inductive.params_of raw_induct), - preprocess thy intrs)) + Codegen.preprocess thy intrs)) | SOME _ => let val SOME names = find_first (fn xs => member (op =) xs s) (Graph.strong_conn graph); val intrs as (_, (thyname, nparms)) :: _ = maps (the o Symtab.lookup intros) names; - in SOME (names, thyname, nparms, preprocess thy (map fst (rev intrs))) end + in SOME (names, thyname, nparms, Codegen.preprocess thy (map fst (rev intrs))) end end; @@ -127,7 +125,7 @@ | SOME js => enclose "[" "]" (commas (map string_of_int js))) (iss @ [SOME is])); -fun print_modes modes = message ("Inferred modes:\n" ^ +fun print_modes modes = Codegen.message ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map (fn (m, rnd) => string_of_mode m ^ (if rnd then " (random)" else "")) ms)) modes)); @@ -279,7 +277,7 @@ let val xs = map (check_mode_clause thy arg_vs modes m) rs in case find_index is_none xs of ~1 => SOME (m', exists (fn SOME b => b) xs) - | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^ + | i => (Codegen.message ("Clause " ^ string_of_int (i+1) ^ " of " ^ p ^ " violates mode " ^ string_of_mode m'); NONE) end) ms) end; @@ -299,12 +297,12 @@ fun mk_eq (x::xs) = let fun mk_eqs _ [] = [] - | mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs + | mk_eqs a (b::cs) = Codegen.str (a ^ " = " ^ b) :: mk_eqs b cs in mk_eqs x xs end; -fun mk_tuple xs = Pretty.block (str "(" :: - flat (separate [str ",", Pretty.brk 1] (map single xs)) @ - [str ")"]); +fun mk_tuple xs = Pretty.block (Codegen.str "(" :: + flat (separate [Codegen.str ",", Pretty.brk 1] (map single xs)) @ + [Codegen.str ")"]); fun mk_v s (names, vs) = (case AList.lookup (op =) vs s of @@ -329,37 +327,37 @@ | is_exhaustive _ = false; fun compile_match nvs eq_ps out_ps success_p can_fail = - let val eqs = flat (separate [str " andalso", Pretty.brk 1] + let val eqs = flat (separate [Codegen.str " andalso", Pretty.brk 1] (map single (maps (mk_eq o snd) nvs @ eq_ps))); in Pretty.block - ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ - (Pretty.block ((if null eqs then [] else str "if " :: - [Pretty.block eqs, Pretty.brk 1, str "then "]) @ + ([Codegen.str "(fn ", mk_tuple out_ps, Codegen.str " =>", Pretty.brk 1] @ + (Pretty.block ((if null eqs then [] else Codegen.str "if " :: + [Pretty.block eqs, Pretty.brk 1, Codegen.str "then "]) @ (success_p :: - (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: + (if null eqs then [] else [Pretty.brk 1, Codegen.str "else DSeq.empty"]))) :: (if can_fail then - [Pretty.brk 1, str "| _ => DSeq.empty)"] - else [str ")"]))) + [Pretty.brk 1, Codegen.str "| _ => DSeq.empty)"] + else [Codegen.str ")"]))) end; fun modename module s (iss, is) gr = let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr) - else mk_const_id module s gr + else Codegen.mk_const_id module s gr in (space_implode "__" - (mk_qual_id module id :: + (Codegen.mk_qual_id module id :: map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr') end; -fun mk_funcomp brack s k p = (if brack then parens else I) - (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @ - separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @ - (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]); +fun mk_funcomp brack s k p = (if brack then Codegen.parens else I) + (Pretty.block [Pretty.block ((if k = 0 then [] else [Codegen.str "("]) @ + separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @ + (if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]); fun compile_expr thy defs dep module brack modes (NONE, t) gr = - apfst single (invoke_codegen thy defs dep module brack t gr) + apfst single (Codegen.invoke_codegen thy defs dep module brack t gr) | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = - ([str name], gr) + ([Codegen.str name], gr) | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = (case strip_comb t of (Const (name, _), args) => @@ -370,18 +368,18 @@ (compile_expr thy defs dep module true modes) (ms ~~ args1) ||>> modename module name mode; val (ps', gr'') = (case mode of - ([], []) => ([str "()"], gr') + ([], []) => ([Codegen.str "()"], gr') | _ => fold_map - (invoke_codegen thy defs dep module true) args2 gr') + (Codegen.invoke_codegen thy defs dep module true) args2 gr') in ((if brack andalso not (null ps andalso null ps') then - single o parens o Pretty.block else I) + single o Codegen.parens o Pretty.block else I) (flat (separate [Pretty.brk 1] - ([str mode_id] :: ps @ map single ps'))), gr') + ([Codegen.str mode_id] :: ps @ map single ps'))), gr') end else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) - (invoke_codegen thy defs dep module true t gr) + (Codegen.invoke_codegen thy defs dep module true t gr) | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) - (invoke_codegen thy defs dep module true t gr)); + (Codegen.invoke_codegen thy defs dep module true t gr)); fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = let @@ -396,8 +394,8 @@ in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end; fun compile_eq (s, t) gr = - apfst (Pretty.block o cons (str (s ^ " = ")) o single) - (invoke_codegen thy defs dep module false t gr); + apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single) + (Codegen.invoke_codegen thy defs dep module false t gr); val (in_ts, out_ts) = get_args is 1 ts; val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); @@ -405,32 +403,33 @@ fun compile_prems out_ts' vs names [] gr = let val (out_ps, gr2) = - fold_map (invoke_codegen thy defs dep module false) out_ts gr; + fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr; val (eq_ps, gr3) = fold_map compile_eq eqs gr2; val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); val (out_ts''', nvs) = fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); val (out_ps', gr4) = - fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3; + fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3; val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; val vs' = distinct (op =) (flat (vs :: map term_vs out_ts')); val missing_vs = missing_vars vs' out_ts; val final_p = Pretty.block - [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps] + [Codegen.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps] in if null missing_vs then (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' final_p (exists (not o is_exhaustive) out_ts'''), gr5) else let - val (pat_p, gr6) = invoke_codegen thy defs dep module true + val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true (HOLogic.mk_tuple (map Var missing_vs)) gr5; - val gen_p = mk_gen gr6 module true [] "" - (HOLogic.mk_tupleT (map snd missing_vs)) + val gen_p = + Codegen.mk_gen gr6 module true [] "" + (HOLogic.mk_tupleT (map snd missing_vs)) in (compile_match (snd nvs) eq_ps' out_ps' - (Pretty.block [str "DSeq.generator ", gen_p, - str " :->", Pretty.brk 1, + (Pretty.block [Codegen.str "DSeq.generator ", gen_p, + Codegen.str " :->", Pretty.brk 1, compile_match [] eq_ps [pat_p] final_p false]) (exists (not o is_exhaustive) out_ts'''), gr6) @@ -441,7 +440,8 @@ val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); - val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr; + val (out_ps, gr0) = + fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr; val (eq_ps, gr1) = fold_map compile_eq eqs gr0; in (case hd (select_mode_prem thy modes' vs' ps) of @@ -449,8 +449,8 @@ let val ps' = filter_out (equal p) ps; val (in_ts, out_ts''') = get_args js 1 us; - val (in_ps, gr2) = fold_map - (invoke_codegen thy defs dep module true) in_ts gr1; + val (in_ps, gr2) = + fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1; val (ps, gr3) = if not is_set then apfst (fn ps => ps @ @@ -459,52 +459,54 @@ (compile_expr thy defs dep module false modes (SOME mode, t) gr2) else - apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p, - str "of", str "Set", str "xs", str "=>", str "xs)"]) + apfst (fn p => + Pretty.breaks [Codegen.str "DSeq.of_list", Codegen.str "(case", p, + Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>", + Codegen.str "xs)"]) (*this is a very strong assumption about the generated code!*) - (invoke_codegen thy defs dep module true t gr2); + (Codegen.invoke_codegen thy defs dep module true t gr2); val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; in (compile_match (snd nvs) eq_ps out_ps (Pretty.block (ps @ - [str " :->", Pretty.brk 1, rest])) + [Codegen.str " :->", Pretty.brk 1, rest])) (exists (not o is_exhaustive) out_ts''), gr4) end | (p as Sidecond t, [(_, [])]) => let val ps' = filter_out (equal p) ps; - val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1; + val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1; val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2; in (compile_match (snd nvs) eq_ps out_ps - (Pretty.block [str "?? ", side_p, - str " :->", Pretty.brk 1, rest]) + (Pretty.block [Codegen.str "?? ", side_p, + Codegen.str " :->", Pretty.brk 1, rest]) (exists (not o is_exhaustive) out_ts''), gr3) end | (_, (_, missing_vs) :: _) => let val T = HOLogic.mk_tupleT (map snd missing_vs); - val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1; - val gen_p = mk_gen gr2 module true [] "" T; + val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1; + val gen_p = Codegen.mk_gen gr2 module true [] "" T; val (rest, gr3) = compile_prems [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2 in (compile_match (snd nvs) eq_ps out_ps - (Pretty.block [str "DSeq.generator", Pretty.brk 1, - gen_p, str " :->", Pretty.brk 1, rest]) + (Pretty.block [Codegen.str "DSeq.generator", Pretty.brk 1, + gen_p, Codegen.str " :->", Pretty.brk 1, rest]) (exists (not o is_exhaustive) out_ts''), gr3) end) end; val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ; in - (Pretty.block [str "DSeq.single", Pretty.brk 1, inp, - str " :->", Pretty.brk 1, prem_p], gr') + (Pretty.block [Codegen.str "DSeq.single", Pretty.brk 1, inp, + Codegen.str " :->", Pretty.brk 1, prem_p], gr') end; fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr = let - val xs = map str (Name.variant_list arg_vs + val xs = map Codegen.str (Name.variant_list arg_vs (map (fn i => "x" ^ string_of_int i) (snd mode))); val ((cl_ps, mode_id), gr') = gr |> fold_map (fn cl => compile_clause thy defs @@ -513,12 +515,12 @@ in (Pretty.block ([Pretty.block (separate (Pretty.brk 1) - (str (prfx ^ mode_id) :: - map str arg_vs @ - (case mode of ([], []) => [str "()"] | _ => xs)) @ - [str " ="]), + (Codegen.str (prfx ^ mode_id) :: + map Codegen.str arg_vs @ + (case mode of ([], []) => [Codegen.str "()"] | _ => xs)) @ + [Codegen.str " ="]), Pretty.brk 1] @ - flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) + flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) end; fun compile_preds thy defs dep module all_vs arg_vs modes preds gr = @@ -527,7 +529,7 @@ dep module prfx' all_vs arg_vs modes s cls mode gr') (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") in - (space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr') + (space_implode "\n\n" (map Codegen.string_of (flat prs)) ^ ";\n\n", gr') end; (**** processing of introduction rules ****) @@ -537,16 +539,17 @@ (string * (int option list * int)) list; fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip - (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr) + (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o Codegen.get_node gr) (Graph.all_preds (fst gr) [dep])))); -fun print_arities arities = message ("Arities:\n" ^ +fun print_arities arities = Codegen.message ("Arities:\n" ^ cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ space_implode " -> " (map (fn NONE => "X" | SOME k' => string_of_int k') (ks @ [SOME k]))) arities)); -fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.export_without_context) intrs; +fun prep_intrs intrs = + map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs; fun constrain cs [] = [] | constrain cs ((s, xs) :: ys) = @@ -562,12 +565,12 @@ (case get_clauses thy name of NONE => gr | SOME (names, thyname, nparms, intrs) => - mk_ind_def thy defs gr dep names (if_library thyname module) + mk_ind_def thy defs gr dep names (Codegen.if_library thyname module) [] (prep_intrs intrs) nparms)) (fold Term.add_const_names ts []) gr and mk_ind_def thy defs gr dep names module modecs intrs nparms = - add_edge_acyclic (hd names, dep) gr handle + Codegen.add_edge_acyclic (hd names, dep) gr handle Graph.CYCLES (xs :: _) => error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs) | Graph.UNDEF _ => @@ -611,8 +614,8 @@ end; val gr' = mk_extra_defs thy defs - (add_edge (hd names, dep) - (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; + (Codegen.add_edge (hd names, dep) + (Codegen.new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; val (extra_modes, extra_arities) = lookup_modes gr' (hd names); val (clauses, arities) = fold add_clause intrs ([], []); val modes = constrain modecs @@ -622,13 +625,13 @@ val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs) arg_vs (modes @ extra_modes) clauses gr'; in - (map_node (hd names) + (Codegen.map_node (hd names) (K (SOME (Modes (modes, arities)), module, s)) gr'') end; fun find_mode gr dep s u modes is = (case find_first (fn Mode (_, js, _) => is=js) (modes_of modes u handle Option => []) of - NONE => codegen_error gr dep + NONE => Codegen.codegen_error gr dep ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is)) | mode => mode); @@ -640,7 +643,7 @@ fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1) | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); - val module' = if_library thyname module; + val module' = Codegen.if_library thyname module; val gr1 = mk_extra_defs thy defs (mk_ind_def thy defs gr dep names module' [] (prep_intrs intrs) k) dep names module' [u]; @@ -651,7 +654,7 @@ val mode = find_mode gr1 dep s u modes is; val _ = if is_query orelse not (needs_random (the mode)) then () else warning ("Illegal use of random data generators in " ^ s); - val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1; + val (in_ps, gr2) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts' gr1; val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2; in (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @ @@ -664,12 +667,12 @@ val (Const (s, T), ts) = strip_comb t; val (Ts, U) = strip_type T in - rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop + Codegen.rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u])))) end; fun mk_fun thy defs name eqns dep module module' gr = - case try (get_node gr) name of + case try (Codegen.get_node gr) name of NONE => let val clauses = map clause_of_eqn eqns; @@ -678,30 +681,30 @@ (HOLogic.dest_Trueprop (concl_of (hd eqns))))))); val mode = 1 upto arity; val ((fun_id, mode_id), gr') = gr |> - mk_const_id module' name ||>> + Codegen.mk_const_id module' name ||>> modename module' pname ([], mode); - val vars = map (fn i => str ("x" ^ string_of_int i)) mode; - val s = string_of (Pretty.block - [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =", - Pretty.brk 1, str "DSeq.hd", Pretty.brk 1, - parens (Pretty.block (separate (Pretty.brk 1) (str mode_id :: + val vars = map (fn i => Codegen.str ("x" ^ string_of_int i)) mode; + val s = Codegen.string_of (Pretty.block + [Codegen.mk_app false (Codegen.str ("fun " ^ snd fun_id)) vars, Codegen.str " =", + Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1, + Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id :: vars)))]) ^ ";\n\n"; - val gr'' = mk_ind_def thy defs (add_edge (name, dep) - (new_node (name, (NONE, module', s)) gr')) name [pname] module' + val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep) + (Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module' [(pname, [([], mode)])] clauses 0; val (modes, _) = lookup_modes gr'' dep; val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd clauses)))) modes mode - in (mk_qual_id module fun_id, gr'') end + in (Codegen.mk_qual_id module fun_id, gr'') end | SOME _ => - (mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr); + (Codegen.mk_qual_id module (Codegen.get_const_id gr name), Codegen.add_edge (name, dep) gr); (* convert n-tuple to nested pairs *) fun conv_ntuple fs ts p = let val k = length fs; - val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); + val xs = map_range (fn i => Codegen.str ("x" ^ string_of_int i)) (k + 1); val xs' = map (fn Bound i => nth xs (k - i)) ts; fun conv xs js = if member (op =) fs js then @@ -713,9 +716,9 @@ in if k > 0 then Pretty.block - [str "DSeq.map (fn", Pretty.brk 1, - mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []), - str ")", Pretty.brk 1, parens p] + [Codegen.str "DSeq.map (fn", Pretty.brk 1, + mk_tuple xs', Codegen.str " =>", Pretty.brk 1, fst (conv xs []), + Codegen.str ")", Pretty.brk 1, Codegen.parens p] else p end; @@ -724,7 +727,7 @@ let val (r, Ts, fs) = HOLogic.strip_psplits u in case strip_comb r of (Const (s, T), ts) => - (case (get_clauses thy s, get_assoc_code thy (s, T)) of + (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of (SOME (names, thyname, k, intrs), NONE) => let val (ts1, ts2) = chop k ts; @@ -738,9 +741,9 @@ then let val (call_p, gr') = mk_ind_call thy defs dep module true s T (ts1 @ ts2') names thyname k intrs gr - in SOME ((if brack then parens else I) (Pretty.block - [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(", - conv_ntuple fs ots call_p, str "))"]), + in SOME ((if brack then Codegen.parens else I) (Pretty.block + [Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1, + Codegen.str "(", conv_ntuple fs ots call_p, Codegen.str "))"]), (*this is a very strong assumption about the generated code!*) gr') end @@ -749,30 +752,32 @@ | _ => NONE) | _ => NONE end - | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of - NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of + | (Const (s, T), ts) => + (case Symtab.lookup (#eqns (CodegenData.get thy)) s of + NONE => + (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of (SOME (names, thyname, k, intrs), NONE) => if length ts < k then NONE else SOME (let val (call_p, gr') = mk_ind_call thy defs dep module false s T (map Term.no_dummy_patterns ts) names thyname k intrs gr in (mk_funcomp brack "?!" - (length (binder_types T) - length ts) (parens call_p), gr') + (length (binder_types T) - length ts) (Codegen.parens call_p), gr') end handle TERM _ => mk_ind_call thy defs dep module true s T ts names thyname k intrs gr ) | _ => NONE) | SOME eqns => let val (_, thyname) :: _ = eqns; - val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns))) - dep module (if_library thyname module) gr; + val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns))) + dep module (Codegen.if_library thyname module) gr; val (ps, gr'') = fold_map - (invoke_codegen thy defs dep module true) ts gr'; - in SOME (mk_app brack (str id) ps, gr'') + (Codegen.invoke_codegen thy defs dep module true) ts gr'; + in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end) | _ => NONE); val setup = - add_codegen "inductive" inductive_codegen #> + Codegen.add_codegen "inductive" inductive_codegen #> Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add)) @@ -820,21 +825,21 @@ val pred = HOLogic.mk_Trueprop (list_comb (Const (Sign.intern_const thy' "quickcheckp", T), map Term.dummy_pattern Ts)); - val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"] - (generate_code_i thy' [] "Generated") [("testf", pred)]; + val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"] + (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)]; val s = "structure TestTerm =\nstruct\n\n" ^ cat_lines (map snd code) ^ - "\nopen Generated;\n\n" ^ string_of - (Pretty.block [str "val () = Inductive_Codegen.test_fn :=", - Pretty.brk 1, str "(fn p =>", Pretty.brk 1, - str "case Seq.pull (testf p) of", Pretty.brk 1, - str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"], - str " =>", Pretty.brk 1, str "SOME ", + "\nopen Generated;\n\n" ^ Codegen.string_of + (Pretty.block [Codegen.str "val () = Inductive_Codegen.test_fn :=", + Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1, + Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1, + Codegen.str "SOME ", mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"], + Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ", Pretty.enum "," "[" "]" (map (fn (s, T) => Pretty.block - [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'), + [Codegen.mk_term_of gr "Generated" false T, Pretty.brk 1, Codegen.str s]) args'), Pretty.brk 1, - str "| NONE => NONE);"]) ^ + Codegen.str "| NONE => NONE);"]) ^ "\n\nend;\n"; val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; val values = Config.get ctxt random_values; diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/prop_logic.ML Fri Jan 07 23:46:06 2011 +0100 @@ -7,39 +7,39 @@ signature PROP_LOGIC = sig - datatype prop_formula = - True - | False - | BoolVar of int (* NOTE: only use indices >= 1 *) - | Not of prop_formula - | Or of prop_formula * prop_formula - | And of prop_formula * prop_formula + datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula - val SNot : prop_formula -> prop_formula - val SOr : prop_formula * prop_formula -> prop_formula - val SAnd : prop_formula * prop_formula -> prop_formula - val simplify : prop_formula -> prop_formula (* eliminates True/False and double-negation *) + val SNot: prop_formula -> prop_formula + val SOr: prop_formula * prop_formula -> prop_formula + val SAnd: prop_formula * prop_formula -> prop_formula + val simplify: prop_formula -> prop_formula (* eliminates True/False and double-negation *) - val indices : prop_formula -> int list (* set of all variable indices *) - val maxidx : prop_formula -> int (* maximal variable index *) + val indices: prop_formula -> int list (* set of all variable indices *) + val maxidx: prop_formula -> int (* maximal variable index *) - val exists : prop_formula list -> prop_formula (* finite disjunction *) - val all : prop_formula list -> prop_formula (* finite conjunction *) - val dot_product : prop_formula list * prop_formula list -> prop_formula + val exists: prop_formula list -> prop_formula (* finite disjunction *) + val all: prop_formula list -> prop_formula (* finite conjunction *) + val dot_product: prop_formula list * prop_formula list -> prop_formula - val is_nnf : prop_formula -> bool (* returns true iff the formula is in negation normal form *) - val is_cnf : prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *) + val is_nnf: prop_formula -> bool (* returns true iff the formula is in negation normal form *) + val is_cnf: prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *) - val nnf : prop_formula -> prop_formula (* negation normal form *) - val cnf : prop_formula -> prop_formula (* conjunctive normal form *) - val defcnf : prop_formula -> prop_formula (* definitional cnf *) + val nnf: prop_formula -> prop_formula (* negation normal form *) + val cnf: prop_formula -> prop_formula (* conjunctive normal form *) + val defcnf: prop_formula -> prop_formula (* definitional cnf *) - val eval : (int -> bool) -> prop_formula -> bool (* semantics *) + val eval: (int -> bool) -> prop_formula -> bool (* semantics *) - (* propositional representation of HOL terms *) - val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table - (* HOL term representation of propositional formulae *) - val term_of_prop_formula : prop_formula -> term + (* propositional representation of HOL terms *) + val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table + (* HOL term representation of propositional formulae *) + val term_of_prop_formula: prop_formula -> term end; structure PropLogic : PROP_LOGIC = @@ -51,13 +51,13 @@ (* not/or/and *) (* ------------------------------------------------------------------------- *) - datatype prop_formula = - True - | False - | BoolVar of int (* NOTE: only use indices >= 1 *) - | Not of prop_formula - | Or of prop_formula * prop_formula - | And of prop_formula * prop_formula; +datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula; (* ------------------------------------------------------------------------- *) (* The following constructor functions make sure that True and False do not *) @@ -65,114 +65,93 @@ (* perform double-negation elimination. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun SNot True = False - | SNot False = True - | SNot (Not fm) = fm - | SNot fm = Not fm; - - (* prop_formula * prop_formula -> prop_formula *) +fun SNot True = False + | SNot False = True + | SNot (Not fm) = fm + | SNot fm = Not fm; - fun SOr (True, _) = True - | SOr (_, True) = True - | SOr (False, fm) = fm - | SOr (fm, False) = fm - | SOr (fm1, fm2) = Or (fm1, fm2); +fun SOr (True, _) = True + | SOr (_, True) = True + | SOr (False, fm) = fm + | SOr (fm, False) = fm + | SOr (fm1, fm2) = Or (fm1, fm2); - (* prop_formula * prop_formula -> prop_formula *) - - fun SAnd (True, fm) = fm - | SAnd (fm, True) = fm - | SAnd (False, _) = False - | SAnd (_, False) = False - | SAnd (fm1, fm2) = And (fm1, fm2); +fun SAnd (True, fm) = fm + | SAnd (fm, True) = fm + | SAnd (False, _) = False + | SAnd (_, False) = False + | SAnd (fm1, fm2) = And (fm1, fm2); (* ------------------------------------------------------------------------- *) (* simplify: eliminates True/False below other connectives, and double- *) (* negation *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun simplify (Not fm) = SNot (simplify fm) - | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) - | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) - | simplify fm = fm; +fun simplify (Not fm) = SNot (simplify fm) + | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) + | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) + | simplify fm = fm; (* ------------------------------------------------------------------------- *) (* indices: collects all indices of Boolean variables that occur in a *) (* propositional formula 'fm'; no duplicates *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> int list *) - - fun indices True = [] - | indices False = [] - | indices (BoolVar i) = [i] - | indices (Not fm) = indices fm - | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) - | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); +fun indices True = [] + | indices False = [] + | indices (BoolVar i) = [i] + | indices (Not fm) = indices fm + | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) + | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); (* ------------------------------------------------------------------------- *) (* maxidx: computes the maximal variable index occuring in a formula of *) (* propositional logic 'fm'; 0 if 'fm' contains no variable *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> int *) - - fun maxidx True = 0 - | maxidx False = 0 - | maxidx (BoolVar i) = i - | maxidx (Not fm) = maxidx fm - | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) - | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); +fun maxidx True = 0 + | maxidx False = 0 + | maxidx (BoolVar i) = i + | maxidx (Not fm) = maxidx fm + | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) + | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); (* ------------------------------------------------------------------------- *) (* exists: computes the disjunction over a list 'xs' of propositional *) (* formulas *) (* ------------------------------------------------------------------------- *) - (* prop_formula list -> prop_formula *) - - fun exists xs = Library.foldl SOr (False, xs); +fun exists xs = Library.foldl SOr (False, xs); (* ------------------------------------------------------------------------- *) (* all: computes the conjunction over a list 'xs' of propositional formulas *) (* ------------------------------------------------------------------------- *) - (* prop_formula list -> prop_formula *) - - fun all xs = Library.foldl SAnd (True, xs); +fun all xs = Library.foldl SAnd (True, xs); (* ------------------------------------------------------------------------- *) (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *) (* ------------------------------------------------------------------------- *) - (* prop_formula list * prop_formula list -> prop_formula *) - - fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); +fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys)); (* ------------------------------------------------------------------------- *) (* is_nnf: returns 'true' iff the formula is in negation normal form (i.e., *) (* only variables may be negated, but not subformulas). *) (* ------------------------------------------------------------------------- *) - local - fun is_literal (BoolVar _) = true - | is_literal (Not (BoolVar _)) = true - | is_literal _ = false - fun is_conj_disj (Or (fm1, fm2)) = - is_conj_disj fm1 andalso is_conj_disj fm2 - | is_conj_disj (And (fm1, fm2)) = - is_conj_disj fm1 andalso is_conj_disj fm2 - | is_conj_disj fm = - is_literal fm - in - fun is_nnf True = true - | is_nnf False = true - | is_nnf fm = is_conj_disj fm - end; +local + fun is_literal (BoolVar _) = true + | is_literal (Not (BoolVar _)) = true + | is_literal _ = false + fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 + | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 + | is_conj_disj fm = is_literal fm +in + fun is_nnf True = true + | is_nnf False = true + | is_nnf fm = is_conj_disj fm +end; (* ------------------------------------------------------------------------- *) (* is_cnf: returns 'true' iff the formula is in conjunctive normal form *) @@ -180,19 +159,19 @@ (* implies 'is_nnf'. *) (* ------------------------------------------------------------------------- *) - local - fun is_literal (BoolVar _) = true - | is_literal (Not (BoolVar _)) = true - | is_literal _ = false - fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 - | is_disj fm = is_literal fm - fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 - | is_conj fm = is_disj fm - in - fun is_cnf True = true - | is_cnf False = true - | is_cnf fm = is_conj fm - end; +local + fun is_literal (BoolVar _) = true + | is_literal (Not (BoolVar _)) = true + | is_literal _ = false + fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 + | is_disj fm = is_literal fm + fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 + | is_conj fm = is_disj fm +in + fun is_cnf True = true + | is_cnf False = true + | is_cnf fm = is_conj fm +end; (* ------------------------------------------------------------------------- *) (* nnf: computes the negation normal form of a formula 'fm' of propositional *) @@ -202,35 +181,31 @@ (* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun nnf fm = - let - fun - (* constants *) - nnf_aux True = True - | nnf_aux False = False - (* variables *) - | nnf_aux (BoolVar i) = (BoolVar i) - (* 'or' and 'and' as outermost connectives are left untouched *) - | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) - | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) - (* 'not' + constant *) - | nnf_aux (Not True) = False - | nnf_aux (Not False) = True - (* 'not' + variable *) - | nnf_aux (Not (BoolVar i)) = Not (BoolVar i) - (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) - | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) - | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) - (* double-negation elimination *) - | nnf_aux (Not (Not fm)) = nnf_aux fm - in - if is_nnf fm then - fm - else - nnf_aux fm - end; +fun nnf fm = + let + fun + (* constants *) + nnf_aux True = True + | nnf_aux False = False + (* variables *) + | nnf_aux (BoolVar i) = (BoolVar i) + (* 'or' and 'and' as outermost connectives are left untouched *) + | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) + | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) + (* 'not' + constant *) + | nnf_aux (Not True) = False + | nnf_aux (Not False) = True + (* 'not' + variable *) + | nnf_aux (Not (BoolVar i)) = Not (BoolVar i) + (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) + | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) + | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) + (* double-negation elimination *) + | nnf_aux (Not (Not fm)) = nnf_aux fm + in + if is_nnf fm then fm + else nnf_aux fm + end; (* ------------------------------------------------------------------------- *) (* cnf: computes the conjunctive normal form (i.e., a conjunction of *) @@ -241,35 +216,30 @@ (* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun cnf fm = - let - (* function to push an 'Or' below 'And's, using distributive laws *) - fun cnf_or (And (fm11, fm12), fm2) = - And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) - | cnf_or (fm1, And (fm21, fm22)) = - And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) - (* neither subformula contains 'And' *) - | cnf_or (fm1, fm2) = - Or (fm1, fm2) - fun cnf_from_nnf True = True - | cnf_from_nnf False = False - | cnf_from_nnf (BoolVar i) = BoolVar i - (* 'fm' must be a variable since the formula is in NNF *) - | cnf_from_nnf (Not fm) = Not fm - (* 'Or' may need to be pushed below 'And' *) - | cnf_from_nnf (Or (fm1, fm2)) = - cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) - (* 'And' as outermost connective is left untouched *) - | cnf_from_nnf (And (fm1, fm2)) = - And (cnf_from_nnf fm1, cnf_from_nnf fm2) - in - if is_cnf fm then - fm - else - (cnf_from_nnf o nnf) fm - end; +fun cnf fm = + let + (* function to push an 'Or' below 'And's, using distributive laws *) + fun cnf_or (And (fm11, fm12), fm2) = + And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) + | cnf_or (fm1, And (fm21, fm22)) = + And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) + (* neither subformula contains 'And' *) + | cnf_or (fm1, fm2) = Or (fm1, fm2) + fun cnf_from_nnf True = True + | cnf_from_nnf False = False + | cnf_from_nnf (BoolVar i) = BoolVar i + (* 'fm' must be a variable since the formula is in NNF *) + | cnf_from_nnf (Not fm) = Not fm + (* 'Or' may need to be pushed below 'And' *) + | cnf_from_nnf (Or (fm1, fm2)) = + cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) + (* 'And' as outermost connective is left untouched *) + | cnf_from_nnf (And (fm1, fm2)) = + And (cnf_from_nnf fm1, cnf_from_nnf fm2) + in + if is_cnf fm then fm + else (cnf_from_nnf o nnf) fm + end; (* ------------------------------------------------------------------------- *) (* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *) @@ -282,86 +252,80 @@ (* 'is_cnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun defcnf fm = - if is_cnf fm then - fm - else - let - val fm' = nnf fm - (* 'new' specifies the next index that is available to introduce an auxiliary variable *) - (* int ref *) - val new = Unsynchronized.ref (maxidx fm' + 1) - (* unit -> int *) - fun new_idx () = let val idx = !new in new := idx+1; idx end - (* replaces 'And' by an auxiliary variable (and its definition) *) - (* prop_formula -> prop_formula * prop_formula list *) - fun defcnf_or (And x) = - let - val i = new_idx () - in - (* Note that definitions are in NNF, but not CNF. *) - (BoolVar i, [Or (Not (BoolVar i), And x)]) - end - | defcnf_or (Or (fm1, fm2)) = - let - val (fm1', defs1) = defcnf_or fm1 - val (fm2', defs2) = defcnf_or fm2 - in - (Or (fm1', fm2'), defs1 @ defs2) - end - | defcnf_or fm = - (fm, []) - (* prop_formula -> prop_formula *) - fun defcnf_from_nnf True = True - | defcnf_from_nnf False = False - | defcnf_from_nnf (BoolVar i) = BoolVar i - (* 'fm' must be a variable since the formula is in NNF *) - | defcnf_from_nnf (Not fm) = Not fm - (* 'Or' may need to be pushed below 'And' *) - (* 'Or' of literal and 'And': use distributivity *) - | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = - And (defcnf_from_nnf (Or (BoolVar i, fm1)), - defcnf_from_nnf (Or (BoolVar i, fm2))) - | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = - And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), - defcnf_from_nnf (Or (Not (BoolVar i), fm2))) - | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = - And (defcnf_from_nnf (Or (fm1, BoolVar i)), - defcnf_from_nnf (Or (fm2, BoolVar i))) - | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = - And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), - defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) - (* all other cases: turn the formula into a disjunction of literals, *) - (* adding definitions as necessary *) - | defcnf_from_nnf (Or x) = - let - val (fm, defs) = defcnf_or (Or x) - val cnf_defs = map defcnf_from_nnf defs - in - all (fm :: cnf_defs) - end - (* 'And' as outermost connective is left untouched *) - | defcnf_from_nnf (And (fm1, fm2)) = - And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) - in - defcnf_from_nnf fm' - end; +fun defcnf fm = + if is_cnf fm then fm + else + let + val fm' = nnf fm + (* 'new' specifies the next index that is available to introduce an auxiliary variable *) + (* int ref *) + val new = Unsynchronized.ref (maxidx fm' + 1) + (* unit -> int *) + fun new_idx () = let val idx = !new in new := idx+1; idx end + (* replaces 'And' by an auxiliary variable (and its definition) *) + (* prop_formula -> prop_formula * prop_formula list *) + fun defcnf_or (And x) = + let + val i = new_idx () + in + (* Note that definitions are in NNF, but not CNF. *) + (BoolVar i, [Or (Not (BoolVar i), And x)]) + end + | defcnf_or (Or (fm1, fm2)) = + let + val (fm1', defs1) = defcnf_or fm1 + val (fm2', defs2) = defcnf_or fm2 + in + (Or (fm1', fm2'), defs1 @ defs2) + end + | defcnf_or fm = (fm, []) + (* prop_formula -> prop_formula *) + fun defcnf_from_nnf True = True + | defcnf_from_nnf False = False + | defcnf_from_nnf (BoolVar i) = BoolVar i + (* 'fm' must be a variable since the formula is in NNF *) + | defcnf_from_nnf (Not fm) = Not fm + (* 'Or' may need to be pushed below 'And' *) + (* 'Or' of literal and 'And': use distributivity *) + | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = + And (defcnf_from_nnf (Or (BoolVar i, fm1)), + defcnf_from_nnf (Or (BoolVar i, fm2))) + | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = + And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), + defcnf_from_nnf (Or (Not (BoolVar i), fm2))) + | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = + And (defcnf_from_nnf (Or (fm1, BoolVar i)), + defcnf_from_nnf (Or (fm2, BoolVar i))) + | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = + And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), + defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) + (* all other cases: turn the formula into a disjunction of literals, *) + (* adding definitions as necessary *) + | defcnf_from_nnf (Or x) = + let + val (fm, defs) = defcnf_or (Or x) + val cnf_defs = map defcnf_from_nnf defs + in + all (fm :: cnf_defs) + end + (* 'And' as outermost connective is left untouched *) + | defcnf_from_nnf (And (fm1, fm2)) = + And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) + in + defcnf_from_nnf fm' + end; (* ------------------------------------------------------------------------- *) (* eval: given an assignment 'a' of Boolean values to variable indices, the *) (* truth value of a propositional formula 'fm' is computed *) (* ------------------------------------------------------------------------- *) - (* (int -> bool) -> prop_formula -> bool *) - - fun eval a True = true - | eval a False = false - | eval a (BoolVar i) = (a i) - | eval a (Not fm) = not (eval a fm) - | eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) - | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); +fun eval a True = true + | eval a False = false + | eval a (BoolVar i) = (a i) + | eval a (Not fm) = not (eval a fm) + | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2) + | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2); (* ------------------------------------------------------------------------- *) (* prop_formula_of_term: returns the propositional structure of a HOL term, *) @@ -378,52 +342,47 @@ (* so that it does not have to be recomputed (by folding over the *) (* table) for each invocation. *) - (* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *) - fun prop_formula_of_term t table = - let - val next_idx_is_valid = Unsynchronized.ref false - val next_idx = Unsynchronized.ref 0 - fun get_next_idx () = - if !next_idx_is_valid then - Unsynchronized.inc next_idx - else ( - next_idx := Termtab.fold (Integer.max o snd) table 0; - next_idx_is_valid := true; - Unsynchronized.inc next_idx - ) - fun aux (Const (@{const_name True}, _)) table = - (True, table) - | aux (Const (@{const_name False}, _)) table = - (False, table) - | aux (Const (@{const_name Not}, _) $ x) table = - apfst Not (aux x table) - | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table = - let - val (fm1, table1) = aux x table - val (fm2, table2) = aux y table1 - in - (Or (fm1, fm2), table2) - end - | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table = - let - val (fm1, table1) = aux x table - val (fm2, table2) = aux y table1 - in - (And (fm1, fm2), table2) - end - | aux x table = - (case Termtab.lookup table x of - SOME i => - (BoolVar i, table) - | NONE => - let - val i = get_next_idx () - in - (BoolVar i, Termtab.update (x, i) table) - end) - in - aux t table - end; +fun prop_formula_of_term t table = + let + val next_idx_is_valid = Unsynchronized.ref false + val next_idx = Unsynchronized.ref 0 + fun get_next_idx () = + if !next_idx_is_valid then + Unsynchronized.inc next_idx + else ( + next_idx := Termtab.fold (Integer.max o snd) table 0; + next_idx_is_valid := true; + Unsynchronized.inc next_idx + ) + fun aux (Const (@{const_name True}, _)) table = (True, table) + | aux (Const (@{const_name False}, _)) table = (False, table) + | aux (Const (@{const_name Not}, _) $ x) table = apfst Not (aux x table) + | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table = + let + val (fm1, table1) = aux x table + val (fm2, table2) = aux y table1 + in + (Or (fm1, fm2), table2) + end + | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table = + let + val (fm1, table1) = aux x table + val (fm2, table2) = aux y table1 + in + (And (fm1, fm2), table2) + end + | aux x table = + (case Termtab.lookup table x of + SOME i => (BoolVar i, table) + | NONE => + let + val i = get_next_idx () + in + (BoolVar i, Termtab.update (x, i) table) + end) + in + aux t table + end; (* ------------------------------------------------------------------------- *) (* term_of_prop_formula: returns a HOL term that corresponds to a *) @@ -435,18 +394,13 @@ (* Boolean variables in the formula, similar to 'prop_formula_of_term' *) (* (but the other way round). *) - (* prop_formula -> Term.term *) - fun term_of_prop_formula True = - HOLogic.true_const - | term_of_prop_formula False = - HOLogic.false_const - | term_of_prop_formula (BoolVar i) = - Free ("v" ^ Int.toString i, HOLogic.boolT) - | term_of_prop_formula (Not fm) = - HOLogic.mk_not (term_of_prop_formula fm) - | term_of_prop_formula (Or (fm1, fm2)) = - HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) - | term_of_prop_formula (And (fm1, fm2)) = - HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); +fun term_of_prop_formula True = HOLogic.true_const + | term_of_prop_formula False = HOLogic.false_const + | term_of_prop_formula (BoolVar i) = Free ("v" ^ Int.toString i, HOLogic.boolT) + | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm) + | term_of_prop_formula (Or (fm1, fm2)) = + HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) + | term_of_prop_formula (And (fm1, fm2)) = + HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); end; diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Fri Jan 07 23:46:06 2011 +0100 @@ -12,8 +12,6 @@ structure RecfunCodegen : RECFUN_CODEGEN = struct -open Codegen; - val const_of = dest_Const o head_of o fst o Logic.dest_equals; structure ModuleData = Theory_Data @@ -47,21 +45,24 @@ val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c |> Code.bare_thms_of_cert thy |> map (AxClass.overload thy) - |> filter (is_instance T o snd o const_of o prop_of); + |> filter (Codegen.is_instance T o snd o const_of o prop_of); val module_name = case Symtab.lookup (ModuleData.get thy) c of SOME module_name => module_name - | NONE => case get_defn thy defs c T + | NONE => + case Codegen.get_defn thy defs c T of SOME ((_, (thyname, _)), _) => thyname | NONE => Codegen.thyname_of_const thy c; in if null raw_thms then ([], "") else raw_thms - |> preprocess thy + |> Codegen.preprocess thy |> avoid_value thy |> rpair module_name end; -fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of - SOME (_, SOME i) => " def" ^ string_of_int i | _ => ""); +fun mk_suffix thy defs (s, T) = + (case Codegen.get_defn thy defs s T of + SOME (_, SOME i) => " def" ^ string_of_int i + | _ => ""); exception EQN of string * typ * string; @@ -72,7 +73,7 @@ fun add_rec_funs thy defs dep module eqs gr = let fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t), - Logic.dest_equals (rename_term t)); + Logic.dest_equals (Codegen.rename_term t)); val eqs' = map dest_eq eqs; val (dname, _) :: _ = eqs'; val (s, T) = const_of (hd eqs); @@ -80,49 +81,51 @@ fun mk_fundef module fname first [] gr = ([], gr) | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr = let - val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr; - val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1; + val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr; + val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1; val (rest, gr3) = mk_fundef module fname' false xs gr2 ; - val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3; + val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3; val num_args = (length o snd o strip_comb) lhs; val prfx = if fname = fname' then " |" else if not first then "and" else if num_args = 0 then "val" else "fun"; - val pl' = Pretty.breaks (str prfx - :: (if num_args = 0 then [pl, str ":", ty] else [pl])); + val pl' = Pretty.breaks (Codegen.str prfx + :: (if num_args = 0 then [pl, Codegen.str ":", ty] else [pl])); in (Pretty.blk (4, pl' - @ [str " =", Pretty.brk 1, pr]) :: rest, gr4) + @ [Codegen.str " =", Pretty.brk 1, pr]) :: rest, gr4) end; - fun put_code module fundef = map_node dname - (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0, - separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n")); + fun put_code module fundef = Codegen.map_node dname + (K (SOME (EQN ("", dummyT, dname)), module, Codegen.string_of (Pretty.blk (0, + separate Pretty.fbrk fundef @ [Codegen.str ";"])) ^ "\n\n")); in - (case try (get_node gr) dname of + (case try (Codegen.get_node gr) dname of NONE => let - val gr1 = add_edge (dname, dep) - (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); + val gr1 = Codegen.add_edge (dname, dep) + (Codegen.new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ; val xs = cycle gr2 dname []; - val cs = map (fn x => case get_node gr2 x of + val cs = map (fn x => + case Codegen.get_node gr2 x of (SOME (EQN (s, T, _)), _, _) => (s, T) | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ implode (separate ", " xs))) xs - in (case xs of + in + (case xs of [_] => (module, put_code module fundef gr2) | _ => if not (member (op =) xs dep) then let val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; - val module' = if_library thyname module; + val module' = Codegen.if_library thyname module; val eqs'' = map (dest_eq o prop_of) (maps fst thmss); val (fundef', gr3) = mk_fundef module' "" true eqs'' - (add_edge (dname, dep) - (List.foldr (uncurry new_node) (del_nodes xs gr2) + (Codegen.add_edge (dname, dep) + (List.foldr (uncurry Codegen.new_node) (Codegen.del_nodes xs gr2) (map (fn k => (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) in (module', put_code module' fundef' gr3) end @@ -130,30 +133,32 @@ end | SOME (SOME (EQN (_, _, s)), module', _) => (module', if s = "" then - if dname = dep then gr else add_edge (dname, dep) gr - else if s = dep then gr else add_edge (s, dep) gr)) + if dname = dep then gr else Codegen.add_edge (dname, dep) gr + else if s = dep then gr else Codegen.add_edge (s, dep) gr)) end; -fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of - (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of +fun recfun_codegen thy defs dep module brack t gr = + (case strip_comb t of + (Const (p as (s, T)), ts) => + (case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of (([], _), _) => NONE | (_, SOME _) => NONE | ((eqns, thyname), NONE) => let - val module' = if_library thyname module; + val module' = Codegen.if_library thyname module; val (ps, gr') = fold_map - (invoke_codegen thy defs dep module true) ts gr; + (Codegen.invoke_codegen thy defs dep module true) ts gr; val suffix = mk_suffix thy defs p; val (module'', gr'') = add_rec_funs thy defs dep module' (map prop_of eqns) gr'; - val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr'' + val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr'' in - SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''') + SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''') end) | _ => NONE); val setup = - add_codegen "recfun" recfun_codegen + Codegen.add_codegen "recfun" recfun_codegen #> Code.set_code_target_attr add_thm_target; end; diff -r 79ec1ddf49df -r 73981e95b30b src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Fri Jan 07 23:46:06 2011 +0100 @@ -48,13 +48,13 @@ signature SAT = sig - val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) - val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) - val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) - val rawsat_thm: Proof.context -> cterm list -> thm - val rawsat_tac: Proof.context -> int -> tactic - val sat_tac: Proof.context -> int -> tactic - val satx_tac: Proof.context -> int -> tactic + val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) + val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) + val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) + val rawsat_thm: Proof.context -> cterm list -> thm + val rawsat_tac: Proof.context -> int -> tactic + val sat_tac: Proof.context -> int -> tactic + val satx_tac: Proof.context -> int -> tactic end functor SATFunc(cnf : CNF) : SAT = @@ -78,8 +78,7 @@ (* or negatively) as equal *) (* ------------------------------------------------------------------------- *) -fun lit_ord (i, j) = - int_ord (abs i, abs j); +fun lit_ord (i, j) = int_ord (abs i, abs j); (* ------------------------------------------------------------------------- *) (* CLAUSE: during proof reconstruction, three kinds of clauses are *) @@ -91,9 +90,10 @@ (* reconstruction *) (* ------------------------------------------------------------------------- *) -datatype CLAUSE = NO_CLAUSE - | ORIG_CLAUSE of thm - | RAW_CLAUSE of thm * (int * cterm) list; +datatype CLAUSE = + NO_CLAUSE + | ORIG_CLAUSE of thm + | RAW_CLAUSE of thm * (int * cterm) list; (* ------------------------------------------------------------------------- *) (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) @@ -117,88 +117,87 @@ (* cterms. *) (* ------------------------------------------------------------------------- *) -(* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *) - fun resolve_raw_clauses [] = raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) | resolve_raw_clauses (c::cs) = - let - (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) - fun merge xs [] = xs - | merge [] ys = ys - | merge (x::xs) (y::ys) = - (case (lit_ord o pairself fst) (x, y) of - LESS => x :: merge xs (y::ys) - | EQUAL => x :: merge xs ys - | GREATER => y :: merge (x::xs) ys) + let + (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) + fun merge xs [] = xs + | merge [] ys = ys + | merge (x :: xs) (y :: ys) = + (case (lit_ord o pairself fst) (x, y) of + LESS => x :: merge xs (y :: ys) + | EQUAL => x :: merge xs ys + | GREATER => y :: merge (x :: xs) ys) - (* find out which two hyps are used in the resolution *) - (* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *) - fun find_res_hyps ([], _) _ = - raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) - | find_res_hyps (_, []) _ = - raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) - | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = - (case (lit_ord o pairself fst) (h1, h2) of - LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) - | EQUAL => let - val (i1, chyp1) = h1 - val (i2, chyp2) = h2 - in - if i1 = ~ i2 then - (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) - else (* i1 = i2 *) - find_res_hyps (hyps1, hyps2) (h1 :: acc) - end - | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) + (* find out which two hyps are used in the resolution *) + fun find_res_hyps ([], _) _ = + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) + | find_res_hyps (_, []) _ = + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) + | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = + (case (lit_ord o pairself fst) (h1, h2) of + LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) + | EQUAL => + let + val (i1, chyp1) = h1 + val (i2, chyp2) = h2 + in + if i1 = ~ i2 then + (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) + else (* i1 = i2 *) + find_res_hyps (hyps1, hyps2) (h1 :: acc) + end + | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) - (* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *) - fun resolution (c1, hyps1) (c2, hyps2) = - let - val _ = - if ! trace_sat then - tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) - ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") - else () + fun resolution (c1, hyps1) (c2, hyps2) = + let + val _ = + if ! trace_sat then + tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) + ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") + else () - (* the two literals used for resolution *) - val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] + (* the two literals used for resolution *) + val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] - val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) - val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) + val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) + val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) - val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) - let - val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) - in - Thm.instantiate ([], [(cP, cLit)]) resolution_thm - end + val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) + let + val cLit = + snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) + in + Thm.instantiate ([], [(cP, cLit)]) resolution_thm + end - val _ = - if !trace_sat then - tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) - else () + val _ = + if !trace_sat then + tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) + else () - (* Gamma1, Gamma2 |- False *) - val c_new = Thm.implies_elim - (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) - (if hyp1_is_neg then c1' else c2') + (* Gamma1, Gamma2 |- False *) + val c_new = + Thm.implies_elim + (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) + (if hyp1_is_neg then c1' else c2') - val _ = - if !trace_sat then - tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ - " (hyps: " ^ ML_Syntax.print_list - (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") - else () - val _ = Unsynchronized.inc counter - in - (c_new, new_hyps) - end - in - fold resolution cs c - end; + val _ = + if !trace_sat then + tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ + " (hyps: " ^ ML_Syntax.print_list + (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") + else () + val _ = Unsynchronized.inc counter + in + (c_new, new_hyps) + end + in + fold resolution cs c + end; (* ------------------------------------------------------------------------- *) (* replay_proof: replays the resolution proof returned by the SAT solver; *) @@ -210,68 +209,71 @@ (* occur (as part of a literal) in 'clauses' to positive integers. *) (* ------------------------------------------------------------------------- *) -(* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *) - fun replay_proof atom_table clauses (clause_table, empty_id) = -let - (* Thm.cterm -> int option *) - fun index_of_literal chyp = ( - case (HOLogic.dest_Trueprop o Thm.term_of) chyp of - (Const (@{const_name Not}, _) $ atom) => - SOME (~ (the (Termtab.lookup atom_table atom))) - | atom => - SOME (the (Termtab.lookup atom_table atom)) - ) handle TERM _ => NONE; (* 'chyp' is not a literal *) + let + fun index_of_literal chyp = + (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of + (Const (@{const_name Not}, _) $ atom) => + SOME (~ (the (Termtab.lookup atom_table atom))) + | atom => SOME (the (Termtab.lookup atom_table atom))) + handle TERM _ => NONE; (* 'chyp' is not a literal *) - (* int -> Thm.thm * (int * Thm.cterm) list *) - fun prove_clause id = - case Array.sub (clauses, id) of - RAW_CLAUSE clause => - clause - | ORIG_CLAUSE thm => - (* convert the original clause *) - let - val _ = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () - val raw = cnf.clause2raw_thm thm - val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => - Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) - val clause = (raw, hyps) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) - in - clause - end - | NO_CLAUSE => - (* prove the clause, using information from 'clause_table' *) - let - val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () - val ids = the (Inttab.lookup clause_table id) - val clause = resolve_raw_clauses (map prove_clause ids) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) - val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else () - in - clause - end + fun prove_clause id = + (case Array.sub (clauses, id) of + RAW_CLAUSE clause => clause + | ORIG_CLAUSE thm => + (* convert the original clause *) + let + val _ = + if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () + val raw = cnf.clause2raw_thm thm + val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => + Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) + val clause = (raw, hyps) + val _ = Array.update (clauses, id, RAW_CLAUSE clause) + in + clause + end + | NO_CLAUSE => + (* prove the clause, using information from 'clause_table' *) + let + val _ = + if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () + val ids = the (Inttab.lookup clause_table id) + val clause = resolve_raw_clauses (map prove_clause ids) + val _ = Array.update (clauses, id, RAW_CLAUSE clause) + val _ = + if !trace_sat then + tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) + else () + in + clause + end) - val _ = counter := 0 - val empty_clause = fst (prove_clause empty_id) - val _ = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else () -in - empty_clause -end; + val _ = counter := 0 + val empty_clause = fst (prove_clause empty_id) + val _ = + if !trace_sat then + tracing ("Proof reconstruction successful; " ^ + string_of_int (!counter) ^ " resolution step(s) total.") + else () + in + empty_clause + end; (* ------------------------------------------------------------------------- *) (* string_of_prop_formula: return a human-readable string representation of *) (* a 'prop_formula' (just for tracing) *) (* ------------------------------------------------------------------------- *) -(* PropLogic.prop_formula -> string *) - -fun string_of_prop_formula PropLogic.True = "True" - | string_of_prop_formula PropLogic.False = "False" - | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i - | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm - | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" - | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; +fun string_of_prop_formula PropLogic.True = "True" + | string_of_prop_formula PropLogic.False = "False" + | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i + | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm + | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = + "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" + | string_of_prop_formula (PropLogic.And (fm1, fm2)) = + "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; (* ------------------------------------------------------------------------- *) (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) @@ -281,112 +283,120 @@ (* ------------------------------------------------------------------------- *) fun rawsat_thm ctxt clauses = -let - (* remove premises that equal "True" *) - val clauses' = filter (fn clause => - (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause - handle TERM ("dest_Trueprop", _) => true) clauses - (* remove non-clausal premises -- of course this shouldn't actually *) - (* remove anything as long as 'rawsat_tac' is only called after the *) - (* premises have been converted to clauses *) - val clauses'' = filter (fn clause => - ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause - handle TERM ("dest_Trueprop", _) => false) - orelse ( - warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); - false)) clauses' - (* remove trivial clauses -- this is necessary because zChaff removes *) - (* trivial clauses during preprocessing, and otherwise our clause *) - (* numbering would be off *) - val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' - (* sort clauses according to the term order -- an optimization, *) - (* useful because forming the union of hypotheses, as done by *) - (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) - (* terms sorted in descending order, while only linear for terms *) - (* sorted in ascending order *) - val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses - val _ = if !trace_sat then - tracing ("Sorted non-trivial clauses:\n" ^ - cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) - else () - (* translate clauses from HOL terms to PropLogic.prop_formula *) - val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty - val _ = if !trace_sat then - tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) - else () - val fm = PropLogic.all fms - (* unit -> Thm.thm *) - fun make_quick_and_dirty_thm () = - let - val _ = if !trace_sat then - tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." - else () - val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) - in - (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) - (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) - (* clauses in ascending order (which is linear for *) - (* 'Conjunction.intr_balanced', used below) *) - fold Thm.weaken (rev sorted_clauses) False_thm - end -in - case - let val the_solver = ! solver - in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end - of - SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( - if !trace_sat then - tracing ("Proof trace from SAT solver:\n" ^ - "clauses: " ^ ML_Syntax.print_list - (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) - (Inttab.dest clause_table) ^ "\n" ^ - "empty clause: " ^ Int.toString empty_id) - else (); - if !quick_and_dirty then - make_quick_and_dirty_thm () - else - let - (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) - (* this avoids accumulation of hypotheses during resolution *) - (* [c_1, ..., c_n] |- c_1 && ... && c_n *) - val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) - (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) - val cnf_cterm = cprop_of clauses_thm - val cnf_thm = Thm.assume cnf_cterm - (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) - val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm - (* initialize the clause array with the given clauses *) - val max_idx = the (Inttab.max_key clause_table) - val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) - val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0 - (* replay the proof to derive the empty clause *) - (* [c_1 && ... && c_n] |- False *) - val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) - in - (* [c_1, ..., c_n] |- False *) - Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm - end) - | SatSolver.UNSATISFIABLE NONE => - if !quick_and_dirty then ( - warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; - make_quick_and_dirty_thm () - ) else - raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) - | SatSolver.SATISFIABLE assignment => - let - val msg = "SAT solver found a countermodel:\n" - ^ (commas - o map (fn (term, idx) => - Syntax.string_of_term_global @{theory} term ^ ": " ^ - (case assignment idx of NONE => "arbitrary" - | SOME true => "true" | SOME false => "false"))) - (Termtab.dest atom_table) - in - raise THM (msg, 0, []) - end - | SatSolver.UNKNOWN => - raise THM ("SAT solver failed to decide the formula", 0, []) -end; + let + (* remove premises that equal "True" *) + val clauses' = filter (fn clause => + (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause + handle TERM ("dest_Trueprop", _) => true) clauses + (* remove non-clausal premises -- of course this shouldn't actually *) + (* remove anything as long as 'rawsat_tac' is only called after the *) + (* premises have been converted to clauses *) + val clauses'' = filter (fn clause => + ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause + handle TERM ("dest_Trueprop", _) => false) + orelse ( + warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); + false)) clauses' + (* remove trivial clauses -- this is necessary because zChaff removes *) + (* trivial clauses during preprocessing, and otherwise our clause *) + (* numbering would be off *) + val nontrivial_clauses = + filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' + (* sort clauses according to the term order -- an optimization, *) + (* useful because forming the union of hypotheses, as done by *) + (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) + (* terms sorted in descending order, while only linear for terms *) + (* sorted in ascending order *) + val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses + val _ = + if !trace_sat then + tracing ("Sorted non-trivial clauses:\n" ^ + cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) + else () + (* translate clauses from HOL terms to PropLogic.prop_formula *) + val (fms, atom_table) = + fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) + sorted_clauses Termtab.empty + val _ = + if !trace_sat then + tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) + else () + val fm = PropLogic.all fms + (* unit -> Thm.thm *) + fun make_quick_and_dirty_thm () = + let + val _ = + if !trace_sat then + tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." + else () + val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) + in + (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) + (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) + (* clauses in ascending order (which is linear for *) + (* 'Conjunction.intr_balanced', used below) *) + fold Thm.weaken (rev sorted_clauses) False_thm + end + in + case + let val the_solver = ! solver + in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end + of + SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => + (if !trace_sat then + tracing ("Proof trace from SAT solver:\n" ^ + "clauses: " ^ ML_Syntax.print_list + (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) + (Inttab.dest clause_table) ^ "\n" ^ + "empty clause: " ^ Int.toString empty_id) + else (); + if !quick_and_dirty then + make_quick_and_dirty_thm () + else + let + (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) + (* this avoids accumulation of hypotheses during resolution *) + (* [c_1, ..., c_n] |- c_1 && ... && c_n *) + val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) + (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) + val cnf_cterm = cprop_of clauses_thm + val cnf_thm = Thm.assume cnf_cterm + (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) + val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm + (* initialize the clause array with the given clauses *) + val max_idx = the (Inttab.max_key clause_table) + val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) + val _ = + fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) + cnf_clauses 0 + (* replay the proof to derive the empty clause *) + (* [c_1 && ... && c_n] |- False *) + val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) + in + (* [c_1, ..., c_n] |- False *) + Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm + end) + | SatSolver.UNSATISFIABLE NONE => + if !quick_and_dirty then + (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; + make_quick_and_dirty_thm ()) + else + raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) + | SatSolver.SATISFIABLE assignment => + let + val msg = + "SAT solver found a countermodel:\n" ^ + (commas o map (fn (term, idx) => + Syntax.string_of_term_global @{theory} term ^ ": " ^ + (case assignment idx of NONE => "arbitrary" + | SOME true => "true" | SOME false => "false"))) + (Termtab.dest atom_table) + in + raise THM (msg, 0, []) + end + | SatSolver.UNKNOWN => + raise THM ("SAT solver failed to decide the formula", 0, []) + end; (* ------------------------------------------------------------------------- *) (* Tactics *) @@ -417,9 +427,9 @@ (* ------------------------------------------------------------------------- *) val pre_cnf_tac = - rtac ccontr THEN' - Object_Logic.atomize_prems_tac THEN' - CONVERSION Drule.beta_eta_conversion; + rtac ccontr THEN' + Object_Logic.atomize_prems_tac THEN' + CONVERSION Drule.beta_eta_conversion; (* ------------------------------------------------------------------------- *) (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) @@ -429,7 +439,7 @@ (* ------------------------------------------------------------------------- *) fun cnfsat_tac ctxt i = - (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); + (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); (* ------------------------------------------------------------------------- *) (* cnfxsat_tac: checks if the empty clause "False" occurs among the *) @@ -439,8 +449,8 @@ (* ------------------------------------------------------------------------- *) fun cnfxsat_tac ctxt i = - (etac FalseE i) ORELSE - (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); + (etac FalseE i) ORELSE + (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); (* ------------------------------------------------------------------------- *) (* sat_tac: tactic for calling an external SAT solver, taking as input an *) @@ -449,7 +459,7 @@ (* ------------------------------------------------------------------------- *) fun sat_tac ctxt i = - pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; + pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; (* ------------------------------------------------------------------------- *) (* satx_tac: tactic for calling an external SAT solver, taking as input an *) @@ -458,6 +468,6 @@ (* ------------------------------------------------------------------------- *) fun satx_tac ctxt i = - pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; + pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; end; diff -r 79ec1ddf49df -r 73981e95b30b src/Sequents/modal.ML --- a/src/Sequents/modal.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/Sequents/modal.ML Fri Jan 07 23:46:06 2011 +0100 @@ -5,7 +5,6 @@ Simple modal reasoner. *) - signature MODAL_PROVER_RULE = sig val rewrite_rls : thm list @@ -25,8 +24,6 @@ functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = struct -local open Modal_Rule -in (*Returns the list of all formulas in the sequent*) fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u @@ -62,12 +59,12 @@ (* NB No back tracking possible with aside rules *) -fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n)); +fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n)); fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n; -val fres_safe_tac = fresolve_tac safe_rls; -val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac; -val fres_bound_tac = fresolve_tac bound_rls; +val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls; +val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac; +val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls; fun UPTOGOAL n tf = let fun tac i = if i"] - else List.concat ( + else flat ( [[">"]] @ map show inner @@ -304,7 +304,7 @@ fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]), Tag ("dd", [], [tag])]; fun dl (common_atts, dtdds) = - Tag ("dl", from_common common_atts, (List.concat o map to_dtdd) dtdds); + Tag ("dl", from_common common_atts, maps to_dtdd dtdds); fun alternate_class { class0, class1 } rows = let fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs) diff -r 79ec1ddf49df -r 73981e95b30b src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Jan 07 18:10:43 2011 +0100 +++ b/src/ZF/Tools/inductive_package.ML Fri Jan 07 23:46:06 2011 +0100 @@ -43,8 +43,6 @@ : INDUCTIVE_PACKAGE = struct -open Ind_Syntax; - val co_prefix = if coind then "co" else ""; @@ -84,7 +82,7 @@ (fn a => "Base name of recursive set not an identifier: " ^ a); local (*Checking the introduction rules*) - val intr_sets = map (#2 o rule_concl_msg thy) intr_tms; + val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms; fun intr_ok set = case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false; in @@ -109,16 +107,16 @@ (*Makes a disjunct from an introduction rule*) fun fp_part intr = (*quantify over rule's free vars except parameters*) let val prems = map dest_tprop (Logic.strip_imp_prems intr) - val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds + val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr) - val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr)) + val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr)) in List.foldr FOLogic.mk_exists (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees end; (*The Part(A,h) terms -- compose injections to make h*) - fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) - | mk_Part h = @{const Part} $ Free(X',iT) $ Abs(w',iT,h); + fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*) + | mk_Part h = @{const Part} $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h); (*Access to balanced disjoint sums via injections*) val parts = map mk_Part @@ -128,9 +126,10 @@ (*replace each set by the corresponding Part(A,h)*) val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms; - val fp_abs = absfree(X', iT, - mk_Collect(z', dom_sum, - Balanced_Tree.make FOLogic.mk_disj part_intrs)); + val fp_abs = + absfree (X', Ind_Syntax.iT, + Ind_Syntax.mk_Collect (z', dom_sum, + Balanced_Tree.make FOLogic.mk_disj part_intrs)); val fp_rhs = Fp.oper $ dom_sum $ fp_abs @@ -161,7 +160,7 @@ (case parts of [_] => [] (*no mutual recursion*) | _ => rec_tms ~~ (*define the sets as Parts*) - map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); + map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts)); (*tracing: print the fixedpoint definition*) val dummy = if !Ind_Syntax.trace then