--- a/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy Thu Jan 16 16:20:17 2014 +0100
@@ -8,7 +8,7 @@
header {* More on Well-Founded Relations (FP) *}
theory Wellfounded_More_FP
-imports Order_Relation_More_FP "~~/src/HOL/Library/Wfrec"
+imports Wfrec Order_Relation_More_FP
begin
@@ -98,7 +98,7 @@
let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
have "wf r = (\<forall>A. ?phi A)"
by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
- (rule wfI_min, metis)
+ (rule wfI_min, fast)
(* *)
also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
proof
@@ -151,7 +151,7 @@
moreover
{fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
- unfolding order_on_defs using Case1 rel.Total_subset_Id by metis
+ unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
}
--- a/src/HOL/Induct/Sexp.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Induct/Sexp.thy Thu Jan 16 16:20:17 2014 +0100
@@ -6,7 +6,9 @@
structures by hand.
*)
-theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin
+theory Sexp
+imports Main
+begin
type_synonym 'a item = "'a Datatype.item"
abbreviation "Leaf == Datatype.Leaf"
--- a/src/HOL/Library/Library.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Library/Library.thy Thu Jan 16 16:20:17 2014 +0100
@@ -63,7 +63,6 @@
Sublist
Sum_of_Squares
Transitive_Closure_Table
- Wfrec
While_Combinator
Zorn
begin
--- a/src/HOL/Library/Old_Recdef.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Thu Jan 16 16:20:17 2014 +0100
@@ -5,7 +5,7 @@
header {* TFL: recursive function definitions *}
theory Old_Recdef
-imports Wfrec
+imports Main
keywords
"recdef" "defer_recdef" :: thy_decl and
"recdef_tc" :: thy_goal and
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Jan 16 16:20:17 2014 +0100
@@ -5,7 +5,7 @@
header {* \isaheader{Relations between Java Types} *}
theory TypeRel
-imports Decl "~~/src/HOL/Library/Wfrec"
+imports Decl
begin
-- "direct subclass, cf. 8.1.3"
--- a/src/HOL/NanoJava/TypeRel.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Jan 16 16:20:17 2014 +0100
@@ -4,7 +4,9 @@
header "Type relations"
-theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
+theory TypeRel
+imports Decl
+begin
text{* Direct subclass relation *}
--- a/src/HOL/Nitpick.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Nitpick.thy Thu Jan 16 16:20:17 2014 +0100
@@ -8,7 +8,7 @@
header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
theory Nitpick
-imports Map Record Sledgehammer
+imports Map Record Sledgehammer Wfrec
keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
begin
@@ -197,6 +197,15 @@
definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
"of_frac q \<equiv> of_int (num q) / of_int (denom q)"
+axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition wf_wfrec' :: "('a \<times> 'a) set \<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) set \<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"
+
ML_file "Tools/Nitpick/kodkod.ML"
ML_file "Tools/Nitpick/kodkod_sat.ML"
ML_file "Tools/Nitpick/nitpick_util.ML"
@@ -218,14 +227,17 @@
[(@{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}, @{const_name wf'}),
+ (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
+ (@{const_name wfrec}, @{const_name wfrec'})]
*}
hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
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
+ number_of_frac inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec
+ wfrec'
hide_type (open) 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 card'_def setsum'_def
@@ -233,6 +245,7 @@
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
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
+ inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
+ wfrec'_def
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jan 16 16:20:17 2014 +0100
@@ -1832,7 +1832,7 @@
"too many nested definitions (" ^
string_of_int depth ^ ") while expanding " ^
quote s)
- else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) then
+ else if s = @{const_name wfrec'} then
(do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
else if not unfold andalso
size_of_term def > def_inline_threshold () then
--- a/src/HOL/Wfrec.thy Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Wfrec.thy Thu Jan 16 16:20:17 2014 +0100
@@ -7,7 +7,7 @@
header {* Well-Founded Recursion Combinator *}
theory Wfrec
-imports Main
+imports Wellfounded
begin
inductive
@@ -74,26 +74,6 @@
done
-subsection {* Nitpick setup *}
-
-axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-
-definition wf_wfrec' :: "('a \<times> 'a) set \<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) set \<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 {* Wellfoundedness of @{text same_fst} *}
definition