--- 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;
--- 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
--- 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.
--- 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 $!;
}
}
--- 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;
--- 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
--- 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"
--- 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)]]
--- 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
--- 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
--- 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 _ =
--- 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 *)
--- 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)
--- 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
--- 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 *)
--- 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_<int>" *)
- 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_<int>" *)
+ 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;
--- 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))
--- 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;
--- 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;
--- 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;
--- 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;
--- 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<n then all_tac
else tf(i) THEN tac(i-1)
@@ -81,7 +78,7 @@
((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND
(fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1)))));
-fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
+fun solve_tac d = rewrite_goals_tac Modal_Rule.rewrite_rls THEN solven_tac d 1;
fun step_tac n =
COND (has_fewer_prems 1) all_tac
@@ -89,4 +86,3 @@
(fres_unsafe_tac n APPEND fres_bound_tac n));
end;
-end;
--- a/src/Tools/WWW_Find/xhtml.ML Fri Jan 07 18:10:43 2011 +0100
+++ b/src/Tools/WWW_Find/xhtml.ML Fri Jan 07 23:46:06 2011 +0100
@@ -183,7 +183,7 @@
@
(if length inner = 0
then ["/>"]
- 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)
--- 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