Switched function package to use the new package for inductive predicates.
--- 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 \<Rightarrow> 'a \<Rightarrow> 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) \<in> R"
+
+lemma wf_in_rel:
+ "wf R \<Longrightarrow> wfP (in_rel R)"
+ unfolding wfP_def wf_def in_rel_def .
+
+
+inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> 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 ==> \<forall>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: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
+ shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
+proof-
+ fix x assume "accP R2 x"
+ then show "accP R1 x"
+ proof (induct x)
+ fix x
+ assume ih: "\<And>y. R2 y x \<Longrightarrow> accP R1 y"
+ with sub show "accP R1 x"
+ by (blast intro:accPI)
+ qed
+qed
+
+
+lemma accP_subset_induct:
+ assumes subset: "\<And>x. D x \<Longrightarrow> accP R x"
+ and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
+ and "D x"
+ and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> 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 "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
+ with dcl and istep show "P x" by blast
+ qed
+qed
+
+
+section {* Definitions with default value *}
definition
THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
@@ -41,37 +124,41 @@
lemma fundef_ex1_existence:
-assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
-assumes ex1: "\<exists>!y. (x,y)\<in>G"
-shows "(x, f x)\<in>G"
+assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+assumes ex1: "\<exists>!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 \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
-assumes ex1: "\<exists>!y. (x,y)\<in>G"
-assumes elm: "(x, h x)\<in>G"
+assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+assumes ex1: "\<exists>!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 \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
-assumes ex1: "\<exists>!y. (x,y)\<in>G"
-shows "((x, y)\<in>G) = (f x = y)"
+assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+assumes ex1: "\<exists>!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 \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
-assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D"
+assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
+assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D"
assumes "x \<notin> D"
shows "f x = d x"
proof -
- have "\<not>(\<exists>y. (x, y) \<in> G)"
+ have "\<not>(\<exists>y. G x y)"
proof
- assume "(\<exists>y. (x, y) \<in> G)"
+ assume "(\<exists>y. G x y)"
with graph and `x\<notin>D` show False by blast
qed
- hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast
+ hence "\<not>(\<exists>!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 \<Longrightarrow> P" .
+
use "Tools/function_package/sum_tools.ML"
use "Tools/function_package/fundef_common.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" *)
--- 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
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *)
--- 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 __ *)
--- 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 =
--- 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 \<Rightarrow> 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 \<in> 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