src/HOL/Bali/TypeRel.thy
changeset 58887 38db8ddc0f57
parent 47176 568fdc70e565
child 60754 02924903a6fd
equal deleted inserted replaced
58886:8a6cac7c7247 58887:38db8ddc0f57
     1 (*  Title:      HOL/Bali/TypeRel.thy
     1 (*  Title:      HOL/Bali/TypeRel.thy
     2     Author:     David von Oheimb
     2     Author:     David von Oheimb
     3 *)
     3 *)
     4 header {* The relations between Java types *}
     4 subsection {* The relations between Java types *}
     5 
     5 
     6 theory TypeRel imports Decl begin
     6 theory TypeRel imports Decl begin
     7 
     7 
     8 text {*
     8 text {*
     9 simplifications:
     9 simplifications:
    53   subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
    53   subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
    54   subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
    54   subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
    55   implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    55   implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    56 
    56 
    57 
    57 
    58 section "subclass and subinterface relations"
    58 subsubsection "subclass and subinterface relations"
    59 
    59 
    60   (* direct subinterface in Decl.thy, cf. 9.1.3 *)
    60   (* direct subinterface in Decl.thy, cf. 9.1.3 *)
    61   (* direct subclass     in Decl.thy, cf. 8.1.3 *)
    61   (* direct subclass     in Decl.thy, cf. 8.1.3 *)
    62 
    62 
    63 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
    63 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
   325     case Subcls
   325     case Subcls
   326     with clsC show ?thesis by (blast dest: subcls_superD)
   326     with clsC show ?thesis by (blast dest: subcls_superD)
   327   qed
   327   qed
   328 qed
   328 qed
   329 
   329 
   330 section "implementation relation"
   330 subsubsection "implementation relation"
   331 
   331 
   332 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
   332 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
   333 apply (unfold implmt1_def)
   333 apply (unfold implmt1_def)
   334 apply auto
   334 apply auto
   335 done
   335 done
   364 apply (erule implmt.induct)
   364 apply (erule implmt.induct)
   365 apply (auto dest: implmt1D subcls1D)
   365 apply (auto dest: implmt1D subcls1D)
   366 done
   366 done
   367 
   367 
   368 
   368 
   369 section "widening relation"
   369 subsubsection "widening relation"
   370 
   370 
   371 inductive
   371 inductive
   372  --{*widening, viz. method invocation conversion, cf. 5.3
   372  --{*widening, viz. method invocation conversion, cf. 5.3
   373                             i.e. kind of syntactic subtyping *}
   373                             i.e. kind of syntactic subtyping *}
   374   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   374   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   581 apply (unfold widens_def)
   581 apply (unfold widens_def)
   582 apply auto
   582 apply auto
   583 done
   583 done
   584 
   584 
   585 
   585 
   586 section "narrowing relation"
   586 subsubsection "narrowing relation"
   587 
   587 
   588 (* all properties of narrowing and casting conversions we actually need *)
   588 (* all properties of narrowing and casting conversions we actually need *)
   589 (* these can easily be proven from the definitions below *)
   589 (* these can easily be proven from the definitions below *)
   590 (*
   590 (*
   591 rules
   591 rules
   641 by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   641 by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   642 
   642 
   643 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   643 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   644 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   644 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   645 
   645 
   646 section "casting relation"
   646 subsubsection "casting relation"
   647 
   647 
   648 inductive --{* casting conversion, cf. 5.5 *}
   648 inductive --{* casting conversion, cf. 5.5 *}
   649   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   649   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   650   for G :: prog
   650   for G :: prog
   651 where
   651 where