--- a/src/HOL/Hoare/hoare_tac.ML Fri Jan 07 18:07:27 2011 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Fri Jan 07 18:32:19 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/Sequents/modal.ML Fri Jan 07 18:07:27 2011 +0100
+++ b/src/Sequents/modal.ML Fri Jan 07 18:32:19 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/ZF/Tools/inductive_package.ML Fri Jan 07 18:07:27 2011 +0100
+++ b/src/ZF/Tools/inductive_package.ML Fri Jan 07 18:32:19 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