--- a/src/HOL/Bali/Basis.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Aug 02 10:36:50 2011 +0200
@@ -3,7 +3,7 @@
*)
header {* Definitions extending HOL as logical basis of Bali *}
-theory Basis imports Main begin
+theory Basis imports Main "~~/src/HOL/Library/Old_Recdef" begin
section "misc"
--- a/src/HOL/Bali/Decl.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Bali/Decl.thy Tue Aug 02 10:36:50 2011 +0200
@@ -5,7 +5,8 @@
*}
theory Decl
-imports Term Table (** order is significant, because of clash for "var" **)
+imports Term Table
+ (** order is significant, because of clash for "var" **)
begin
text {*
--- a/src/HOL/Decision_Procs/Cooper.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Tue Aug 02 10:36:50 2011 +0200
@@ -3,7 +3,7 @@
*)
theory Cooper
-imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
+imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
uses ("cooper_tac.ML")
begin
--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
theory Ferrack
imports Complex_Main Dense_Linear_Order DP_Library
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
uses ("ferrack_tac.ML")
begin
--- a/src/HOL/Decision_Procs/MIR.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
theory MIR
imports Complex_Main Dense_Linear_Order DP_Library
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
uses ("mir_tac.ML")
begin
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
theory Parametric_Ferrante_Rackoff
imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
- "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
begin
subsection {* Terms *}
--- a/src/HOL/Induct/Sexp.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Induct/Sexp.thy Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
structures by hand.
*)
-theory Sexp imports Main begin
+theory Sexp imports Main "~~/src/HOL/Library/Old_Recdef" begin
type_synonym 'a item = "'a Datatype.item"
abbreviation "Leaf == Datatype.Leaf"
--- a/src/HOL/IsaMakefile Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 02 10:36:50 2011 +0200
@@ -292,7 +292,6 @@
Quotient.thy \
Random.thy \
Random_Sequence.thy \
- Recdef.thy \
Record.thy \
Refute.thy \
Semiring_Normalization.thy \
@@ -359,7 +358,6 @@
Tools/Quotient/quotient_tacs.ML \
Tools/Quotient/quotient_term.ML \
Tools/Quotient/quotient_typ.ML \
- Tools/recdef.ML \
Tools/record.ML \
Tools/semiring_normalizer.ML \
Tools/Sledgehammer/async_manager.ML \
@@ -389,15 +387,6 @@
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
- Tools/TFL/casesplit.ML \
- Tools/TFL/dcterm.ML \
- Tools/TFL/post.ML \
- Tools/TFL/rules.ML \
- Tools/TFL/tfl.ML \
- Tools/TFL/thms.ML \
- Tools/TFL/thry.ML \
- Tools/TFL/usyntax.ML \
- Tools/TFL/utils.ML
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
@@ -464,7 +453,8 @@
Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
Library/Nat_Bijection.thy Library/Nested_Environment.thy \
- Library/Numeral_Type.thy Library/OptionalSugar.thy \
+ Library/Numeral_Type.thy Library/Old_Recdef.thy \
+ Library/OptionalSugar.thy \
Library/Order_Relation.thy Library/Permutation.thy \
Library/Permutations.thy Library/Poly_Deriv.thy \
Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
@@ -486,7 +476,11 @@
Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
- Library/document/root.bib Library/document/root.tex
+ Library/document/root.bib Library/document/root.tex \
+ Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML \
+ Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML \
+ Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML \
+ Tools/recdef.ML
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
--- a/src/HOL/Library/Library.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Library/Library.thy Tue Aug 02 10:36:50 2011 +0200
@@ -39,6 +39,7 @@
Multiset
Nested_Environment
Numeral_Type
+ Old_Recdef
OptionalSugar
Option_ord
Permutation
--- a/src/HOL/Library/More_List.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Library/More_List.thy Tue Aug 02 10:36:50 2011 +0200
@@ -35,7 +35,7 @@
"fold f (rev xs) = foldr f xs"
by (simp add: foldr_fold_rev)
-lemma fold_cong [fundef_cong, recdef_cong]:
+lemma fold_cong [fundef_cong]:
"a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
\<Longrightarrow> fold f xs a = fold g ys b"
by (induct ys arbitrary: a b xs) simp_all
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Old_Recdef.thy Tue Aug 02 10:36:50 2011 +0200
@@ -0,0 +1,214 @@
+(* Title: HOL/Library/Old_Recdef.thy
+ Author: Konrad Slind and Markus Wenzel, TU Muenchen
+*)
+
+header {* TFL: recursive function definitions *}
+
+theory Old_Recdef
+imports Main
+uses
+ ("~~/src/HOL/Tools/TFL/casesplit.ML")
+ ("~~/src/HOL/Tools/TFL/utils.ML")
+ ("~~/src/HOL/Tools/TFL/usyntax.ML")
+ ("~~/src/HOL/Tools/TFL/dcterm.ML")
+ ("~~/src/HOL/Tools/TFL/thms.ML")
+ ("~~/src/HOL/Tools/TFL/rules.ML")
+ ("~~/src/HOL/Tools/TFL/thry.ML")
+ ("~~/src/HOL/Tools/TFL/tfl.ML")
+ ("~~/src/HOL/Tools/TFL/post.ML")
+ ("~~/src/HOL/Tools/recdef.ML")
+begin
+
+inductive
+ wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
+ for R :: "('a * 'a) set"
+ and F :: "('a => 'b) => 'a => 'b"
+where
+ wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
+ wfrec_rel R F x (F g x)"
+
+definition
+ cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
+ "cut f r x == (%y. if (y,x):r then f y else undefined)"
+
+definition
+ adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
+ "adm_wf R F == ALL f g x.
+ (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+
+definition
+ wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
+ "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+subsection{*Well-Founded Recursion*}
+
+text{*cut*}
+
+lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
+by (simp add: fun_eq_iff cut_def)
+
+lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
+by (simp add: cut_def)
+
+text{*Inductive characterization of wfrec combinator; for details see:
+John Harrison, "Inductive definitions: automation and application"*}
+
+lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
+apply (simp add: adm_wf_def)
+apply (erule_tac a=x in wf_induct)
+apply (rule ex1I)
+apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
+apply (fast dest!: theI')
+apply (erule wfrec_rel.cases, simp)
+apply (erule allE, erule allE, erule allE, erule mp)
+apply (fast intro: the_equality [symmetric])
+done
+
+lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
+apply (simp add: adm_wf_def)
+apply (intro strip)
+apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
+apply (rule refl)
+done
+
+lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+apply (simp add: wfrec_def)
+apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
+apply (rule wfrec_rel.wfrecI)
+apply (intro strip)
+apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
+done
+
+
+text{** This form avoids giant explosions in proofs. NOTE USE OF ==*}
+lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"
+apply auto
+apply (blast intro: wfrec)
+done
+
+
+subsection {* Nitpick setup *}
+
+axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
+
+definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
+ else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+setup {*
+ Nitpick_HOL.register_ersatz_global
+ [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
+ (@{const_name wfrec}, @{const_name wfrec'})]
+*}
+
+hide_const (open) wf_wfrec wf_wfrec' wfrec'
+hide_fact (open) wf_wfrec'_def wfrec'_def
+
+
+subsection {* Lemmas for TFL *}
+
+lemma tfl_wf_induct: "ALL R. wf R -->
+ (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
+apply clarify
+apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
+done
+
+lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
+apply clarify
+apply (rule cut_apply, assumption)
+done
+
+lemma tfl_wfrec:
+ "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
+apply clarify
+apply (erule wfrec)
+done
+
+lemma tfl_eq_True: "(x = True) --> x"
+ by blast
+
+lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
+ by blast
+
+lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
+ by blast
+
+lemma tfl_P_imp_P_iff_True: "P ==> P = True"
+ by blast
+
+lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
+ by blast
+
+lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
+ by simp
+
+lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
+ by blast
+
+lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
+ by blast
+
+use "~~/src/HOL/Tools/TFL/casesplit.ML"
+use "~~/src/HOL/Tools/TFL/utils.ML"
+use "~~/src/HOL/Tools/TFL/usyntax.ML"
+use "~~/src/HOL/Tools/TFL/dcterm.ML"
+use "~~/src/HOL/Tools/TFL/thms.ML"
+use "~~/src/HOL/Tools/TFL/rules.ML"
+use "~~/src/HOL/Tools/TFL/thry.ML"
+use "~~/src/HOL/Tools/TFL/tfl.ML"
+use "~~/src/HOL/Tools/TFL/post.ML"
+use "~~/src/HOL/Tools/recdef.ML"
+setup Recdef.setup
+
+text {*Wellfoundedness of @{text same_fst}*}
+
+definition
+ same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
+where
+ "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
+ --{*For @{text rec_def} declarations where the first n parameters
+ stay unchanged in the recursive call. *}
+
+lemma same_fstI [intro!]:
+ "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
+by (simp add: same_fst_def)
+
+lemma wf_same_fst:
+ assumes prem: "(!!x. P x ==> wf(R x))"
+ shows "wf(same_fst P R)"
+apply (simp cong del: imp_cong add: wf_def same_fst_def)
+apply (intro strip)
+apply (rename_tac a b)
+apply (case_tac "wf (R a)")
+ apply (erule_tac a = b in wf_induct, blast)
+apply (blast intro: prem)
+done
+
+text {*Rule setup*}
+
+lemmas [recdef_simp] =
+ inv_image_def
+ measure_def
+ lex_prod_def
+ same_fst_def
+ less_Suc_eq [THEN iffD2]
+
+lemmas [recdef_cong] =
+ if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
+ map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong
+
+lemmas [recdef_wf] =
+ wf_trancl
+ wf_less_than
+ wf_lex_prod
+ wf_inv_image
+ wf_measure
+ wf_measures
+ wf_pred_nat
+ wf_same_fst
+ wf_empty
+
+end
--- a/src/HOL/List.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/List.thy Tue Aug 02 10:36:50 2011 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Presburger Recdef Code_Numeral Quotient ATP
+imports Plain Presburger Code_Numeral Quotient ATP
uses
("Tools/list_code.ML")
("Tools/list_to_set_comprehension.ML")
@@ -800,7 +800,7 @@
lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
by (induct xs) auto
-lemma map_cong [fundef_cong, recdef_cong]:
+lemma map_cong [fundef_cong]:
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
by simp
@@ -1237,7 +1237,7 @@
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
by(auto dest:Cons_eq_filterD)
-lemma filter_cong[fundef_cong, recdef_cong]:
+lemma filter_cong[fundef_cong]:
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
apply simp
apply(erule thin_rl)
@@ -2003,12 +2003,12 @@
apply(auto)
done
-lemma takeWhile_cong [fundef_cong, recdef_cong]:
+lemma takeWhile_cong [fundef_cong]:
"[| l = k; !!x. x : set l ==> P x = Q x |]
==> takeWhile P l = takeWhile Q k"
by (induct k arbitrary: l) (simp_all)
-lemma dropWhile_cong [fundef_cong, recdef_cong]:
+lemma dropWhile_cong [fundef_cong]:
"[| l = k; !!x. x : set l ==> P x = Q x |]
==> dropWhile P l = dropWhile Q k"
by (induct k arbitrary: l, simp_all)
@@ -2349,12 +2349,12 @@
shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
-lemma foldl_cong [fundef_cong, recdef_cong]:
+lemma foldl_cong [fundef_cong]:
"[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
==> foldl f a l = foldl g b k"
by (induct k arbitrary: a b l) simp_all
-lemma foldr_cong [fundef_cong, recdef_cong]:
+lemma foldr_cong [fundef_cong]:
"[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
==> foldr f l a = foldr g k b"
by (induct k arbitrary: a b l) simp_all
@@ -4586,7 +4586,7 @@
definition
"measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
-lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
+lemma wf_measures[simp]: "wf (measures fs)"
unfolding measures_def
by blast
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
header {* \isaheader{Relations between Java Types} *}
-theory TypeRel imports Decl begin
+theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
-- "direct subclass, cf. 8.1.3"
--- a/src/HOL/NanoJava/TypeRel.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
header "Type relations"
-theory TypeRel imports Decl begin
+theory TypeRel imports Decl "~~/src/HOL/Library/Old_Recdef" begin
consts
subcls1 :: "(cname \<times> cname) set" --{* subclass *}
--- a/src/HOL/Nitpick.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Nitpick.thy Tue Aug 02 10:36:50 2011 +0200
@@ -82,15 +82,6 @@
definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
-axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-
-definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x"
-
-definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
-"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
- else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
-
definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
@@ -238,14 +229,14 @@
setup {* Nitpick_Isar.setup *}
hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
- FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
+ FunBox PairBox Word prod refl' wf' card' setsum'
fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
number_of_frac inverse_frac less_frac less_eq_frac of_frac
hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
word
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
- prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
+ prod_def refl'_def wf'_def card'_def setsum'_def
fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
--- a/src/HOL/Recdef.thy Tue Aug 02 10:03:14 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-(* Title: HOL/Recdef.thy
- Author: Konrad Slind and Markus Wenzel, TU Muenchen
-*)
-
-header {* TFL: recursive function definitions *}
-
-theory Recdef
-imports Plain Hilbert_Choice
-uses
- ("Tools/TFL/casesplit.ML")
- ("Tools/TFL/utils.ML")
- ("Tools/TFL/usyntax.ML")
- ("Tools/TFL/dcterm.ML")
- ("Tools/TFL/thms.ML")
- ("Tools/TFL/rules.ML")
- ("Tools/TFL/thry.ML")
- ("Tools/TFL/tfl.ML")
- ("Tools/TFL/post.ML")
- ("Tools/recdef.ML")
-begin
-
-inductive
- wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
- for R :: "('a * 'a) set"
- and F :: "('a => 'b) => 'a => 'b"
-where
- wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
- wfrec_rel R F x (F g x)"
-
-definition
- cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
- "cut f r x == (%y. if (y,x):r then f y else undefined)"
-
-definition
- adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
- "adm_wf R F == ALL f g x.
- (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
-
-definition
- wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
- "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
-
-subsection{*Well-Founded Recursion*}
-
-text{*cut*}
-
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: fun_eq_iff cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
-
-text{*Inductive characterization of wfrec combinator; for details see:
-John Harrison, "Inductive definitions: automation and application"*}
-
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct)
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (fast intro: the_equality [symmetric])
-done
-
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
-
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
-apply (simp add: wfrec_def)
-apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
-apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
-apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
-done
-
-
-text{** This form avoids giant explosions in proofs. NOTE USE OF ==*}
-lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"
-apply auto
-apply (blast intro: wfrec)
-done
-
-
-lemma tfl_wf_induct: "ALL R. wf R -->
- (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
-apply clarify
-apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
-done
-
-lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
-apply clarify
-apply (rule cut_apply, assumption)
-done
-
-lemma tfl_wfrec:
- "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
-apply clarify
-apply (erule wfrec)
-done
-
-lemma tfl_eq_True: "(x = True) --> x"
- by blast
-
-lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
- by blast
-
-lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"
- by blast
-
-lemma tfl_P_imp_P_iff_True: "P ==> P = True"
- by blast
-
-lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
- by blast
-
-lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
- by simp
-
-lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
- by blast
-
-lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
- by blast
-
-use "Tools/TFL/casesplit.ML"
-use "Tools/TFL/utils.ML"
-use "Tools/TFL/usyntax.ML"
-use "Tools/TFL/dcterm.ML"
-use "Tools/TFL/thms.ML"
-use "Tools/TFL/rules.ML"
-use "Tools/TFL/thry.ML"
-use "Tools/TFL/tfl.ML"
-use "Tools/TFL/post.ML"
-use "Tools/recdef.ML"
-setup Recdef.setup
-
-text {*Wellfoundedness of @{text same_fst}*}
-
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
- "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
- --{*For @{text rec_def} declarations where the first n parameters
- stay unchanged in the recursive call. *}
-
-lemma same_fstI [intro!]:
- "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
-
-lemma wf_same_fst:
- assumes prem: "(!!x. P x ==> wf(R x))"
- shows "wf(same_fst P R)"
-apply (simp cong del: imp_cong add: wf_def same_fst_def)
-apply (intro strip)
-apply (rename_tac a b)
-apply (case_tac "wf (R a)")
- apply (erule_tac a = b in wf_induct, blast)
-apply (blast intro: prem)
-done
-
-text {*Rule setup*}
-
-lemmas [recdef_simp] =
- inv_image_def
- measure_def
- lex_prod_def
- same_fst_def
- less_Suc_eq [THEN iffD2]
-
-lemmas [recdef_cong] =
- if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
-
-lemmas [recdef_wf] =
- wf_trancl
- wf_less_than
- wf_lex_prod
- wf_inv_image
- wf_measure
- wf_pred_nat
- wf_same_fst
- wf_empty
-
-end
--- a/src/HOL/Subst/Unify.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Subst/Unify.thy Tue Aug 02 10:36:50 2011 +0200
@@ -6,7 +6,7 @@
header {* Unification Algorithm *}
theory Unify
-imports Unifier
+imports Unifier "~~/src/HOL/Library/Old_Recdef"
begin
subsection {* Substitution and Unification in Higher-Order Logic. *}
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 02 10:36:50 2011 +0200
@@ -1779,7 +1779,7 @@
"too many nested definitions (" ^
string_of_int depth ^ ") while expanding " ^
quote s)
- else if s = @{const_name wfrec'} then
+ else if s = "Old_Recdef.wfrec'" (* FIXME unchecked! *) then
(do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
else if not unfold andalso
size_of_term def > def_inline_threshold () then
@@ -1873,9 +1873,7 @@
[(@{const_name card}, @{const_name card'}),
(@{const_name setsum}, @{const_name setsum'}),
(@{const_name fold_graph}, @{const_name fold_graph'}),
- (@{const_name wf}, @{const_name wf'}),
- (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
- (@{const_name wfrec}, @{const_name wfrec'})]
+ (@{const_name wf}, @{const_name wf'})]
fun ersatz_table ctxt =
(basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
--- a/src/HOL/Tools/TFL/rules.ML Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Aug 02 10:36:50 2011 +0200
@@ -445,7 +445,7 @@
fun is_cong thm =
case (Thm.prop_of thm)
of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
- (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const (@{const_name Old_Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
@@ -645,7 +645,7 @@
end;
fun restricted t = is_some (USyntax.find_term
- (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
+ (fn (Const(@{const_name Old_Recdef.cut},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
--- a/src/HOL/Tools/recdef.ML Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Tools/recdef.ML Tue Aug 02 10:36:50 2011 +0200
@@ -182,7 +182,7 @@
(** add_recdef(_i) **)
-fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
+fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
let
--- a/src/HOL/ex/InductiveInvariant.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
header {* Some of the results in Inductive Invariants for Nested Recursion *}
-theory InductiveInvariant imports Main begin
+theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" begin
text {* A formalization of some of the results in \emph{Inductive
Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
--- a/src/HOL/ex/Recdefs.thy Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/ex/Recdefs.thy Tue Aug 02 10:36:50 2011 +0200
@@ -7,7 +7,7 @@
header {* Examples of recdef definitions *}
-theory Recdefs imports Main begin
+theory Recdefs imports "~~/src/HOL/Library/Old_Recdef" begin
consts fact :: "nat => nat"
recdef fact less_than