Commit e11e092b authored by Gerwin Klein's avatar Gerwin Klein
Browse files

Aux.thy -> Auxiliary.thy because AUX is a reserved name in Windows

parent ebac351de7ad
......@@ -8,7 +8,7 @@ header {*
\isaheader{Auxiliary Definitions and Lemmata}
*}
theory Aux
theory Auxiliary
imports
Main
"~~/src/HOL/Library/FinFun_Syntax"
......
......@@ -18,7 +18,7 @@ imports Main
"../../Collections/impl/TrieMapImpl"
"../../Collections/impl/ListMapImpl"
"../../Collections/impl/Fifo"
Aux
Auxiliary
begin
end
theory Common_Main
imports
"../Basic/Aux"
"../Basic/Auxiliary"
"../Framework/FWProgress"
"../Framework/FWBisimDeadlock"
"../Framework/FWBisimLift"
......
......@@ -11,7 +11,7 @@ header {*
theory Type
imports
"../Basic/Aux"
"../Basic/Auxiliary"
begin
type_synonym cname = String.literal -- "class names"
......
......@@ -13,12 +13,12 @@ theory Compiler1 imports
begin
definition fresh_var :: "vname list \<Rightarrow> vname"
where "fresh_var Vs \<equiv> Aux.concat (STR ''V'' # Vs)"
where "fresh_var Vs \<equiv> Auxiliary.concat (STR ''V'' # Vs)"
lemma fresh_var_fresh: "fresh_var Vs \<notin> set Vs"
proof -
have "\<forall>V \<in> set Vs. length (explode V) < length (explode (fresh_var Vs))"
by(induct Vs)(auto simp add: fresh_var_def Aux.concat_def STR_inverse implode_def)
by(induct Vs)(auto simp add: fresh_var_def Auxiliary.concat_def STR_inverse implode_def)
thus ?thesis by auto
qed
......
......@@ -8,7 +8,7 @@ Kildall's algorithm.
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
theory Kildall
imports SemilatAlg "../Basic/Aux"
imports SemilatAlg "../Basic/Auxiliary"
begin
locale Kildall_base =
......
......@@ -31,9 +31,9 @@ text {* Various other functions *}
instantiation heapobj :: toString begin
primrec toString_heapobj :: "heapobj \<Rightarrow> String.literal" where
"toString (Obj C fs) = Aux.concat [STR ''(Obj '', toString C, STR '', '', toString fs, STR '')'']"
"toString (Obj C fs) = Auxiliary.concat [STR ''(Obj '', toString C, STR '', '', toString fs, STR '')'']"
| "toString (Arr T si fs el) =
Aux.concat [STR ''(['', toString si, STR '']'', toString T, STR '', '', toString fs, STR '', '', toString (map snd (rm_to_list el)), STR '')'']"
Auxiliary.concat [STR ''(['', toString si, STR '']'', toString T, STR '', '', toString fs, STR '', '', toString (map snd (rm_to_list el)), STR '')'']"
instance proof qed
end
......
......@@ -37,7 +37,7 @@ where
instantiation list :: (toString) toString begin
definition [code]:
"toString (xs :: 'a list) = Aux.concat (STR ''['' # list_toString (STR '','') xs @ [STR '']''])"
"toString (xs :: 'a list) = Auxiliary.concat (STR ''['' # list_toString (STR '','') xs @ [STR '']''])"
instance proof qed
end
......@@ -80,7 +80,7 @@ by pat_completeness simp
termination by size_change
instantiation int :: toString begin
definition [code]: "toString i = Aux.concat (int_toString i)"
definition [code]: "toString i = Auxiliary.concat (int_toString i)"
instance proof qed
end
......@@ -92,14 +92,14 @@ end
instantiation option :: (toString) toString begin
primrec toString_option :: "'a option \<Rightarrow> String.literal" where
"toString None = STR ''None''"
| "toString (Some a) = Aux.concat [STR ''Some ('', toString a, STR '')'']"
| "toString (Some a) = Auxiliary.concat [STR ''Some ('', toString a, STR '')'']"
instance proof qed
end
instantiation finfun :: ("{toString, card_UNIV, equal, linorder}", toString) toString begin
definition [code]:
"toString (f :: 'a \<Rightarrow>f 'b) =
Aux.concat
Auxiliary.concat
(STR ''(''
# toString (finfun_default f)
# concat (map (\<lambda>x. [STR '','', toString x, STR ''|->'', toString (f $ x)]) (finfun_to_list f))
......@@ -122,9 +122,9 @@ fun toString_val :: "('a :: toString) val \<Rightarrow> String.literal"
where
"toString Unit = STR ''Unit''"
| "toString Null = STR ''Null''"
| "toString (Bool b) = Aux.concat [STR ''Bool '', toString b]"
| "toString (Intg i) = Aux.concat [STR ''Intg '', toString i]"
| "toString (Addr a) = Aux.concat [STR ''Addr '', toString a]"
| "toString (Bool b) = Auxiliary.concat [STR ''Bool '', toString b]"
| "toString (Intg i) = Auxiliary.concat [STR ''Intg '', toString i]"
| "toString (Addr a) = Auxiliary.concat [STR ''Addr '', toString a]"
instance proof qed
end
......@@ -135,8 +135,8 @@ where
| "toString Boolean = STR ''Boolean''"
| "toString Integer = STR ''Integer''"
| "toString NT = STR ''NT''"
| "toString (Class C) = Aux.concat [STR ''Class '', toString C]"
| "toString (T\<lfloor>\<rceil>) = Aux.concat [toString T, STR ''[]'']"
| "toString (Class C) = Auxiliary.concat [STR ''Class '', toString C]"
| "toString (T\<lfloor>\<rceil>) = Auxiliary.concat [toString T, STR ''[]'']"
instance proof qed
end
......@@ -164,15 +164,15 @@ end
instantiation addr_loc :: toString begin
primrec toString_addr_loc :: "addr_loc \<Rightarrow> String.literal" where
"toString (CField C F) = Aux.concat [STR ''CField '', F, STR ''{'', C, STR ''}'']"
| "toString (ACell n) = Aux.concat [STR ''ACell '', toString n]"
"toString (CField C F) = Auxiliary.concat [STR ''CField '', F, STR ''{'', C, STR ''}'']"
| "toString (ACell n) = Auxiliary.concat [STR ''ACell '', toString n]"
instance proof qed
end
instantiation htype :: toString begin
fun toString_htype :: "htype \<Rightarrow> String.literal" where
"toString (Class_type C) = C"
| "toString (Array_type T n) = Aux.concat [toString T, STR ''['', toString n, STR '']'']"
| "toString (Array_type T n) = Auxiliary.concat [toString T, STR ''['', toString n, STR '']'']"
instance proof qed
end
......@@ -180,28 +180,28 @@ instantiation obs_event :: (toString, toString) toString begin
primrec toString_obs_event :: "('a :: toString, 'b :: toString) obs_event \<Rightarrow> String.literal"
where
"toString (ExternalCall ad M vs v) =
Aux.concat [STR ''ExternalCall '', M, STR ''('', toString vs, STR '') = '', toString v]"
Auxiliary.concat [STR ''ExternalCall '', M, STR ''('', toString vs, STR '') = '', toString v]"
| "toString (ReadMem ad al v) =
Aux.concat [STR ''ReadMem '', toString ad, STR ''@'', toString al, STR ''='', toString v]"
Auxiliary.concat [STR ''ReadMem '', toString ad, STR ''@'', toString al, STR ''='', toString v]"
| "toString (WriteMem ad al v) =
Aux.concat [STR ''WriteMem '', toString ad, STR ''@'', toString al, STR ''='', toString v]"
| "toString (NewHeapElem ad hT) = Aux.concat [STR ''Allocate '', toString ad, STR '':'', toString hT]"
| "toString (ThreadStart t) = Aux.concat [STR ''ThreadStart '', toString t]"
| "toString (ThreadJoin t) = Aux.concat [STR ''ThreadJoin '', toString t]"
| "toString (SyncLock ad) = Aux.concat [STR ''SyncLock '', toString ad]"
| "toString (SyncUnlock ad) = Aux.concat [STR ''SyncUnlock '', toString ad]"
| "toString (ObsInterrupt t) = Aux.concat [STR ''Interrupt '', toString t]"
| "toString (ObsInterrupted t) = Aux.concat [STR ''Interrupted '', toString t]"
Auxiliary.concat [STR ''WriteMem '', toString ad, STR ''@'', toString al, STR ''='', toString v]"
| "toString (NewHeapElem ad hT) = Auxiliary.concat [STR ''Allocate '', toString ad, STR '':'', toString hT]"
| "toString (ThreadStart t) = Auxiliary.concat [STR ''ThreadStart '', toString t]"
| "toString (ThreadJoin t) = Auxiliary.concat [STR ''ThreadJoin '', toString t]"
| "toString (SyncLock ad) = Auxiliary.concat [STR ''SyncLock '', toString ad]"
| "toString (SyncUnlock ad) = Auxiliary.concat [STR ''SyncUnlock '', toString ad]"
| "toString (ObsInterrupt t) = Auxiliary.concat [STR ''Interrupt '', toString t]"
| "toString (ObsInterrupted t) = Auxiliary.concat [STR ''Interrupted '', toString t]"
instance proof qed
end
instantiation prod :: (toString, toString) toString begin
definition "toString = (\<lambda>(a, b). Aux.concat [STR ''('', toString a, STR '', '', toString b, STR '')''])"
definition "toString = (\<lambda>(a, b). Auxiliary.concat [STR ''('', toString a, STR '', '', toString b, STR '')''])"
instance proof qed
end
instantiation fmod_ext :: (toString) toString begin
definition "toString fd = Aux.concat [STR ''{|volatile='', toString (volatile fd), STR '', '', toString (fmod.more fd), STR ''|}'']"
definition "toString fd = Auxiliary.concat [STR ''{|volatile='', toString (volatile fd), STR '', '', toString (fmod.more fd), STR ''|}'']"
instance proof qed
end
......@@ -213,53 +213,53 @@ end
instantiation exp :: (toString, toString, toString) toString begin
fun toString_exp :: "('a :: toString, 'b :: toString, 'c :: toString) exp \<Rightarrow> String.literal"
where
"toString (new C) = Aux.concat [STR ''new '', C]"
| "toString (newArray T e) = Aux.concat [STR ''new '', toString T, STR ''['', toString e, STR '']'']"
| "toString (Cast T e) = Aux.concat [STR ''('', toString T, STR '') ('', toString e, STR '')'']"
| "toString (InstanceOf e T) = Aux.concat [STR ''('', toString e, STR '') instanceof '', toString T]"
| "toString (Val v) = Aux.concat [STR ''Val ('', toString v, STR '')'']"
| "toString (e1 \<guillemotleft>bop\<guillemotright> e2) = Aux.concat [STR ''('', toString e1, STR '') '', toString bop, STR '' ('', toString e2, STR '')'']"
| "toString (Var V) = Aux.concat [STR ''Var '', toString V]"
| "toString (V := e) = Aux.concat [toString V, STR '' := ('', toString e, STR '')'']"
| "toString (AAcc a i) = Aux.concat [STR ''('', toString a, STR '')['', toString i, STR '']'']"
| "toString (AAss a i e) = Aux.concat [STR ''('', toString a, STR '')['', toString i, STR ''] := ('', toString e, STR '')'']"
| "toString (ALen a) = Aux.concat [STR ''('', toString a, STR '').length'']"
| "toString (FAcc e F D) = Aux.concat [STR ''('', toString e, STR '').'', F, STR ''{'', D, STR ''}'']"
| "toString (FAss e F D e') = Aux.concat [STR ''('', toString e, STR '').'', F, STR ''{'', D, STR ''} := ('', toString e', STR '')'']"
| "toString (Call e M es) = Aux.concat ([STR ''('', toString e, STR '').'', M, STR ''(''] @ map toString es @ [STR '')''])"
| "toString (Block V T vo e) = Aux.concat ([STR ''{'', toString V, STR '':'', toString T] @ (case vo of None \<Rightarrow> [] | Some v \<Rightarrow> [STR ''='', toString v]) @ [STR ''; '', toString e, STR ''}''])"
| "toString (Synchronized V e e') = Aux.concat [STR ''synchronized_'', toString V, STR ''_('', toString e, STR '') {'', toString e', STR ''}'']"
| "toString (InSynchronized V ad e) = Aux.concat [STR ''insynchronized_'', toString V, STR ''_('', toString ad, STR '') {'', toString e, STR ''}'']"
| "toString (e;;e') = Aux.concat [toString e, STR ''; '', toString e']"
| "toString (if (e) e' else e'') = Aux.concat [STR ''if ('', toString e, STR '') { '', toString e', STR '' } else { '', toString e'', STR ''}'']"
| "toString (while (e) e') = Aux.concat [STR ''while ('', toString e, STR '') { '', toString e', STR '' }'']"
| "toString (throw e) = Aux.concat [STR ''throw ('', toString e, STR '')'']"
| "toString (try e catch(C V) e') = Aux.concat [STR ''try { '', toString e, STR '' } catch ('', C, STR '' '', toString V, STR '') { '', toString e', STR '' }'']"
"toString (new C) = Auxiliary.concat [STR ''new '', C]"
| "toString (newArray T e) = Auxiliary.concat [STR ''new '', toString T, STR ''['', toString e, STR '']'']"
| "toString (Cast T e) = Auxiliary.concat [STR ''('', toString T, STR '') ('', toString e, STR '')'']"
| "toString (InstanceOf e T) = Auxiliary.concat [STR ''('', toString e, STR '') instanceof '', toString T]"
| "toString (Val v) = Auxiliary.concat [STR ''Val ('', toString v, STR '')'']"
| "toString (e1 \<guillemotleft>bop\<guillemotright> e2) = Auxiliary.concat [STR ''('', toString e1, STR '') '', toString bop, STR '' ('', toString e2, STR '')'']"
| "toString (Var V) = Auxiliary.concat [STR ''Var '', toString V]"
| "toString (V := e) = Auxiliary.concat [toString V, STR '' := ('', toString e, STR '')'']"
| "toString (AAcc a i) = Auxiliary.concat [STR ''('', toString a, STR '')['', toString i, STR '']'']"
| "toString (AAss a i e) = Auxiliary.concat [STR ''('', toString a, STR '')['', toString i, STR ''] := ('', toString e, STR '')'']"
| "toString (ALen a) = Auxiliary.concat [STR ''('', toString a, STR '').length'']"
| "toString (FAcc e F D) = Auxiliary.concat [STR ''('', toString e, STR '').'', F, STR ''{'', D, STR ''}'']"
| "toString (FAss e F D e') = Auxiliary.concat [STR ''('', toString e, STR '').'', F, STR ''{'', D, STR ''} := ('', toString e', STR '')'']"
| "toString (Call e M es) = Auxiliary.concat ([STR ''('', toString e, STR '').'', M, STR ''(''] @ map toString es @ [STR '')''])"
| "toString (Block V T vo e) = Auxiliary.concat ([STR ''{'', toString V, STR '':'', toString T] @ (case vo of None \<Rightarrow> [] | Some v \<Rightarrow> [STR ''='', toString v]) @ [STR ''; '', toString e, STR ''}''])"
| "toString (Synchronized V e e') = Auxiliary.concat [STR ''synchronized_'', toString V, STR ''_('', toString e, STR '') {'', toString e', STR ''}'']"
| "toString (InSynchronized V ad e) = Auxiliary.concat [STR ''insynchronized_'', toString V, STR ''_('', toString ad, STR '') {'', toString e, STR ''}'']"
| "toString (e;;e') = Auxiliary.concat [toString e, STR ''; '', toString e']"
| "toString (if (e) e' else e'') = Auxiliary.concat [STR ''if ('', toString e, STR '') { '', toString e', STR '' } else { '', toString e'', STR ''}'']"
| "toString (while (e) e') = Auxiliary.concat [STR ''while ('', toString e, STR '') { '', toString e', STR '' }'']"
| "toString (throw e) = Auxiliary.concat [STR ''throw ('', toString e, STR '')'']"
| "toString (try e catch(C V) e') = Auxiliary.concat [STR ''try { '', toString e, STR '' } catch ('', C, STR '' '', toString V, STR '') { '', toString e', STR '' }'']"
instance proof qed
end
instantiation instr :: (toString) toString begin
primrec toString_instr :: "'a instr \<Rightarrow> String.literal" where
"toString (Load i) = Aux.concat [STR ''Load ('', toString i, STR '')'']"
| "toString (Store i) = Aux.concat [STR ''Store ('', toString i, STR '')'']"
| "toString (Push v) = Aux.concat [STR ''Push ('', toString v, STR '')'']"
| "toString (New C) = Aux.concat [STR ''New '', toString C]"
| "toString (NewArray T) = Aux.concat [STR ''NewArray '', toString T]"
"toString (Load i) = Auxiliary.concat [STR ''Load ('', toString i, STR '')'']"
| "toString (Store i) = Auxiliary.concat [STR ''Store ('', toString i, STR '')'']"
| "toString (Push v) = Auxiliary.concat [STR ''Push ('', toString v, STR '')'']"
| "toString (New C) = Auxiliary.concat [STR ''New '', toString C]"
| "toString (NewArray T) = Auxiliary.concat [STR ''NewArray '', toString T]"
| "toString ALoad = STR ''ALoad''"
| "toString AStore = STR ''AStore''"
| "toString ALength = STR ''ALength''"
| "toString (Getfield F D) = Aux.concat [STR ''Getfield '', toString F, STR '' '', toString D]"
| "toString (Putfield F D) = Aux.concat [STR ''Putfield '', toString F, STR '' '', toString D]"
| "toString (Checkcast T) = Aux.concat [STR ''Checkcast '', toString T]"
| "toString (Instanceof T) = Aux.concat [STR ''Instanceof '', toString T]"
| "toString (Invoke M n) = Aux.concat [STR ''Invoke '', toString M, STR '' '', toString n]"
| "toString (Getfield F D) = Auxiliary.concat [STR ''Getfield '', toString F, STR '' '', toString D]"
| "toString (Putfield F D) = Auxiliary.concat [STR ''Putfield '', toString F, STR '' '', toString D]"
| "toString (Checkcast T) = Auxiliary.concat [STR ''Checkcast '', toString T]"
| "toString (Instanceof T) = Auxiliary.concat [STR ''Instanceof '', toString T]"
| "toString (Invoke M n) = Auxiliary.concat [STR ''Invoke '', toString M, STR '' '', toString n]"
| "toString Return = STR ''Return''"
| "toString Pop = STR ''Pop''"
| "toString Dup = STR ''Dup''"
| "toString Swap = STR ''Swap''"
| "toString (BinOpInstr bop) = Aux.concat [STR ''BinOpInstr '', toString bop]"
| "toString (Goto i) = Aux.concat [STR ''Goto '', toString i]"
| "toString (IfFalse i) = Aux.concat [STR ''IfFalse '', toString i]"
| "toString (BinOpInstr bop) = Auxiliary.concat [STR ''BinOpInstr '', toString bop]"
| "toString (Goto i) = Auxiliary.concat [STR ''Goto '', toString i]"
| "toString (IfFalse i) = Auxiliary.concat [STR ''IfFalse '', toString i]"
| "toString ThrowExc = STR ''ThrowExc''"
| "toString MEnter = STR ''monitorenter''"
| "toString MExit = STR ''monitorexit''"
......@@ -274,7 +274,7 @@ end
instantiation rbt :: ("{toString,linorder}", toString) toString begin
definition [code]:
"toString (t :: ('a, 'b) rbt) =
Aux.concat (list_toString (STR [Char Nibble2 NibbleC, Char Nibble0 NibbleA]) (rm_to_list t))"
Auxiliary.concat (list_toString (STR [Char Nibble2 NibbleC, Char Nibble0 NibbleA]) (rm_to_list t))"
instance proof qed
end
......
......@@ -8,7 +8,7 @@ header {*
theory FWState
imports
"../Basic/Aux"
"../Basic/Auxiliary"
begin
datatype lock_action =
......
......@@ -6,7 +6,7 @@ header {* \isaheader{Labelled transition systems} *}
theory LTS
imports
"../Basic/Aux"
"../Basic/Auxiliary"
"../../Coinductive/TLList"
"~~/src/HOL/Library/Quotient_Option"
begin
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment