Turned subcls1 into an inductive relation to make it executable.
authorberghofe
Mon Dec 10 15:26:42 2001 +0100 (2001-12-10)
changeset 12443e56ab6134b41
parent 12442 0ecba8660de7
child 12444 a2a1c74374ce
Turned subcls1 into an inductive relation to make it executable.
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/J/TypeRel.thy
     1.1 --- a/src/HOL/MicroJava/BV/JType.thy	Mon Dec 10 15:24:48 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Mon Dec 10 15:26:42 2001 +0100
     1.3 @@ -66,9 +66,10 @@
     1.4      moreover    
     1.5      from R wf ty
     1.6      have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
     1.7 -      by (auto simp add: is_ty_def subcls1_def is_class_def
     1.8 +     by (auto simp add: is_ty_def is_class_def split_tupled_all
     1.9 +               elim!: subcls1.elims
    1.10                 elim: converse_rtranclE
    1.11 -               split: ref_ty.splits)    
    1.12 +               split: ref_ty.splits)
    1.13      ultimately    
    1.14      show ?thesis by blast
    1.15    qed
    1.16 @@ -282,7 +283,8 @@
    1.17  
    1.18  lemma single_valued_subcls1:
    1.19    "wf_prog wf_mb G ==> single_valued (subcls1 G)"
    1.20 -  by (unfold wf_prog_def unique_def single_valued_def subcls1_def) auto
    1.21 +  by (auto simp add: wf_prog_def unique_def single_valued_def
    1.22 +    intro: subcls1I elim!: subcls1.elims)
    1.23  
    1.24  theorem err_semilat_JType_esl:
    1.25    "wf_prog wf_mb G ==> err_semilat (esl G)"
     2.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Dec 10 15:24:48 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Dec 10 15:26:42 2001 +0100
     2.3 @@ -31,27 +31,20 @@
     2.4    "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
     2.5    "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
     2.6  
     2.7 -defs
     2.8 +inductive "subcls1 G" intros
     2.9  
    2.10    (* direct subclass, cf. 8.1.3 *)
    2.11 - subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
    2.12 +  subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    2.13    
    2.14  lemma subcls1D: 
    2.15    "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    2.16 -apply (unfold subcls1_def)
    2.17 -apply auto
    2.18 -done
    2.19 -
    2.20 -lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    2.21 -apply (unfold subcls1_def)
    2.22 +apply (erule subcls1.elims)
    2.23  apply auto
    2.24  done
    2.25  
    2.26  lemma subcls1_def2: 
    2.27  "subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    2.28 -apply (unfold subcls1_def is_class_def)
    2.29 -apply auto
    2.30 -done
    2.31 +  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    2.32  
    2.33  lemma finite_subcls1: "finite (subcls1 G)"
    2.34  apply(subst subcls1_def2)