src/HOL/Bali/TypeRel.thy
changeset 37956 ee939247b2fb
parent 35416 d8d7d1b785af
child 38541 9cfafdb56749
     1.1 --- a/src/HOL/Bali/TypeRel.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/TypeRel.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -25,14 +25,17 @@
     1.4  \end{itemize}
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -
     1.9  (*subint1, in Decl.thy*)                     (* direct subinterface       *)
    1.10  (*subint , by translation*)                  (* subinterface (+ identity) *)
    1.11  (*subcls1, in Decl.thy*)                     (* direct subclass           *)
    1.12  (*subcls , by translation*)                  (*        subclass           *)
    1.13  (*subclseq, by translation*)                 (* subclass + identity       *)
    1.14 -  implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
    1.15 +
    1.16 +definition
    1.17 +  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
    1.18 +  --{* direct implementation, cf. 8.1.3 *}
    1.19 +  where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
    1.20 +
    1.21  
    1.22  abbreviation
    1.23    subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
    1.24 @@ -325,16 +328,11 @@
    1.25  
    1.26  section "implementation relation"
    1.27  
    1.28 -defs
    1.29 -  --{* direct implementation, cf. 8.1.3 *}
    1.30 -implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
    1.31 -
    1.32  lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
    1.33  apply (unfold implmt1_def)
    1.34  apply auto
    1.35  done
    1.36  
    1.37 -
    1.38  inductive --{* implementation, cf. 8.1.4 *}
    1.39    implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
    1.40    for G :: prog
    1.41 @@ -568,8 +566,9 @@
    1.42  apply (fast dest: widen_Class_Class widen_Class_Iface)
    1.43  done
    1.44  
    1.45 -definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
    1.46 - "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
    1.47 +definition
    1.48 +  widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
    1.49 +  where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
    1.50  
    1.51  lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
    1.52  apply (unfold widens_def)