# HG changeset patch # User blanchet # Date 1389885617 -3600 # Node ID 2df6ad1dbd66c56802a753dccec7bdd1a6438b81 # Parent 9fc7e7753d863b38ad81ab15528bcc255fb723c0 adapted to move of Wfrec diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Cardinals/Wellfounded_More_FP.thy --- 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 = "\ A. A \ {} \ (\a \ A. \a' \ A. \ (a',a) \ r)" have "wf r = (\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 "(\A. ?phi A) = (\B \ Field r. ?phi B)" proof @@ -151,7 +151,7 @@ moreover {fix A assume *: "A \ Field r" and **: "A \ {}" obtain a where 1: "r = {} \ 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} \ r = {(a,a)}" using * ** unfolding Field_def by blast hence "\a \ A. \a' \ A. (a,a') \ r" using 1 by blast } diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Induct/Sexp.thy --- 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" diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Library/Library.thy --- 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 diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Library/Old_Recdef.thy --- 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 diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/MicroJava/J/TypeRel.thy --- 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" diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/NanoJava/TypeRel.thy --- 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 *} diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Nitpick.thy --- 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 \ 'b\{inverse,ring_1}" where "of_frac q \ of_int (num q) / of_int (denom q)" +axiomatization wf_wfrec :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" + +definition wf_wfrec' :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" + +definition wfrec' :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where +"wfrec' R F x \ 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 diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 9fc7e7753d86 -r 2df6ad1dbd66 src/HOL/Wfrec.thy --- 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 \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" - -definition wf_wfrec' :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" - -definition wfrec' :: "('a \ 'a) set \ (('a \ 'b) \ 'a \ 'b) \ 'a \ 'b" where -"wfrec' R F x \ 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