header {*
\chapter{Concepts for all JinjaThreads Languages}\label{cha:j}
\isaheader{JinjaThreads types}
*}
theory Type imports
Aux
begin
types
cname = String.literal -- "class names"
mname = String.literal -- "method name"
vname = String.literal -- "names for local/field variables"
constdefs
Object :: cname
"Object ≡ STR ''Object''"
Thread :: cname
"Thread ≡ STR ''Thread''"
Throwable :: cname
"Throwable ≡ STR ''Throwable''"
this :: vname
"this ≡ STR ''this''"
run :: mname
"run ≡ STR ''run''"
start :: mname
"start ≡ STR ''start''"
wait :: mname
"wait ≡ STR ''wait''"
notify :: mname
"notify ≡ STR ''notify''"
notifyAll :: mname
"notifyAll ≡ STR ''notifyAll''"
join :: mname
"join ≡ STR ''join''"
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"
"wait ≠ notify" "wait ≠ notifyAll" "wait ≠ join" "notify ≠ notifyAll"
"notify ≠ join" "notifyAll ≠ join"
by(auto simp add: start_def wait_def notify_def notifyAll_def join_def)
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"
inductive is_refT :: "ty => bool" where
"is_refT NT"
| "is_refT (Class C)"
| "is_refT (A⌊⌉)"
declare is_refT.intros[iff]
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 (T⌊⌉) = ground_type T"
| "ground_type T = T"
abbreviation is_NT_Array :: "ty => bool" where
"is_NT_Array T ≡ ground_type T = NT"
consts
the_Class :: "ty => cname"
primrec
"the_Class (Class C) = C"
consts
the_Array :: "ty => ty"
primrec
"the_Array (T⌊⌉) = T"
end