moved obsolete same_fst to Recdef.thy
authorkrauss
Tue Jul 28 08:48:56 2009 +0200 (2009-07-28)
changeset 32244a99723d77ae0
parent 32243 64660a887b15
child 32245 0c1cb95a434d
moved obsolete same_fst to Recdef.thy
src/HOL/Recdef.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Recdef.thy	Tue Jul 28 08:48:48 2009 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Tue Jul 28 08:48:56 2009 +0200
     1.3 @@ -79,6 +79,32 @@
     1.4  use "Tools/recdef.ML"
     1.5  setup Recdef.setup
     1.6  
     1.7 +text {*Wellfoundedness of @{text same_fst}*}
     1.8 +
     1.9 +definition
    1.10 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    1.11 +where
    1.12 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
    1.13 +   --{*For @{text rec_def} declarations where the first n parameters
    1.14 +       stay unchanged in the recursive call. *}
    1.15 +
    1.16 +lemma same_fstI [intro!]:
    1.17 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
    1.18 +by (simp add: same_fst_def)
    1.19 +
    1.20 +lemma wf_same_fst:
    1.21 +  assumes prem: "(!!x. P x ==> wf(R x))"
    1.22 +  shows "wf(same_fst P R)"
    1.23 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
    1.24 +apply (intro strip)
    1.25 +apply (rename_tac a b)
    1.26 +apply (case_tac "wf (R a)")
    1.27 + apply (erule_tac a = b in wf_induct, blast)
    1.28 +apply (blast intro: prem)
    1.29 +done
    1.30 +
    1.31 +text {*Rule setup*}
    1.32 +
    1.33  lemmas [recdef_simp] =
    1.34    inv_image_def
    1.35    measure_def
     2.1 --- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:48 2009 +0200
     2.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:56 2009 +0200
     2.3 @@ -886,30 +886,6 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 -text {*Wellfoundedness of @{text same_fst}*}
     2.8 -
     2.9 -definition
    2.10 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    2.11 -where
    2.12 -    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
    2.13 -   --{*For @{text rec_def} declarations where the first n parameters
    2.14 -       stay unchanged in the recursive call. *}
    2.15 -
    2.16 -lemma same_fstI [intro!]:
    2.17 -     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
    2.18 -by (simp add: same_fst_def)
    2.19 -
    2.20 -lemma wf_same_fst:
    2.21 -  assumes prem: "(!!x. P x ==> wf(R x))"
    2.22 -  shows "wf(same_fst P R)"
    2.23 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
    2.24 -apply (intro strip)
    2.25 -apply (rename_tac a b)
    2.26 -apply (case_tac "wf (R a)")
    2.27 - apply (erule_tac a = b in wf_induct, blast)
    2.28 -apply (blast intro: prem)
    2.29 -done
    2.30 -
    2.31  
    2.32  subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
    2.33     stabilize.*}