--- a/src/HOL/Tools/function_package/context_tree.ML Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML Mon Nov 06 12:04:44 2006 +0100
@@ -55,8 +55,11 @@
(*** Dependency analysis for congruence rules ***)
fun branch_vars t =
- let val (assumes, term) = dest_implies_list (snd (dest_all_all t))
- in (fold (curry add_term_vars) assumes [], term_vars term)
+ let
+ val t' = snd (dest_all_all t)
+ val assumes = Logic.strip_imp_prems t'
+ val concl = Logic.strip_imp_concl t'
+ in (fold (curry add_term_vars) assumes [], term_vars concl)
end
fun cong_deps crule =
@@ -78,9 +81,8 @@
fun mk_branch ctx t =
let
val (ctx', fixes, impl) = dest_all_all_ctx ctx t
- val (assumes, term) = dest_implies_list impl
in
- (ctx', fixes, assumes, rhs_of term)
+ (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
end
fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
--- a/src/HOL/Tools/function_package/fundef_lib.ML Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Nov 06 12:04:44 2006 +0100
@@ -12,29 +12,26 @@
fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
-fun mk_forall (var as Free (v,T)) t =
- all T $ Abs (v,T, abstract_over (var,t))
- | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
-
+fun mk_forall v t = all (fastype_of v) $ lambda v t
(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
fun tupled_lambda vars t =
case vars of
- (Free v) => lambda (Free v) t
- | (Var v) => lambda (Var v) t
- | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
- (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
- | _ => raise Match
-
-
+ (Free v) => lambda (Free v) t
+ | (Var v) => lambda (Var v) t
+ | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
+ (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
+ | _ => raise Match
+
+
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
let
- val (n, body) = Term.dest_abs a
+ val (n, body) = Term.dest_abs a
in
- (Free (n, T), body)
+ (Free (n, T), body)
end
| dest_all _ = raise Match
-
+
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
fun dest_all_all (t as (Const ("all",_) $ _)) =
@@ -63,13 +60,6 @@
(ctx, [], t)
-
-(* unfold *)
-fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
-
-val dest_implies_list =
- split_last o (unfold (can Logic.dest_implies) (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
-
fun implies_elim_swp a b = implies_elim b a
fun map3 _ [] [] [] = []
--- a/src/HOL/Tools/function_package/fundef_prep.ML Sun Nov 05 21:44:42 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Nov 06 12:04:44 2006 +0100
@@ -48,33 +48,31 @@
end
-
-(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
-(* Takes bound form of qglrs tuples *)
-fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+fun mk_compat_proof_obligations domT ranT fvar f glrs =
let
- val shift = incr_boundvars (length qs')
+ fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+ let
+ val shift = incr_boundvars (length qs')
+ in
+ (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
+ $ Trueprop (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')
+ |> curry abstract_over fvar
+ |> curry subst_bound f
+ end
in
- (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
- $ Trueprop (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')
- |> curry abstract_over fvar
- |> curry subst_bound f
+ map mk_impl (unordered_pairs glrs)
end
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
- map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs)
-
-fun mk_completeness globals clauses qglrs =
+fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
let
- val Globals {x, Pbool, ...} = globals
-
- fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool
- |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+ Trueprop Pbool
+ |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
in
Trueprop Pbool
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
@@ -244,15 +242,6 @@
end
-
-
-fun pr (s:string) x =
- let val _ = print s
- in
- x
- end
-
-
fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
let
val Globals {h, y, x, fvar, ...} = globals