# HG changeset patch # User krauss # Date 1262470738 -3600 # Node ID 36a2a3029fd3ed1906aa7dfe19b48aa443607d70 # Parent da4d7d40f2f97ed511559ec5fd0962a23dc8e4d6 new year's resolution: reindented code in function package diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/context_tree.ML Sat Jan 02 23:18:58 2010 +0100 @@ -1,39 +1,41 @@ (* Title: HOL/Tools/Function/context_tree.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. +A package for general recursive function definitions. Builds and traverses trees of nested contexts along a term. *) signature FUNCTION_CTXTREE = sig - type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *) - type ctx_tree + (* poor man's contexts: fixes + assumes *) + type ctxt = (string * typ) list * thm list + type ctx_tree - (* FIXME: This interface is a mess and needs to be cleaned up! *) - val get_function_congs : Proof.context -> thm list - val add_function_cong : thm -> Context.generic -> Context.generic - val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic + (* FIXME: This interface is a mess and needs to be cleaned up! *) + val get_function_congs : Proof.context -> thm list + val add_function_cong : thm -> Context.generic -> Context.generic + val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic - val cong_add: attribute - val cong_del: attribute + val cong_add: attribute + val cong_del: attribute - val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree + val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree - val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree + val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree - val export_term : ctxt -> term -> term - val export_thm : theory -> ctxt -> thm -> thm - val import_thm : theory -> ctxt -> thm -> thm + val export_term : ctxt -> term -> term + val export_thm : theory -> ctxt -> thm -> thm + val import_thm : theory -> ctxt -> thm -> thm - val traverse_tree : + val traverse_tree : (ctxt -> term -> (ctxt * thm) list -> (ctxt * thm) list * 'b -> (ctxt * thm) list * 'b) -> ctx_tree -> 'b -> 'b - val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list + val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> + ctx_tree -> thm * (thm * thm) list end structure Function_Ctx_Tree : FUNCTION_CTXTREE = @@ -64,8 +66,8 @@ type depgraph = int IntGraph.T -datatype ctx_tree - = Leaf of term +datatype ctx_tree = + Leaf of term | Cong of (thm * depgraph * (ctxt * ctx_tree) list) | RCall of (term * ctx_tree) @@ -76,204 +78,210 @@ (*** Dependency analysis for congruence rules ***) -fun branch_vars t = - let - val t' = snd (dest_all_all t) - val (assumes, concl) = Logic.strip_horn t' - in (fold Term.add_vars assumes [], Term.add_vars concl []) - end +fun branch_vars t = + let + val t' = snd (dest_all_all t) + val (assumes, concl) = Logic.strip_horn t' + in + (fold Term.add_vars assumes [], Term.add_vars concl []) + end fun cong_deps crule = - let - val num_branches = map_index (apsnd branch_vars) (prems_of crule) - in - IntGraph.empty - |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches - |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => - if i = j orelse null (inter (op =) c1 t2) - then I else IntGraph.add_edge_acyclic (i,j)) - num_branches num_branches + let + val num_branches = map_index (apsnd branch_vars) (prems_of crule) + in + IntGraph.empty + |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches + |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => + if i = j orelse null (inter (op =) c1 t2) + then I else IntGraph.add_edge_acyclic (i,j)) + num_branches num_branches end - -val default_congs = map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}] - +val default_congs = + map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}] (* Called on the INSTANTIATED branches of the congruence rule *) -fun mk_branch ctx t = - let - val (ctx', fixes, impl) = dest_all_all_ctx ctx t - val (assms, concl) = Logic.strip_horn impl - in - (ctx', fixes, assms, rhs_of concl) - end - +fun mk_branch ctx t = + let + val (ctx', fixes, impl) = dest_all_all_ctx ctx t + val (assms, concl) = Logic.strip_horn impl + in + (ctx', fixes, assms, rhs_of concl) + end + fun find_cong_rule ctx fvar h ((r,dep)::rs) t = - (let - val thy = ProofContext.theory_of ctx + (let + val thy = ProofContext.theory_of ctx - val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t) - val (c, subs) = (concl_of r, prems_of r) + val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t) + val (c, subs) = (concl_of r, prems_of r) - val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty) - val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs - val inst = map (fn v => - (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c []) - in - (cterm_instantiate inst r, dep, branches) - end - handle Pattern.MATCH => find_cong_rule ctx fvar h rs t) + val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty) + val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs + val inst = map (fn v => + (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c []) + in + (cterm_instantiate inst r, dep, branches) + end + handle Pattern.MATCH => find_cong_rule ctx fvar h rs t) | find_cong_rule _ _ _ [] _ = sys_error "Function/context_tree.ML: No cong rule found!" fun mk_tree fvar h ctxt t = - let - val congs = get_function_congs ctxt - val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *) + let + val congs = get_function_congs ctxt - fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE - | matchcall _ = NONE + (* FIXME: Save in theory: *) + val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) + + fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE + | matchcall _ = NONE - fun mk_tree' ctx t = - case matchcall t of - SOME arg => RCall (t, mk_tree' ctx arg) - | NONE => - if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t - else - let val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t in - Cong (r, dep, - map (fn (ctx', fixes, assumes, st) => - ((fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes), - mk_tree' ctx' st)) branches) - end - in - mk_tree' ctxt t - end - + fun mk_tree' ctx t = + case matchcall t of + SOME arg => RCall (t, mk_tree' ctx arg) + | NONE => + if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t + else + let + val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t + fun subtree (ctx', fixes, assumes, st) = + ((fixes, + map (assume o cterm_of (ProofContext.theory_of ctx)) assumes), + mk_tree' ctx' st) + in + Cong (r, dep, map subtree branches) + end + in + mk_tree' ctxt t + end fun inst_tree thy fvar f tr = - let - val cfvar = cterm_of thy fvar - val cf = cterm_of thy f - - fun inst_term t = - subst_bound(f, abstract_over (fvar, t)) + let + val cfvar = cterm_of thy fvar + val cf = cterm_of thy f - val inst_thm = forall_elim cf o forall_intr cfvar + fun inst_term t = + subst_bound(f, abstract_over (fvar, t)) + + val inst_thm = forall_elim cf o forall_intr cfvar - fun inst_tree_aux (Leaf t) = Leaf t - | inst_tree_aux (Cong (crule, deps, branches)) = - Cong (inst_thm crule, deps, map inst_branch branches) - | inst_tree_aux (RCall (t, str)) = - RCall (inst_term t, inst_tree_aux str) - and inst_branch ((fxs, assms), str) = - ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms), inst_tree_aux str) - in - inst_tree_aux tr - end + fun inst_tree_aux (Leaf t) = Leaf t + | inst_tree_aux (Cong (crule, deps, branches)) = + Cong (inst_thm crule, deps, map inst_branch branches) + | inst_tree_aux (RCall (t, str)) = + RCall (inst_term t, inst_tree_aux str) + and inst_branch ((fxs, assms), str) = + ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms), + inst_tree_aux str) + in + inst_tree_aux tr + end (* Poor man's contexts: Only fixes and assumes *) fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2) fun export_term (fixes, assumes) = - fold_rev (curry Logic.mk_implies o prop_of) assumes + fold_rev (curry Logic.mk_implies o prop_of) assumes #> fold_rev (Logic.all o Free) fixes fun export_thm thy (fixes, assumes) = - fold_rev (implies_intr o cprop_of) assumes + fold_rev (implies_intr o cprop_of) assumes #> fold_rev (forall_intr o cterm_of thy o Free) fixes fun import_thm thy (fixes, athms) = - fold (forall_elim o cterm_of thy o Free) fixes + fold (forall_elim o cterm_of thy o Free) fixes #> fold Thm.elim_implies athms (* 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 - - val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x) - in - (Inttab.fold (cons o snd) T [], x) - end - + 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 + + val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x) + in + (Inttab.fold (cons o snd) T [], x) + end + fun traverse_tree rcOp tr = - let - fun traverse_help ctx (Leaf _) _ x = ([], x) - | traverse_help ctx (RCall (t, st)) u x = - rcOp ctx t u (traverse_help ctx st u x) - | traverse_help ctx (Cong (_, deps, branches)) u x = + let + fun traverse_help ctx (Leaf _) _ x = ([], x) + | traverse_help ctx (RCall (t, st)) u x = + rcOp ctx t u (traverse_help ctx st u x) + | traverse_help ctx (Cong (_, deps, branches)) u x = let - fun sub_step lu i x = - let - val (ctx', subtree) = nth branches i - val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u - val (subs, x') = traverse_help (compose ctx ctx') subtree used x - val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *) - in - (exported_subs, x') - end + fun sub_step lu i x = + let + val (ctx', subtree) = nth branches i + val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u + val (subs, x') = traverse_help (compose ctx ctx') subtree used x + val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *) + in + (exported_subs, x') + end in fold_deps deps sub_step x - |> apfst flat + |> apfst flat end - in - snd o traverse_help ([], []) tr [] - end + in + snd o traverse_help ([], []) tr [] + end fun rewrite_by_tree thy h ih x tr = - let - fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x) - | rewrite_help fix h_as x (RCall (_ $ arg, st)) = - let - val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *) - - val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *) - |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner)))) + let + fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x) + | rewrite_help fix h_as x (RCall (_ $ arg, st)) = + let + val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *) + + val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *) + |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner)))) (* (a, h a) : G *) - val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih - val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *) - - val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner - 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 h_as x (Cong (crule, deps, branches)) = - let - fun sub_step lu i x = - let - val ((fixes, assumes), st) = nth branches i - val used = map lu (IntGraph.imm_succs deps i) - |> map (fn u_eq => (u_eq RS sym) RS eq_reflection) - |> filter_out Thm.is_reflexive + val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih + val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *) + + val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner + 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 h_as x (Cong (crule, deps, branches)) = + let + fun sub_step lu i x = + let + val ((fixes, assumes), st) = nth branches i + val used = map lu (IntGraph.imm_succs deps i) + |> map (fn u_eq => (u_eq RS sym) RS eq_reflection) + |> filter_out Thm.is_reflexive - val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes - - val (subeq, x') = rewrite_help (fix @ fixes) (h_as @ assumes') x st - val subeq_exp = export_thm thy (fixes, 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 - end - + val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes + + val (subeq, x') = + rewrite_help (fix @ fixes) (h_as @ assumes') x st + val subeq_exp = + export_thm thy (fixes, 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 + end + end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/fun.ML Sat Jan 02 23:18:58 2010 +0100 @@ -7,14 +7,14 @@ signature FUNCTION_FUN = sig - val add_fun : Function_Common.function_config -> - (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> - bool -> local_theory -> Proof.context - val add_fun_cmd : Function_Common.function_config -> - (binding * string option * mixfix) list -> (Attrib.binding * string) list -> - bool -> local_theory -> Proof.context + val add_fun : Function_Common.function_config -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + bool -> local_theory -> Proof.context + val add_fun_cmd : Function_Common.function_config -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> + bool -> local_theory -> Proof.context - val setup : theory -> theory + val setup : theory -> theory end structure Function_Fun : FUNCTION_FUN = @@ -25,64 +25,64 @@ fun check_pats ctxt geq = - let - fun err str = error (cat_lines ["Malformed definition:", - str ^ " not allowed in sequential mode.", - Syntax.string_of_term ctxt geq]) - val thy = ProofContext.theory_of ctxt - - fun check_constr_pattern (Bound _) = () - | check_constr_pattern t = - let - val (hd, args) = strip_comb t - in - (((case Datatype.info_of_constr thy (dest_Const hd) of - SOME _ => () - | NONE => err "Non-constructor pattern") - handle TERM ("dest_Const", _) => err "Non-constructor patterns"); - map check_constr_pattern args; - ()) - end - - val (_, qs, gs, args, _) = split_def ctxt geq - - val _ = if not (null gs) then err "Conditional equations" else () - val _ = map check_constr_pattern args - - (* just count occurrences to check linearity *) - val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs - then err "Nonlinear patterns" else () - in - () - end - + let + fun err str = error (cat_lines ["Malformed definition:", + str ^ " not allowed in sequential mode.", + Syntax.string_of_term ctxt geq]) + val thy = ProofContext.theory_of ctxt + + fun check_constr_pattern (Bound _) = () + | check_constr_pattern t = + let + val (hd, args) = strip_comb t + in + (((case Datatype.info_of_constr thy (dest_Const hd) of + SOME _ => () + | NONE => err "Non-constructor pattern") + handle TERM ("dest_Const", _) => err "Non-constructor patterns"); + map check_constr_pattern args; + ()) + end + + val (_, qs, gs, args, _) = split_def ctxt geq + + val _ = if not (null gs) then err "Conditional equations" else () + val _ = map check_constr_pattern args + + (* just count occurrences to check linearity *) + val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs + then err "Nonlinear patterns" else () + in + () + end + val by_pat_completeness_auto = - Proof.global_future_terminal_proof - (Method.Basic Pat_Completeness.pat_completeness, - SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) + Proof.global_future_terminal_proof + (Method.Basic Pat_Completeness.pat_completeness, + SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) fun termination_by method int = - Function.termination_proof NONE - #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int + Function.termination_proof NONE + #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int fun mk_catchall fixes arity_of = - let - fun mk_eqn ((fname, fT), _) = - let - val n = arity_of fname - val (argTs, rT) = chop n (binder_types fT) - |> apsnd (fn Ts => Ts ---> body_type fT) - - val qs = map Free (Name.invent_list [] "a" n ~~ argTs) - in - HOLogic.mk_eq(list_comb (Free (fname, fT), qs), - Const ("HOL.undefined", rT)) - |> HOLogic.mk_Trueprop - |> fold_rev Logic.all qs - end - in - map mk_eqn fixes - end + let + fun mk_eqn ((fname, fT), _) = + let + val n = arity_of fname + val (argTs, rT) = chop n (binder_types fT) + |> apsnd (fn Ts => Ts ---> body_type fT) + + val qs = map Free (Name.invent_list [] "a" n ~~ argTs) + in + HOLogic.mk_eq(list_comb (Free (fname, fT), qs), + Const ("HOL.undefined", rT)) + |> HOLogic.mk_Trueprop + |> fold_rev Logic.all qs + end + in + map mk_eqn fixes + end fun add_catchall ctxt fixes spec = let val fqgars = map (split_def ctxt) spec @@ -93,55 +93,53 @@ end fun warn_if_redundant ctxt origs tss = - let - fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t) - - val (tss', _) = chop (length origs) tss - fun check (t, []) = (warning (msg t); []) - | check (t, s) = s - in - (map check (origs ~~ tss'); tss) - end + let + fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t) + val (tss', _) = chop (length origs) tss + fun check (t, []) = (warning (msg t); []) + | check (t, s) = s + in + (map check (origs ~~ tss'); tss) + end fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec = - if sequential then - let - val (bnds, eqss) = split_list spec - - val eqs = map the_single eqss - - val feqs = eqs - |> tap (check_defs ctxt fixes) (* Standard checks *) - |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) + if sequential then + let + val (bnds, eqss) = split_list spec + + val eqs = map the_single eqss - val compleqs = add_catchall ctxt fixes feqs (* Completion *) + val feqs = eqs + |> tap (check_defs ctxt fixes) (* Standard checks *) + |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) + + val compleqs = add_catchall ctxt fixes feqs (* Completion *) - val spliteqs = warn_if_redundant ctxt feqs - (Function_Split.split_all_equations ctxt compleqs) + val spliteqs = warn_if_redundant ctxt feqs + (Function_Split.split_all_equations ctxt compleqs) + + fun restore_spec thms = + bnds ~~ take (length bnds) (unflat spliteqs thms) - fun restore_spec thms = - bnds ~~ take (length bnds) (unflat spliteqs thms) - - val spliteqs' = flat (take (length bnds) spliteqs) - val fnames = map (fst o fst) fixes - val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' + val spliteqs' = flat (take (length bnds) spliteqs) + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' - fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) - |> map (map snd) + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) + |> map (map snd) - val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding + val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding - (* using theorem names for case name currently disabled *) - val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) - (bnds' ~~ spliteqs) - |> flat - in - (flat spliteqs, restore_spec, sort, case_names) - end - else - Function_Common.empty_preproc check_defs config ctxt fixes spec + (* using theorem names for case name currently disabled *) + val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) + (bnds' ~~ spliteqs) |> flat + in + (flat spliteqs, restore_spec, sort, case_names) + end + else + Function_Common.empty_preproc check_defs config ctxt fixes spec val setup = Context.theory_map (Function_Common.set_preproc sequential_preproc) @@ -152,10 +150,10 @@ fun gen_fun add config fixes statements int lthy = lthy - |> add fixes statements config - |> by_pat_completeness_auto int - |> Local_Theory.restore - |> termination_by (Function_Common.get_termination_prover lthy) int + |> add fixes statements config + |> by_pat_completeness_auto int + |> Local_Theory.restore + |> termination_by (Function_Common.get_termination_prover lthy) int val add_fun = gen_fun Function.add_function val add_fun_cmd = gen_fun Function.add_function_cmd diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function.ML Sat Jan 02 23:18:58 2010 +0100 @@ -7,26 +7,23 @@ signature FUNCTION = sig - include FUNCTION_DATA + include FUNCTION_DATA + + val add_function: (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> Function_Common.function_config -> + local_theory -> Proof.state - val add_function : (binding * typ option * mixfix) list - -> (Attrib.binding * term) list - -> Function_Common.function_config - -> local_theory - -> Proof.state - val add_function_cmd : (binding * string option * mixfix) list - -> (Attrib.binding * string) list - -> Function_Common.function_config - -> local_theory - -> Proof.state + val add_function_cmd: (binding * string option * mixfix) list -> + (Attrib.binding * string) list -> Function_Common.function_config -> + local_theory -> Proof.state - val termination_proof : term option -> local_theory -> Proof.state - val termination_proof_cmd : string option -> local_theory -> Proof.state + val termination_proof : term option -> local_theory -> Proof.state + val termination_proof_cmd : string option -> local_theory -> Proof.state - val setup : theory -> theory - val get_congs : Proof.context -> thm list + val setup : theory -> theory + val get_congs : Proof.context -> thm list - val get_info : Proof.context -> term -> info + val get_info : Proof.context -> term -> info end @@ -37,148 +34,149 @@ open Function_Common val simp_attribs = map (Attrib.internal o K) - [Simplifier.simp_add, - Code.add_default_eqn_attribute, - Nitpick_Simps.add] + [Simplifier.simp_add, + Code.add_default_eqn_attribute, + Nitpick_Simps.add] val psimp_attribs = map (Attrib.internal o K) - [Simplifier.simp_add, - Nitpick_Psimps.add] + [Simplifier.simp_add, + Nitpick_Psimps.add] fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" -fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = - let - val spec = post simps - |> map (apfst (apsnd (fn ats => moreatts @ ats))) - |> map (apfst (apfst extra_qualify)) +fun add_simps fnames post sort extra_qualify label mod_binding moreatts + simps lthy = + let + val spec = post simps + |> map (apfst (apsnd (fn ats => moreatts @ ats))) + |> map (apfst (apfst extra_qualify)) - val (saved_spec_simps, lthy) = - fold_map Local_Theory.note spec lthy + val (saved_spec_simps, lthy) = + fold_map Local_Theory.note spec lthy - val saved_simps = maps snd saved_spec_simps - val simps_by_f = sort saved_simps + val saved_simps = maps snd saved_spec_simps + val simps_by_f = sort saved_simps - fun add_for_f fname simps = - Local_Theory.note - ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) - #> snd - in - (saved_simps, - fold2 add_for_f fnames simps_by_f lthy) - end + fun add_for_f fname simps = + Local_Theory.note + ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) + #> snd + in + (saved_simps, fold2 add_for_f fnames simps_by_f lthy) + end fun gen_add_function is_external prep default_constraint fixspec eqns config lthy = - let - val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) - val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy - val fixes = map (apfst (apfst Binding.name_of)) fixes0; - val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; - val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec + let + val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) + val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy + val fixes = map (apfst (apfst Binding.name_of)) fixes0; + val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; + val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec - val defname = mk_defname fixes - val FunctionConfig {partials, ...} = config + val defname = mk_defname fixes + val FunctionConfig {partials, ...} = config - val ((goalstate, cont), lthy) = - Function_Mutual.prepare_function_mutual config defname fixes eqs lthy + val ((goalstate, cont), lthy) = + Function_Mutual.prepare_function_mutual config defname fixes eqs lthy - fun afterqed [[proof]] lthy = - let - val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, termination, - domintros, cases, ...} = + fun afterqed [[proof]] lthy = + let + val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, + termination, domintros, cases, ...} = cont (Thm.close_derivation proof) - val fnames = map (fst o fst) fixes - fun qualify n = Binding.name n - |> Binding.qualify true defname - val conceal_partial = if partials then I else Binding.conceal + val fnames = map (fst o fst) fixes + fun qualify n = Binding.name n + |> Binding.qualify true defname + val conceal_partial = if partials then I else Binding.conceal - val addsmps = add_simps fnames post sort_cont + val addsmps = add_simps fnames post sort_cont - val (((psimps', pinducts'), (_, [termination'])), lthy) = - lthy - |> addsmps (conceal_partial o Binding.qualify false "partial") - "psimps" conceal_partial psimp_attribs psimps - ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps - ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), - [Attrib.internal (K (Rule_Cases.case_names cnames)), - Attrib.internal (K (Rule_Cases.consumes 1)), - Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) - ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) - ||> (snd o Local_Theory.note ((qualify "cases", - [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) - ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros + val (((psimps', pinducts'), (_, [termination'])), lthy) = + lthy + |> addsmps (conceal_partial o Binding.qualify false "partial") + "psimps" conceal_partial psimp_attribs psimps + ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps + ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), + [Attrib.internal (K (Rule_Cases.case_names cnames)), + Attrib.internal (K (Rule_Cases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) + ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) + ||> (snd o Local_Theory.note ((qualify "cases", + [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) + ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros - val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', - pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', - fs=fs, R=R, defname=defname, is_partial=true } + val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', + pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', + fs=fs, R=R, defname=defname, is_partial=true } - val _ = - if not is_external then () - else Specification.print_consts lthy (K false) (map fst fixes) - in - lthy - |> Local_Theory.declaration false (add_function_data o morph_function_data info) - end - in - lthy - |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] - |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd - end + val _ = + if not is_external then () + else Specification.print_consts lthy (K false) (map fst fixes) + in + lthy + |> Local_Theory.declaration false (add_function_data o morph_function_data info) + end + in + lthy + |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] + |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd + end -val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) +val add_function = + gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) val add_function_cmd = gen_add_function true Specification.read_spec "_::type" fun gen_termination_proof prep_term raw_term_opt lthy = - let - val term_opt = Option.map (prep_term lthy) raw_term_opt - val info = the (case term_opt of - SOME t => (import_function_data t lthy - handle Option.Option => - error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) - | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) + let + val term_opt = Option.map (prep_term lthy) raw_term_opt + val info = the (case term_opt of + SOME t => (import_function_data t lthy + handle Option.Option => + error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) + | NONE => (import_last_function lthy handle Option.Option => error "Not a function")) - val { termination, fs, R, add_simps, case_names, psimps, - pinducts, defname, ...} = info - val domT = domain_type (fastype_of R) - val goal = HOLogic.mk_Trueprop - (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) - fun afterqed [[totality]] lthy = - let - val totality = Thm.close_derivation totality - val remove_domain_condition = - full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - val tsimps = map remove_domain_condition psimps - val tinduct = map remove_domain_condition pinducts + val { termination, fs, R, add_simps, case_names, psimps, + pinducts, defname, ...} = info + val domT = domain_type (fastype_of R) + val goal = HOLogic.mk_Trueprop + (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) + fun afterqed [[totality]] lthy = + let + val totality = Thm.close_derivation totality + val remove_domain_condition = + full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) + val tsimps = map remove_domain_condition psimps + val tinduct = map remove_domain_condition pinducts - fun qualify n = Binding.name n - |> Binding.qualify true defname - in - lthy - |> add_simps I "simps" I simp_attribs tsimps - ||>> Local_Theory.note - ((qualify "induct", - [Attrib.internal (K (Rule_Cases.case_names case_names))]), - tinduct) - |-> (fn (simps, (_, inducts)) => - let val info' = { is_partial=false, defname=defname, add_simps=add_simps, - case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, - simps=SOME simps, inducts=SOME inducts, termination=termination } - in - Local_Theory.declaration false (add_function_data o morph_function_data info') - end) - end - in - lthy - |> ProofContext.note_thmss "" - [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" - [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" - [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), - [([Goal.norm_result termination], [])])] |> snd - |> Proof.theorem_i NONE afterqed [[(goal, [])]] - end + fun qualify n = Binding.name n + |> Binding.qualify true defname + in + lthy + |> add_simps I "simps" I simp_attribs tsimps + ||>> Local_Theory.note + ((qualify "induct", + [Attrib.internal (K (Rule_Cases.case_names case_names))]), + tinduct) + |-> (fn (simps, (_, inducts)) => + let val info' = { is_partial=false, defname=defname, add_simps=add_simps, + case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, + simps=SOME simps, inducts=SOME inducts, termination=termination } + in + Local_Theory.declaration false (add_function_data o morph_function_data info') + end) + end + in + lthy + |> ProofContext.note_thmss "" + [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd + |> ProofContext.note_thmss "" + [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), + [([Goal.norm_result termination], [])])] |> snd + |> Proof.theorem_i NONE afterqed [[(goal, [])]] + end val termination_proof = gen_termination_proof Syntax.check_term val termination_proof_cmd = gen_termination_proof Syntax.read_term @@ -188,11 +186,13 @@ fun add_case_cong n thy = - Context.theory_map (Function_Ctx_Tree.map_function_congs (Thm.add_thm - (Datatype.the_info thy n - |> #case_cong - |> safe_mk_meta_eq))) - thy + let + val cong = #case_cong (Datatype.the_info thy n) + |> safe_mk_meta_eq + in + Context.theory_map + (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy + end val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Sat Jan 02 23:18:58 2010 +0100 @@ -1,7 +1,7 @@ -(* Title: HOL/Tools/Function/fundef_common.ML +(* Title: HOL/Tools/Function/function_common.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. +A package for general recursive function definitions. Common definitions and other infrastructure. *) @@ -21,8 +21,7 @@ pinducts: thm list, simps : thm list option, inducts : thm list option, - termination: thm - } + termination: thm} end @@ -42,8 +41,7 @@ pinducts: thm list, simps : thm list option, inducts : thm list option, - termination: thm - } + termination: thm} end @@ -62,7 +60,7 @@ val acc_const_name = @{const_name accp} fun mk_acc domT R = - Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R + Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R val function_name = suffix "C" val graph_name = suffix "_graph" @@ -86,21 +84,18 @@ (* Function definition result data *) -datatype function_result = - FunctionResult of - { - fs: term list, - G: term, - R: term, +datatype function_result = FunctionResult of + {fs: term list, + G: term, + R: term, - psimps : thm list, - trsimps : thm list option, + psimps : thm list, + trsimps : thm list option, - simple_pinducts : thm list, - cases : thm, - termination : thm, - domintros : thm list option - } + simple_pinducts : thm list, + cases : thm, + termination : thm, + domintros : thm list option} fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, simps, inducts, termination, defname, is_partial} : info) phi = @@ -109,7 +104,7 @@ val name = Binding.name_of o Morphism.binding phi o Binding.name in { add_simps = add_simps, case_names = case_names, - fs = map term fs, R = term R, psimps = fact psimps, + fs = map term fs, R = term R, psimps = fact psimps, pinducts = fact pinducts, simps = Option.map fact simps, inducts = Option.map fact inducts, termination = thm termination, defname = name defname, is_partial=is_partial } @@ -121,57 +116,56 @@ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); val extend = I; fun merge tabs : T = Item_Net.merge tabs; -); +) val get_function = FunctionData.get o Context.Proof; -(* Generally useful?? *) -fun lift_morphism thy f = - let - val term = Drule.term_rule thy f - in - Morphism.thm_morphism f $> Morphism.term_morphism term - $> Morphism.typ_morphism (Logic.type_map term) - end +fun lift_morphism thy f = + let + val term = Drule.term_rule thy f + in + Morphism.thm_morphism f $> Morphism.term_morphism term + $> Morphism.typ_morphism (Logic.type_map term) + end fun import_function_data t ctxt = - let - val thy = ProofContext.theory_of ctxt - val ct = cterm_of thy t - val inst_morph = lift_morphism thy o Thm.instantiate + let + val thy = ProofContext.theory_of ctxt + val ct = cterm_of thy t + val inst_morph = lift_morphism thy o Thm.instantiate - fun match (trm, data) = - SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) - handle Pattern.MATCH => NONE - in - get_first match (Item_Net.retrieve (get_function ctxt) t) - end + fun match (trm, data) = + SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) + handle Pattern.MATCH => NONE + in + get_first match (Item_Net.retrieve (get_function ctxt) t) + end fun import_last_function ctxt = - case Item_Net.content (get_function ctxt) of - [] => NONE - | (t, data) :: _ => - let - val ([t'], ctxt') = Variable.import_terms true [t] ctxt - in - import_function_data t' ctxt' - end + case Item_Net.content (get_function ctxt) of + [] => NONE + | (t, data) :: _ => + let + val ([t'], ctxt') = Variable.import_terms true [t] ctxt + in + import_function_data t' ctxt' + end val all_function_data = Item_Net.content o get_function fun add_function_data (data : info as {fs, termination, ...}) = - FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) - #> store_termination_rule termination + FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) + #> store_termination_rule termination (* Simp rules for termination proofs *) structure Termination_Simps = Named_Thms ( - val name = "termination_simp" + val name = "termination_simp" val description = "Simplification rule for termination proofs" -); +) (* Default Termination Prover *) @@ -182,29 +176,26 @@ val empty = (fn _ => error "Termination prover not configured") val extend = I fun merge (a, b) = b (* FIXME ? *) -); +) val set_termination_prover = TerminationProver.put val get_termination_prover = TerminationProver.get o Context.Proof (* Configuration management *) -datatype function_opt +datatype function_opt = Sequential | Default of string | DomIntros | No_Partials | Tailrec -datatype function_config - = FunctionConfig of - { - sequential: bool, - default: string, - domintros: bool, - partials: bool, - tailrec: bool - } +datatype function_config = FunctionConfig of + {sequential: bool, + default: string, + domintros: bool, + partials: bool, + tailrec: bool} fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) = FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec} @@ -225,97 +216,94 @@ (* Analyzing function equations *) fun split_def ctxt geq = - let - fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] - val qs = Term.strip_qnt_vars "all" geq - val imp = Term.strip_qnt_body "all" geq - val (gs, eq) = Logic.strip_horn imp + let + fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] + val qs = Term.strip_qnt_vars "all" geq + val imp = Term.strip_qnt_body "all" geq + val (gs, eq) = Logic.strip_horn imp - val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) - handle TERM _ => error (input_error "Not an equation") + val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) + handle TERM _ => error (input_error "Not an equation") - val (head, args) = strip_comb f_args + val (head, args) = strip_comb f_args - val fname = fst (dest_Free head) - handle TERM _ => error (input_error "Head symbol must not be a bound variable") - in - (fname, qs, gs, args, rhs) - end + val fname = fst (dest_Free head) + handle TERM _ => error (input_error "Head symbol must not be a bound variable") + in + (fname, qs, gs, args, rhs) + end (* Check for all sorts of errors in the input *) fun check_defs ctxt fixes eqs = - let - val fnames = map (fst o fst) fixes - - fun check geq = - let - fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) - - val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq - - val _ = fname mem fnames - orelse input_error - ("Head symbol of left hand side must be " - ^ plural "" "one out of " fnames ^ commas_quote fnames) - - val _ = length args > 0 orelse input_error "Function has no arguments:" + let + val fnames = map (fst o fst) fixes + + fun check geq = + let + fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) - fun add_bvs t is = add_loose_bnos (t, 0, is) + val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq + + val _ = fname mem fnames + orelse input_error ("Head symbol of left hand side must be " ^ + plural "" "one out of " fnames ^ commas_quote fnames) + + val _ = length args > 0 orelse input_error "Function has no arguments:" + + fun add_bvs t is = add_loose_bnos (t, 0, is) val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |> map (fst o nth (rev qs)) - - val _ = null rvs orelse input_error - ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs - ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") - - val _ = forall (not o Term.exists_subterm - (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) - orelse input_error "Defined function may not occur in premises or arguments" + + val _ = null rvs orelse input_error + ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ + " occur" ^ plural "s" "" rvs ^ " on right hand side only:") + + val _ = forall (not o Term.exists_subterm + (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) + orelse input_error "Defined function may not occur in premises or arguments" - val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args - val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs - val _ = null funvars - orelse (warning (cat_lines - ["Bound variable" ^ plural " " "s " funvars - ^ commas_quote (map fst funvars) ^ - " occur" ^ plural "s" "" funvars ^ " in function position.", - "Misspelled constructor???"]); true) - in - (fname, length args) - end + val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args + val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs + val _ = null funvars orelse (warning (cat_lines + ["Bound variable" ^ plural " " "s " funvars ^ + commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ + " in function position.", "Misspelled constructor???"]); true) + in + (fname, length args) + end - val grouped_args = AList.group (op =) (map check eqs) - val _ = grouped_args - |> map (fn (fname, ars) => - length (distinct (op =) ars) = 1 - orelse error ("Function " ^ quote fname ^ - " has different numbers of arguments in different equations")) + val grouped_args = AList.group (op =) (map check eqs) + val _ = grouped_args + |> map (fn (fname, ars) => + length (distinct (op =) ars) = 1 + orelse error ("Function " ^ quote fname ^ + " has different numbers of arguments in different equations")) - val not_defined = subtract (op =) (map fst grouped_args) fnames - val _ = null not_defined - orelse error ("No defining equations for function" ^ - plural " " "s " not_defined ^ commas_quote not_defined) + val not_defined = subtract (op =) (map fst grouped_args) fnames + val _ = null not_defined + orelse error ("No defining equations for function" ^ + plural " " "s " not_defined ^ commas_quote not_defined) - fun check_sorts ((fname, fT), _) = - Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) - orelse error (cat_lines - ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", - setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT]) + fun check_sorts ((fname, fT), _) = + Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) + orelse error (cat_lines + ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", + setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT]) - val _ = map check_sorts fixes - in - () - end + val _ = map check_sorts fixes + in + () + end (* Preprocessors *) type fixes = ((string * typ) * mixfix) list type 'a spec = (Attrib.binding * 'a list) list -type preproc = function_config -> Proof.context -> fixes -> term spec - -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) +type preproc = function_config -> Proof.context -> fixes -> term spec -> + (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) -val fname_of = fst o dest_Free o fst o strip_comb o fst - o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o + HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k | mk_case_names _ n 0 = [] @@ -323,22 +311,21 @@ | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) fun empty_preproc check _ ctxt fixes spec = - let - val (bnds, tss) = split_list spec - val ts = flat tss - val _ = check ctxt fixes ts - val fnames = map (fst o fst) fixes - val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts + let + val (bnds, tss) = split_list spec + val ts = flat tss + val _ = check ctxt fixes ts + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts - fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) - (indices ~~ xs) - |> map (map snd) + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) + (indices ~~ xs) |> map (map snd) - (* using theorem names for case name currently disabled *) - val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat - in - (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) - end + (* using theorem names for case name currently disabled *) + val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat + in + (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) + end structure Preprocessor = Generic_Data ( @@ -346,32 +333,31 @@ val empty : T = empty_preproc check_defs val extend = I fun merge (a, _) = a -); +) val get_preproc = Preprocessor.get o Context.Proof val set_preproc = Preprocessor.map o K -local +local structure P = OuterParse and K = OuterKeyword - val option_parser = - P.group "option" ((P.reserved "sequential" >> K Sequential) - || ((P.reserved "default" |-- P.term) >> Default) - || (P.reserved "domintros" >> K DomIntros) - || (P.reserved "no_partials" >> K No_Partials) - || (P.reserved "tailrec" >> K Tailrec)) + val option_parser = P.group "option" + ((P.reserved "sequential" >> K Sequential) + || ((P.reserved "default" |-- P.term) >> Default) + || (P.reserved "domintros" >> K DomIntros) + || (P.reserved "no_partials" >> K No_Partials) + || (P.reserved "tailrec" >> K Tailrec)) - fun config_parser default = - (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") []) - >> (fn opts => fold apply_opt opts default) + fun config_parser default = + (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") []) + >> (fn opts => fold apply_opt opts default) in - fun function_parser default_cfg = + fun function_parser default_cfg = config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs end end end - diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Sat Jan 02 23:18:58 2010 +0100 @@ -7,26 +7,25 @@ signature FUNCTION_CORE = sig - val trace: bool Unsynchronized.ref + val trace: bool Unsynchronized.ref - val prepare_function : Function_Common.function_config - -> string (* defname *) - -> ((bstring * typ) * mixfix) list (* defined symbol *) - -> ((bstring * typ) list * term list * term * term) list (* specification *) - -> local_theory - - -> (term (* f *) - * thm (* goalstate *) - * (thm -> Function_Common.function_result) (* continuation *) - ) * local_theory + val prepare_function : Function_Common.function_config + -> string (* defname *) + -> ((bstring * typ) * mixfix) list (* defined symbol *) + -> ((bstring * typ) list * term list * term * term) list (* specification *) + -> local_theory + -> (term (* f *) + * thm (* goalstate *) + * (thm -> Function_Common.function_result) (* continuation *) + ) * local_theory end structure Function_Core : FUNCTION_CORE = struct -val trace = Unsynchronized.ref false; -fun trace_msg msg = if ! trace then tracing (msg ()) else (); +val trace = Unsynchronized.ref false +fun trace_msg msg = if ! trace then tracing (msg ()) else () val boolT = HOLogic.boolT val mk_eq = HOLogic.mk_eq @@ -34,149 +33,134 @@ open Function_Lib open Function_Common -datatype globals = - Globals of { - fvar: term, - domT: typ, - ranT: typ, - h: term, - y: term, - x: term, - z: term, - a: term, - P: term, - D: term, - Pbool:term -} +datatype globals = Globals of + {fvar: term, + domT: typ, + ranT: typ, + h: term, + y: term, + x: term, + z: term, + a: term, + P: term, + D: term, + Pbool:term} + +datatype rec_call_info = RCInfo of + {RIvs: (string * typ) list, (* Call context: fixes and assumes *) + CCas: thm list, + rcarg: term, (* The recursive argument *) + llRI: thm, + h_assum: term} -datatype rec_call_info = - RCInfo of - { - RIvs: (string * typ) list, (* Call context: fixes and assumes *) - CCas: thm list, - rcarg: term, (* The recursive argument *) - - llRI: thm, - h_assum: term - } - - -datatype clause_context = - ClauseContext of - { - ctxt : Proof.context, - - qs : term list, - gs : term list, - lhs: term, - rhs: term, - - cqs: cterm list, - ags: thm list, - case_hyp : thm - } +datatype clause_context = ClauseContext of + {ctxt : Proof.context, + qs : term list, + gs : term list, + lhs: term, + rhs: term, + cqs: cterm list, + ags: thm list, + case_hyp : thm} fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = - ClauseContext { ctxt = ProofContext.transfer thy ctxt, - qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } + ClauseContext { ctxt = ProofContext.transfer thy ctxt, + qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } -datatype clause_info = - ClauseInfo of - { - no: int, - qglr : ((string * typ) list * term list * term * term), - cdata : clause_context, - - tree: Function_Ctx_Tree.ctx_tree, - lGI: thm, - RCs: rec_call_info list - } +datatype clause_info = ClauseInfo of + {no: int, + qglr : ((string * typ) list * term list * term * term), + cdata : clause_context, + tree: Function_Ctx_Tree.ctx_tree, + lGI: thm, + RCs: rec_call_info list} (* Theory dependencies. *) -val acc_induct_rule = @{thm accp_induct_rule}; +val acc_induct_rule = @{thm accp_induct_rule} -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}; -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}; -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}; +val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence} +val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness} +val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff} -val acc_downward = @{thm accp_downward}; -val accI = @{thm accp.accI}; -val case_split = @{thm HOL.case_split}; -val fundef_default_value = @{thm FunDef.fundef_default_value}; -val not_acc_down = @{thm not_accp_down}; +val acc_downward = @{thm accp_downward} +val accI = @{thm accp.accI} +val case_split = @{thm HOL.case_split} +val fundef_default_value = @{thm FunDef.fundef_default_value} +val not_acc_down = @{thm not_accp_down} fun find_calls tree = - let - fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) - | add_Ri _ _ _ _ = raise Match - in - rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) - end + let + fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = + ([], (fixes, assumes, arg) :: xs) + | add_Ri _ _ _ _ = raise Match + in + rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) + end (** building proof obligations *) fun mk_compat_proof_obligations domT ranT fvar f glrs = - let - fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = - let - val shift = incr_boundvars (length qs') - in - Logic.mk_implies - (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), - HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) - |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') - |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') - |> curry abstract_over fvar - |> curry subst_bound f - end - in - map mk_impl (unordered_pairs glrs) - end + let + fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = + let + val shift = incr_boundvars (length qs') + in + Logic.mk_implies + (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), + HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) + |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') + |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') + |> curry abstract_over fvar + |> curry subst_bound f + end + in + map mk_impl (unordered_pairs glrs) + end fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = - let - fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = - HOLogic.mk_Trueprop Pbool - |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - in - HOLogic.mk_Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) - |> mk_forall_rename ("x", x) - |> mk_forall_rename ("P", Pbool) - end + let + fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = + HOLogic.mk_Trueprop Pbool + |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) + in + HOLogic.mk_Trueprop Pbool + |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) + |> mk_forall_rename ("x", x) + |> mk_forall_rename ("P", Pbool) + end (** making a context with it's own local bindings **) fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = - let - val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt - |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs + let + val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt + |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs - val thy = ProofContext.theory_of ctxt' + val thy = ProofContext.theory_of ctxt' - fun inst t = subst_bounds (rev qs, t) - val gs = map inst pre_gs - val lhs = inst pre_lhs - val rhs = inst pre_rhs + fun inst t = subst_bounds (rev qs, t) + val gs = map inst pre_gs + val lhs = inst pre_lhs + val rhs = inst pre_rhs - val cqs = map (cterm_of thy) qs - val ags = map (assume o cterm_of thy) gs + val cqs = map (cterm_of thy) qs + val ags = map (assume o cterm_of thy) gs - val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) - in - ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, - cqs = cqs, ags = ags, case_hyp = case_hyp } - end + val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) + in + ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, + cqs = cqs, ags = ags, case_hyp = case_hyp } + end (* lowlevel term function. FIXME: remove *) @@ -188,7 +172,7 @@ (case tm of Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) | t $ u => abs lev v t $ abs lev v u - | t => t); + | t => t) in fold_index (fn (i, v) => fn t => abs i v t) vs body end @@ -196,258 +180,249 @@ fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = - let - val Globals {h, ...} = globals + let + val Globals {h, ...} = globals - val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata - val cert = Thm.cterm_of (ProofContext.theory_of ctxt) + val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata + val cert = Thm.cterm_of (ProofContext.theory_of ctxt) - (* Instantiate the GIntro thm with "f" and import into the clause context. *) - val lGI = GIntro_thm - |> forall_elim (cert f) - |> fold forall_elim cqs - |> fold Thm.elim_implies ags - - fun mk_call_info (rcfix, rcassm, rcarg) RI = - let - val llRI = RI - |> fold forall_elim cqs - |> fold (forall_elim o cert o Free) rcfix - |> fold Thm.elim_implies ags - |> fold Thm.elim_implies rcassm + (* Instantiate the GIntro thm with "f" and import into the clause context. *) + val lGI = GIntro_thm + |> forall_elim (cert f) + |> fold forall_elim cqs + |> fold Thm.elim_implies ags - val h_assum = - HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (Logic.all o Free) rcfix - |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] - |> abstract_over_list (rev qs) - in - RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} - end + fun mk_call_info (rcfix, rcassm, rcarg) RI = + let + val llRI = RI + |> fold forall_elim cqs + |> fold (forall_elim o cert o Free) rcfix + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies rcassm - val RC_infos = map2 mk_call_info RCs RIntro_thms - in - ClauseInfo - { - no=no, - cdata=cdata, - qglr=qglr, + val h_assum = + HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (Logic.all o Free) rcfix + |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] + |> abstract_over_list (rev qs) + in + RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} + end - lGI=lGI, - RCs=RC_infos, - tree=tree - } - end + val RC_infos = map2 mk_call_info RCs RIntro_thms + in + ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, + tree=tree} + end - - - - - -(* replace this by a table later*) fun store_compat_thms 0 thms = [] | store_compat_thms n thms = - let - val (thms1, thms2) = chop n thms - in - (thms1 :: store_compat_thms (n - 1) thms2) - end + let + val (thms1, thms2) = chop n thms + in + (thms1 :: store_compat_thms (n - 1) thms2) + end (* expects i <= j *) fun lookup_compat_thm i j cts = - nth (nth cts (i - 1)) (j - i) + nth (nth cts (i - 1)) (j - i) (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) fun get_compat_thm thy cts i j ctxi ctxj = - let - val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi - val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj + let + val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi + val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj - val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) - in if j < i then - let - val compat = lookup_compat_thm j i cts - in - compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - |> fold Thm.elim_implies agsj - |> fold Thm.elim_implies agsi - |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) - end - else - let - val compat = lookup_compat_thm i j cts - in - compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - |> fold Thm.elim_implies agsi - |> fold Thm.elim_implies agsj - |> Thm.elim_implies (assume lhsi_eq_lhsj) - |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) - end + val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) + in if j < i then + let + val compat = lookup_compat_thm j i cts + in + compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + |> fold Thm.elim_implies agsj + |> fold Thm.elim_implies agsi + |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end - - - + else + let + val compat = lookup_compat_thm i j cts + in + compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) + |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) + |> fold Thm.elim_implies agsi + |> fold Thm.elim_implies agsj + |> Thm.elim_implies (assume lhsi_eq_lhsj) + |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) + end + end (* Generates the replacement lemma in fully quantified form. *) fun mk_replacement_lemma thy h ih_elim clause = - let - val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause - local open Conv in - val ih_conv = arg1_conv o arg_conv o arg_conv - end + let + val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, + RCs, tree, ...} = clause + local open Conv in + val ih_conv = arg1_conv o arg_conv o arg_conv + end - val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim - - val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs - val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs + val ih_elim_case = + Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim - val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree + val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs + val h_assums = map (fn RCInfo {h_assum, ...} => + assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs + + val (eql, _) = + Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree - val replace_lemma = (eql RS meta_eq_to_obj_eq) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) h_assums - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs - |> Thm.close_derivation - in - replace_lemma - end + val replace_lemma = (eql RS meta_eq_to_obj_eq) + |> implies_intr (cprop_of case_hyp) + |> fold_rev (implies_intr o cprop_of) h_assums + |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev forall_intr cqs + |> Thm.close_derivation + in + replace_lemma + end fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj = - let - val Globals {h, y, x, fvar, ...} = globals - val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei - val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej + let + val Globals {h, y, x, fvar, ...} = globals + val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei + val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej + + val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = + mk_clause_context x ctxti cdescj - val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} - = mk_clause_context x ctxti cdescj + val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' + val compat = get_compat_thm thy compat_store i j cctxi cctxj + val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj - val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' - val compat = get_compat_thm thy compat_store i j cctxi cctxj - val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj + val RLj_import = RLj + |> fold forall_elim cqsj' + |> fold Thm.elim_implies agsj' + |> fold Thm.elim_implies Ghsj' - val RLj_import = - RLj |> fold forall_elim cqsj' - |> fold Thm.elim_implies agsj' - |> fold Thm.elim_implies Ghsj' - - val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) - in - (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) - |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) - |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) - |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) - |> fold_rev (implies_intr o cprop_of) Ghsj' - |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) - |> implies_intr (cprop_of y_eq_rhsj'h) - |> implies_intr (cprop_of lhsi_eq_lhsj') - |> fold_rev forall_intr (cterm_of thy h :: cqsj') - end + val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) + (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) + in + (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) + |> implies_elim RLj_import + (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) + |> (fn it => trans OF [it, compat]) + (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) + |> (fn it => trans OF [y_eq_rhsj'h, it]) + (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) + |> fold_rev (implies_intr o cprop_of) Ghsj' + |> fold_rev (implies_intr o cprop_of) agsj' + (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) + |> implies_intr (cprop_of y_eq_rhsj'h) + |> implies_intr (cprop_of lhsi_eq_lhsj') + |> fold_rev forall_intr (cterm_of thy h :: cqsj') + end fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = - let - val Globals {x, y, ranT, fvar, ...} = globals - val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei - val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs + let + val Globals {x, y, ranT, fvar, ...} = globals + val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei + val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs - val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro + val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro - fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) - |> fold_rev (implies_intr o cprop_of) CCas - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) + |> fold_rev (implies_intr o cprop_of) CCas + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + + val existence = fold (curry op COMP o prep_RC) RCs lGI - val existence = fold (curry op COMP o prep_RC) RCs lGI + val P = cterm_of thy (mk_eq (y, rhsC)) + val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) - val P = cterm_of thy (mk_eq (y, rhsC)) - val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) - - val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas + val unique_clauses = + map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas - val uniqueness = G_cases - |> forall_elim (cterm_of thy lhs) - |> forall_elim (cterm_of thy y) - |> forall_elim P - |> Thm.elim_implies G_lhs_y - |> fold Thm.elim_implies unique_clauses - |> implies_intr (cprop_of G_lhs_y) - |> forall_intr (cterm_of thy y) + val uniqueness = G_cases + |> forall_elim (cterm_of thy lhs) + |> forall_elim (cterm_of thy y) + |> forall_elim P + |> Thm.elim_implies G_lhs_y + |> fold Thm.elim_implies unique_clauses + |> implies_intr (cprop_of G_lhs_y) + |> forall_intr (cterm_of thy y) - val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) + val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) - val exactly_one = - ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] - |> curry (op COMP) existence - |> curry (op COMP) uniqueness - |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs + val exactly_one = + ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] + |> curry (op COMP) existence + |> curry (op COMP) uniqueness + |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) + |> implies_intr (cprop_of case_hyp) + |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev forall_intr cqs - val function_value = - existence - |> implies_intr ihyp - |> implies_intr (cprop_of case_hyp) - |> forall_intr (cterm_of thy x) - |> forall_elim (cterm_of thy lhs) - |> curry (op RS) refl - in - (exactly_one, function_value) - end - - + val function_value = + existence + |> implies_intr ihyp + |> implies_intr (cprop_of case_hyp) + |> forall_intr (cterm_of thy x) + |> forall_elim (cterm_of thy lhs) + |> curry (op RS) refl + in + (exactly_one, function_value) + end fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = - let - val Globals {h, domT, ranT, x, ...} = globals - val thy = ProofContext.theory_of ctxt + let + val Globals {h, domT, ranT, x, ...} = globals + val thy = ProofContext.theory_of ctxt - (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) - val ihyp = Term.all domT $ Abs ("z", domT, - Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), - HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ - Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) - |> cterm_of thy + (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) + val ihyp = Term.all domT $ Abs ("z", domT, + Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), + HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ + Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) + |> cterm_of thy - val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0 - val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) - val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) - |> instantiate' [] [NONE, SOME (cterm_of thy h)] + val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0 + val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) + val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) + |> instantiate' [] [NONE, SOME (cterm_of thy h)] - val _ = trace_msg (K "Proving Replacement lemmas...") - val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses + val _ = trace_msg (K "Proving Replacement lemmas...") + val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses - val _ = trace_msg (K "Proving cases for unique existence...") - val (ex1s, values) = - split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) + val _ = trace_msg (K "Proving cases for unique existence...") + val (ex1s, values) = + split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) - val _ = trace_msg (K "Proving: Graph is a function") - val graph_is_function = complete - |> Thm.forall_elim_vars 0 - |> fold (curry op COMP) ex1s - |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) - |> forall_intr (cterm_of thy x) - |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) - |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) + val _ = trace_msg (K "Proving: Graph is a function") + val graph_is_function = complete + |> Thm.forall_elim_vars 0 + |> fold (curry op COMP) ex1s + |> implies_intr (ihyp) + |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) + |> forall_intr (cterm_of thy x) + |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) + |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) - val goalstate = Conjunction.intr graph_is_function complete - |> Thm.close_derivation - |> Goal.protect - |> fold_rev (implies_intr o cprop_of) compat - |> implies_intr (cprop_of complete) - in - (goalstate, values) - end + val goalstate = Conjunction.intr graph_is_function complete + |> Thm.close_derivation + |> Goal.protect + |> fold_rev (implies_intr o cprop_of) compat + |> implies_intr (cprop_of complete) + in + (goalstate, values) + end (* wrapper -- restores quantifiers in rule specifications *) fun inductive_def (binding as ((R, T), _)) intrs lthy = @@ -483,7 +458,7 @@ forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm end in - ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) + ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) end fun define_graph Gname fvar domT ranT clauses RCss lthy = @@ -544,33 +519,30 @@ fun fix_globals domT ranT fvar ctxt = - let - val ([h, y, x, z, a, D, P, Pbool],ctxt') = - Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt - in - (Globals {h = Free (h, domT --> ranT), - y = Free (y, ranT), - x = Free (x, domT), - z = Free (z, domT), - a = Free (a, domT), - D = Free (D, domT --> boolT), - P = Free (P, domT --> boolT), - Pbool = Free (Pbool, boolT), - fvar = fvar, - domT = domT, - ranT = ranT - }, - ctxt') - end - - + let + val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes + ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt + in + (Globals {h = Free (h, domT --> ranT), + y = Free (y, ranT), + x = Free (x, domT), + z = Free (z, domT), + a = Free (a, domT), + D = Free (D, domT --> boolT), + P = Free (P, domT --> boolT), + Pbool = Free (Pbool, boolT), + fvar = fvar, + domT = domT, + ranT = ranT}, + ctxt') + end fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = - let - 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 + let + 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 @@ -579,27 +551,27 @@ **********************************************************) fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = - let - val Globals {domT, z, ...} = globals + let + val Globals {domT, z, ...} = globals - fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = - let - val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) - val z_smaller = cterm_of thy (HOLogic.mk_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) - end - in - map2 mk_psimp clauses valthms - end + fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = + let + val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) + val z_smaller = cterm_of thy (HOLogic.mk_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) + end + in + map2 mk_psimp clauses valthms + end (** Induction rule **) @@ -609,232 +581,236 @@ fun mk_partial_induct_rule thy globals R complete_thm clauses = - let - val Globals {domT, x, z, a, P, D, ...} = globals - val acc_R = mk_acc domT R + let + val Globals {domT, x, z, a, P, D, ...} = globals + val acc_R = mk_acc domT R - val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) - val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) + val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) + val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) - val D_subset = cterm_of thy (Logic.all x - (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) + val D_subset = cterm_of thy (Logic.all x + (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) - val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) - Logic.all x - (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), - Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), - HOLogic.mk_Trueprop (D $ z))))) - |> cterm_of thy - + val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) + Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), + Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), + HOLogic.mk_Trueprop (D $ z))))) + |> cterm_of thy - (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = Term.all domT $ Abs ("z", domT, - Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), - HOLogic.mk_Trueprop (P $ Bound 0))) - |> cterm_of thy + (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) + val ihyp = Term.all domT $ Abs ("z", domT, + Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), + HOLogic.mk_Trueprop (P $ Bound 0))) + |> cterm_of thy - val aihyp = assume ihyp + val aihyp = assume ihyp - fun prove_case clause = + fun prove_case clause = let - val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, - qglr = (oqs, _, _, _), ...} = clause + val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, + RCs, qglr = (oqs, _, _, _), ...} = clause - val case_hyp_conv = K (case_hyp RS eq_reflection) - local open Conv in - val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D - val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp - end + val case_hyp_conv = K (case_hyp RS eq_reflection) + local open Conv in + val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D + val sih = + fconv_rule (More_Conv.binder_conv + (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp + end - fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = - sih |> forall_elim (cterm_of thy rcarg) - |> Thm.elim_implies llRI - |> fold_rev (implies_intr o cprop_of) CCas - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih + |> forall_elim (cterm_of thy rcarg) + |> Thm.elim_implies 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 P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) - val step = HOLogic.mk_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 (HOLogic.mk_Trueprop (D $ lhs)) - |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> cterm_of thy + val step = HOLogic.mk_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 (HOLogic.mk_Trueprop (D $ lhs)) + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) + |> cterm_of thy - val P_lhs = assume step - |> fold forall_elim cqs - |> Thm.elim_implies lhs_D - |> fold Thm.elim_implies ags - |> fold Thm.elim_implies P_recs + val P_lhs = assume step + |> fold forall_elim cqs + |> Thm.elim_implies lhs_D + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies P_recs - val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) - |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) - |> 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 + val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) + |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) + |> 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) + val (cases, steps) = split_list (map prove_case clauses) - val istep = complete_thm - |> 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 istep = complete_thm + |> 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 = + 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 + |> (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 = + 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 - simple_induct_rule - end + |> 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 + simple_induct_rule + end - -(* FIXME: This should probably use fixed goals, to be more reliable and faster *) +(* FIXME: broken by design *) fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = - let - val thy = ProofContext.theory_of ctxt - val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, - qglr = (oqs, _, _, _), ...} = clause - val goal = HOLogic.mk_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 [Thm.forall_elim_vars 0 R_cases] 1)) |> the - |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the - |> Goal.conclude - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) - end + let + val thy = ProofContext.theory_of ctxt + val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, + qglr = (oqs, _, _, _), ...} = clause + val goal = HOLogic.mk_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 [Thm.forall_elim_vars 0 R_cases] 1)) |> the + |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the + |> Goal.conclude + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) + end (** Termination rule **) -val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}; -val wf_in_rel = @{thm FunDef.wf_in_rel}; -val in_rel_def = @{thm FunDef.in_rel_def}; +val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} +val wf_in_rel = @{thm FunDef.wf_in_rel} +val in_rel_def = @{thm FunDef.in_rel_def} fun mk_nest_term_case thy globals R' ihyp clause = - let - val Globals {z, ...} = globals - val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree, - qglr=(oqs, _, _, _), ...} = clause + let + val Globals {z, ...} = globals + val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, + qglr=(oqs, _, _, _), ...} = clause - val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp + 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 (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub) + fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = + let + val used = (u @ sub) + |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) - val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) - |> Function_Ctx_Tree.export_term (fixes, assumes) - |> fold_rev (curry Logic.mk_implies o prop_of) ags - |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> cterm_of thy + val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) + |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) + |> Function_Ctx_Tree.export_term (fixes, 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 Thm.elim_implies ags - |> Function_Ctx_Tree.import_thm thy (fixes, assumes) - |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) + val thm = assume hyp + |> fold forall_elim cqs + |> fold Thm.elim_implies ags + |> Function_Ctx_Tree.import_thm thy (fixes, assumes) + |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) - val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg)))) + val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) + |> cterm_of thy |> assume - val acc = thm COMP ih_case - val z_acc_local = acc - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) + val acc = thm COMP ih_case + val z_acc_local = acc + |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) - val ethm = z_acc_local - |> Function_Ctx_Tree.export_thm thy (fixes, - z_eq_arg :: case_hyp :: ags @ assumes) - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) + val ethm = z_acc_local + |> Function_Ctx_Tree.export_thm thy (fixes, + z_eq_arg :: case_hyp :: 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 - in - Function_Ctx_Tree.traverse_tree step tree - end + val sub' = sub @ [(([],[]), acc)] + in + (sub', (hyp :: hyps, ethm :: thms)) + end + | step _ _ _ _ = raise Match + in + Function_Ctx_Tree.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 + let + val Globals { domT, x, z, ... } = globals + val acc_R = mk_acc domT R - val R' = Free ("R", fastype_of R) + val R' = Free ("R", fastype_of R) - val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) - val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel + val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) + val inrel_R = Const (@{const_name FunDef.in_rel}, + HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel - val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) + val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, + (domT --> domT --> boolT) --> boolT) $ R') + |> cterm_of thy (* "wf R'" *) - (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) - val ihyp = Term.all domT $ Abs ("z", domT, - Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), - HOLogic.mk_Trueprop (acc_R $ Bound 0))) - |> cterm_of thy + (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) + val ihyp = Term.all domT $ Abs ("z", domT, + Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), + HOLogic.mk_Trueprop (acc_R $ Bound 0))) + |> cterm_of thy - val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 + val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 - val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) + val R_z_x = cterm_of thy (HOLogic.mk_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') - |> forall_intr_vars - |> (fn it => it COMP allI) - |> 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 + 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') + |> forall_intr_vars + |> (fn it => it COMP allI) + |> 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 @@ -846,135 +822,150 @@ * - Splitting is not configured automatically: Problems with case? *) fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps = - let - val Globals {domT, ranT, fvar, ...} = globals + let + val Globals {domT, ranT, fvar, ...} = globals - val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) + val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) - val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) - Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] - (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) - (fn {prems=[a], ...} => - ((rtac (G_induct OF [a])) - THEN_ALL_NEW (rtac accI) - THEN_ALL_NEW (etac R_cases) - THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1) + val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) + Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] + (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) + (fn {prems=[a], ...} => + ((rtac (G_induct OF [a])) + THEN_ALL_NEW rtac accI + THEN_ALL_NEW etac R_cases + THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1) - val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value) + val default_thm = + forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value) - fun mk_trsimp clause psimp = - let - val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause - val thy = ProofContext.theory_of ctxt - val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs + fun mk_trsimp clause psimp = + let + val ClauseInfo {qglr = (oqs, _, _, _), cdata = + ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause + val thy = ProofContext.theory_of ctxt + val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs - val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) - val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) - fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def]) - in - Goal.prove ctxt [] [] trsimp - (fn _ => - rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 - THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 - THEN (simp_default_tac (simpset_of ctxt) 1) - THEN (etac not_acc_down 1) - THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1) - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) - end - in - map2 mk_trsimp clauses psimps - end + val trsimp = Logic.list_implies(gs, + HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) + val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) + fun simp_default_tac ss = + asm_full_simp_tac (ss addsimps [default_thm, Let_def]) + in + Goal.prove ctxt [] [] trsimp (fn _ => + rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 + THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 + THEN (simp_default_tac (simpset_of ctxt) 1) + THEN (etac not_acc_down 1) + THEN ((etac R_cases) + THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1) + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) + end + in + map2 mk_trsimp clauses psimps + end fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = - let - val FunctionConfig {domintros, tailrec, default=default_str, ...} = config + let + val FunctionConfig {domintros, tailrec, default=default_str, ...} = config - val fvar = Free (fname, fT) - val domT = domain_type fT - val ranT = range_type fT + val fvar = Free (fname, fT) + val domT = domain_type fT + val ranT = range_type fT - val default = Syntax.parse_term lthy default_str - |> TypeInfer.constrain fT |> Syntax.check_term lthy + val default = Syntax.parse_term lthy default_str + |> TypeInfer.constrain fT |> Syntax.check_term lthy + + val (globals, ctxt') = fix_globals domT ranT fvar lthy - val (globals, ctxt') = fix_globals domT ranT fvar lthy + val Globals { x, h, ... } = globals - val Globals { x, h, ... } = globals + val clauses = map (mk_clause_context x ctxt') abstract_qglrs + + val n = length abstract_qglrs - val clauses = map (mk_clause_context x ctxt') abstract_qglrs + fun build_tree (ClauseContext { ctxt, rhs, ...}) = + Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs - val n = length abstract_qglrs - - fun build_tree (ClauseContext { ctxt, rhs, ...}) = - Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs + val trees = map build_tree clauses + val RCss = map find_calls trees - val trees = map build_tree clauses - val RCss = map find_calls trees + val ((G, GIntro_thms, G_elim, G_induct), lthy) = + PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy + + val ((f, (_, f_defthm)), lthy) = + PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy - val ((G, GIntro_thms, G_elim, G_induct), lthy) = - PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy + val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss + val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees - val ((f, (_, f_defthm)), lthy) = - PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy + val ((R, RIntro_thmss, R_elim), lthy) = + PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy - val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss - val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees + val (_, lthy) = + Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy - val ((R, RIntro_thmss, R_elim), lthy) = - PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy + val newthy = ProofContext.theory_of lthy + val clauses = map (transfer_clause_ctx newthy) clauses - val (_, lthy) = - Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy + val cert = cterm_of (ProofContext.theory_of lthy) - val newthy = ProofContext.theory_of lthy - val clauses = map (transfer_clause_ctx newthy) clauses - - val cert = cterm_of (ProofContext.theory_of lthy) + val xclauses = PROFILE "xclauses" + (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees + RCss GIntro_thms) RIntro_thmss - val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss - - val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume - val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume) + val complete = + mk_completeness globals clauses abstract_qglrs |> cert |> assume - val compat_store = store_compat_thms n compat + val compat = + mk_compat_proof_obligations domT ranT fvar f abstract_qglrs + |> map (cert #> assume) - val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm - - val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses + val compat_store = store_compat_thms n compat - fun mk_partial_rules provedgoal = - let - val newthy = theory_of_thm provedgoal (*FIXME*) + val (goalstate, values) = PROFILE "prove_stuff" + (prove_stuff lthy globals G f R xclauses complete compat + compat_store G_elim) f_defthm + + val mk_trsimps = + mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses - val (graph_is_function, complete_thm) = - provedgoal - |> Conjunction.elim - |> apfst (Thm.forall_elim_vars 0) + fun mk_partial_rules provedgoal = + let + val newthy = theory_of_thm provedgoal (*FIXME*) - val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) + val (graph_is_function, complete_thm) = + provedgoal + |> Conjunction.elim + |> apfst (Thm.forall_elim_vars 0) - val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function + val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) + + val psimps = PROFILE "Proving simplification rules" + (mk_psimps newthy globals R xclauses values f_iff) graph_is_function - val simple_pinduct = PROFILE "Proving partial induction rule" - (mk_partial_induct_rule newthy globals R complete_thm) xclauses + val simple_pinduct = PROFILE "Proving partial induction rule" + (mk_partial_induct_rule newthy globals R complete_thm) xclauses - - val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses + val total_intro = PROFILE "Proving nested termination rule" + (mk_nest_term_rule newthy globals R R_elim) xclauses - val dom_intros = if domintros - then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) - else NONE - val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE + val dom_intros = + if domintros then SOME (PROFILE "Proving domain introduction rules" + (map (mk_domain_intro lthy globals R R_elim)) xclauses) + else NONE + val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE - in - FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, - psimps=psimps, simple_pinducts=[simple_pinduct], - termination=total_intro, trsimps=trsimps, - domintros=dom_intros} - end - in - ((f, goalstate, mk_partial_rules), lthy) - end + in + FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, + psimps=psimps, simple_pinducts=[simple_pinduct], + termination=total_intro, trsimps=trsimps, + domintros=dom_intros} + end + in + ((f, goalstate, mk_partial_rules), lthy) + end end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/function_lib.ML Sat Jan 02 23:18:58 2010 +0100 @@ -1,14 +1,14 @@ (* Title: HOL/Tools/Function/fundef_lib.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. -Some fairly general functions that should probably go somewhere else... +A package for general recursive function definitions. +Some fairly general functions that should probably go somewhere else... *) structure Function_Lib = struct -fun map_option f NONE = NONE +fun map_option f NONE = NONE | map_option f (SOME x) = SOME (f x); fun fold_option f NONE y = y @@ -21,50 +21,50 @@ (* lambda-abstracts over an arbitrarily nested tuple ==> hologic.ML? *) fun tupled_lambda vars t = - case vars of - (Free v) => lambda (Free v) t - | (Var v) => lambda (Var v) t - | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs => + case vars of + (Free v) => lambda (Free v) t + | (Var v) => lambda (Var v) t + | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs => (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t)) - | _ => raise Match + | _ => raise Match fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) = - let - val (n, body) = Term.dest_abs a - in - (Free (n, T), body) - end + let + val (n, body) = Term.dest_abs a + in + (Free (n, T), body) + end | dest_all _ = raise Match (* Removes all quantifiers from a term, replacing bound variables by frees. *) -fun dest_all_all (t as (Const ("all",_) $ _)) = - let - val (v,b) = dest_all t - val (vs, b') = dest_all_all b - in - (v :: vs, b') - end +fun dest_all_all (t as (Const ("all",_) $ _)) = + let + val (v,b) = dest_all t + val (vs, b') = dest_all_all b + in + (v :: vs, b') + end | dest_all_all t = ([],t) (* FIXME: similar to Variable.focus *) fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) = - let - val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] - val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx + let + val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] + val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx - val (n'', body) = Term.dest_abs (n', T, b) - val _ = (n' = n'') orelse error "dest_all_ctx" + val (n'', body) = Term.dest_abs (n', T, b) + val _ = (n' = n'') orelse error "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) - val (ctx'', vs, bd) = dest_all_all_ctx ctx' body - in - (ctx'', (n', T) :: vs, bd) - end - | dest_all_all_ctx ctx t = - (ctx, [], t) + val (ctx'', vs, bd) = dest_all_all_ctx ctx' body + in + (ctx'', (n', T) :: vs, bd) + end + | dest_all_all_ctx ctx t = + (ctx, [], t) fun map3 _ [] [] [] = [] @@ -86,52 +86,51 @@ (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) -(* ==> library *) fun unordered_pairs [] = [] | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs (* Replaces Frees by name. Works with loose Bounds. *) fun replace_frees assoc = - map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) - | t => t) + map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) + | t => t) -fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) +fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b)) | rename_bound n _ = raise Match fun mk_forall_rename (n, v) = - rename_bound n o Logic.all v + rename_bound n o Logic.all v fun forall_intr_rename (n, cv) thm = - let - val allthm = forall_intr cv thm - val (_ $ abs) = prop_of allthm - in - Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm - end + let + val allthm = forall_intr cv thm + val (_ $ abs) = prop_of allthm + in + Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm + end (* Returns the frees in a term in canonical order, excluding the fixes from the context *) fun frees_in_term ctxt t = - Term.add_frees t [] - |> filter_out (Variable.is_fixed ctxt o fst) - |> rev + Term.add_frees t [] + |> filter_out (Variable.is_fixed ctxt o fst) + |> rev datatype proof_attempt = Solved of thm | Stuck of thm | Fail -fun try_proof cgoal tac = - case SINGLE tac (Goal.init cgoal) of - NONE => Fail - | SOME st => - if Thm.no_prems st - then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) - else Stuck st +fun try_proof cgoal tac = + case SINGLE tac (Goal.init cgoal) of + NONE => Fail + | SOME st => + if Thm.no_prems st + then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) + else Stuck st -fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = - if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] +fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = + if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] | dest_binop_list _ t = [ t ] @@ -168,10 +167,10 @@ end (* instance for unions *) -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup} - (map (fn t => t RS eq_reflection) (@{thms Un_ac} @ - @{thms Un_empty_right} @ - @{thms Un_empty_left})) t +val regroup_union_conv = + regroup_conv @{const_name Set.empty} @{const_name Lattices.sup} + (map (fn t => t RS eq_reflection) + (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left})) end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Jan 02 23:18:58 2010 +0100 @@ -18,370 +18,367 @@ open Function_Lib - type rec_call_info = int * (string * typ) list * term list * term list -datatype scheme_case = - SchemeCase of - { - bidx : int, - qs: (string * typ) list, - oqnames: string list, - gs: term list, - lhs: term list, - rs: rec_call_info list - } +datatype scheme_case = SchemeCase of + {bidx : int, + qs: (string * typ) list, + oqnames: string list, + gs: term list, + lhs: term list, + rs: rec_call_info list} -datatype scheme_branch = - SchemeBranch of - { - P : term, - xs: (string * typ) list, - ws: (string * typ) list, - Cs: term list - } +datatype scheme_branch = SchemeBranch of + {P : term, + xs: (string * typ) list, + ws: (string * typ) list, + Cs: term list} -datatype ind_scheme = - IndScheme of - { - T: typ, (* sum of products *) - branches: scheme_branch list, - cases: scheme_case list - } +datatype ind_scheme = IndScheme of + {T: typ, (* sum of products *) + branches: scheme_branch list, + cases: scheme_case list} val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize} val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify} fun meta thm = thm RS eq_reflection -val sum_prod_conv = MetaSimplifier.rewrite true - (map meta (@{thm split_conv} :: @{thms sum.cases})) +val sum_prod_conv = MetaSimplifier.rewrite true + (map meta (@{thm split_conv} :: @{thms sum.cases})) -fun term_conv thy cv t = - cv (cterm_of thy t) - |> prop_of |> Logic.dest_equals |> snd +fun term_conv thy cv t = + cv (cterm_of thy t) + |> prop_of |> Logic.dest_equals |> snd fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) -fun dest_hhf ctxt t = - let - val (ctxt', vars, imp) = dest_all_all_ctx ctxt t - in - (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) - end - +fun dest_hhf ctxt t = + let + val (ctxt', vars, imp) = dest_all_all_ctx ctxt t + in + (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) + end fun mk_scheme' ctxt cases concl = - let - fun mk_branch concl = + let + fun mk_branch concl = + let + val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl + val (P, xs) = strip_comb Pxs + in + SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } + end + + val (branches, cases') = (* correction *) + case Logic.dest_conjunction_list concl of + [conc] => + let + val _ $ Pxs = Logic.strip_assums_concl conc + val (P, _) = strip_comb Pxs + val (cases', conds) = + take_prefix (Term.exists_subterm (curry op aconv P)) cases + val concl' = fold_rev (curry Logic.mk_implies) conds conc + in + ([mk_branch concl'], cases') + end + | concls => (map mk_branch concls, cases) + + fun mk_case premise = + let + val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise + val (P, lhs) = strip_comb Plhs + + fun bidx Q = + find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches + + fun mk_rcinfo pr = let - val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl - val (P, xs) = strip_comb Pxs + val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr + val (P', rcs) = strip_comb Phyp in - SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } + (bidx P', Gvs, Gas, rcs) end - val (branches, cases') = (* correction *) - case Logic.dest_conjunction_list concl of - [conc] => - let - val _ $ Pxs = Logic.strip_assums_concl conc - val (P, _) = strip_comb Pxs - val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases - val concl' = fold_rev (curry Logic.mk_implies) conds conc - in - ([mk_branch concl'], cases') - end - | concls => (map mk_branch concls, cases) - - fun mk_case premise = - let - val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise - val (P, lhs) = strip_comb Plhs - - fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches + fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches - fun mk_rcinfo pr = - let - val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr - val (P', rcs) = strip_comb Phyp - in - (bidx P', Gvs, Gas, rcs) - end - - fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches + val (gs, rcprs) = + take_prefix (not o Term.exists_subterm is_pred) prems + in + SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), + gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} + end - val (gs, rcprs) = - take_prefix (not o Term.exists_subterm is_pred) prems - in - SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} - end + fun PT_of (SchemeBranch { xs, ...}) = + foldr1 HOLogic.mk_prodT (map snd xs) - fun PT_of (SchemeBranch { xs, ...}) = - foldr1 HOLogic.mk_prodT (map snd xs) - - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) - in - IndScheme {T=ST, cases=map mk_case cases', branches=branches } - end - - + val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) + in + IndScheme {T=ST, cases=map mk_case cases', branches=branches } + end fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx - val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases + let + val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx + val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases + + val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] + val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) + val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs - val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] - val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) - val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs - - fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = - HOLogic.mk_Trueprop Pbool - |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) - (xs' ~~ lhs) - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in + fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = HOLogic.mk_Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - |> fold_rev mk_forall_rename (map fst xs ~~ xs') - |> mk_forall_rename ("P", Pbool) - end + |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) + (xs' ~~ lhs) + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) + in + HOLogic.mk_Trueprop Pbool + |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases + |> fold_rev (curry Logic.mk_implies) Cs' + |> fold_rev (Logic.all o Free) ws + |> fold_rev mk_forall_rename (map fst xs ~~ xs') + |> mk_forall_rename ("P", Pbool) + end fun mk_wf R (IndScheme {T, ...}) = - HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) + HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) fun mk_ineqs R (IndScheme {T, cases, branches}) = - let - fun inject i ts = - SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) + let + fun inject i ts = + SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) - val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) + val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) - fun mk_pres bdx args = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx - fun replace (x, v) t = betapply (lambda (Free x) t, v) - val Cs' = map (fold replace (xs ~~ args)) Cs - val cse = - HOLogic.mk_Trueprop thesis - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - in - Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) - end + fun mk_pres bdx args = + let + val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx + fun replace (x, v) t = betapply (lambda (Free x) t, v) + val Cs' = map (fold replace (xs ~~ args)) Cs + val cse = + HOLogic.mk_Trueprop thesis + |> fold_rev (curry Logic.mk_implies) Cs' + |> fold_rev (Logic.all o Free) ws + in + Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) + end - fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = - let - fun g (bidx', Gvs, Gas, rcarg) = - let val export = - fold_rev (curry Logic.mk_implies) Gas - #> fold_rev (curry Logic.mk_implies) gs - #> fold_rev (Logic.all o Free) Gvs - #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in - (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) - |> HOLogic.mk_Trueprop - |> export, - mk_pres bidx' rcarg - |> export - |> Logic.all thesis) - end + fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = + let + fun g (bidx', Gvs, Gas, rcarg) = + let val export = + fold_rev (curry Logic.mk_implies) Gas + #> fold_rev (curry Logic.mk_implies) gs + #> fold_rev (Logic.all o Free) Gvs + #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) in - map g rs + (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) + |> HOLogic.mk_Trueprop + |> export, + mk_pres bidx' rcarg + |> export + |> Logic.all thesis) end - in - map f cases - end + in + map g rs + end + in + map f cases + end fun mk_ind_goal thy branches = - let - fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = - HOLogic.mk_Trueprop (list_comb (P, map Free xs)) - |> fold_rev (curry Logic.mk_implies) Cs - |> fold_rev (Logic.all o Free) ws - |> term_conv thy ind_atomize - |> ObjectLogic.drop_judgment thy - |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) - in - SumTree.mk_sumcases HOLogic.boolT (map brnch branches) - end + let + fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = + HOLogic.mk_Trueprop (list_comb (P, map Free xs)) + |> fold_rev (curry Logic.mk_implies) Cs + |> fold_rev (Logic.all o Free) ws + |> term_conv thy ind_atomize + |> ObjectLogic.drop_judgment thy + |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) + in + SumTree.mk_sumcases HOLogic.boolT (map brnch branches) + end + +fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss + (IndScheme {T, cases=scases, branches}) = + let + val n = length branches + val scases_idx = map_index I scases + + fun inject i ts = + SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) + val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) + + val thy = ProofContext.theory_of ctxt + val cert = cterm_of thy + + val P_comp = mk_ind_goal thy branches + + (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) + val ihyp = Term.all T $ Abs ("z", T, + Logic.mk_implies + (HOLogic.mk_Trueprop ( + Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) + $ (HOLogic.pair_const T T $ Bound 0 $ x) + $ R), + HOLogic.mk_Trueprop (P_comp $ Bound 0))) + |> cert + + val aihyp = assume ihyp + + (* Rule for case splitting along the sum types *) + val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches + val pats = map_index (uncurry inject) xss + val sum_split_rule = + Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) + + fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = + let + val fxs = map Free xs + val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) + + val C_hyps = map (cert #> assume) Cs + + val (relevant_cases, ineqss') = + (scases_idx ~~ ineqss) + |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) + |> split_list + + fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = + let + val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) + + val cqs = map (cert o Free) qs + val ags = map (assume o cert) gs + + val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) + val sih = full_simplify replace_x_ss aihyp + + fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = + let + val cGas = map (assume o cert) Gas + val cGvs = map (cert o Free) Gvs + val import = fold forall_elim (cqs @ cGvs) + #> fold Thm.elim_implies (ags @ cGas) + val ipres = pres + |> forall_elim (cert (list_comb (P_of idx, rcargs))) + |> import + in + sih + |> forall_elim (cert (inject idx rcargs)) + |> Thm.elim_implies (import ineq) (* Psum rcargs *) + |> Conv.fconv_rule sum_prod_conv + |> Conv.fconv_rule ind_rulify + |> (fn th => th COMP ipres) (* P rs *) + |> fold_rev (implies_intr o cprop_of) cGas + |> fold_rev forall_intr cGvs + end + + val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) + + val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) + |> fold_rev (curry Logic.mk_implies o prop_of) P_recs + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev (Logic.all o Free) qs + |> cert + + val Plhs_to_Pxs_conv = + foldl1 (uncurry Conv.combination_conv) + (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) + + val res = assume step + |> fold forall_elim cqs + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies P_recs (* P lhs *) + |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) + |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) + |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) + in + (res, (cidx, step)) + end + + val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') + + val bstep = complete_thm + |> forall_elim (cert (list_comb (P, fxs))) + |> fold (forall_elim o cert) (fxs @ map Free ws) + |> fold Thm.elim_implies C_hyps + |> fold Thm.elim_implies cases (* P xs *) + |> fold_rev (implies_intr o cprop_of) C_hyps + |> fold_rev (forall_intr o cert o Free) ws + + val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) + |> Goal.init + |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) + THEN CONVERSION ind_rulify 1) + |> Seq.hd + |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) + |> Goal.finish ctxt + |> implies_intr (cprop_of branch_hyp) + |> fold_rev (forall_intr o cert) fxs + in + (Pxs, steps) + end + + val (branches, steps) = + map_index prove_branch (branches ~~ (complete_thms ~~ pats)) + |> split_list |> apsnd flat + + val istep = sum_split_rule + |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches + |> implies_intr ihyp + |> forall_intr (cert x) (* "!!x. (!!y P x" *) + + val induct_rule = + @{thm "wf_induct_rule"} + |> (curry op COMP) wf_thm + |> (curry op COMP) istep + + val steps_sorted = map snd (sort (int_ord o pairself fst) steps) + in + (steps_sorted, induct_rule) + end -fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) = - let - val n = length branches - - val scases_idx = map_index I scases - - fun inject i ts = - SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) - val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) - - val thy = ProofContext.theory_of ctxt - val cert = cterm_of thy - - val P_comp = mk_ind_goal thy branches - - (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = Term.all T $ Abs ("z", T, - Logic.mk_implies - (HOLogic.mk_Trueprop ( - Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) - $ (HOLogic.pair_const T T $ Bound 0 $ x) - $ R), - HOLogic.mk_Trueprop (P_comp $ Bound 0))) - |> cert - - val aihyp = assume ihyp - - (* Rule for case splitting along the sum types *) - val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches - val pats = map_index (uncurry inject) xss - val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) - - fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = - let - val fxs = map Free xs - val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) - - val C_hyps = map (cert #> assume) Cs - - val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss) - |> split_list - - fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = - let - val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) - - val cqs = map (cert o Free) qs - val ags = map (assume o cert) gs - - val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) - val sih = full_simplify replace_x_ss aihyp - - fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = - let - val cGas = map (assume o cert) Gas - val cGvs = map (cert o Free) Gvs - val import = fold forall_elim (cqs @ cGvs) - #> fold Thm.elim_implies (ags @ cGas) - val ipres = pres - |> forall_elim (cert (list_comb (P_of idx, rcargs))) - |> import - in - sih |> forall_elim (cert (inject idx rcargs)) - |> Thm.elim_implies (import ineq) (* Psum rcargs *) - |> Conv.fconv_rule sum_prod_conv - |> Conv.fconv_rule ind_rulify - |> (fn th => th COMP ipres) (* P rs *) - |> fold_rev (implies_intr o cprop_of) cGas - |> fold_rev forall_intr cGvs - end - - val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) - - val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) - |> fold_rev (curry Logic.mk_implies o prop_of) P_recs - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev (Logic.all o Free) qs - |> cert - - val Plhs_to_Pxs_conv = - foldl1 (uncurry Conv.combination_conv) - (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) - - val res = assume step - |> fold forall_elim cqs - |> fold Thm.elim_implies ags - |> fold Thm.elim_implies P_recs (* P lhs *) - |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) - |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) - |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) - in - (res, (cidx, step)) - end - - val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') - - val bstep = complete_thm - |> forall_elim (cert (list_comb (P, fxs))) - |> fold (forall_elim o cert) (fxs @ map Free ws) - |> fold Thm.elim_implies C_hyps (* FIXME: optimization using rotate_prems *) - |> fold Thm.elim_implies cases (* P xs *) - |> fold_rev (implies_intr o cprop_of) C_hyps - |> fold_rev (forall_intr o cert o Free) ws - - val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) - |> Goal.init - |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) - THEN CONVERSION ind_rulify 1) - |> Seq.hd - |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) - |> Goal.finish ctxt - |> implies_intr (cprop_of branch_hyp) - |> fold_rev (forall_intr o cert) fxs - in - (Pxs, steps) - end - - val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats))) - |> apsnd flat - - val istep = sum_split_rule - |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches - |> implies_intr ihyp - |> forall_intr (cert x) (* "!!x. (!!y P x" *) - - val induct_rule = - @{thm "wf_induct_rule"} - |> (curry op COMP) wf_thm - |> (curry op COMP) istep - - val steps_sorted = map snd (sort (int_ord o pairself fst) steps) - in - (steps_sorted, induct_rule) - end - - -fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL -(SUBGOAL (fn (t, i) => +fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = + (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) => let val (ctxt', _, cases, concl) = dest_hhf ctxt t val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl -(* val _ = tracing (makestring scheme)*) val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' val R = Free (Rn, mk_relT ST) val x = Free (xn, ST) val cert = cterm_of (ProofContext.theory_of ctxt) val ineqss = mk_ineqs R scheme - |> map (map (pairself (assume o cert))) - val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) + |> map (map (pairself (assume o cert))) + val complete = + map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) val wf_thm = mk_wf R scheme |> cert |> assume val (descent, pres) = split_list (flat ineqss) - val newgoals = complete @ pres @ wf_thm :: descent + val newgoals = complete @ pres @ wf_thm :: descent - val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme + val (steps, indthm) = + mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme fun project (i, SchemeBranch {xs, ...}) = - let - val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs))) - in - indthm |> Drule.instantiate' [] [SOME inst] - |> simplify SumTree.sumcase_split_ss - |> Conv.fconv_rule ind_rulify -(* |> (fn thm => (tracing (makestring thm); thm))*) - end + let + val inst = (foldr1 HOLogic.mk_prod (map Free xs)) + |> SumTree.mk_inj ST (length branches) (i + 1) + |> cert + in + indthm + |> Drule.instantiate' [] [SOME inst] + |> simplify SumTree.sumcase_split_ss + |> Conv.fconv_rule ind_rulify + end val res = Conjunction.intr_balanced (map_index project branches) - |> fold_rev implies_intr (map cprop_of newgoals @ steps) - |> Drule.generalize ([], [Rn]) + |> fold_rev implies_intr (map cprop_of newgoals @ steps) + |> Drule.generalize ([], [Rn]) val nbranches = length branches val npres = length pres diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Jan 02 23:18:58 2010 +0100 @@ -21,26 +21,27 @@ (** General stuff **) fun mk_measures domT mfuns = - let - val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) - val mlexT = (domT --> HOLogic.natT) --> relT --> relT - fun mk_ms [] = Const (@{const_name Set.empty}, relT) - | mk_ms (f::fs) = - Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs - in - mk_ms mfuns - end + let + val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) + val mlexT = (domT --> HOLogic.natT) --> relT --> relT + fun mk_ms [] = Const (@{const_name Set.empty}, relT) + | mk_ms (f::fs) = + Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs + in + mk_ms mfuns + end 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) (** Matrix cell datatype **) -datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm; +datatype cell = + Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm; fun is_Less (Less _) = true | is_Less _ = false @@ -57,39 +58,39 @@ (** Proof attempts to build the matrix **) fun dest_term (t : term) = - let - val (vars, prop) = Function_Lib.dest_all_all t - val (prems, concl) = Logic.strip_horn prop - val (lhs, rhs) = concl - |> HOLogic.dest_Trueprop - |> HOLogic.dest_mem |> fst - |> HOLogic.dest_prod - in - (vars, prems, lhs, rhs) - end + let + val (vars, prop) = Function_Lib.dest_all_all t + val (prems, concl) = Logic.strip_horn prop + val (lhs, rhs) = concl + |> HOLogic.dest_Trueprop + |> HOLogic.dest_mem |> fst + |> HOLogic.dest_prod + in + (vars, prems, lhs, rhs) + end fun mk_goal (vars, prems, lhs, rhs) rel = - let - val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop - in - fold_rev Logic.all vars (Logic.list_implies (prems, concl)) - end + let + val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop + in + fold_rev Logic.all vars (Logic.list_implies (prems, concl)) + end fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = - let - val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) - in - case try_proof (goals @{const_name HOL.less}) solve_tac of - Solved thm => Less thm - | Stuck thm => - (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of - Solved thm2 => LessEq (thm2, thm) - | Stuck thm2 => - if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2 - else None (thm2, thm) - | _ => raise Match) (* FIXME *) - | _ => raise Match - end + let + val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) + in + case try_proof (goals @{const_name HOL.less}) solve_tac of + Solved thm => Less thm + | Stuck thm => + (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of + Solved thm2 => LessEq (thm2, thm) + | Stuck thm2 => + if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2 + else None (thm2, thm) + | _ => raise Match) (* FIXME *) + | _ => raise Match + end (** Search algorithms **) @@ -102,21 +103,21 @@ (* simple depth-first search algorithm for the table *) fun search_table table = - case table of - [] => SOME [] - | _ => - let - val col = find_index (check_col) (transpose table) - in case col of - ~1 => NONE - | _ => - let - val order_opt = (table, col) |-> transform_table |> search_table - in case order_opt of - NONE => NONE - | SOME order =>SOME (col :: transform_order col order) - end - end + case table of + [] => SOME [] + | _ => + let + val col = find_index (check_col) (transpose table) + in case col of + ~1 => NONE + | _ => + let + val order_opt = (table, col) |-> transform_table |> search_table + in case order_opt of + NONE => NONE + | SOME order =>SOME (col :: transform_order col order) + end + end (** Proof Reconstruction **) @@ -134,9 +135,9 @@ (** Error reporting **) fun pr_goals ctxt st = - Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st - |> Pretty.chunks - |> Pretty.string_of + Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st + |> Pretty.chunks + |> Pretty.string_of fun row_index i = chr (i + 97) fun col_index j = string_of_int (j + 1) @@ -151,65 +152,67 @@ "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st fun pr_unprovable_subgoals ctxt table = - table - |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) - |> flat - |> map (pr_unprovable_cell ctxt) + table + |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) + |> flat + |> map (pr_unprovable_cell ctxt) fun no_order_msg ctxt table tl measure_funs = - let - val prterm = Syntax.string_of_term ctxt - fun pr_fun t i = string_of_int i ^ ") " ^ prterm t + let + val prterm = Syntax.string_of_term ctxt + fun pr_fun t i = string_of_int i ^ ") " ^ prterm t - fun pr_goal t i = - let - val (_, _, lhs, rhs) = dest_term t - in (* also show prems? *) - i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs - end + fun pr_goal t i = + let + val (_, _, lhs, rhs) = dest_term t + in (* also show prems? *) + i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs + end - val gc = map (fn i => chr (i + 96)) (1 upto length table) - val mc = 1 upto length measure_funs - val tstr = "Result matrix:" :: (" " ^ implode (map (enclose " " " " o string_of_int) mc)) - :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc - val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc - val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc - val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table - in - cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) - end + val gc = map (fn i => chr (i + 96)) (1 upto length table) + val mc = 1 upto length measure_funs + val tstr = "Result matrix:" :: (" " ^ implode (map (enclose " " " " o string_of_int) mc)) + :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc + val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc + val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc + val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table + in + cat_lines (ustr @ gstr @ mstr @ tstr @ + ["", "Could not find lexicographic termination order."]) + end (** The Main Function **) fun lex_order_tac quiet ctxt solve_tac (st: thm) = - let - val thy = ProofContext.theory_of ctxt - val ((_ $ (_ $ rel)) :: tl) = prems_of st + let + val thy = ProofContext.theory_of ctxt + val ((_ $ (_ $ rel)) :: tl) = prems_of st - val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) + val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) - val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *) + val measure_funs = (* 1: generate measures *) + MeasureFunctions.get_measure_functions ctxt domT - (* 2: create table *) - val table = Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl - in - case search_table table of - NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs) - | SOME order => - let - val clean_table = map (fn x => map (nth x) order) table - val relation = mk_measures domT (map (nth measure_funs) order) - val _ = if not quiet - then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation)) - else () + val table = (* 2: create table *) + Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl + in + case search_table table of + NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs) + | SOME order => + let + val clean_table = map (fn x => map (nth x) order) table + val relation = mk_measures domT (map (nth measure_funs) order) + val _ = if not quiet + then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation)) + else () - in (* 4: proof reconstruction *) - st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) - THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) - THEN (rtac @{thm "wf_empty"} 1) - THEN EVERY (map prove_row clean_table)) - end - end + in (* 4: proof reconstruction *) + st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) + THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) + THEN (rtac @{thm "wf_empty"} 1) + THEN EVERY (map prove_row clean_table)) + end + end fun lexicographic_order_tac quiet ctxt = TRY (Function_Common.apply_termination_rule ctxt 1) @@ -225,4 +228,3 @@ #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order) end; - diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/measure_functions.ML Sat Jan 02 23:18:58 2010 +0100 @@ -8,26 +8,28 @@ sig val get_measure_functions : Proof.context -> typ -> term list - val setup : theory -> theory + val setup : theory -> theory end -structure MeasureFunctions : MEASURE_FUNCTIONS = -struct +structure MeasureFunctions : MEASURE_FUNCTIONS = +struct (** User-declared size functions **) structure Measure_Heuristic_Rules = Named_Thms ( - val name = "measure_function" - val description = "Rules that guide the heuristic generation of measure functions" + val name = "measure_function" + val description = + "Rules that guide the heuristic generation of measure functions" ); -fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t +fun mk_is_measure t = + Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t fun find_measures ctxt T = - DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) - (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT))) - |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) + DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) + (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) + |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |> Seq.list_of @@ -38,13 +40,13 @@ fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) fun mk_funorder_funs (Type ("+", [fT, sT])) = - map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) - @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) + map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT) + @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) | mk_funorder_funs T = [ constant_1 T ] fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) = - map_product (SumTree.mk_sumcase fT sT HOLogic.natT) - (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) + map_product (SumTree.mk_sumcase fT sT HOLogic.natT) + (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) | mk_ext_base_funs ctxt T = find_measures ctxt T fun mk_all_measure_funs ctxt (T as Type ("+", _)) = @@ -56,4 +58,3 @@ val setup = Measure_Heuristic_Rules.setup end - diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Sat Jan 02 23:18:58 2010 +0100 @@ -9,13 +9,13 @@ sig val prepare_function_mutual : Function_Common.function_config - -> string (* defname *) - -> ((string * typ) * mixfix) list - -> term list - -> local_theory - -> ((thm (* goalstate *) - * (thm -> Function_Common.function_result) (* proof continuation *) - ) * local_theory) + -> string (* defname *) + -> ((string * typ) * mixfix) list + -> term list + -> local_theory + -> ((thm (* goalstate *) + * (thm -> Function_Common.function_result) (* proof continuation *) + ) * local_theory) end @@ -28,282 +28,269 @@ type qgar = string * (string * typ) list * term list * term list * term -datatype mutual_part = - MutualPart of - { - i : int, - i' : int, - fvar : string * typ, - cargTs: typ list, - f_def: term, +datatype mutual_part = MutualPart of + {i : int, + i' : int, + fvar : string * typ, + cargTs: typ list, + f_def: term, - f: term option, - f_defthm : thm option - } - + f: term option, + f_defthm : thm option} -datatype mutual_info = - Mutual of - { - n : int, - n' : int, - fsum_var : string * typ, +datatype mutual_info = Mutual of + {n : int, + n' : int, + fsum_var : string * typ, - ST: typ, - RST: typ, + ST: typ, + RST: typ, - 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} fun mutual_induct_Pnames n = - if n < 5 then fst (chop n ["P","Q","R","S"]) - else map (fn i => "P" ^ string_of_int i) (1 upto n) + if n < 5 then fst (chop n ["P","Q","R","S"]) + else map (fn i => "P" ^ string_of_int i) (1 upto n) fun get_part fname = - the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) - + the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) + (* FIXME *) fun mk_prod_abs e (t1, t2) = - let - val bTs = rev (map snd e) - val T1 = fastype_of1 (bTs, t1) - val T2 = fastype_of1 (bTs, t2) - in - HOLogic.pair_const T1 T2 $ t1 $ t2 - end; - + let + val bTs = rev (map snd e) + val T1 = fastype_of1 (bTs, t1) + val T2 = fastype_of1 (bTs, t2) + in + HOLogic.pair_const T1 T2 $ t1 $ t2 + end fun analyze_eqs ctxt defname fs eqs = - let - val num = length fs - val fqgars = map (split_def ctxt) eqs - val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars - |> AList.lookup (op =) #> the + let + val num = length fs + val fqgars = map (split_def ctxt) eqs + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the - fun curried_types (fname, fT) = - let - val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) - in - (caTs, uaTs ---> body_type fT) - end + fun curried_types (fname, fT) = + let + val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) + in + (caTs, uaTs ---> body_type fT) + end - val (caTss, resultTs) = split_list (map curried_types fs) - val argTs = map (foldr1 HOLogic.mk_prodT) caTss + val (caTss, resultTs) = split_list (map curried_types fs) + val argTs = map (foldr1 HOLogic.mk_prodT) caTss - val dresultTs = distinct (op =) resultTs - val n' = length dresultTs + val dresultTs = distinct (op =) resultTs + val n' = length dresultTs - val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs + val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs + val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs - val fsum_type = ST --> RST + val fsum_type = ST --> RST - val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt - val fsum_var = (fsum_var_name, fsum_type) + val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt + val fsum_var = (fsum_var_name, fsum_type) - fun define (fvar as (n, _)) caTs resultT i = - let - val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) - val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 + fun define (fvar as (n, _)) caTs resultT i = + let + val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) + val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 - val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) - val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) + val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) + val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) - val rew = (n, fold_rev lambda vars f_exp) - in - (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) - end - - val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) + val rew = (n, fold_rev lambda vars f_exp) + in + (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) + end + + val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) - fun convert_eqs (f, qs, gs, args, rhs) = - let - val MutualPart {i, i', ...} = get_part f parts - in - (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), - SumTree.mk_inj RST n' i' (replace_frees rews rhs) - |> Envir.beta_norm) - end + fun convert_eqs (f, qs, gs, args, rhs) = + let + val MutualPart {i, i', ...} = get_part f parts + in + (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), + SumTree.mk_inj RST n' i' (replace_frees rews rhs) + |> Envir.beta_norm) + end - val qglrs = map convert_eqs fqgars - in - Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, - parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} - end - - - + val qglrs = map convert_eqs fqgars + in + Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, + parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} + end fun define_projections fixes mutual fsum lthy = - let - fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = - let - val ((f, (_, f_defthm)), lthy') = - Local_Theory.define - ((Binding.name fname, mixfix), - ((Binding.conceal (Binding.name (fname ^ "_def")), []), - Term.subst_bound (fsum, f_def))) lthy - in - (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, - f=SOME f, f_defthm=SOME f_defthm }, - lthy') - end - - val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual - val (parts', lthy') = fold_map def (parts ~~ fixes) lthy - in - (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', - fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, - lthy') - end + let + fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = + let + val ((f, (_, f_defthm)), lthy') = + Local_Theory.define + ((Binding.name fname, mixfix), + ((Binding.conceal (Binding.name (fname ^ "_def")), []), + Term.subst_bound (fsum, f_def))) lthy + in + (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, + f=SOME f, f_defthm=SOME f_defthm }, + lthy') + end + val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual + val (parts', lthy') = fold_map def (parts ~~ fixes) lthy + in + (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', + fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, + lthy') + end 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, _) = Variable.variant_fixes oqnames ctxt - |>> 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 - val rhs = inst pre_rhs + let + val thy = ProofContext.theory_of ctxt + + val oqnames = map fst pre_qs + val (qs, _) = Variable.variant_fixes oqnames ctxt + |>> 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 + val rhs = inst pre_rhs - val cqs = map (cterm_of thy) qs - val ags = map (assume o cterm_of thy) gs + val cqs = map (cterm_of thy) qs + val ags = map (assume o cterm_of thy) gs - val import = fold forall_elim cqs - #> fold Thm.elim_implies ags + val import = fold forall_elim cqs + #> fold Thm.elim_implies ags - val export = fold_rev (implies_intr o cprop_of) ags - #> fold_rev forall_intr_rename (oqnames ~~ cqs) - in - F ctxt (f, qs, gs, args, rhs) import export - end - -fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq = - let - val (MutualPart {f=SOME f, ...}) = get_part fname parts + val export = fold_rev (implies_intr o cprop_of) ags + #> fold_rev forall_intr_rename (oqnames ~~ cqs) + in + F ctxt (f, qs, gs, args, rhs) import export + end - val psimp = import sum_psimp_eq - val (simp, restore_cond) = case cprems_of psimp of - [] => (psimp, I) - | [cond] => (implies_elim psimp (assume cond), implies_intr cond) - | _ => sys_error "Too many conditions" - in - Goal.prove ctxt [] [] - (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) - (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs) - THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1) - |> restore_cond - |> export - end +fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) + import (export : thm -> thm) sum_psimp_eq = + let + val (MutualPart {f=SOME f, ...}) = get_part fname parts + + val psimp = import sum_psimp_eq + val (simp, restore_cond) = + case cprems_of psimp of + [] => (psimp, I) + | [cond] => (implies_elim psimp (assume cond), implies_intr cond) + | _ => sys_error "Too many conditions" + in + Goal.prove ctxt [] [] + (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) + (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs) + THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 + THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1) + |> restore_cond + |> export + end -(* FIXME HACK *) fun mk_applied_form ctxt caTs thm = - let - val thy = ProofContext.theory_of ctxt - val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) - in - fold (fn x => fn thm => combination thm (reflexive x)) xs thm - |> Conv.fconv_rule (Thm.beta_conversion true) - |> fold_rev forall_intr xs - |> Thm.forall_elim_vars 0 - end - + let + val thy = ProofContext.theory_of ctxt + val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) + in + fold (fn x => fn thm => combination thm (reflexive x)) xs thm + |> Conv.fconv_rule (Thm.beta_conversion true) + |> fold_rev forall_intr xs + |> Thm.forall_elim_vars 0 + end fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = - let - val cert = cterm_of (ProofContext.theory_of lthy) - val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => - 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 = SumTree.mk_sumcases HOLogic.boolT Ps - - val induct_inst = - forall_elim (cert case_exp) induct - |> full_simplify SumTree.sumcase_split_ss - |> full_simplify (HOL_basic_ss addsimps all_f_defs) - - fun project rule (MutualPart {cargTs, i, ...}) k = - let - val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) - val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) - in - (rule - |> forall_elim (cert inj) - |> full_simplify SumTree.sumcase_split_ss - |> fold_rev (forall_intr o cert) (afs @ newPs), - k + length cargTs) - end - in - fst (fold_map (project induct_inst) parts 0) - end - + let + val cert = cterm_of (ProofContext.theory_of lthy) + val newPs = + map2 (fn Pname => fn MutualPart {cargTs, ...} => + 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 = SumTree.mk_sumcases HOLogic.boolT Ps + + val induct_inst = + forall_elim (cert case_exp) induct + |> full_simplify SumTree.sumcase_split_ss + |> full_simplify (HOL_basic_ss addsimps all_f_defs) + + fun project rule (MutualPart {cargTs, i, ...}) k = + let + val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) + val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) + in + (rule + |> forall_elim (cert inj) + |> full_simplify SumTree.sumcase_split_ss + |> fold_rev (forall_intr o cert) (afs @ newPs), + k + length cargTs) + end + in + fst (fold_map (project induct_inst) parts 0) + end fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = - let - val result = inner_cont proof - val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct], - termination, domintros, ...} = result - - val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => - (mk_applied_form lthy cargTs (symmetric f_def), f)) - parts - |> split_list + let + val result = inner_cont proof + val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct], + termination, domintros, ...} = result + + val (all_f_defs, fs) = + map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => + (mk_applied_form lthy cargTs (symmetric f_def), f)) + parts + |> split_list + + val all_orig_fdefs = + map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts + + fun mk_mpsimp fqgar sum_psimp = + in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp - val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts - - fun mk_mpsimp fqgar sum_psimp = - in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp - - val rew_ss = HOL_basic_ss addsimps all_f_defs - val mpsimps = map2 mk_mpsimp fqgars psimps - val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps - val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m - val mtermination = full_simplify rew_ss termination - val mdomintros = map_option (map (full_simplify rew_ss)) domintros - in - FunctionResult { fs=fs, G=G, R=R, - psimps=mpsimps, simple_pinducts=minducts, - cases=cases, termination=mtermination, - domintros=mdomintros, - trsimps=mtrsimps} - end - + val rew_ss = HOL_basic_ss addsimps all_f_defs + val mpsimps = map2 mk_mpsimp fqgars psimps + val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps + val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m + val mtermination = full_simplify rew_ss termination + val mdomintros = map_option (map (full_simplify rew_ss)) domintros + in + FunctionResult { fs=fs, G=G, R=R, + psimps=mpsimps, simple_pinducts=minducts, + cases=cases, termination=mtermination, + domintros=mdomintros, trsimps=mtrsimps} + end + fun prepare_function_mutual config defname fixes eqss lthy = - let - val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) - val Mutual {fsum_var=(n, T), qglrs, ...} = mutual - - val ((fsum, goalstate, cont), lthy') = - Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy - - val (mutual', lthy'') = define_projections fixes mutual fsum lthy' + let + val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = + analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) + + val ((fsum, goalstate, cont), lthy') = + Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy - val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' - in - ((goalstate, mutual_cont), lthy'') - end + val (mutual', lthy'') = define_projections fixes mutual fsum lthy' - + val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' + in + ((goalstate, mutual_cont), lthy'') + end + end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/pattern_split.ML Sat Jan 02 23:18:58 2010 +0100 @@ -1,10 +1,7 @@ (* Title: HOL/Tools/Function/pattern_split.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. - -Automatic splitting of overlapping constructor patterns. This is a preprocessing step which -turns a specification with overlaps into an overlap-free specification. +Fairly ad-hoc pattern splitting. *) @@ -22,114 +19,102 @@ open Function_Lib -(* We use proof context for the variable management *) -(* FIXME: no __ *) - fun new_var ctx vs T = - let - val [v] = Variable.variant_frees ctx vs [("v", T)] - in - (Free v :: vs, Free v) - end + let + val [v] = Variable.variant_frees ctx vs [("v", T)] + in + (Free v :: vs, Free v) + end fun saturate ctx vs t = - fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t)) - (binder_types (fastype_of t)) (vs, t) - - -(* This is copied from "fundef_datatype.ML" *) + 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 "pat_completeness.ML" *) fun inst_constrs_of thy (T as Type (name, _)) = - map (fn (Cn,CT) => - Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) - (the (Datatype.get_constrs thy name)) + map (fn (Cn,CT) => + Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) + (the (Datatype.get_constrs thy name)) | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) - - - + fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2) fun join_product (xs, ys) = map_product (curry join) xs ys - exception DISJ fun pattern_subtract_subst ctx vs t t' = - let - exception DISJ - fun pattern_subtract_subst_aux vs _ (Free v2) = [] - | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' = + let + exception DISJ + fun pattern_subtract_subst_aux vs _ (Free v2) = [] + | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' = + let + fun foo constr = let - fun foo constr = - let - val (vs', t) = saturate ctx vs constr - val substs = pattern_subtract_subst ctx vs' t t' - in - map (fn (vs, subst) => (vs, (v,t)::subst)) substs - end + val (vs', t) = saturate ctx vs constr + val substs = pattern_subtract_subst ctx vs' t t' in - maps foo (inst_constrs_of (ProofContext.theory_of ctx) T) + map (fn (vs, subst) => (vs, (v,t)::subst)) substs end - | pattern_subtract_subst_aux vs t t' = - let - val (C, ps) = strip_comb t - val (C', qs) = strip_comb t' - in - if C = C' - then flat (map2 (pattern_subtract_subst_aux vs) ps qs) - else raise DISJ - end - in - pattern_subtract_subst_aux vs t t' - handle DISJ => [(vs, [])] - end - + in + maps foo (inst_constrs_of (ProofContext.theory_of ctx) T) + end + | pattern_subtract_subst_aux vs t t' = + let + val (C, ps) = strip_comb t + val (C', qs) = strip_comb t' + in + if C = C' + then flat (map2 (pattern_subtract_subst_aux vs) ps qs) + else raise DISJ + end + in + pattern_subtract_subst_aux vs t t' + handle DISJ => [(vs, [])] + end (* p - q *) 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 - in - fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t - end - in - map instantiate substs - end - + 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 + in + fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t + end + in + map instantiate substs + end (* ps - p' *) fun pattern_subtract_from_many ctx p'= - maps (pattern_subtract ctx p') + maps (pattern_subtract ctx p') (* in reverse order *) fun pattern_subtract_many ctx ps' = - fold_rev (pattern_subtract_from_many ctx) ps' - - + fold_rev (pattern_subtract_from_many ctx) ps' fun split_some_equations ctx eqns = - let - fun split_aux prev [] = [] - | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq] - :: split_aux (eq :: prev) es - | split_aux prev ((false, eq) :: es) = [eq] - :: split_aux (eq :: prev) es - in - split_aux [] eqns - end - + let + fun split_aux prev [] = [] + | split_aux prev ((true, eq) :: es) = + pattern_subtract_many ctx prev [eq] :: split_aux (eq :: prev) es + | split_aux prev ((false, eq) :: es) = + [eq] :: split_aux (eq :: prev) es + in + split_aux [] eqns + end + fun split_all_equations ctx = - split_some_equations ctx o map (pair true) - - + split_some_equations ctx o map (pair true) end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/relation.ML Sat Jan 02 23:18:58 2010 +0100 @@ -15,18 +15,18 @@ struct fun inst_thm ctxt rel st = - let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt) - val rel' = cert (singleton (Variable.polymorphic ctxt) rel) - val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st - val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) - in - Drule.cterm_instantiate [(Rvar, rel')] st' - end + let + val cert = Thm.cterm_of (ProofContext.theory_of ctxt) + val rel' = cert (singleton (Variable.polymorphic ctxt) rel) + val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st + val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) + in + Drule.cterm_instantiate [(Rvar, rel')] st' + end -fun relation_tac ctxt rel i = - TRY (Function_Common.apply_termination_rule ctxt i) - THEN PRIMITIVE (inst_thm ctxt rel) +fun relation_tac ctxt rel i = + TRY (Function_Common.apply_termination_rule ctxt i) + THEN PRIMITIVE (inst_thm ctxt rel) val setup = Method.setup @{binding relation} diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/sum_tree.ML --- a/src/HOL/Tools/Function/sum_tree.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/sum_tree.ML Sat Jan 02 23:18:58 2010 +0100 @@ -9,35 +9,43 @@ (* Theory dependencies *) val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}] -val sumcase_split_ss = HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) +val sumcase_split_ss = + HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) (* top-down access in balanced tree *) fun access_top_down {left, right, init} len i = - Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init + Balanced_Tree.access + {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init (* Sum types *) fun mk_sumT LT RT = Type ("+", [LT, RT]) -fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r +fun mk_sumcase TL TR T l r = + Const (@{const_name sum.sum_case}, + (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r val App = curry op $ -fun mk_inj ST n i = - access_top_down - { init = (ST, I : term -> term), - left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))), - right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i - |> snd +fun mk_inj ST n i = + access_top_down + { init = (ST, I : term -> term), + left = (fn (T as Type ("+", [LT, RT]), inj) => + (LT, inj o App (Const (@{const_name Inl}, LT --> T)))), + right =(fn (T as Type ("+", [LT, RT]), inj) => + (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i + |> snd -fun mk_proj ST n i = - access_top_down - { init = (ST, I : term -> term), - left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)), - right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i - |> snd +fun mk_proj ST n i = + access_top_down + { init = (ST, I : term -> term), + left = (fn (T as Type ("+", [LT, RT]), proj) => + (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)), + right =(fn (T as Type ("+", [LT, RT]), proj) => + (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i + |> snd fun mk_sumcases T fs = - Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) - (map (fn f => (f, domain_type (fastype_of f))) fs) - |> fst + Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) + (map (fn f => (f, domain_type (fastype_of f))) fs) + |> fst end diff -r da4d7d40f2f9 -r 36a2a3029fd3 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Sat Jan 02 23:18:58 2010 +0100 +++ b/src/HOL/Tools/Function/termination.ML Sat Jan 02 23:18:58 2010 +0100 @@ -245,66 +245,65 @@ (* A tactic to convert open to closed termination goals *) local fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *) - let - val (vars, prop) = Function_Lib.dest_all_all t - val (prems, concl) = Logic.strip_horn prop - val (lhs, rhs) = concl - |> HOLogic.dest_Trueprop - |> HOLogic.dest_mem |> fst - |> HOLogic.dest_prod - in - (vars, prems, lhs, rhs) - end + let + val (vars, prop) = Function_Lib.dest_all_all t + val (prems, concl) = Logic.strip_horn prop + val (lhs, rhs) = concl + |> HOLogic.dest_Trueprop + |> HOLogic.dest_mem |> fst + |> HOLogic.dest_prod + in + (vars, prems, lhs, rhs) + end fun mk_pair_compr (T, qs, l, r, conds) = - let - val pT = HOLogic.mk_prodT (T, T) - val n = length qs - val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r) - val conds' = if null conds then [HOLogic.true_const] else conds - in - HOLogic.Collect_const pT $ - Abs ("uu_", pT, - (foldr1 HOLogic.mk_conj (peq :: conds') - |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs)) - end + let + val pT = HOLogic.mk_prodT (T, T) + val n = length qs + val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r) + val conds' = if null conds then [HOLogic.true_const] else conds + in + HOLogic.Collect_const pT $ + Abs ("uu_", pT, + (foldr1 HOLogic.mk_conj (peq :: conds') + |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs)) + end in fun wf_union_tac ctxt st = - let - val thy = ProofContext.theory_of ctxt - val cert = cterm_of (theory_of_thm st) - val ((_ $ (_ $ rel)) :: ineqs) = prems_of st + let + val thy = ProofContext.theory_of ctxt + val cert = cterm_of (theory_of_thm st) + val ((_ $ (_ $ rel)) :: ineqs) = prems_of st - fun mk_compr ineq = - let - val (vars, prems, lhs, rhs) = dest_term ineq - in - mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems) - end + fun mk_compr ineq = + let + val (vars, prems, lhs, rhs) = dest_term ineq + in + mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems) + end - val relation = - if null ineqs then - Const (@{const_name Set.empty}, fastype_of rel) - else - foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) (map mk_compr ineqs) + val relation = + if null ineqs + then Const (@{const_name Set.empty}, fastype_of rel) + else map mk_compr ineqs + |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) - fun solve_membership_tac i = - (EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *) - THEN' (fn j => TRY (rtac @{thm UnI1} j)) - THEN' (rtac @{thm CollectI}) (* unfold comprehension *) - THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) - THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) - ORELSE' ((rtac @{thm conjI}) - THEN' (rtac @{thm refl}) - THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) - ) i - in - ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) - THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st - end - + fun solve_membership_tac i = + (EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *) + THEN' (fn j => TRY (rtac @{thm UnI1} j)) + THEN' (rtac @{thm CollectI}) (* unfold comprehension *) + THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) + THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) + ORELSE' ((rtac @{thm conjI}) + THEN' (rtac @{thm refl}) + THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) + ) i + in + ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) + THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st + end end @@ -332,67 +331,65 @@ fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) => let - val thy = ProofContext.theory_of ctxt + val thy = ProofContext.theory_of ctxt - fun derive_chain c1 c2 D = - if is_some (get_chain D c1 c2) then D else - note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D + fun derive_chain c1 c2 D = + if is_some (get_chain D c1 c2) then D else + note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D in cont (fold_product derive_chain cs cs D) i end) fun mk_dgraph D cs = - TermGraph.empty - |> fold (fn c => TermGraph.new_node (c,())) cs - |> fold_product (fn c1 => fn c2 => - if is_none (get_chain D c1 c2 |> the_default NONE) - then TermGraph.add_edge (c1, c2) else I) - cs cs - + TermGraph.empty + |> fold (fn c => TermGraph.new_node (c,())) cs + |> fold_product (fn c1 => fn c2 => + if is_none (get_chain D c1 c2 |> the_default NONE) + then TermGraph.add_edge (c1, c2) else I) + cs cs fun ucomp_empty_tac T = - REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR} - ORELSE' rtac @{thm union_comp_emptyL} - ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i)) + REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR} + ORELSE' rtac @{thm union_comp_emptyL} + ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i)) fun regroup_calls_tac cs = CALLS (fn (cs', i) => - let - val is = map (fn c => find_index (curry op aconv c) cs') cs - in - CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv is))) i - end) + let + val is = map (fn c => find_index (curry op aconv c) cs') cs + in + CONVERSION (Conv.arg_conv (Conv.arg_conv + (Function_Lib.regroup_union_conv is))) i + end) -fun solve_trivial_tac D = CALLS -(fn ([c], i) => - (case get_chain D c c of - SOME (SOME thm) => rtac @{thm wf_no_loop} i - THEN rtac thm i - | _ => no_tac) +fun solve_trivial_tac D = CALLS (fn ([c], i) => + (case get_chain D c c of + SOME (SOME thm) => rtac @{thm wf_no_loop} i + THEN rtac thm i + | _ => no_tac) | _ => no_tac) fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) => - let - val G = mk_dgraph D cs - val sccs = TermGraph.strong_conn G + let + val G = mk_dgraph D cs + val sccs = TermGraph.strong_conn G - fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i) - | split (SCC::rest) i = - regroup_calls_tac SCC i - THEN rtac @{thm wf_union_compatible} i - THEN rtac @{thm less_by_empty} (i + 2) - THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2) - THEN split rest (i + 1) - THEN (solve_trivial_tac D i ORELSE cont D i) - in - if length sccs > 1 then split sccs i - else solve_trivial_tac D i ORELSE err_cont D i - end) + fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i) + | split (SCC::rest) i = + regroup_calls_tac SCC i + THEN rtac @{thm wf_union_compatible} i + THEN rtac @{thm less_by_empty} (i + 2) + THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2) + THEN split rest (i + 1) + THEN (solve_trivial_tac D i ORELSE cont D i) + in + if length sccs > 1 then split sccs i + else solve_trivial_tac D i ORELSE err_cont D i + end) fun decompose_tac ctxt chain_tac cont err_cont = - derive_chains ctxt chain_tac - (decompose_tac' cont err_cont) + derive_chains ctxt chain_tac (decompose_tac' cont err_cont) (*** Local Descent Proofs ***)