--- a/src/HOL/Tools/function_package/context_tree.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML Tue Nov 07 22:06:32 2006 +0100
@@ -55,7 +55,7 @@
(*** Dependency analysis for congruence rules ***)
fun branch_vars t =
- let
+ let
val t' = snd (dest_all_all t)
val assumes = Logic.strip_imp_prems t'
val concl = Logic.strip_imp_concl t'
@@ -64,13 +64,13 @@
fun cong_deps crule =
let
- val branches = map branch_vars (prems_of crule)
- val num_branches = (1 upto (length branches)) ~~ branches
+ val branches = map branch_vars (prems_of crule)
+ val num_branches = (1 upto (length branches)) ~~ branches
in
- IntGraph.empty
- |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
- |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
- (product num_branches num_branches)
+ IntGraph.empty
+ |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
+ |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+ (product num_branches num_branches)
end
val add_congs = map (fn c => c RS eq_reflection) [cong, ext]
@@ -80,7 +80,7 @@
(* Called on the INSTANTIATED branches of the congruence rule *)
fun mk_branch ctx t =
let
- val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+ val (ctx', fixes, impl) = dest_all_all_ctx ctx t
in
(ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
end
@@ -96,7 +96,7 @@
val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
in
- (cterm_instantiate inst r, dep, branches)
+ (cterm_instantiate inst r, dep, branches)
end
handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
| find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
@@ -111,13 +111,13 @@
| 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 t in
- Cong (t, r, dep,
+ let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
+ Cong (t, r, dep,
map (fn (ctx', fixes, assumes, st) =>
- (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes,
+ (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes,
mk_tree congs fvar h ctx' st)) branches)
- end
-
+ end
+
fun inst_tree thy fvar f tr =
let
@@ -142,7 +142,7 @@
-(* FIXME: remove *)
+(* FIXME: remove *)
fun add_context_varnames (Leaf _) = I
| add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub
| add_context_varnames (RCall (_,st)) = add_context_varnames st
@@ -164,30 +164,30 @@
fun assume_in_ctxt thy (fixes, athms) prop =
let
- val global_assum = export_term (fixes, map prop_of athms) prop
+ val global_assum = export_term (fixes, map prop_of athms) prop
in
- (global_assum,
- assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
+ (global_assum,
+ assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
end
(* folds in the order of the dependencies of a graph. *)
fun fold_deps G f x =
let
- fun fill_table i (T, x) =
- case Inttab.lookup T i of
- SOME _ => (T, x)
- | NONE =>
- let
- val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
- val (v, x'') = f (the o Inttab.lookup T') i x
- in
- (Inttab.update (i, v) T', x'')
- end
+ fun fill_table i (T, x) =
+ case Inttab.lookup T i of
+ SOME _ => (T, x)
+ | NONE =>
+ let
+ val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
+ val (v, x'') = f (the o Inttab.lookup T') i x
+ in
+ (Inttab.update (i, v) T', x'')
+ end
- val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
+ val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
in
- (Inttab.fold (cons o snd) T [], x)
+ (Inttab.fold (cons o snd) T [], x)
end
@@ -195,26 +195,26 @@
fun traverse_tree rcOp tr x =
let
- fun traverse_help ctx (Leaf _) u x = ([], x)
- | traverse_help ctx (RCall (t, st)) u x =
- rcOp ctx t u (traverse_help ctx st u x)
- | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
- let
- fun sub_step lu i x =
- let
- val (fixes, assumes, subtree) = nth branches (i - 1)
- val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
- val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
- val exported_subs = map (apfst (compose (fixes, assumes))) subs
- in
- (exported_subs, x')
- end
- in
- fold_deps deps sub_step x
- |> apfst flatten
- end
+ fun traverse_help ctx (Leaf _) u x = ([], x)
+ | traverse_help ctx (RCall (t, st)) u x =
+ rcOp ctx t u (traverse_help ctx st u x)
+ | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
+ let
+ fun sub_step lu i x =
+ let
+ val (fixes, assumes, subtree) = nth branches (i - 1)
+ val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
+ val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
+ val exported_subs = map (apfst (compose (fixes, assumes))) subs
+ in
+ (exported_subs, x')
+ end
+ in
+ fold_deps deps sub_step x
+ |> apfst flatten
+ end
in
- snd (traverse_help ([], []) tr [] x)
+ snd (traverse_help ([], []) tr [] x)
end
@@ -222,48 +222,47 @@
fun rewrite_by_tree thy h ih x tr =
let
- fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
- | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
- let
- val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
-
- (* Need not use the simplifier here. Can use primitive steps! *)
- val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
-
- val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
- val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
- |> rew_ha
-
- val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
- val eq = implies_elim (implies_elim inst_ih lRi) iha
-
- val h_a'_eq_f_a' = eq RS eq_reflection
- val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
- in
- (result, x')
- end
- | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
- let
- fun sub_step lu i x =
- let
- val (fixes, assumes, st) = nth branches (i - 1)
- val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
- val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
- val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
-
- val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
- val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
- in
- (subeq_exp, x')
- end
-
- val (subthms, x') = fold_deps deps sub_step x
- in
- (fold_rev (curry op COMP) subthms crule, x')
- end
-
+ fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
+ | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+ let
+ val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
+
+ (* Need not use the simplifier here. Can use primitive steps! *)
+ val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
+
+ val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
+ val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+ |> rew_ha
+
+ val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+ val eq = implies_elim (implies_elim inst_ih lRi) iha
+
+ val h_a'_eq_f_a' = eq RS eq_reflection
+ val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+ in
+ (result, x')
+ end
+ | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
+ let
+ fun sub_step lu i x =
+ let
+ val (fixes, assumes, st) = nth branches (i - 1)
+ val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
+ val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
+ val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+
+ val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+ val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
+ in
+ (subeq_exp, x')
+ end
+
+ val (subthms, x') = fold_deps deps sub_step x
+ in
+ (fold_rev (curry op COMP) subthms crule, x')
+ end
in
- rewrite_help [] [] [] x tr
+ rewrite_help [] [] [] x tr
end
-
+
end
--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Nov 07 22:06:32 2006 +0100
@@ -97,35 +97,35 @@
datatype mutual_part =
MutualPart of
- {
- fvar : string * typ,
- cargTs: typ list,
- pthA: SumTools.sum_path,
- pthR: SumTools.sum_path,
- f_def: term,
+ {
+ fvar : string * typ,
+ cargTs: typ list,
+ pthA: SumTools.sum_path,
+ pthR: SumTools.sum_path,
+ f_def: term,
- f: term option,
- f_defthm : thm option
- }
-
+ f: term option,
+ f_defthm : thm option
+ }
+
datatype mutual_info =
Mutual of
- {
- defname: string,
- fsum_var : string * typ,
+ {
+ defname: string,
+ fsum_var : string * typ,
- ST: typ,
- RST: typ,
- streeA: SumTools.sum_tree,
- streeR: SumTools.sum_tree,
+ ST: typ,
+ RST: typ,
+ streeA: SumTools.sum_tree,
+ streeR: SumTools.sum_tree,
- parts: mutual_part list,
- fqgars: qgar list,
- qglrs: ((string * typ) list * term list * term * term) list,
+ parts: mutual_part list,
+ fqgars: qgar list,
+ qglrs: ((string * typ) list * term list * term * term) list,
- fsum : term option
- }
+ fsum : term option
+ }
datatype prep_result =
@@ -299,12 +299,12 @@
(* with explicit types: Needed with loose bounds *)
fun mk_relmemT xT yT (x,y) R =
let
- val pT = HOLogic.mk_prodT (xT, yT)
- val RT = HOLogic.mk_setT pT
+ val pT = HOLogic.mk_prodT (xT, yT)
+ val RT = HOLogic.mk_setT pT
in
- Const ("op :", [pT, RT] ---> boolT)
- $ (HOLogic.pair_const xT yT $ x $ y)
- $ R
+ Const ("op :", [pT, RT] ---> boolT)
+ $ (HOLogic.pair_const xT yT $ x $ y)
+ $ R
end
fun free_to_var (Free (v,T)) = Var ((v,0),T)
--- a/src/HOL/Tools/function_package/fundef_lib.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Tue Nov 07 22:06:32 2006 +0100
@@ -17,18 +17,18 @@
(* 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
+ (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))
+ (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
@@ -36,10 +36,10 @@
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
fun dest_all_all (t as (Const ("all",_) $ _)) =
let
- val (v,b) = dest_all t
- val (vs, b') = dest_all_all b
+ val (v,b) = dest_all t
+ val (vs, b') = dest_all_all b
in
- (v :: vs, b')
+ (v :: vs, b')
end
| dest_all_all t = ([],t)
@@ -54,7 +54,7 @@
val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
in
- (ctx'', (n', T) :: vs, bd)
+ (ctx'', (n', T) :: vs, bd)
end
| dest_all_all_ctx ctx t =
(ctx, [], t)
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 22:06:32 2006 +0100
@@ -146,7 +146,7 @@
in
lthy
|> ProofContext.note_thmss_i [(("termination",
- [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
+ [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
|> Proof.theorem_i PureThy.internalK NONE
(total_termination_afterqed name data) NONE ("", [])
[(("", []), [(goal, [])])]
--- a/src/HOL/Tools/function_package/fundef_prep.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Tue Nov 07 22:06:32 2006 +0100
@@ -465,8 +465,7 @@
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
let
- fun inst_term t =
- subst_bound(f, abstract_over (fvar, t))
+ fun inst_term t = subst_bound(f, abstract_over (fvar, t))
in
(rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
end
--- a/src/HOL/Tools/function_package/fundef_proof.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Tue Nov 07 22:06:32 2006 +0100
@@ -11,7 +11,7 @@
sig
val mk_partial_rules : theory -> FundefCommon.prep_result
- -> thm -> FundefCommon.fundef_result
+ -> thm -> FundefCommon.fundef_result
end
@@ -43,128 +43,128 @@
fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
let
- val Globals {domT, z, ...} = globals
+ val Globals {domT, z, ...} = globals
- val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
- val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
+ val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
- ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
- |> (fn it => it COMP graph_is_function)
- |> implies_intr z_smaller
- |> forall_intr (cterm_of thy z)
- |> (fn it => it COMP valthm)
- |> implies_intr lhs_acc
- |> asm_simplify (HOL_basic_ss addsimps [f_iff])
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
+ |> (fn it => it COMP graph_is_function)
+ |> implies_intr z_smaller
+ |> forall_intr (cterm_of thy z)
+ |> (fn it => it COMP valthm)
+ |> implies_intr lhs_acc
+ |> asm_simplify (HOL_basic_ss addsimps [f_iff])
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
- val Globals {domT, x, z, a, P, D, ...} = globals
+ val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
- val x_D = assume (cterm_of thy (Trueprop (D $ x)))
- val a_D = cterm_of thy (Trueprop (D $ a))
+ val x_D = assume (cterm_of thy (Trueprop (D $ x)))
+ val a_D = cterm_of thy (Trueprop (D $ a))
- val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
+ val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ 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 (Trueprop (D $ x),
- Logic.mk_implies (Trueprop (R $ z $ x),
- Trueprop (D $ z)))))
- |> cterm_of thy
+ val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+ mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
+ Logic.mk_implies (Trueprop (R $ z $ x),
+ Trueprop (D $ z)))))
+ |> cterm_of thy
- (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R $ Bound 0 $ x)
- $ Trueprop (P $ Bound 0))
- |> cterm_of thy
-
- val aihyp = assume ihyp
+ (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ val ihyp = all domT $ Abs ("z", domT,
+ implies $ Trueprop (R $ Bound 0 $ x)
+ $ Trueprop (P $ Bound 0))
+ |> cterm_of thy
- fun prove_case clause =
- let
- val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs,
- qglr = (oqs, _, _, _), ...} = clause
-
- val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
- val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
- val sih = full_simplify replace_x_ss aihyp
-
- fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
- sih |> forall_elim (cterm_of thy rcarg)
- |> implies_elim_swp llRI
- |> fold_rev (implies_intr o cprop_of) CCas
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+ val aihyp = assume ihyp
- val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
-
- val step = Trueprop (P $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
- |> fold_rev (curry Logic.mk_implies) gs
- |> curry Logic.mk_implies (Trueprop (D $ lhs))
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
-
- val P_lhs = assume step
- |> fold forall_elim cqs
- |> implies_elim_swp lhs_D
- |> fold_rev implies_elim_swp ags
- |> fold implies_elim_swp P_recs
-
- val res = cterm_of thy (Trueprop (P $ x))
- |> Simplifier.rewrite replace_x_ss
- |> symmetric (* P lhs == P x *)
- |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
- in
- (res, step)
- end
-
- val (cases, steps) = split_list (map prove_case clauses)
+ fun prove_case clause =
+ let
+ val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs,
+ qglr = (oqs, _, _, _), ...} = clause
+
+ val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
+ val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
+ val sih = full_simplify replace_x_ss aihyp
+
+ fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
+ sih |> forall_elim (cterm_of thy rcarg)
+ |> implies_elim_swp llRI
+ |> fold_rev (implies_intr o cprop_of) CCas
+ |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+
+ val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
+
+ val step = Trueprop (P $ lhs)
+ |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> curry Logic.mk_implies (Trueprop (D $ lhs))
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ |> cterm_of thy
+
+ val P_lhs = assume step
+ |> fold forall_elim cqs
+ |> implies_elim_swp lhs_D
+ |> fold_rev implies_elim_swp ags
+ |> fold implies_elim_swp P_recs
+
+ val res = cterm_of thy (Trueprop (P $ x))
+ |> Simplifier.rewrite replace_x_ss
+ |> symmetric (* P lhs == P x *)
+ |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
+ in
+ (res, step)
+ end
- val istep = complete_thm
- |> forall_elim_vars 0
- |> fold (curry op COMP) cases (* P x *)
- |> implies_intr ihyp
- |> implies_intr (cprop_of x_D)
- |> forall_intr (cterm_of thy x)
-
- val subset_induct_rule =
- acc_subset_induct
- |> (curry op COMP) (assume D_subset)
- |> (curry op COMP) (assume D_dcl)
- |> (curry op COMP) (assume a_D)
- |> (curry op COMP) istep
- |> fold_rev implies_intr steps
- |> implies_intr a_D
- |> implies_intr D_dcl
- |> implies_intr D_subset
+ val (cases, steps) = split_list (map prove_case clauses)
- val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+ val istep = complete_thm
+ |> forall_elim_vars 0
+ |> fold (curry op COMP) cases (* P x *)
+ |> implies_intr ihyp
+ |> implies_intr (cprop_of x_D)
+ |> forall_intr (cterm_of thy x)
+
+ val subset_induct_rule =
+ acc_subset_induct
+ |> (curry op COMP) (assume D_subset)
+ |> (curry op COMP) (assume D_dcl)
+ |> (curry op COMP) (assume a_D)
+ |> (curry op COMP) istep
+ |> fold_rev implies_intr steps
+ |> implies_intr a_D
+ |> implies_intr D_dcl
+ |> implies_intr D_subset
- val simple_induct_rule =
- subset_induct_rule
- |> forall_intr (cterm_of thy D)
- |> forall_elim (cterm_of thy acc_R)
- |> assume_tac 1 |> Seq.hd
- |> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (ctyp_of thy domT)]
- (map (SOME o cterm_of thy) [R, x, z]))
- |> forall_intr (cterm_of thy z)
- |> forall_intr (cterm_of thy x))
- |> forall_intr (cterm_of thy a)
- |> forall_intr (cterm_of thy P)
+ val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+
+ val simple_induct_rule =
+ subset_induct_rule
+ |> forall_intr (cterm_of thy D)
+ |> forall_elim (cterm_of thy acc_R)
+ |> assume_tac 1 |> Seq.hd
+ |> (curry op COMP) (acc_downward
+ |> (instantiate' [SOME (ctyp_of thy domT)]
+ (map (SOME o cterm_of thy) [R, x, z]))
+ |> forall_intr (cterm_of thy z)
+ |> forall_intr (cterm_of thy x))
+ |> forall_intr (cterm_of thy a)
+ |> forall_intr (cterm_of thy P)
in
- (subset_induct_all, simple_induct_rule)
+ (subset_induct_all, simple_induct_rule)
end
@@ -172,19 +172,19 @@
(* Does this work with Guards??? *)
fun mk_domain_intro thy globals R R_cases clause =
let
- val Globals {z, domT, ...} = globals
- val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
- qglr = (oqs, _, _, _), ...} = clause
- val goal = Trueprop (mk_acc domT R $ lhs)
- |> fold_rev (curry Logic.mk_implies) gs
- |> cterm_of thy
+ val Globals {z, domT, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
+ qglr = (oqs, _, _, _), ...} = clause
+ val goal = Trueprop (mk_acc domT R $ lhs)
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> cterm_of thy
in
- Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (CLASIMPSET auto_tac)) |> the
- |> Goal.conclude
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ Goal.init goal
+ |> (SINGLE (resolve_tac [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (CLASIMPSET auto_tac)) |> the
+ |> Goal.conclude
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
@@ -192,145 +192,145 @@
fun mk_nest_term_case thy globals R' ihyp clause =
let
- val Globals {x, z, ...} = globals
- val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
- qglr=(oqs, _, _, _), ...} = clause
-
- val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
-
- fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
- let
- val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
-
- val hyp = Trueprop (R' $ arg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) used
- |> FundefCtxTree.export_term (fixes, map prop_of assumes)
- |> fold_rev (curry Logic.mk_implies o prop_of) ags
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
-
- val thm = assume hyp
- |> fold forall_elim cqs
- |> fold implies_elim_swp ags
- |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
- |> fold implies_elim_swp used
-
- val acc = thm COMP ih_case
+ val Globals {x, z, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
+ qglr=(oqs, _, _, _), ...} = clause
+
+ val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+
+ fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
+ let
+ val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
+
+ val hyp = Trueprop (R' $ arg $ lhs)
+ |> fold_rev (curry Logic.mk_implies o prop_of) used
+ |> FundefCtxTree.export_term (fixes, map prop_of assumes)
+ |> fold_rev (curry Logic.mk_implies o prop_of) ags
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ |> cterm_of thy
+
+ val thm = assume hyp
+ |> fold forall_elim cqs
+ |> fold implies_elim_swp ags
+ |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
+ |> fold implies_elim_swp used
+
+ val acc = thm COMP ih_case
+
+ val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
+
+ val arg_eq_z = (assume z_eq_arg) RS sym
+
+ val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
+ |> implies_intr (cprop_of case_hyp)
+ |> implies_intr z_eq_arg
- val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
-
- val arg_eq_z = (assume z_eq_arg) RS sym
-
- val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
- |> implies_intr (cprop_of case_hyp)
- |> implies_intr z_eq_arg
-
- val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
- val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
+ val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+
+ val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
+ |> FundefCtxTree.export_thm thy (fixes,
+ prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
- val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
- |> FundefCtxTree.export_thm thy (fixes,
- prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-
- val sub' = sub @ [(([],[]), acc)]
- in
- (sub', (hyp :: hyps, ethm :: thms))
- end
- | step _ _ _ _ = raise Match
+ val sub' = sub @ [(([],[]), acc)]
+ in
+ (sub', (hyp :: hyps, ethm :: thms))
+ end
+ | step _ _ _ _ = raise Match
in
- FundefCtxTree.traverse_tree step tree
+ FundefCtxTree.traverse_tree step tree
end
-
-
+
+
fun mk_nest_term_rule thy globals R R_cases clauses =
let
- val Globals { domT, x, z, ... } = globals
- val acc_R = mk_acc domT R
-
- val R' = Free ("R", fastype_of R)
-
- val Rrel = Free ("R", mk_relT (domT, domT))
- val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
-
- val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+ val Globals { domT, x, z, ... } = globals
+ val acc_R = mk_acc domT R
+
+ val R' = Free ("R", fastype_of R)
+
+ val Rrel = Free ("R", mk_relT (domT, domT))
+ val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
+
+ val wfR' = cterm_of thy (Trueprop (Const ("FunDef.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 $ Trueprop (R' $ Bound 0 $ x)
+ $ Trueprop (acc_R $ Bound 0))
+ |> cterm_of thy
- (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
- val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R' $ Bound 0 $ x)
- $ Trueprop (acc_R $ Bound 0))
- |> cterm_of thy
-
- val ihyp_a = assume ihyp |> forall_elim_vars 0
-
- val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
-
- val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
+ val ihyp_a = assume ihyp |> forall_elim_vars 0
+
+ val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
+
+ val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
in
- R_cases
- |> forall_elim (cterm_of thy z)
- |> forall_elim (cterm_of thy x)
- |> forall_elim (cterm_of thy (acc_R $ z))
- |> curry op COMP (assume R_z_x)
- |> fold_rev (curry op COMP) cases
- |> implies_intr R_z_x
- |> forall_intr (cterm_of thy z)
- |> (fn it => it COMP accI)
- |> implies_intr ihyp
- |> forall_intr (cterm_of thy x)
- |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
- |> curry op RS (assume wfR')
- |> fold implies_intr hyps
- |> implies_intr wfR'
- |> forall_intr (cterm_of thy R')
- |> forall_elim (cterm_of thy (inrel_R))
- |> curry op RS wf_in_rel
- |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
- |> forall_intr (cterm_of thy Rrel)
+ R_cases
+ |> forall_elim (cterm_of thy z)
+ |> forall_elim (cterm_of thy x)
+ |> forall_elim (cterm_of thy (acc_R $ z))
+ |> curry op COMP (assume R_z_x)
+ |> fold_rev (curry op COMP) cases
+ |> implies_intr R_z_x
+ |> forall_intr (cterm_of thy z)
+ |> (fn it => it COMP accI)
+ |> implies_intr ihyp
+ |> forall_intr (cterm_of thy x)
+ |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+ |> curry op RS (assume wfR')
+ |> fold implies_intr hyps
+ |> implies_intr wfR'
+ |> forall_intr (cterm_of thy R')
+ |> forall_elim (cterm_of thy (inrel_R))
+ |> curry op RS wf_in_rel
+ |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
+ |> forall_intr (cterm_of thy Rrel)
end
-
+
fun mk_partial_rules thy data provedgoal =
let
- val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
-
- val _ = print "Closing Derivation"
-
- val provedgoal = Drule.close_derivation provedgoal
-
- val _ = print "Getting gif"
-
- val graph_is_function = (provedgoal COMP conjunctionD1)
- |> forall_elim_vars 0
-
- val _ = print "Getting cases"
-
- val complete_thm = provedgoal COMP conjunctionD2
-
- val _ = print "making f_iff"
-
- val f_iff = (graph_is_function RS ex1_iff)
-
- val _ = Output.debug "Proving simplification rules"
- val psimps = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
-
- val _ = Output.debug "Proving partial induction rule"
- val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
-
- val _ = Output.debug "Proving nested termination rule"
- val total_intro = mk_nest_term_rule thy globals R R_cases clauses
-
- val _ = Output.debug "Proving domain introduction rules"
- val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
+ val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
+
+ val _ = Output.debug "Closing Derivation"
+
+ val provedgoal = Drule.close_derivation provedgoal
+
+ val _ = Output.debug "Getting function theorem"
+
+ val graph_is_function = (provedgoal COMP conjunctionD1)
+ |> forall_elim_vars 0
+
+ val _ = Output.debug "Getting cases"
+
+ val complete_thm = provedgoal COMP conjunctionD2
+
+ val _ = Output.debug "Making f_iff"
+
+ val f_iff = (graph_is_function RS ex1_iff)
+
+ val _ = Output.debug "Proving simplification rules"
+ val psimps = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
+
+ val _ = Output.debug "Proving partial induction rule"
+ val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
+
+ val _ = Output.debug "Proving nested termination rule"
+ val total_intro = mk_nest_term_rule thy globals R R_cases clauses
+
+ val _ = Output.debug "Proving domain introduction rules"
+ val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
in
- FundefResult {f=f, G=G, R=R, completeness=complete_thm,
- psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
- dom_intros=dom_intros}
+ FundefResult {f=f, G=G, R=R, completeness=complete_thm,
+ psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
+ dom_intros=dom_intros}
end
-
-
+
+
end
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Tue Nov 07 22:06:32 2006 +0100
@@ -3,21 +3,8 @@
Author: Alexander Krauss, TU Muenchen
-This is a wrapper around the inductive package which corrects some of its
-slightly annoying behaviours and makes the whole business more controllable.
-
-Specifically:
-
-- Following newer Isar conventions, declaration and definition are done in one step
-
-- The specification is expected in fully quantified form. This allows the client to
- control the variable order. The variables will appear in the result in the same order.
- This is especially relevant for the elimination rule, where the order usually *does* matter.
-
-
-All this will probably become obsolete in the near future, when the new "predicate" package
-is in place.
-
+A wrapper around the inductive package, restoring the quantifiers in
+the introduction and elimination rules.
*)
signature FUNDEF_INDUCTIVE_WRAP =
@@ -36,7 +23,7 @@
let
val thy = theory_of_thm thm
val frees = frees_in_term ctxt t
- |> remove (op =) lfix
+ |> remove (op =) lfix
val vars = Term.add_vars (prop_of thm) [] |> rev
val varmap = frees ~~ vars
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Tue Nov 07 22:06:32 2006 +0100
@@ -7,8 +7,8 @@
signature LEXICOGRAPHIC_ORDER =
sig
- val lexicographic_order : Method.method
- val setup: theory -> theory
+ val lexicographic_order : Method.method
+ val setup: theory -> theory
end
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
@@ -19,222 +19,222 @@
val wf_measures = thm "wf_measures"
val measures_less = thm "measures_less"
val measures_lesseq = thm "measures_lesseq"
-
+
fun del_index (n, []) = []
| del_index (n, x :: xs) =
- if n>0 then x :: del_index (n - 1, xs) else xs
+ if n>0 then x :: del_index (n - 1, xs) else xs
fun transpose ([]::_) = []
| transpose xss = map hd xss :: transpose (map tl xss)
fun mk_sum_case (f1, f2) =
case (fastype_of f1, fastype_of f2) of
- (Type("fun", [A, B]), Type("fun", [C, D])) =>
- if (B = D) then
- Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
- else raise TERM ("mk_sum_case: range type mismatch", [f1, f2])
- | _ => raise TERM ("mk_sum_case", [f1, f2])
-
+ (Type("fun", [A, B]), Type("fun", [C, D])) =>
+ if (B = D) then
+ Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
+ else raise TERM ("mk_sum_case: range type mismatch", [f1, f2])
+ | _ => raise TERM ("mk_sum_case", [f1, f2])
+
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
| dest_wf t = raise TERM ("dest_wf", [t])
-
+
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
-
+
fun is_Less cell = case cell of (Less _) => true | _ => false
-
+
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
-
+
fun thm_of_cell cell =
case cell of
- Less thm => thm
- | LessEq thm => thm
- | False thm => thm
- | None thm => thm
-
+ Less thm => thm
+ | LessEq thm => thm
+ | False thm => thm
+ | None thm => thm
+
fun mk_base_fun_bodys (t : term) (tt : typ) =
case tt of
- Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)
- | _ => [(t, tt)]
-
+ Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)
+ | _ => [(t, tt)]
+
fun mk_base_fun_header fulltyp (t, typ) =
if typ = HOLogic.natT then
- Abs ("x", fulltyp, t)
+ Abs ("x", fulltyp, t)
else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
-
+
fun mk_base_funs (tt: typ) =
mk_base_fun_bodys (Bound 0) tt |>
- map (mk_base_fun_header tt)
-
+ map (mk_base_fun_header tt)
+
fun mk_ext_base_funs (tt : typ) =
case tt of
- Type("+", [ft, st]) =>
- product (mk_ext_base_funs ft) (mk_ext_base_funs st)
- |> map mk_sum_case
- | _ => mk_base_funs tt
-
+ Type("+", [ft, st]) =>
+ product (mk_ext_base_funs ft) (mk_ext_base_funs st)
+ |> map mk_sum_case
+ | _ => mk_base_funs tt
+
fun dest_term (t : term) =
let
- val (vars, prop) = (FundefLib.dest_all_all t)
- val prems = Logic.strip_imp_prems prop
- val (tuple, rel) = Logic.strip_imp_concl prop
- |> HOLogic.dest_Trueprop
- |> HOLogic.dest_mem
- val (lhs, rhs) = HOLogic.dest_prod tuple
+ val (vars, prop) = (FundefLib.dest_all_all t)
+ val prems = Logic.strip_imp_prems prop
+ val (tuple, rel) = Logic.strip_imp_concl prop
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_mem
+ val (lhs, rhs) = HOLogic.dest_prod tuple
in
- (vars, prems, lhs, rhs, rel)
+ (vars, prems, lhs, rhs, rel)
end
-
+
fun mk_goal (vars, prems, lhs, rhs) rel =
let
- val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
- in
- Logic.list_implies (prems, concl) |>
- fold_rev FundefLib.mk_forall vars
+ val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
+ in
+ Logic.list_implies (prems, concl) |>
+ fold_rev FundefLib.mk_forall vars
end
-
+
fun prove (thy: theory) (t: term) =
cterm_of thy t |> Goal.init
|> SINGLE (CLASIMPSET auto_tac) |> the
-
+
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) =
- let
- val goals = mk_goal (vars, prems, lhs, rhs)
- val less_thm = goals "Orderings.less" |> prove thy
+ let
+ val goals = mk_goal (vars, prems, lhs, rhs)
+ val less_thm = goals "Orderings.less" |> prove thy
in
- if Thm.no_prems less_thm then
- Less (Goal.finish less_thm)
- else
- let
- val lesseq_thm = goals "Orderings.less_eq" |> prove thy
- in
- if Thm.no_prems lesseq_thm then
- LessEq (Goal.finish lesseq_thm)
- else
- if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
- else None lesseq_thm
- end
+ if Thm.no_prems less_thm then
+ Less (Goal.finish less_thm)
+ else
+ let
+ val lesseq_thm = goals "Orderings.less_eq" |> prove thy
+ in
+ if Thm.no_prems lesseq_thm then
+ LessEq (Goal.finish lesseq_thm)
+ else
+ if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
+ else None lesseq_thm
+ end
end
-
+
fun mk_row (thy: theory) base_funs (t : term) =
let
- val (vars, prems, lhs, rhs, _) = dest_term t
- val lhs_list = map (fn x => x $ lhs) base_funs
- val rhs_list = map (fn x => x $ rhs) base_funs
+ val (vars, prems, lhs, rhs, _) = dest_term t
+ val lhs_list = map (fn x => x $ lhs) base_funs
+ val rhs_list = map (fn x => x $ rhs) base_funs
in
- map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
+ map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
end
-
+
(* simple depth-first search algorithm for the table *)
fun search_table table =
case table of
- [] => SOME []
- | _ =>
- let
- val check_col = forall (fn c => is_Less c orelse is_LessEq c)
- val col = find_index (check_col) (transpose table)
- in case col of
- ~1 => NONE
- | _ =>
- let
- val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
- val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
- in case order_opt of
- NONE => NONE
- | SOME order =>SOME (col::(transform_order col order))
- end
- end
-
+ [] => SOME []
+ | _ =>
+ let
+ val check_col = forall (fn c => is_Less c orelse is_LessEq c)
+ val col = find_index (check_col) (transpose table)
+ in case col of
+ ~1 => NONE
+ | _ =>
+ let
+ val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
+ val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
+ in case order_opt of
+ NONE => NONE
+ | SOME order =>SOME (col::(transform_order col order))
+ end
+ end
+
fun prove_row row (st : thm) =
case row of
- [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)"
- | cell::tail =>
- case cell of
- Less less_thm =>
- let
- val next_thm = st |> SINGLE (rtac measures_less 1) |> the
- in
- implies_elim next_thm less_thm
- end
- | LessEq lesseq_thm =>
- let
- val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
- in
- implies_elim next_thm lesseq_thm |>
- prove_row tail
- end
- | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
-
+ [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)"
+ | cell::tail =>
+ case cell of
+ Less less_thm =>
+ let
+ val next_thm = st |> SINGLE (rtac measures_less 1) |> the
+ in
+ implies_elim next_thm less_thm
+ end
+ | LessEq lesseq_thm =>
+ let
+ val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
+ in
+ implies_elim next_thm lesseq_thm
+ |> prove_row tail
+ end
+ | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
+
fun pr_unprovable_subgoals table =
filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
- |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
-
+ |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
+
fun pr_goal thy t i =
let
- val (_, prems, lhs, rhs, _) = dest_term t
- val prterm = string_of_cterm o (cterm_of thy)
+ val (_, prems, lhs, rhs, _) = dest_term t
+ val prterm = string_of_cterm o (cterm_of thy)
in
- (* also show prems? *)
+ (* also show prems? *)
i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs)
end
-
+
fun pr_fun thy t i =
(string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
-
+
fun pr_cell cell = case cell of Less _ => " < "
- | LessEq _ => " <= "
- | None _ => " N "
- | False _ => " F "
-
+ | LessEq _ => " <= "
+ | None _ => " N "
+ | False _ => " F "
+
(* fun pr_err: prints the table if tactic failed *)
fun pr_err table thy tl base_funs =
let
- val gc = map (fn i => chr (i + 96)) (1 upto (length table))
- val mc = 1 upto (length base_funs)
- val tstr = (" " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ " ") mc))) ::
- (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
- val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
- val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))
- val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
+ val gc = map (fn i => chr (i + 96)) (1 upto (length table))
+ val mc = 1 upto (length base_funs)
+ val tstr = (" " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ " ") mc))) ::
+ (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
+ val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
+ val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))
+ val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
in
- tstr @ gstr @ mstr @ ustr
+ tstr @ gstr @ mstr @ ustr
end
-
+
(* the main function: create table, search table, create relation,
and prove the subgoals *)
fun lexicographic_order_tac (st: thm) =
let
- val thy = theory_of_thm st
- val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
- val next_st = SINGLE (rtac termination_thm 1) st |> the
- val premlist = prems_of next_st
+ val thy = theory_of_thm st
+ val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
+ val next_st = SINGLE (rtac termination_thm 1) st |> the
+ val premlist = prems_of next_st
in
- case premlist of
+ case premlist of
[] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal"
| (wf::tl) => let
- val (var, prop) = FundefLib.dest_all wf
- val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
- val crel = cterm_of thy rel
- val base_funs = mk_ext_base_funs (fastype_of var)
- val _ = writeln "Creating table"
- val table = map (mk_row thy base_funs) tl
- val _ = writeln "Searching for lexicographic order"
- val possible_order = search_table table
- in
- case possible_order of
- NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
- | SOME order => let
- val clean_table = map (fn x => map (nth x) order) table
- val funs = map (nth base_funs) order
- val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
- val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
- val crelterm = cterm_of thy relterm
- val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
- val _ = writeln "Proving subgoals"
- in
- next_st |> cterm_instantiate [(crel, crelterm)]
- |> SINGLE (rtac wf_measures 1) |> the
- |> fold prove_row clean_table
- |> Seq.single
+ val (var, prop) = FundefLib.dest_all wf
+ val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
+ val crel = cterm_of thy rel
+ val base_funs = mk_ext_base_funs (fastype_of var)
+ val _ = writeln "Creating table"
+ val table = map (mk_row thy base_funs) tl
+ val _ = writeln "Searching for lexicographic order"
+ val possible_order = search_table table
+ in
+ case possible_order of
+ NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
+ | SOME order => let
+ val clean_table = map (fn x => map (nth x) order) table
+ val funs = map (nth base_funs) order
+ val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
+ val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
+ val crelterm = cterm_of thy relterm
+ val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
+ val _ = writeln "Proving subgoals"
+ in
+ next_st |> cterm_instantiate [(crel, crelterm)]
+ |> SINGLE (rtac wf_measures 1) |> the
+ |> fold prove_row clean_table
+ |> Seq.single
end
end
end
--- a/src/HOL/Tools/function_package/mutual.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Nov 07 22:06:32 2006 +0100
@@ -50,7 +50,7 @@
fun split_def ctxt fnames geq arities =
let
fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
-
+
val (qs, imp) = open_all_all geq
val gs = Logic.strip_imp_prems imp
@@ -69,7 +69,7 @@
fun add_bvs t is = add_loose_bnos (t, 0, is)
val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
|> map (fst o nth (rev qs))
-
+
val _ = if null rvs then ()
else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
@@ -83,17 +83,17 @@
val k = length args
val arities' = case Symtab.lookup arities fname of
- NONE => Symtab.update (fname, k) arities
- | SOME i => if (i <> k)
- then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
- else arities
+ NONE => Symtab.update (fname, k) arities
+ | SOME i => if (i <> k)
+ then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
+ else arities
in
- ((fname, qs, gs, args, rhs), arities')
+ ((fname, qs, gs, args, rhs), arities')
end
-
+
fun get_part fname =
the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
-
+
(* FIXME *)
fun mk_prod_abs e (t1, t2) =
let
@@ -141,7 +141,7 @@
in
(MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
end
-
+
val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)
fun convert_eqs (f, qs, gs, args, rhs) =
@@ -171,10 +171,10 @@
lthy
in
(MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def,
- f=SOME f, f_defthm=SOME f_defthm },
+ f=SOME f, f_defthm=SOME f_defthm },
lthy')
end
-
+
val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
in
@@ -186,39 +186,39 @@
fun prepare_fundef_mutual fixes eqss default lthy =
let
- val mutual = analyze_eqs lthy (map fst fixes) eqss
- val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
-
- val (prep_result, fsum, lthy') =
- FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
-
- val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
+ val mutual = analyze_eqs lthy (map fst fixes) eqss
+ val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
+
+ val (prep_result, fsum, lthy') =
+ FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
+
+ val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
in
((mutual', defname, prep_result), lthy'')
end
-
+
(* Beta-reduce both sides of a meta-equality *)
fun beta_norm_eq thm =
let
- val (lhs, rhs) = dest_equals (cprop_of thm)
- val lhs_conv = beta_conversion false lhs
- val rhs_conv = beta_conversion false rhs
+ val (lhs, rhs) = dest_equals (cprop_of thm)
+ val lhs_conv = beta_conversion false lhs
+ val rhs_conv = beta_conversion false rhs
in
- transitive (symmetric lhs_conv) (transitive thm rhs_conv)
+ transitive (symmetric lhs_conv) (transitive thm rhs_conv)
end
-
+
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-
-
+
+
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
val thy = ProofContext.theory_of ctxt
-
+
val oqnames = map fst pre_qs
val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
- |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
+ |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+
fun inst t = subst_bounds (rev qs, t)
val gs = map inst pre_gs
val args = map inst pre_args
@@ -240,7 +240,7 @@
fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
let
val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
-
+
val psimp = import sum_psimp_eq
val (simp, restore_cond) = case cprems_of psimp of
[] => (psimp, I)
@@ -275,46 +275,46 @@
|> fold_rev forall_intr xs
|> forall_elim_vars 0
end
-
+
fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
let
val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} =>
- Free (Pname, cargTs ---> HOLogic.boolT))
+ Free (Pname, cargTs ---> HOLogic.boolT))
(mutual_induct_Pnames (length parts))
parts
-
- fun mk_P (MutualPart {cargTs, ...}) P =
- let
- val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
- val atup = foldr1 HOLogic.mk_prod avars
- in
- tupled_lambda atup (list_comb (P, avars))
- end
-
- val Ps = map2 mk_P parts newPs
- val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
-
- val induct_inst =
- forall_elim (cterm_of thy case_exp) induct
- |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
- |> full_simplify (HOL_basic_ss addsimps all_f_defs)
-
- fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
- let
- val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
- val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
- in
- rule
- |> forall_elim (cterm_of thy inj)
- |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
- |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
- end
-
+
+ fun mk_P (MutualPart {cargTs, ...}) P =
+ let
+ val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
+ val atup = foldr1 HOLogic.mk_prod avars
+ in
+ tupled_lambda atup (list_comb (P, avars))
+ end
+
+ val Ps = map2 mk_P parts newPs
+ val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
+
+ val induct_inst =
+ forall_elim (cterm_of thy case_exp) induct
+ |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+ |> full_simplify (HOL_basic_ss addsimps all_f_defs)
+
+ fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
+ let
+ val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
+ val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
+ in
+ rule
+ |> forall_elim (cterm_of thy inj)
+ |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+ |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
+ end
+
in
map (mk_proj induct_inst) parts
end
-
+
@@ -322,44 +322,44 @@
fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
let
val thy = ProofContext.theory_of lthy
-
+
(* FIXME !? *)
- val expand = Assumption.export false lthy (LocalTheory.target_of lthy);
- val expand_term = Drule.term_rule thy expand;
-
+ val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
+ val expand_term = Drule.term_rule thy expand
+
val result = FundefProof.mk_partial_rules thy data prep_result
val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
-
+
val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
parts
-
+
fun mk_mpsimp fqgar sum_psimp =
in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
-
+
val mpsimps = map2 mk_mpsimp fqgars psimps
-
+
val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
in
FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
- psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
- cases=expand completeness, termination=expand termination,
+ psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
+ cases=expand completeness, termination=expand termination,
domintros=map expand dom_intros }
end
-
-
-
+
+
+
(* puts an object in the "right bucket" *)
fun store_grouped P x [] = []
| store_grouped P x ((l, xs)::bs) =
if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
-
+
fun sort_by_function (Mutual {fqgars, ...}) names xs =
- fold_rev (store_grouped (eq_str o apfst fst)) (* fill *)
- (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *)
- (map (rpair []) names) (* in the empty buckets labeled with names *)
-
- |> map (snd #> map snd) (* and remove the labels afterwards *)
-
+ fold_rev (store_grouped (eq_str o apfst fst)) (* fill *)
+ (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *)
+ (map (rpair []) names) (* in the empty buckets labeled with names *)
+
+ |> map (snd #> map snd) (* and remove the labels afterwards *)
+
end
--- a/src/HOL/Tools/function_package/pattern_split.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/pattern_split.ML Tue Nov 07 22:06:32 2006 +0100
@@ -12,10 +12,10 @@
signature FUNDEF_SPLIT =
sig
val split_some_equations :
- Proof.context -> (bool * term) list -> term list list
+ Proof.context -> (bool * term) list -> term list list
val split_all_equations :
- Proof.context -> term list -> term list list
+ Proof.context -> term list -> term list list
end
structure FundefSplit : FUNDEF_SPLIT =
@@ -36,16 +36,16 @@
fun saturate ctx vs t =
fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
(binder_types (fastype_of t)) (vs, t)
-
-
+
+
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
- (the (DatatypePackage.get_datatype_constrs thy name))
+ map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ (the (DatatypePackage.get_datatype_constrs thy name))
| inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
-
-
-
+
+
+
fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
fun join_product (xs, ys) = map join (product xs ys)
@@ -91,12 +91,12 @@
fun pattern_subtract ctx eq2 eq1 =
let
val thy = ProofContext.theory_of ctx
-
+
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
-
+
val substs = pattern_subtract_subst ctx vs lhs1 lhs2
-
+
fun instantiate (vs', sigma) =
let
val t = Pattern.rewrite_term thy sigma [] feq1
@@ -106,7 +106,7 @@
in
map instantiate substs
end
-
+
(* ps - p' *)
fun pattern_subtract_from_many ctx p'=
@@ -128,7 +128,7 @@
in
split_aux [] eqns
end
-
+
fun split_all_equations ctx =
split_some_equations ctx o map (pair true)
--- a/src/HOL/Tools/function_package/sum_tools.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/sum_tools.ML Tue Nov 07 22:06:32 2006 +0100
@@ -46,30 +46,30 @@
| Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
type sum_path = bool list (* true: left, false: right *)
-
+
fun sum_type_of (Leaf T) = T
| sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
-
-
+
+
fun mk_tree Ts =
let
- fun mk_tree' 1 [T] = (T, Leaf T, [[]])
- | mk_tree' n Ts =
- let
- val n2 = n div 2
- val (lTs, rTs) = chop n2 Ts
- val (TL, ltree, lpaths) = mk_tree' n2 lTs
- val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
- val T = mk_sumT TL TR
- val pths = map (cons true) lpaths @ map (cons false) rpaths
- in
- (T, Branch (T, (TL, ltree), (TR, rtree)), pths)
- end
+ fun mk_tree' 1 [T] = (T, Leaf T, [[]])
+ | mk_tree' n Ts =
+ let
+ val n2 = n div 2
+ val (lTs, rTs) = chop n2 Ts
+ val (TL, ltree, lpaths) = mk_tree' n2 lTs
+ val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
+ val T = mk_sumT TL TR
+ val pths = map (cons true) lpaths @ map (cons false) rpaths
+ in
+ (T, Branch (T, (TL, ltree), (TR, rtree)), pths)
+ end
in
- mk_tree' (length Ts) Ts
+ mk_tree' (length Ts) Ts
end
-
-
+
+
fun mk_tree_distinct Ts =
let
fun insert_once T Ts =
@@ -78,9 +78,9 @@
in
if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
end
-
+
val (idxs, dist_Ts) = fold_map insert_once Ts []
-
+
val (ST, tree, pths) = mk_tree dist_Ts
in
(ST, tree, map (nth pths) idxs)
@@ -104,19 +104,19 @@
fun mk_sumcases tree T ts =
let
- fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
- | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
- let
- val (lcase, ts') = mk_sumcases' ltr ts
- val (rcase, ts'') = mk_sumcases' rtr ts'
- in
- (mk_sumcase LT RT T lcase rcase, ts'')
- end
- | mk_sumcases' _ [] = sys_error "mk_sumcases"
+ fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
+ | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
+ let
+ val (lcase, ts') = mk_sumcases' ltr ts
+ val (rcase, ts'') = mk_sumcases' rtr ts'
+ in
+ (mk_sumcase LT RT T lcase rcase, ts'')
+ end
+ | mk_sumcases' _ [] = sys_error "mk_sumcases"
in
- fst (mk_sumcases' tree ts)
+ fst (mk_sumcases' tree ts)
end
-
+
end
--- a/src/HOL/Tools/function_package/termination.ML Tue Nov 07 21:30:03 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Tue Nov 07 22:06:32 2006 +0100
@@ -9,8 +9,8 @@
signature FUNDEF_TERMINATION =
sig
- val mk_total_termination_goal : FundefCommon.result_with_names -> term
- val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+ val mk_total_termination_goal : FundefCommon.result_with_names -> term
+ val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
end
structure FundefTermination : FUNDEF_TERMINATION =
@@ -20,41 +20,40 @@
open FundefLib
open FundefCommon
open FundefAbbrev
-
+
fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
let
- val domT = domain_type (fastype_of f)
- val x = Free ("x", domT)
+ val domT = domain_type (fastype_of f)
+ val x = Free ("x", domT)
in
mk_forall x (Trueprop (mk_acc domT R $ x))
end
-
+
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
let
- val domT = domain_type (fastype_of f)
- val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
- val DT = type_of D
- val idomT = HOLogic.dest_setT DT
-
- val x = Free ("x", idomT)
- val z = Free ("z", idomT)
- val Rname = fst (dest_Const R)
- val iRT = mk_relT (idomT, idomT)
- val iR = Const (Rname, iRT)
-
+ val domT = domain_type (fastype_of f)
+ val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
+ val DT = type_of D
+ val idomT = HOLogic.dest_setT DT
+
+ val x = Free ("x", idomT)
+ val z = Free ("z", idomT)
+ val Rname = fst (dest_Const R)
+ val iRT = mk_relT (idomT, idomT)
+ val iR = Const (Rname, iRT)
+
+ val subs = HOLogic.mk_Trueprop
+ (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
+ (Const (acc_const_name, iRT --> DT) $ iR))
+ |> Type.freeze
- val subs = HOLogic.mk_Trueprop
- (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
- (Const (acc_const_name, iRT --> DT) $ iR))
- |> Type.freeze
-
- val dcl = mk_forall x
- (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
- Logic.mk_implies (mk_relmem (z, x) iR,
- Trueprop (mk_mem (z, D))))))
- |> Type.freeze
+ val dcl = mk_forall x
+ (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
+ Logic.mk_implies (mk_relmem (z, x) iR,
+ Trueprop (mk_mem (z, D))))))
+ |> Type.freeze
in
- (subs, dcl)
+ (subs, dcl)
end
end