--- 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
--- 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
--- 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))
--- 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
-
--- 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
--- 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
--- 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<x. P 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<x. P 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
--- 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;
-
--- 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
-
--- 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
--- 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
--- 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}
--- 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
--- 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 ***)