src/HOL/Bali/TypeRel.thy

 (*subcls1, in Decl.thy*)                     (* direct subclass           *)
 (*subcls , by translation*)                  (*        subclass           *)
 (*subclseq, by translation*)                 (* subclass + identity       *)
 
 definition
-  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct implementation\<close>
-  \<comment>\<open>direct implementation, cf. 8.1.3\<close>
+  implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment> \<open>direct implementation\<close>
+  \<comment> \<open>direct implementation, cf. 8.1.3\<close>
   where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
 
 
 abbreviation
   subint1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
   where "G\<turnstile>I \<prec>I1 J == (I,J) \<in> subint1 G"
 
 abbreviation
   subint_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
-  where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)^*" \<comment>\<open>cf. 9.1.3\<close>
+  where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)^*" \<comment> \<open>cf. 9.1.3\<close>
 
 abbreviation
   implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
   where "G\<turnstile>C \<leadsto>1 I == (C,I) \<in> implmt1 G"
 

 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
 apply (unfold implmt1_def)
 apply auto
 done
 
-inductive \<comment>\<open>implementation, cf. 8.1.4\<close>
+inductive \<comment> \<open>implementation, cf. 8.1.4\<close>
   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   for G :: prog
 where
   direct: "G\<turnstile>C\<leadsto>1J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
 | subint: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>C\<leadsto>J"

 
 
 subsubsection "widening relation"
 
 inductive
- \<comment>\<open>widening, viz. method invocation conversion, cf. 5.3
+ \<comment> \<open>widening, viz. method invocation conversion, cf. 5.3
                             i.e. kind of syntactic subtyping\<close>
   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   for G :: prog
 where
-  refl:    "G\<turnstile>T\<preceq>T" \<comment>\<open>identity conversion, cf. 5.1.1\<close>
-| subint:  "G\<turnstile>I\<preceq>I J  \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" \<comment>\<open>wid.ref.conv.,cf. 5.1.4\<close>
+  refl:    "G\<turnstile>T\<preceq>T" \<comment> \<open>identity conversion, cf. 5.1.1\<close>
+| subint:  "G\<turnstile>I\<preceq>I J  \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" \<comment> \<open>wid.ref.conv.,cf. 5.1.4\<close>
 | int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
 | subcls:  "G\<turnstile>C\<preceq>\<^sub>C D  \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D"
 | implmt:  "G\<turnstile>C\<leadsto>I   \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I"
 | null:    "G\<turnstile>NT\<preceq> RefT R"
 | arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"

   cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
   cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
 *)
 
 (* more detailed than necessary for type-safety, see above rules. *)
-inductive \<comment>\<open>narrowing reference conversion, cf. 5.1.5\<close>
+inductive \<comment> \<open>narrowing reference conversion, cf. 5.1.5\<close>
   narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   for G :: prog
 where
   subcls:  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>     Class D\<succ>Class C"
 | implmt:  "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>     Class C\<succ>Iface I"

 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
 
 subsubsection "casting relation"
 
-inductive \<comment>\<open>casting conversion, cf. 5.5\<close>
+inductive \<comment> \<open>casting conversion, cf. 5.5\<close>
   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   for G :: prog
 where
   widen:   "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
 | narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"