--- a/src/HOL/Tools/function_package/fundef_core.ML Mon Jun 23 23:45:48 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jun 23 23:45:49 2008 +0200
@@ -126,10 +126,11 @@
let
val shift = incr_boundvars (length qs')
in
- (implies $ HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs')
- $ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
+ Logic.mk_implies
+ (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
+ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
- |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
+ |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
|> curry abstract_over fvar
|> curry subst_bound f
end
@@ -217,7 +218,7 @@
val h_assum =
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (mk_forall o Free) rcfix
+ |> fold_rev (Logic.all o Free) rcfix
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
|> abstract_over_list (rev qs)
in
@@ -410,10 +411,10 @@
val thy = ProofContext.theory_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
- $ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
- Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
|> cterm_of thy
val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
@@ -458,12 +459,12 @@
fun mk_h_assm (rcfix, rcassm, rcarg) =
HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (mk_forall o Free) rcfix
+ |> fold_rev (Logic.all o Free) rcfix
in
HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
|> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall (fvar :: qs)
+ |> fold_rev Logic.all (fvar :: qs)
end
val G_intros = map2 mk_GIntro clauses RCss
@@ -500,7 +501,7 @@
HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev (mk_forall o Free) rcfix
+ |> fold_rev (Logic.all o Free) rcfix
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
(* "!!qs xs. CS ==> G => (r, lhs) : R" *)
@@ -588,20 +589,21 @@
val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
- val D_subset = cterm_of thy (mk_forall x (implies $ HOLogic.mk_Trueprop (D $ x) $ HOLogic.mk_Trueprop (acc_R $ x)))
+ val D_subset = cterm_of thy (Logic.all x
+ (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
- mk_forall x
- (mk_forall z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
+ Logic.all x
+ (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
HOLogic.mk_Trueprop (D $ z)))))
|> cterm_of thy
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
- $ HOLogic.mk_Trueprop (P $ Bound 0))
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (P $ Bound 0)))
|> cterm_of thy
val aihyp = assume ihyp
@@ -773,9 +775,9 @@
val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ HOLogic.mk_Trueprop (R' $ Bound 0 $ x)
- $ HOLogic.mk_Trueprop (acc_R $ Bound 0))
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (acc_R $ Bound 0)))
|> cterm_of thy
val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
--- a/src/Pure/thm.ML Mon Jun 23 23:45:48 2008 +0200
+++ b/src/Pure/thm.ML Mon Jun 23 23:45:49 2008 +0200
@@ -604,7 +604,7 @@
shyps = Sorts.union sorts shyps,
hyps = OrdList.remove Term.fast_term_ord A hyps,
tpairs = tpairs,
- prop = implies $ A $ prop};
+ prop = Logic.mk_implies (A, prop)};
(*Implication elimination
@@ -653,7 +653,7 @@
shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
- prop = all T $ Abs (a, T, abstract_over (x, prop))};
+ prop = Term.all T $ Abs (a, T, abstract_over (x, prop))};
fun check_occs a x ts =
if exists (fn t => Logic.occs (x, t)) ts then
raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
@@ -1084,7 +1084,7 @@
shyps = sorts,
hyps = [],
tpairs = [],
- prop = implies $ A $ A};
+ prop = Logic.mk_implies (A, A)};
(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
fun class_triv thy c =
@@ -1370,7 +1370,7 @@
introduced by lifting over B, and applies f to remaining part of A*)
fun strip_apply f =
let fun strip(Const("==>",_)$ A1 $ B1,
- Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2)
+ Const("==>",_)$ _ $ B2) = Logic.mk_implies (A1, strip(B1,B2))
| strip((c as Const("all",_)) $ Abs(a,T,t1),
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
| strip(A,_) = f A
@@ -1428,9 +1428,9 @@
val T' = Envir.typ_subst_TVars iTs T
(*Must instantiate types of parameters because they are flattened;
this could be a NEW parameter*)
- in all T' $ Abs(a, T', norm_term_skip env n t) end
+ in Term.all T' $ Abs(a, T', norm_term_skip env n t) end
| norm_term_skip env n (Const("==>", _) $ A $ B) =
- implies $ A $ norm_term_skip env (n-1) B
+ Logic.mk_implies (A, norm_term_skip env (n-1) B)
| norm_term_skip env n t = error"norm_term_skip: too few assumptions??";