adapted to move of Wfrec
authorblanchet
Thu Jan 16 16:20:17 2014 +0100 (2014-01-16)
changeset 550172df6ad1dbd66
parent 55016 9fc7e7753d86
child 55018 2a526bd279ed
adapted to move of Wfrec
src/HOL/Cardinals/Wellfounded_More_FP.thy
src/HOL/Induct/Sexp.thy
src/HOL/Library/Library.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Wfrec.thy
     1.1 --- a/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 15:47:33 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Wellfounded_More_FP.thy	Thu Jan 16 16:20:17 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* More on Well-Founded Relations (FP) *}
     1.5  
     1.6  theory Wellfounded_More_FP
     1.7 -imports Order_Relation_More_FP "~~/src/HOL/Library/Wfrec"
     1.8 +imports Wfrec Order_Relation_More_FP
     1.9  begin
    1.10  
    1.11  
    1.12 @@ -98,7 +98,7 @@
    1.13    let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
    1.14    have "wf r = (\<forall>A. ?phi A)"
    1.15    by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
    1.16 -     (rule wfI_min, metis)
    1.17 +     (rule wfI_min, fast)
    1.18    (*  *)
    1.19    also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
    1.20    proof
    1.21 @@ -151,7 +151,7 @@
    1.22    moreover
    1.23    {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
    1.24     obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
    1.25 -   unfolding order_on_defs using Case1 rel.Total_subset_Id by metis
    1.26 +   unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
    1.27     hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
    1.28     hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
    1.29    }
     2.1 --- a/src/HOL/Induct/Sexp.thy	Thu Jan 16 15:47:33 2014 +0100
     2.2 +++ b/src/HOL/Induct/Sexp.thy	Thu Jan 16 16:20:17 2014 +0100
     2.3 @@ -6,7 +6,9 @@
     2.4  structures by hand.
     2.5  *)
     2.6  
     2.7 -theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin
     2.8 +theory Sexp
     2.9 +imports Main
    2.10 +begin
    2.11  
    2.12  type_synonym 'a item = "'a Datatype.item"
    2.13  abbreviation "Leaf == Datatype.Leaf"
     3.1 --- a/src/HOL/Library/Library.thy	Thu Jan 16 15:47:33 2014 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Jan 16 16:20:17 2014 +0100
     3.3 @@ -63,7 +63,6 @@
     3.4    Sublist
     3.5    Sum_of_Squares
     3.6    Transitive_Closure_Table
     3.7 -  Wfrec
     3.8    While_Combinator
     3.9    Zorn
    3.10  begin
     4.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Jan 16 15:47:33 2014 +0100
     4.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Jan 16 16:20:17 2014 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* TFL: recursive function definitions *}
     4.5  
     4.6  theory Old_Recdef
     4.7 -imports Wfrec
     4.8 +imports Main
     4.9  keywords
    4.10    "recdef" "defer_recdef" :: thy_decl and
    4.11    "recdef_tc" :: thy_goal and
     5.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Jan 16 15:47:33 2014 +0100
     5.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Jan 16 16:20:17 2014 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* \isaheader{Relations between Java Types} *}
     5.5  
     5.6  theory TypeRel
     5.7 -imports Decl "~~/src/HOL/Library/Wfrec"
     5.8 +imports Decl
     5.9  begin
    5.10  
    5.11  -- "direct subclass, cf. 8.1.3"
     6.1 --- a/src/HOL/NanoJava/TypeRel.thy	Thu Jan 16 15:47:33 2014 +0100
     6.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Jan 16 16:20:17 2014 +0100
     6.3 @@ -4,7 +4,9 @@
     6.4  
     6.5  header "Type relations"
     6.6  
     6.7 -theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
     6.8 +theory TypeRel
     6.9 +imports Decl
    6.10 +begin
    6.11  
    6.12  text{* Direct subclass relation *}
    6.13  
     7.1 --- a/src/HOL/Nitpick.thy	Thu Jan 16 15:47:33 2014 +0100
     7.2 +++ b/src/HOL/Nitpick.thy	Thu Jan 16 16:20:17 2014 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     7.5  
     7.6  theory Nitpick
     7.7 -imports Map Record Sledgehammer
     7.8 +imports Map Record Sledgehammer Wfrec
     7.9  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
    7.10  begin
    7.11  
    7.12 @@ -197,6 +197,15 @@
    7.13  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
    7.14  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
    7.15  
    7.16 +axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    7.17 +
    7.18 +definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    7.19 +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    7.20 +
    7.21 +definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    7.22 +"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    7.23 +                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    7.24 +
    7.25  ML_file "Tools/Nitpick/kodkod.ML"
    7.26  ML_file "Tools/Nitpick/kodkod_sat.ML"
    7.27  ML_file "Tools/Nitpick/nitpick_util.ML"
    7.28 @@ -218,14 +227,17 @@
    7.29      [(@{const_name card}, @{const_name card'}),
    7.30       (@{const_name setsum}, @{const_name setsum'}),
    7.31       (@{const_name fold_graph}, @{const_name fold_graph'}),
    7.32 -     (@{const_name wf}, @{const_name wf'})]
    7.33 +     (@{const_name wf}, @{const_name wf'}),
    7.34 +     (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    7.35 +     (@{const_name wfrec}, @{const_name wfrec'})]
    7.36  *}
    7.37  
    7.38  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    7.39      FunBox PairBox Word prod refl' wf' card' setsum'
    7.40      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    7.41      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    7.42 -    number_of_frac inverse_frac less_frac less_eq_frac of_frac
    7.43 +    number_of_frac inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec
    7.44 +    wfrec'
    7.45  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    7.46  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    7.47      prod_def refl'_def wf'_def card'_def setsum'_def
    7.48 @@ -233,6 +245,7 @@
    7.49      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    7.50      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    7.51      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    7.52 -    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    7.53 +    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
    7.54 +    wfrec'_def
    7.55  
    7.56  end
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jan 16 15:47:33 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jan 16 16:20:17 2014 +0100
     8.3 @@ -1832,7 +1832,7 @@
     8.4                                     "too many nested definitions (" ^
     8.5                                     string_of_int depth ^ ") while expanding " ^
     8.6                                     quote s)
     8.7 -                else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) then
     8.8 +                else if s = @{const_name wfrec'} then
     8.9                    (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
    8.10                  else if not unfold andalso
    8.11                       size_of_term def > def_inline_threshold () then
     9.1 --- a/src/HOL/Wfrec.thy	Thu Jan 16 15:47:33 2014 +0100
     9.2 +++ b/src/HOL/Wfrec.thy	Thu Jan 16 16:20:17 2014 +0100
     9.3 @@ -7,7 +7,7 @@
     9.4  header {* Well-Founded Recursion Combinator *}
     9.5  
     9.6  theory Wfrec
     9.7 -imports Main
     9.8 +imports Wellfounded
     9.9  begin
    9.10  
    9.11  inductive
    9.12 @@ -74,26 +74,6 @@
    9.13  done
    9.14  
    9.15  
    9.16 -subsection {* Nitpick setup *}
    9.17 -
    9.18 -axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    9.19 -
    9.20 -definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    9.21 -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    9.22 -
    9.23 -definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    9.24 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    9.25 -                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    9.26 -
    9.27 -setup {*
    9.28 -  Nitpick_HOL.register_ersatz_global
    9.29 -    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    9.30 -     (@{const_name wfrec}, @{const_name wfrec'})]
    9.31 -*}
    9.32 -
    9.33 -hide_const (open) wf_wfrec wf_wfrec' wfrec'
    9.34 -hide_fact (open) wf_wfrec'_def wfrec'_def
    9.35 -
    9.36  subsection {* Wellfoundedness of @{text same_fst} *}
    9.37  
    9.38  definition