# HG changeset patch # User krauss # Date 1162933592 -3600 # Node ID b803f9870e97a581c801343fd7f3d69bca8d5aaf # Parent 890fafbcf8b0fb9cdbeedd3b81db1284a9b4b04c untabified diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/context_tree.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/fundef_common.ML --- 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) diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/fundef_lib.ML --- 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) diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/fundef_package.ML --- 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, [])])] diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/fundef_prep.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/fundef_proof.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/inductive_wrap.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/lexicographic_order.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/mutual.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/pattern_split.ML --- 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) diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/sum_tools.ML --- 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 diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/termination.ML --- 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