--- a/src/HOL/Tools/Function/context_tree.ML Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Sat Apr 16 16:29:13 2011 +0200
@@ -101,29 +101,31 @@
map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
(* Called on the INSTANTIATED branches of the congruence rule *)
-fun mk_branch ctx t =
+fun mk_branch ctxt t =
let
- val ((fixes, impl), ctx') = Function_Lib.focus_term t ctx
+ val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt
val (assms, concl) = Logic.strip_horn impl
in
- (ctx', fixes, assms, rhs_of concl)
+ (ctxt', fixes, assms, rhs_of concl)
end
-fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
- (let
- val thy = Proof_Context.theory_of ctx
+fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
+ (let
+ val thy = Proof_Context.theory_of ctxt
- val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
- val (c, subs) = (concl_of r, prems_of r)
+ val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+ val (c, subs) = (concl_of r, prems_of r)
- val subst = Pattern.match (Proof_Context.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
- val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
- val inst = map (fn v =>
- (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
- in
- (cterm_instantiate inst r, dep, branches)
- end
- handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
+ val subst =
+ Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
+ val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
+ val inst = map (fn v =>
+ (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
+ (Term.add_vars c [])
+ in
+ (cterm_instantiate inst r, dep, branches)
+ end
+ handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
| find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
@@ -137,18 +139,18 @@
fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
| matchcall _ = NONE
- fun mk_tree' ctx t =
+ fun mk_tree' ctxt t =
case matchcall t of
- SOME arg => RCall (t, mk_tree' ctx arg)
+ SOME arg => RCall (t, mk_tree' ctxt arg)
| NONE =>
if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
else
let
- val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t
- fun subtree (ctx', fixes, assumes, st) =
+ val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
+ fun subtree (ctxt', fixes, assumes, st) =
((fixes,
- map (Thm.assume o cterm_of (Proof_Context.theory_of ctx)) assumes),
- mk_tree' ctx' st)
+ map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
+ mk_tree' ctxt' st)
in
Cong (r, dep, map subtree branches)
end
@@ -216,24 +218,24 @@
fun traverse_tree rcOp tr =
let
- fun traverse_help ctx (Leaf _) _ x = ([], x)
- | traverse_help ctx (RCall (t, st)) u x =
- rcOp ctx t u (traverse_help ctx st u x)
- | traverse_help ctx (Cong (_, deps, branches)) u x =
- let
- fun sub_step lu i x =
+ fun traverse_help ctxt (Leaf _) _ x = ([], x)
+ | traverse_help ctxt (RCall (t, st)) u x =
+ rcOp ctxt t u (traverse_help ctxt st u x)
+ | traverse_help ctxt (Cong (_, deps, branches)) u x =
let
- val (ctx', subtree) = nth branches i
- val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
- val (subs, x') = traverse_help (compose ctx ctx') subtree used x
- val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *)
+ fun sub_step lu i x =
+ let
+ val (ctxt', subtree) = nth branches i
+ val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
+ val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
+ val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
+ in
+ (exported_subs, x')
+ end
in
- (exported_subs, x')
+ fold_deps deps sub_step x
+ |> apfst flat
end
- in
- fold_deps deps sub_step x
- |> apfst flat
- end
in
snd o traverse_help ([], []) tr []
end
--- a/src/HOL/Tools/Function/function_core.ML Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Sat Apr 16 16:29:13 2011 +0200
@@ -489,7 +489,7 @@
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
let
val f_def =
- Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
+ Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
in
@@ -726,7 +726,7 @@
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = (u @ sub)
- |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
+ |> map (fn (ctxt, thm) => Function_Ctx_Tree.export_thm thy ctxt thm)
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
--- a/src/HOL/Tools/Function/pattern_split.ML Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Sat Apr 16 16:29:13 2011 +0200
@@ -18,15 +18,15 @@
open Function_Lib
-fun new_var ctx vs T =
+fun new_var ctxt vs T =
let
- val [v] = Variable.variant_frees ctx vs [("v", T)]
+ val [v] = Variable.variant_frees ctxt vs [("v", T)]
in
(Free v :: vs, Free v)
end
-fun saturate ctx vs t =
- fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
+fun saturate ctxt vs t =
+ fold (fn T => fn (vs, t) => new_var ctxt vs T |> apsnd (curry op $ t))
(binder_types (fastype_of t)) (vs, t)
@@ -43,77 +43,77 @@
exception DISJ
-fun pattern_subtract_subst ctx vs t t' =
+fun pattern_subtract_subst ctxt vs t t' =
let
exception DISJ
fun pattern_subtract_subst_aux vs _ (Free v2) = []
| pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
- let
- fun foo constr =
let
- val (vs', t) = saturate ctx vs constr
- val substs = pattern_subtract_subst ctx vs' t t'
+ fun foo constr =
+ let
+ val (vs', t) = saturate ctxt vs constr
+ val substs = pattern_subtract_subst ctxt vs' t t'
+ in
+ map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+ end
in
- map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+ maps foo (inst_constrs_of (Proof_Context.theory_of ctxt) T)
end
- in
- maps foo (inst_constrs_of (Proof_Context.theory_of ctx) T)
- end
| pattern_subtract_subst_aux vs t t' =
- let
- val (C, ps) = strip_comb t
- val (C', qs) = strip_comb t'
- in
- if C = C'
- then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
- else raise DISJ
- end
+ let
+ val (C, ps) = strip_comb t
+ val (C', qs) = strip_comb t'
+ in
+ if C = C'
+ then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
+ else raise DISJ
+ end
in
pattern_subtract_subst_aux vs t t'
handle DISJ => [(vs, [])]
end
(* p - q *)
-fun pattern_subtract ctx eq2 eq1 =
+fun pattern_subtract ctxt eq2 eq1 =
let
- val thy = Proof_Context.theory_of ctx
+ val thy = Proof_Context.theory_of ctxt
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
- val substs = pattern_subtract_subst ctx vs lhs1 lhs2
+ val substs = pattern_subtract_subst ctxt vs lhs1 lhs2
fun instantiate (vs', sigma) =
let
val t = Pattern.rewrite_term thy sigma [] feq1
in
- fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
+ fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctxt t))) t
end
in
map instantiate substs
end
(* ps - p' *)
-fun pattern_subtract_from_many ctx p'=
- maps (pattern_subtract ctx p')
+fun pattern_subtract_from_many ctxt p'=
+ maps (pattern_subtract ctxt p')
(* in reverse order *)
-fun pattern_subtract_many ctx ps' =
- fold_rev (pattern_subtract_from_many ctx) ps'
+fun pattern_subtract_many ctxt ps' =
+ fold_rev (pattern_subtract_from_many ctxt) ps'
-fun split_some_equations ctx eqns =
+fun split_some_equations ctxt eqns =
let
fun split_aux prev [] = []
| split_aux prev ((true, eq) :: es) =
- pattern_subtract_many ctx prev [eq] :: split_aux (eq :: prev) es
+ pattern_subtract_many ctxt prev [eq] :: split_aux (eq :: prev) es
| split_aux prev ((false, eq) :: es) =
- [eq] :: split_aux (eq :: prev) es
+ [eq] :: split_aux (eq :: prev) es
in
split_aux [] eqns
end
-fun split_all_equations ctx =
- split_some_equations ctx o map (pair true)
+fun split_all_equations ctxt =
+ split_some_equations ctxt o map (pair true)
end