# HG changeset patch # User wenzelm # Date 1294421539 -3600 # Node ID 7339f0e7c513bd45bdf61b698e53064602f0fee3 # Parent 72ba43b47c7fccce2713e06db8b714a5ff82c2c4 do not open ML structures; diff -r 72ba43b47c7f -r 7339f0e7c513 src/HOL/Hoare/hoare_tac.ML --- 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; diff -r 72ba43b47c7f -r 7339f0e7c513 src/Sequents/modal.ML --- 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 "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