Theory Type

(*  Title:      JinjaThreads/Common/Type.thy
    Author:     David von Oheimb, Tobias Nipkow, Andreas Lochbihler

    Based on the Jinja theory Common/Type.thy by David von Oheimb and Tobias Nipkow
*)

chapter ‹Concepts for all JinjaThreads Languages \label{cha:j}›

section ‹JinjaThreads types›

theory Type
imports
  "../Basic/Auxiliary"
begin

type_synonym cname = String.literal ― ‹class names›
type_synonym mname = String.literal ― ‹method name›
type_synonym vname = String.literal ― ‹names for local/field variables›

definition Object :: cname
where "Object ≡ STR ''java/lang/Object''"

definition Thread :: cname
where "Thread ≡ STR ''java/lang/Thread''"

definition Throwable :: cname
where "Throwable ≡ STR ''java/lang/Throwable''"

definition this :: vname
where "this ≡ STR ''this''"

definition run :: mname
where "run ≡ STR ''run()V''"

definition start :: mname
where "start ≡ STR ''start()V''"

definition wait :: mname
where "wait ≡ STR ''wait()V''"

definition notify :: mname
where "notify ≡ STR ''notify()V''"

definition notifyAll :: mname
where "notifyAll ≡ STR ''notifyAll()V''"

definition join :: mname
where "join ≡ STR ''join()V''"

definition interrupt :: mname
where "interrupt ≡ STR ''interrupt()V''"

definition isInterrupted :: mname
where "isInterrupted ≡ STR ''isInterrupted()Z''"

(* Method names for Class Object *)

definition hashcode :: mname
where "hashcode = STR ''hashCode()I''"

definition clone :: mname
where "clone = STR ''clone()Ljava/lang/Object;''"

definition print :: mname
where "print = STR ''~print(I)V''"

definition currentThread :: mname
where "currentThread = STR ''~Thread.currentThread()Ljava/lang/Thread;''"

definition interrupted :: mname
where "interrupted = STR ''~Thread.interrupted()Z''"

definition yield :: mname
where "yield = STR ''~Thread.yield()V''"

lemmas identifier_name_defs [code_unfold] =
  this_def run_def start_def wait_def notify_def notifyAll_def join_def interrupt_def isInterrupted_def
  hashcode_def clone_def print_def currentThread_def interrupted_def yield_def

lemma Object_Thread_Throwable_neq [simp]:
  "Thread ≠ Object" "Object ≠ Thread"
  "Object ≠ Throwable" "Throwable ≠ Object"
  "Thread ≠ Throwable" "Throwable ≠ Thread"
by(auto simp add: Thread_def Object_def Throwable_def)

lemma synth_method_names_neq_aux:
  "start ≠ wait" "start ≠ notify" "start ≠ notifyAll" "start ≠ join" "start ≠ interrupt" "start ≠ isInterrupted"
  "start ≠ hashcode" "start ≠ clone" "start ≠ print" "start ≠ currentThread"
  "start ≠ interrupted" "start ≠ yield" "start ≠ run"
  "wait ≠ notify" "wait ≠ notifyAll" "wait ≠ join"  "wait ≠ interrupt" "wait ≠ isInterrupted"
  "wait ≠ hashcode" "wait ≠ clone" "wait ≠ print" "wait ≠ currentThread" 
  "wait ≠ interrupted" "wait ≠ yield"  "wait ≠ run"
  "notify ≠ notifyAll" "notify ≠ join" "notify ≠ interrupt" "notify ≠ isInterrupted"
  "notify ≠ hashcode" "notify ≠ clone" "notify ≠ print" "notify ≠ currentThread"
  "notify ≠ interrupted" "notify ≠ yield" "notify ≠ run"
  "notifyAll ≠ join" "notifyAll ≠ interrupt" "notifyAll ≠ isInterrupted"
  "notifyAll ≠ hashcode" "notifyAll ≠ clone" "notifyAll ≠ print" "notifyAll ≠ currentThread"
  "notifyAll ≠ interrupted" "notifyAll ≠ yield" "notifyAll ≠ run"
  "join ≠ interrupt" "join ≠ isInterrupted"
  "join ≠ hashcode" "join ≠ clone" "join ≠ print" "join ≠ currentThread" 
  "join ≠ interrupted" "join ≠ yield" "join ≠ run"
  "interrupt ≠ isInterrupted"
  "interrupt ≠ hashcode" "interrupt ≠ clone" "interrupt ≠ print" "interrupt ≠ currentThread" 
  "interrupt ≠ interrupted" "interrupt ≠ yield" "interrupt ≠ run"
  "isInterrupted ≠ hashcode" "isInterrupted ≠ clone" "isInterrupted ≠ print" "isInterrupted ≠ currentThread" 
  "isInterrupted ≠ interrupted" "isInterrupted ≠ yield" "isInterrupted ≠ run"
  "hashcode ≠ clone" "hashcode ≠ print" "hashcode ≠ currentThread" 
  "hashcode ≠ interrupted" "hashcode ≠ yield" "hashcode ≠ run"
  "clone ≠ print" "clone ≠ currentThread" 
  "clone ≠ interrupted" "clone ≠ yield" "clone ≠ run"
  "print ≠ currentThread" 
  "print ≠ interrupted" "print ≠ yield" "print ≠ run"
  "currentThread ≠ interrupted" "currentThread ≠ yield" "currentThread ≠ run"
  "interrupted ≠ yield" "interrupted ≠ run"
  "yield ≠ run"
by(simp_all add: identifier_name_defs)

lemmas synth_method_names_neq [simp] = synth_method_names_neq_aux synth_method_names_neq_aux[symmetric]

― ‹types›
datatype ty
  = Void          ― ‹type of statements›
  | Boolean
  | Integer
  | NT            ― ‹null type›
  | Class cname   ― ‹class type›
  | Array ty      ("_⌊⌉" 95) ― ‹array type›

context
  notes [[inductive_internals]]
begin

inductive is_refT :: "ty ⇒ bool" where
  "is_refT NT"
| "is_refT (Class C)"
| "is_refT (A⌊⌉)"

declare is_refT.intros[iff]

end

lemmas refTE [consumes 1, case_names NT Class Array] = is_refT.cases

lemma not_refTE [consumes 1, case_names Void Boolean Integer]:
  "⟦ ¬is_refT T; T = Void ⟹ P; T = Boolean ⟹ P; T = Integer ⟹ P ⟧ ⟹ P"
by (cases T, auto)

fun ground_type :: "ty ⇒ ty" where
  "ground_type (Array T) = ground_type T"
| "ground_type T = T"

abbreviation is_NT_Array :: "ty ⇒ bool" where
  "is_NT_Array T ≡ ground_type T = NT"

primrec the_Class :: "ty ⇒ cname"
where
  "the_Class (Class C) = C"

primrec the_Array :: "ty ⇒ ty"
where
  "the_Array (T⌊⌉) = T"


datatype htype =
  Class_type "cname"
| Array_type "ty" "nat"

primrec ty_of_htype :: "htype ⇒ ty"
where
  "ty_of_htype (Class_type C) = Class C"
| "ty_of_htype (Array_type T n) = Array T"

primrec alen_of_htype :: "htype ⇒ nat"
where
  "alen_of_htype (Array_type T n) = n"

primrec class_type_of :: "htype ⇒ cname"
where 
  "class_type_of (Class_type C) = C"
| "class_type_of (Array_type T n) = Object"

fun class_type_of' :: "ty ⇒ cname option"
where 
  "class_type_of' (Class C) = ⌊C⌋"
| "class_type_of' (Array T) = ⌊Object⌋"
| "class_type_of' _ = None" 

lemma rec_htype_is_case [simp]: "rec_htype = case_htype"
by(auto simp add: fun_eq_iff split: htype.split)

lemma ty_of_htype_eq_convs [simp]:
  shows ty_of_htype_eq_Boolean: "ty_of_htype hT ≠ Boolean"
  and ty_of_htype_eq_Void: "ty_of_htype hT ≠ Void"
  and ty_of_htype_eq_Integer: "ty_of_htype hT ≠ Integer"
  and ty_of_htype_eq_NT: "ty_of_htype hT ≠ NT"
  and ty_of_htype_eq_Class: "ty_of_htype hT = Class C ⟷ hT = Class_type C"
  and ty_of_htype_eq_Array: "ty_of_htype hT = Array T ⟷ (∃n. hT = Array_type T n)"
by(case_tac [!] hT) simp_all

lemma class_type_of_eq:
  "class_type_of hT = 
  (case hT of Class_type C ⇒ C | Array_type T n ⇒ Object)"
by(simp split: htype.split)

lemma class_type_of'_ty_of_htype [simp]:
  "class_type_of' (ty_of_htype hT) = ⌊class_type_of hT⌋"
by(cases hT) simp_all

fun is_Array :: "ty ⇒ bool"
where
  "is_Array (Array T) = True"
| "is_Array _ = False"

lemma is_Array_conv [simp]: "is_Array T ⟷ (∃U. T = Array U)"
by(cases T) simp_all

fun is_Class :: "ty ⇒ bool"
where
  "is_Class (Class C) = True"
| "is_Class _ = False"

lemma is_Class_conv [simp]: "is_Class T ⟷ (∃C. T = Class C)"
by(cases T) simp_all

subsection ‹Code generator setup›

code_pred is_refT .

end