# HG changeset patch # User krauss # Date 1161180783 -7200 # Node ID c49467a9c1e147bd51334f0b5af8446ac269750d # Parent d0447a511edb5d8bfcb0dd53546061415c4338c8 Switched function package to use the new package for inductive predicates. diff -r d0447a511edb -r c49467a9c1e1 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/FunDef.thy Wed Oct 18 16:13:03 2006 +0200 @@ -23,6 +23,89 @@ ("Tools/function_package/auto_term.ML") begin +section {* Wellfoundedness and Accessibility: Predicate versions *} + + +constdefs + wfP :: "('a \ 'a \ bool) => bool" + "wfP(r) == (!P. (!x. (!y. r y x --> P(y)) --> P(x)) --> (!x. P(x)))" + +lemma wfP_induct: + "[| wfP r; + !!x.[| ALL y. r y x --> P(y) |] ==> P(x) + |] ==> P(a)" +by (unfold wfP_def, blast) + +lemmas wfP_induct_rule = wfP_induct [rule_format, consumes 1, case_names less] + +definition in_rel_def[simp]: + "in_rel R x y == (x, y) \ R" + +lemma wf_in_rel: + "wf R \ wfP (in_rel R)" + unfolding wfP_def wf_def in_rel_def . + + +inductive2 accP :: "('a \ 'a \ bool) \ 'a \ bool" + for r :: "'a \ 'a \ bool" +intros + accPI: "(!!y. r y x ==> accP r y) ==> accP r x" + + +theorem accP_induct: + assumes major: "accP r a" + assumes hyp: "!!x. accP r x ==> \y. r y x --> P y ==> P x" + shows "P a" + apply (rule major [THEN accP.induct]) + apply (rule hyp) + apply (rule accPI) + apply fast + apply fast + done + +theorems accP_induct_rule = accP_induct [rule_format, induct set: accP] + +theorem accP_downward: "accP r b ==> r a b ==> accP r a" + apply (erule accP.cases) + apply fast + done + + +lemma accP_subset: + assumes sub: "\x y. R1 x y \ R2 x y" + shows "\x. accP R2 x \ accP R1 x" +proof- + fix x assume "accP R2 x" + then show "accP R1 x" + proof (induct x) + fix x + assume ih: "\y. R2 y x \ accP R1 y" + with sub show "accP R1 x" + by (blast intro:accPI) + qed +qed + + +lemma accP_subset_induct: + assumes subset: "\x. D x \ accP R x" + and dcl: "\x z. \D x; R z x\ \ D z" + and "D x" + and istep: "\x. \D x; (\z. R z x \ P z)\ \ P x" + shows "P x" +proof - + from subset and `D x` + have "accP R x" . + then show "P x" using `D x` + proof (induct x) + fix x + assume "D x" + and "\y. R y x \ D y \ P y" + with dcl and istep show "P x" by blast + qed +qed + + +section {* Definitions with default value *} definition THE_default :: "'a \ ('a \ bool) \ 'a" @@ -41,37 +124,41 @@ lemma fundef_ex1_existence: -assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" -assumes ex1: "\!y. (x,y)\G" -shows "(x, f x)\G" +assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" +assumes ex1: "\!y. G x y" +shows "G x (f x)" by (simp only:f_def, rule THE_defaultI', rule ex1) + + + + lemma fundef_ex1_uniqueness: -assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" -assumes ex1: "\!y. (x,y)\G" -assumes elm: "(x, h x)\G" +assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" +assumes ex1: "\!y. G x y" +assumes elm: "G x (h x)" shows "h x = f x" by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) lemma fundef_ex1_iff: -assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" -assumes ex1: "\!y. (x,y)\G" -shows "((x, y)\G) = (f x = y)" +assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" +assumes ex1: "\!y. G x y" +shows "(G x y) = (f x = y)" apply (auto simp:ex1 f_def THE_default1_equality) by (rule THE_defaultI', rule ex1) lemma fundef_default_value: -assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" -assumes graph: "\x y. (x,y) \ G \ x \ D" +assumes f_def: "f == (\x::'a. THE_default (d x) (\y. G x y))" +assumes graph: "\x y. G x y \ x \ D" assumes "x \ D" shows "f x = d x" proof - - have "\(\y. (x, y) \ G)" + have "\(\y. G x y)" proof - assume "(\y. (x, y) \ G)" + assume "(\y. G x y)" with graph and `x\D` show False by blast qed - hence "\(\!y. (x, y) \ G)" by blast + hence "\(\!y. G x y)" by blast thus ?thesis unfolding f_def @@ -80,8 +167,7 @@ - -subsection {* Projections *} +section {* Projections *} consts lpg::"(('a + 'b) * 'a) set" rpg::"(('a + 'b) * 'b) set" @@ -105,6 +191,8 @@ +lemma P_imp_P: "P \ P" . + use "Tools/function_package/sum_tools.ML" use "Tools/function_package/fundef_common.ML" diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Wed Oct 18 16:13:03 2006 +0200 @@ -42,6 +42,7 @@ struct open FundefCommon +open FundefLib (* Maps "Trueprop A = B" to "A" *) diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Oct 18 16:13:03 2006 +0200 @@ -10,10 +10,10 @@ struct (* Theory Dependencies *) -val acc_const_name = "Accessible_Part.acc" +val acc_const_name = "FunDef.accP" fun mk_acc domT R = - Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R + Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R type depgraph = int IntGraph.T @@ -221,36 +221,41 @@ = Sequential | Default of string | Preprocessor of string + | Target of xstring datatype fundef_config = FundefConfig of { sequential: bool, default: string, - preprocessor: string option + preprocessor: string option, + target: xstring option } -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE } -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE } +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE } +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE } -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor}) = - FundefConfig {sequential=true, default=default, preprocessor=preprocessor } - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor}) = - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor } - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor}) = - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p } +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target}) = + FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target } + | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target}) = + FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target } + | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target}) = + FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target } + | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t } - + local structure P = OuterParse and K = OuterKeyword in val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false val option_parser = (P.$$$ "sequential" >> K Sequential) || ((P.reserved "default" |-- P.term) >> Default) + || ((P.$$$ "in" |-- P.xname) >> Target) -val config_parser = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) - >> (fn opts => fold apply_opt opts default_config) +fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) + >> (fn opts => fold apply_opt opts def) end @@ -263,6 +268,7 @@ + end diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Wed Oct 18 16:13:03 2006 +0200 @@ -17,6 +17,8 @@ structure FundefDatatype : FUNDEF_DATATYPE = struct +open FundefLib +open FundefCommon fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Wed Oct 18 16:13:03 2006 +0200 @@ -7,6 +7,9 @@ *) + +structure FundefLib = struct + fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) fun mk_forall (var as Free (v,T)) t = @@ -128,3 +131,6 @@ fun plural sg pl [] = sys_error "plural" | plural sg pl [x] = sg | plural sg pl (x::y::ys) = pl + + +end \ No newline at end of file diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Oct 18 16:13:03 2006 +0200 @@ -32,6 +32,7 @@ structure FundefPackage = struct +open FundefLib open FundefCommon (*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*) @@ -187,12 +188,13 @@ val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) + ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) >> (fn (((config, target), fixes), statements) => Toplevel.print o Toplevel.local_theory_to_proof target (add_fundef fixes statements config))); + val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal (P.opt_locale_target -- Scan.option P.name diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Wed Oct 18 16:13:03 2006 +0200 @@ -22,13 +22,14 @@ struct +open FundefLib open FundefCommon open FundefAbbrev (* Theory dependencies. *) val Pair_inject = thm "Product_Type.Pair_inject"; -val acc_induct_rule = thm "Accessible_Part.acc_induct_rule" +val acc_induct_rule = thm "FunDef.accP_induct_rule" val ex1_implies_ex = thm "FunDef.fundef_ex1_existence" val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness" @@ -143,7 +144,7 @@ |> fold implies_elim_swp rcassm val h_assum = - mk_relmem (rcarg, h $ rcarg) G + Trueprop (G $ rcarg $ (h $ rcarg)) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (mk_forall o Free) rcfix |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] @@ -272,20 +273,15 @@ val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) - - val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h))))) 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') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *) - |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) - |> implies_elim_swp eq_pairs - |> fold_rev (implies_intr o cprop_of) Ghsj' - |> fold_rev (implies_intr o cprop_of) agsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) - |> implies_intr (cprop_of eq_pairs) + |> implies_intr (cprop_of lhsi_eq_lhsj') |> fold_rev forall_intr (cterm_of thy h :: cqsj') end @@ -305,21 +301,21 @@ val existence = fold (curry op COMP o prep_RC) RCs lGI - val a = cterm_of thy (mk_prod (lhs, y)) val P = cterm_of thy (mk_eq (y, rhsC)) - val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G)))) + val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y))) val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas val uniqueness = G_cases - |> forall_elim a + |> forall_elim (cterm_of thy lhs) + |> forall_elim (cterm_of thy y) |> forall_elim P - |> implies_elim_swp a_in_G + |> implies_elim_swp G_lhs_y |> fold implies_elim_swp unique_clauses - |> implies_intr (cprop_of a_in_G) + |> implies_intr (cprop_of G_lhs_y) |> forall_intr (cterm_of thy y) - val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* 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)] @@ -332,11 +328,11 @@ 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 + |> 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 @@ -348,15 +344,15 @@ let val Globals {h, domT, ranT, x, ...} = globals - val inst_ex1_ex = f_def RS ex1_implies_ex - val inst_ex1_un = f_def RS ex1_implies_un + val inst_ex1_ex = f_def RS ex1_implies_ex + val inst_ex1_un = f_def RS ex1_implies_un val inst_ex1_iff = f_def RS ex1_implies_iff (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R) + implies $ Trueprop (R $ Bound 0 $ x) $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ - Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))) + Abs ("y", ranT, G $ Bound 1 $ Bound 0))) |> cterm_of thy val ihyp_thm = assume ihyp |> forall_elim_vars 0 @@ -375,7 +371,7 @@ |> forall_elim_vars 0 |> fold (curry op COMP) ex1s |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, mk_acc domT R)))) + |> implies_intr (cterm_of thy (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) (term_vars (prop_of it)) it) @@ -394,17 +390,17 @@ fun define_graph Gname fvar domT ranT clauses RCss lthy = let - val GT = mk_relT (domT, ranT) + val GT = domT --> ranT --> boolT val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)])) fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = let fun mk_h_assm (rcfix, rcassm, rcarg) = - mk_relmem (rcarg, fvar $ rcarg) Gvar + Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (mk_forall o Free) rcfix in - mk_relmem (lhs, rhs) Gvar + Trueprop (Gvar $ lhs $ rhs) |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |> fold_rev (curry Logic.mk_implies) gs |> fold_rev mk_forall (fvar :: qs) @@ -424,7 +420,8 @@ let val f_def = Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ - Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)) + Abs ("y", ranT, G $ Bound 1 $ Bound 0)) + |> Envir.beta_norm (* Fixme: LocalTheory.def does not work if not beta-normal *) val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy in @@ -435,11 +432,11 @@ fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy = let - val RT = mk_relT (domT, domT) + val RT = domT --> domT --> boolT val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)])) fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = - mk_relmem (rcarg, lhs) Rvar + Trueprop (Rvar $ rcarg $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (mk_forall o Free) rcfix @@ -465,7 +462,7 @@ x = Free (x, domT), z = Free (z, domT), a = Free (a, domT), - D = Free (D, HOLogic.mk_setT domT), + D = Free (D, domT --> boolT), P = Free (P, domT --> boolT), Pbool = Free (Pbool, boolT), fvar = fvar, @@ -521,7 +518,7 @@ val ((R, RIntro_thmss, R_elim), lthy) = define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy - val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", fastype_of (mk_acc domT R)), mk_acc domT R) + val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R) val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy val newthy = ProofContext.theory_of lthy diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Wed Oct 18 16:13:03 2006 +0200 @@ -18,21 +18,24 @@ structure FundefProof : FUNDEF_PROOF = struct +open FundefLib open FundefCommon open FundefAbbrev (* Theory dependencies *) val subsetD = thm "subsetD" -val subset_refl = thm "subset_refl" val split_apply = thm "Product_Type.split" -val wf_induct_rule = thm "wf_induct_rule"; +val wf_induct_rule = thm "FunDef.wfP_induct_rule"; val Pair_inject = thm "Product_Type.Pair_inject"; -val acc_induct_rule = thm "Accessible_Part.acc_induct_rule" -val acc_downward = thm "Accessible_Part.acc_downward" -val accI = thm "Accessible_Part.accI" +val wf_in_rel = thm "FunDef.wf_in_rel"; +val in_rel_def = thm "FunDef.in_rel_def"; -val acc_subset_induct = thm "Accessible_Part.acc_subset_induct" +val acc_induct_rule = thm "FunDef.accP_induct_rule" +val acc_downward = thm "FunDef.accP_downward" +val accI = thm "FunDef.accPI" + +val acc_subset_induct = thm "FunDef.accP_subset_induct" val conjunctionD1 = thm "conjunctionD1" val conjunctionD2 = thm "conjunctionD2" @@ -43,18 +46,18 @@ val Globals {domT, z, ...} = globals val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause - val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, mk_acc domT R))) (* "lhs : acc R" *) - val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *) + val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) + val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *) in ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) - |> (fn it => it COMP graph_is_function) - |> implies_intr z_smaller - |> forall_intr (cterm_of thy z) - |> (fn it => it COMP valthm) - |> implies_intr lhs_acc - |> asm_simplify (HOL_basic_ss addsimps [f_iff]) - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) + |> (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 @@ -64,22 +67,22 @@ val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R - val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D)))) - val a_D = cterm_of thy (Trueprop (mk_mem (a, D))) + val x_D = assume (cterm_of thy (Trueprop (D $ x))) + val a_D = cterm_of thy (Trueprop (D $ a)) - val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R)) + val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) mk_forall x - (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)), - Logic.mk_implies (mk_relmem (z, x) R, - Trueprop (mk_mem (z, D)))))) + (mk_forall z (Logic.mk_implies (Trueprop (D $ x), + Logic.mk_implies (Trueprop (R $ z $ x), + Trueprop (D $ z))))) |> cterm_of thy (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R) + implies $ Trueprop (R $ Bound 0 $ x) $ Trueprop (P $ Bound 0)) |> cterm_of thy @@ -105,7 +108,7 @@ val step = Trueprop (P $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs - |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D))) + |> curry Logic.mk_implies (Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy @@ -152,10 +155,10 @@ subset_induct_rule |> forall_intr (cterm_of thy D) |> forall_elim (cterm_of thy acc_R) - |> (curry op COMP) subset_refl + |> assume_tac 1 |> Seq.hd |> (curry op COMP) (acc_downward |> (instantiate' [SOME (ctyp_of thy domT)] - (map (SOME o cterm_of thy) [x, R, z])) + (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) @@ -172,7 +175,7 @@ val Globals {z, domT, ...} = globals val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause - val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs, mk_acc domT R))) + val goal = Trueprop (mk_acc domT R $ lhs) |> fold_rev (curry Logic.mk_implies) gs |> cterm_of thy in @@ -199,7 +202,7 @@ let val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub) - val hyp = mk_relmem (arg, lhs) R' + val hyp = Trueprop (R' $ arg $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) used |> FundefCtxTree.export_term (fixes, map prop_of assumes) |> fold_rev (curry Logic.mk_implies o prop_of) ags @@ -222,11 +225,12 @@ |> implies_intr (cprop_of case_hyp) |> implies_intr z_eq_arg - val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs)))) + val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg)))) + val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) - val ethm = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)) + val ethm = (z_acc OF [z_eq_arg, x_eq_lhs]) |> FundefCtxTree.export_thm thy (fixes, - (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes)) + prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes)) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) val sub' = sub @ [(([],[]), acc)] @@ -246,36 +250,43 @@ val R' = Free ("R", fastype_of R) - val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *) + val Rrel = Free ("R", mk_relT (domT, domT)) + val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel + + val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R') - $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT)) - $ Bound 0 $ acc_R)) + implies $ Trueprop (R' $ Bound 0 $ x) + $ Trueprop (acc_R $ Bound 0)) |> cterm_of thy val ihyp_a = assume ihyp |> forall_elim_vars 0 - val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *) + val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) in R_cases - |> forall_elim (cterm_of thy (mk_prod (z,x))) - |> forall_elim (cterm_of thy (mk_mem (z, acc_R))) - |> curry op COMP (assume z_ltR_x) + |> 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 z_ltR_x + |> 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)) - |> implies_elim_swp (assume wfR') + |> curry op RS (assume wfR') |> fold implies_intr hyps |> implies_intr wfR' |> forall_intr (cterm_of thy R') + |> forall_elim (cterm_of thy (inrel_R)) + |> curry op RS wf_in_rel + |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) + |> forall_intr (cterm_of thy Rrel) end diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/inductive_wrap.ML --- a/src/HOL/Tools/function_package/inductive_wrap.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Wed Oct 18 16:13:03 2006 +0200 @@ -30,81 +30,61 @@ structure FundefInductiveWrap = struct - -fun inst_forall (Free (n,_)) (_ $ Abs (_, T, b)) = subst_bound (Free (n, T), b) - | inst_forall t1 t2 = sys_error ((Sign.string_of_term (the_context ()) t1)) - -fun permute_bounds_in_premises thy [] impl = impl - | permute_bounds_in_premises thy ((oldvs, newvs) :: perms) impl = - let - val (prem, concl) = dest_implies (cprop_of impl) +open FundefLib - val newprem = term_of prem - |> fold inst_forall oldvs - |> fold_rev mk_forall newvs - |> cterm_of thy +fun requantify ctxt lfix (qs, t) thm = + let + val thy = theory_of_thm (print thm) + val frees = frees_in_term ctxt t + |> remove (op =) lfix + val vars = Term.add_vars (prop_of thm) [] |> rev + + val varmap = frees ~~ vars in - assume newprem - |> fold (forall_elim o cterm_of thy) newvs - |> fold_rev (forall_intr o cterm_of thy) oldvs - |> implies_elim impl - |> permute_bounds_in_premises thy perms - |> implies_intr newprem - end - + fold_rev (fn Free (n, T) => + forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T)))))) + qs + thm + end + + fun inductive_def defs (((R, T), mixfix), lthy) = let - fun wrap1 thy = - let - val thy = Sign.add_consts_i [(R, T, mixfix)] thy - val RC = Const (Sign.full_name thy R, T) - - val cdefs = map (Pattern.rewrite_term thy [(Free (R, T), RC)] []) defs - val qdefs = map dest_all_all cdefs - - val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = - OldInductivePackage.add_inductive_i true (*verbose*) - false (* dont add_consts *) - "" (* no altname *) - false (* no coind *) - false (* elims, please *) - false (* induction thm please *) - [RC] (* the constant *) - (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *) - [] (* no special monos *) - thy - - val perms = map (fn (qs, t) => ((term_frees t) inter qs, qs)) qdefs + val qdefs = map dest_all_all defs + + val (lthy, {intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}) = + InductivePackage.add_inductive_i true (*verbose*) + "" (* no altname *) + false (* no coind *) + false (* elims, please *) + false (* induction thm please *) + [(R, SOME T, NoSyn)] (* the relation *) + [] (* no parameters *) + (map (fn t => (("", []), t)) defs) (* the intros *) + [] (* no special monos *) + lthy - fun inst (qs, _) intr_gen = - intr_gen - |> Thm.freezeT - |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs - - - val a = cterm_of thy (Free ("a0123", HOLogic.dest_setT T)) (* Let's just hope there are no clashes :-} *) - val P = cterm_of thy (Free ("P0123", HOLogic.boolT)) + val thy = ProofContext.theory_of lthy - val intrs = map2 inst qdefs intrs_gen + fun inst qdef intr_gen = + intr_gen + |> Thm.freezeT + |> requantify lthy (R, T) qdef + + val intrs = map2 inst qdefs intrs_gen + + val elim = elim_gen + |> Thm.freezeT + |> forall_intr_vars (* FIXME... *) - val elim = elim_gen - |> Thm.freezeT - |> forall_intr_vars (* FIXME... *) - |> forall_elim a - |> forall_elim P - |> permute_bounds_in_premises thy (([],[]) :: perms) - |> forall_intr P - |> forall_intr a - in - ((RC, (intrs, elim)), thy) - end - - val ((RC, (intrs, elim)), lthy) = LocalTheory.theory_result wrap1 lthy + val Rdef_real = prop_of (Thm.freezeT elim_gen) + |> Logic.dest_implies |> fst + |> Term.strip_comb |> snd |> hd (* Trueprop *) + |> Term.strip_comb |> fst in - (intrs, (RC, elim, lthy)) + (intrs, (Rdef_real, elim, lthy)) end - - + end diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Wed Oct 18 16:13:03 2006 +0200 @@ -27,6 +27,7 @@ structure FundefMutual: FUNDEF_MUTUAL = struct +open FundefLib open FundefCommon (* Theory dependencies *) diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/pattern_split.ML --- a/src/HOL/Tools/function_package/pattern_split.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Oct 18 16:13:03 2006 +0200 @@ -21,6 +21,7 @@ structure FundefSplit : FUNDEF_SPLIT = struct +open FundefLib (* We use proof context for the variable management *) (* FIXME: no __ *) diff -r d0447a511edb -r c49467a9c1e1 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/Tools/function_package/termination.ML Wed Oct 18 16:13:03 2006 +0200 @@ -17,6 +17,7 @@ struct +open FundefLib open FundefCommon open FundefAbbrev @@ -25,7 +26,7 @@ val domT = domain_type (fastype_of f) val x = Free ("x", domT) in - Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R)) + Trueprop (mk_acc domT R $ x) end fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom = diff -r d0447a511edb -r c49467a9c1e1 src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Wed Oct 18 10:15:39 2006 +0200 +++ b/src/HOL/ex/Fundefs.thy Wed Oct 18 16:13:03 2006 +0200 @@ -11,7 +11,6 @@ section {* Very basic *} - fun fib :: "nat \ nat" where "fib 0 = 1" @@ -58,7 +57,7 @@ | "nz (Suc x) = nz (nz x)" lemma nz_is_zero: -- {* A lemma we need to prove termination *} - assumes trm: "x \ nz_dom" + assumes trm: "nz_dom x" shows "nz x = 0" using trm by induct auto @@ -72,14 +71,14 @@ text {* Here comes McCarthy's 91-function *} + fun f91 :: "nat => nat" where "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" - (* Prove a lemma before attempting a termination proof *) lemma f91_estimate: - assumes trm: "n : f91_dom" + assumes trm: "f91_dom n" shows "n < f91 n + 11" using trm by induct auto @@ -91,7 +90,7 @@ fix n::nat assume "~ 100 < n" (* Inner call *) thus "(n + 11, n) : ?R" by simp - assume inner_trm: "n + 11 : f91_dom" (* Outer call *) + assume inner_trm: "f91_dom (n + 11)" (* Outer call *) with f91_estimate have "n + 11 < f91 (n + 11) + 11" . with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp qed