src/HOL/MicroJava/J/TypeRel.thy
changeset 23757 087b0a241557
parent 22597 284b2183d070
child 28524 644b62cf678f
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:29:44 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:32:02 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  theory TypeRel imports Decl begin
     1.5  
     1.6  -- "direct subclass, cf. 8.1.3"
     1.7 -inductive2
     1.8 +inductive
     1.9    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    1.10    for G :: "'c prog"
    1.11  where
    1.12 @@ -26,12 +26,12 @@
    1.13  done
    1.14  
    1.15  lemma subcls1_def2: 
    1.16 -  "subcls1 G = member2
    1.17 -     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    1.18 +  "subcls1 G = (\<lambda>C D. (C, D) \<in>
    1.19 +     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D}))"
    1.20    by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
    1.21  
    1.22 -lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
    1.23 -apply(simp add: subcls1_def2)
    1.24 +lemma finite_subcls1: "finite {(C, D). subcls1 G C D}"
    1.25 +apply(simp add: subcls1_def2 del: mem_Sigma_iff)
    1.26  apply(rule finite_SigmaI [OF finite_is_class])
    1.27  apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
    1.28  apply  auto
    1.29 @@ -39,14 +39,14 @@
    1.30  
    1.31  lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
    1.32  apply (unfold is_class_def)
    1.33 -apply(erule trancl_trans_induct')
    1.34 +apply(erule tranclp_trans_induct)
    1.35  apply (auto dest!: subcls1D)
    1.36  done
    1.37  
    1.38  lemma subcls_is_class2 [rule_format (no_asm)]: 
    1.39    "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    1.40  apply (unfold is_class_def)
    1.41 -apply (erule rtrancl_induct')
    1.42 +apply (erule rtranclp_induct)
    1.43  apply  (drule_tac [2] subcls1D)
    1.44  apply  auto
    1.45  done
    1.46 @@ -54,7 +54,7 @@
    1.47  constdefs
    1.48    class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    1.49      (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.50 -  "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
    1.51 +  "class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
    1.52      (\<lambda>r C t f. case class G C of
    1.53           None \<Rightarrow> arbitrary
    1.54         | Some (D,fs,ms) \<Rightarrow> 
    1.55 @@ -62,8 +62,8 @@
    1.56  
    1.57  lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
    1.58   class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
    1.59 -  by (simp add: class_rec_def wfrec [to_pred]
    1.60 -    cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
    1.61 +  by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
    1.62 +    cut_apply [where r="{(C, D). subcls1 G D C}", simplified, OF subcls1I])
    1.63  
    1.64  definition
    1.65    "wf_class G = wfP ((subcls1 G)^--1)"
    1.66 @@ -84,8 +84,8 @@
    1.67    proof (cases "class G C")
    1.68      case None
    1.69      with wf show ?thesis
    1.70 -      by (simp add: class_rec_def wfrec [to_pred]
    1.71 -        cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
    1.72 +      by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
    1.73 +        cut_apply [where r="{(C, D).subcls1 G D C}", simplified, OF subcls1I])
    1.74    next
    1.75      case (Some x) show ?thesis
    1.76      proof (cases x)
    1.77 @@ -142,7 +142,7 @@
    1.78  
    1.79  
    1.80  -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
    1.81 -inductive2
    1.82 +inductive
    1.83    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    1.84    for G :: "'c prog"
    1.85  where
    1.86 @@ -154,7 +154,7 @@
    1.87  
    1.88  -- "casting conversion, cf. 5.5 / 5.1.5"
    1.89  -- "left out casts on primitve types"
    1.90 -inductive2
    1.91 +inductive
    1.92    cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    1.93    for G :: "'c prog"
    1.94  where
    1.95 @@ -168,34 +168,34 @@
    1.96  done
    1.97  
    1.98  lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
    1.99 -apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
   1.100 +apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
   1.101  apply auto
   1.102  done
   1.103  
   1.104  lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
   1.105 -apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
   1.106 +apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
   1.107  apply auto
   1.108  done
   1.109  
   1.110  lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
   1.111 -apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
   1.112 +apply (ind_cases "G\<turnstile>Class C\<preceq>T")
   1.113  apply auto
   1.114  done
   1.115  
   1.116  lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
   1.117  apply (rule iffI)
   1.118 -apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
   1.119 +apply (ind_cases "G\<turnstile>Class C\<preceq>NT")
   1.120  apply auto
   1.121  done
   1.122  
   1.123  lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
   1.124  apply (rule iffI)
   1.125 -apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
   1.126 +apply (ind_cases "G\<turnstile>Class C \<preceq> Class D")
   1.127  apply (auto elim: widen.subcls)
   1.128  done
   1.129  
   1.130  lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
   1.131 -by (ind_cases2 "G \<turnstile> T \<preceq> NT",  auto)
   1.132 +by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
   1.133  
   1.134  lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
   1.135  apply (rule iffI)