made same_fst recdef_simp
authornipkow
Fri May 04 15:38:48 2001 +0200 (2001-05-04)
changeset 11284981ea92a86dd
parent 11283 358f82c4550d
child 11285 3826c51d980e
made same_fst recdef_simp
src/HOL/Library/While_Combinator.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu May 03 18:22:36 2001 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri May 04 15:38:48 2001 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4        then arbitrary
     1.5        else if b s then while_aux (b, c, c s)
     1.6        else s)"
     1.7 +thm while_aux.simps
     1.8    apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
     1.9 -   apply (simp add: same_fst_def)
    1.10    apply (rule refl)
    1.11    done
    1.12  
     2.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu May 03 18:22:36 2001 +0200
     2.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri May 04 15:38:48 2001 +0200
     2.3 @@ -74,8 +74,6 @@
     2.4  apply  auto
     2.5  done
     2.6  
     2.7 -declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
     2.8 -
     2.9  consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
    2.10          'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    2.11  
    2.12 @@ -84,8 +82,10 @@
    2.13                           | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
    2.14        f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
    2.15  (hints intro: subcls1I)
    2.16 +
    2.17  declare class_rec.simps [simp del]
    2.18  
    2.19 +
    2.20  lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
    2.21   class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
    2.22    apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
     3.1 --- a/src/HOL/Recdef.thy	Thu May 03 18:22:36 2001 +0200
     3.2 +++ b/src/HOL/Recdef.thy	Fri May 04 15:38:48 2001 +0200
     3.3 @@ -59,6 +59,7 @@
     3.4    inv_image_def
     3.5    measure_def
     3.6    lex_prod_def
     3.7 +  same_fst_def
     3.8    less_Suc_eq [THEN iffD2]
     3.9  
    3.10  lemmas [recdef_cong] = if_cong image_cong