--- a/src/HOL/MicroJava/BV/Altern.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Altern.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: Martin Strecker
*)
-section {* Alternative definition of well-typing of bytecode, used in compiler type correctness proof *}
+section \<open>Alternative definition of well-typing of bytecode, used in compiler type correctness proof\<close>
theory Altern
imports BVSpec
--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: Gerwin Klein
*)
-section {* Example Welltypings \label{sec:BVExample} *}
+section \<open>Example Welltypings \label{sec:BVExample}\<close>
theory BVExample
imports
@@ -11,26 +11,26 @@
JVM
begin
-text {*
+text \<open>
This theory shows type correctness of the example program in section
\ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
explicitly providing a welltyping. It also shows that the start
state of the program conforms to the welltyping; hence type safe
execution is guaranteed.
-*}
+\<close>
subsection "Setup"
-text {* Abbreviations for definitions we will have to use often in the
-proofs below: *}
+text \<open>Abbreviations for definitions we will have to use often in the
+proofs below:\<close>
lemmas name_defs = list_name_def test_name_def val_name_def next_name_def
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def
OutOfMemoryC_def ClassCastC_def
lemmas class_defs = list_class_def test_class_def
-text {* These auxiliary proofs are for efficiency: class lookup,
+text \<open>These auxiliary proofs are for efficiency: class lookup,
subclass relation, method and field lookup are computed only once:
-*}
+\<close>
lemma class_Object [simp]:
"class E Object = Some (undefined, [],[])"
by (simp add: class_def system_defs E_def)
@@ -60,7 +60,7 @@
Xcpt ClassCast, Xcpt OutOfMemory, Object}"
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
-text {* The subclass releation spelled out: *}
+text \<open>The subclass releation spelled out:\<close>
lemma subcls1:
"subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
@@ -70,7 +70,7 @@
apply auto
done
-text {* The subclass relation is acyclic; hence its converse is well founded: *}
+text \<open>The subclass relation is acyclic; hence its converse is well founded:\<close>
lemma notin_rtrancl:
"(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False"
by (auto elim: converse_rtranclE)
@@ -88,7 +88,7 @@
apply (rule acyclic_subcls1_E)
done
-text {* Method and field lookup: *}
+text \<open>Method and field lookup:\<close>
lemma method_Object [simp]:
"method (E, Object) = Map.empty"
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
@@ -150,7 +150,7 @@
lemmas [simp] = is_class_def
-text {*
+text \<open>
The next definition and three proof rules implement an algorithm to
enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"}
transforms a goal of the form
@@ -162,7 +162,7 @@
@{text "\<dots>"}
@{prop [display] "P n"}
-*}
+\<close>
definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
@@ -180,9 +180,9 @@
subsection "Program structure"
-text {*
+text \<open>
The program is structurally wellformed:
-*}
+\<close>
lemma wf_struct:
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
@@ -226,10 +226,10 @@
qed
subsection "Welltypings"
-text {*
+text \<open>
We show welltypings of the methods @{term append_name} in class @{term list_name},
and @{term makelist_name} in class @{term test_name}:
-*}
+\<close>
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
declare appInvoke [simp del]
@@ -289,7 +289,7 @@
apply simp
done
-text {* Some abbreviations for readability *}
+text \<open>Some abbreviations for readability\<close>
abbreviation Clist :: ty
where "Clist == Class list_name"
abbreviation Ctest :: ty
@@ -368,7 +368,7 @@
apply simp
done
-text {* The whole program is welltyped: *}
+text \<open>The whole program is welltyped:\<close>
definition Phi :: prog_type ("\<Phi>") where
"\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else
if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
@@ -386,8 +386,8 @@
subsection "Conformance"
-text {* Execution of the program will be typesafe, because its
- start state conforms to the welltyping: *}
+text \<open>Execution of the program will be typesafe, because its
+ start state conforms to the welltyping:\<close>
lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
apply (rule BV_correct_initial)
@@ -437,7 +437,7 @@
code_printing
constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
-text {* This code setup is just a demonstration and \emph{not} sound! *}
+text \<open>This code setup is just a demonstration and \emph{not} sound!\<close>
lemma False
proof -
@@ -480,10 +480,10 @@
definition test2 where
"test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
-ML_val {*
+ML_val \<open>
@{code test1};
@{code test2};
-*}
+\<close>
end
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,16 +2,16 @@
Author: Gerwin Klein
*)
-section {* Welltyped Programs produce no Type Errors *}
+section \<open>Welltyped Programs produce no Type Errors\<close>
theory BVNoTypeError
imports "../JVM/JVMDefensive" BVSpecTypeSafe
begin
-text {*
+text \<open>
Some simple lemmas about the type testing functions of the
defensive JVM:
-*}
+\<close>
lemma typeof_NoneD [simp,dest]:
"typeof (\<lambda>v. None) v = Some x \<Longrightarrow> \<not>isAddr v"
by (cases v) auto
@@ -217,10 +217,10 @@
done
-text {*
+text \<open>
The main theorem: welltyped programs do not produce type errors if they
are started in a conformant state.
-*}
+\<close>
theorem no_type_error:
assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
shows "exec_d G (Normal s) \<noteq> TypeError"
@@ -391,11 +391,11 @@
qed
-text {*
+text \<open>
The theorem above tells us that, in welltyped programs, the
defensive machine reaches the same result as the aggressive
one (after arbitrarily many steps).
-*}
+\<close>
theorem welltyped_aggressive_imp_defensive:
"wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t
\<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)"
@@ -441,11 +441,11 @@
from wt this s show ?thesis by (rule no_type_errors)
qed
-text {*
+text \<open>
As corollary we get that the aggressive and the defensive machine
are equivalent for welltyped programs (if started in a conformant
state or in the canonical start state)
-*}
+\<close>
corollary welltyped_commutes:
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
--- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,17 +3,17 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* The Bytecode Verifier \label{sec:BVSpec} *}
+section \<open>The Bytecode Verifier \label{sec:BVSpec}\<close>
theory BVSpec
imports Effect
begin
-text {*
+text \<open>
This theory contains a specification of the BV. The specification
describes correct typings of method bodies; it corresponds
to type \emph{checking}.
-*}
+\<close>
definition
-- "The program counter will always be inside the method:"
@@ -37,7 +37,7 @@
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
definition
- -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
+ -- \<open>The type at @{text "pc=0"} conforms to the method calling convention:\<close>
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where
"wt_start G C pTs mxl phi \<longleftrightarrow>
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
@@ -96,10 +96,10 @@
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
-text {*
+text \<open>
We could leave out the check @{term "pc' < max_pc"} in the
definition of @{term wt_instr} in the context of @{term wt_method}.
-*}
+\<close>
lemma wt_instr_def2:
"\<lbrakk> wt_jvm_prog G Phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins;
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,22 +3,22 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* BV Type Safety Proof \label{sec:BVSpecTypeSafe} *}
+section \<open>BV Type Safety Proof \label{sec:BVSpecTypeSafe}\<close>
theory BVSpecTypeSafe
imports Correct
begin
-text {*
+text \<open>
This theory contains proof that the specification of the bytecode
verifier only admits type safe programs.
-*}
+\<close>
-subsection {* Preliminaries *}
+subsection \<open>Preliminaries\<close>
-text {*
+text \<open>
Simp and intro setup for the type safety proof:
-*}
+\<close>
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def
wt_instr_def eff_def norm_eff_def
@@ -27,10 +27,10 @@
lemmas [simp del] = split_paired_All
-text {*
+text \<open>
If we have a welltyped program and a conforming state, we
can directly infer that the current instruction is well typed:
-*}
+\<close>
lemma wt_jvm_prog_impl_wt_instr_cor:
"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
@@ -41,11 +41,11 @@
done
-subsection {* Exception Handling *}
+subsection \<open>Exception Handling\<close>
-text {*
+text \<open>
Exceptions don't touch anything except the stack:
-*}
+\<close>
lemma exec_instr_xcpt:
"(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
= (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs =
@@ -53,10 +53,10 @@
by (cases i, auto simp add: split_beta split: split_if_asm)
-text {*
+text \<open>
Relates @{text match_any} from the Bytecode Verifier with
@{text match_exception_table} from the operational semantics:
-*}
+\<close>
lemma in_match_any:
"match_exception_table G xcpt pc et = Some pc' \<Longrightarrow>
\<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and>
@@ -123,14 +123,14 @@
apply (auto split: split_if_asm)
done
-text {*
+text \<open>
We can prove separately that the recursive search for exception
handlers (@{text find_handler}) in the frame stack results in
a conforming state (if there was no matching exception handler
in the current frame). We require that the exception is a valid
heap address, and that the state before the exception occured
conforms.
-*}
+\<close>
lemma uncaught_xcpt_correct:
"\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
@@ -244,11 +244,11 @@
qed
declare raise_if_def [simp]
-text {*
+text \<open>
The requirement of lemma @{text uncaught_xcpt_correct} (that
the exception is a valid reference on the heap) is always met
for welltyped instructions and conformant states:
-*}
+\<close>
lemma exec_instr_xcpt_hp:
"\<lbrakk> fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
@@ -280,10 +280,10 @@
by (auto elim: preallocatedE [of hp x])
-text {*
+text \<open>
Finally we can state that, whenever an exception occurs, the
resulting next state always conforms:
-*}
+\<close>
lemma xcpt_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
@@ -582,14 +582,14 @@
-subsection {* Single Instructions *}
+subsection \<open>Single Instructions\<close>
-text {*
+text \<open>
In this section we look at each single (welltyped) instruction, and
prove that the state after execution of the instruction still conforms.
Since we have already handled exceptions above, we can now assume, that
on exception occurs for this (single step) execution.
-*}
+\<close>
lemmas [iff] = not_Err_eq
@@ -1220,13 +1220,13 @@
by simp
-text {*
+text \<open>
The next theorem collects the results of the sections above,
i.e.~exception handling and the execution step for each
instruction. It states type safety for single step execution:
in welltyped programs, a conforming state is transformed
into another conforming state when one instruction is executed.
-*}
+\<close>
theorem instr_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
@@ -1265,7 +1265,7 @@
apply (rule Throw_correct, assumption+)
done
-subsection {* Main *}
+subsection \<open>Main\<close>
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* BV Type Safety Invariant *}
+section \<open>BV Type Safety Invariant\<close>
theory Correct
imports BVSpec "../JVM/JVMExec"
@@ -64,7 +64,7 @@
by (cases X) auto
-subsection {* approx-val *}
+subsection \<open>approx-val\<close>
lemma approx_val_Err [simp,intro!]:
"approx_val G hp x Err"
@@ -92,7 +92,7 @@
\<Longrightarrow> approx_val G hp v T'"
by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
-subsection {* approx-loc *}
+subsection \<open>approx-loc\<close>
lemma approx_loc_Nil [simp,intro!]:
"approx_loc G hp [] []"
@@ -166,7 +166,7 @@
apply blast
done
-subsection {* approx-stk *}
+subsection \<open>approx-stk\<close>
lemma approx_stk_rev_lem:
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
@@ -217,7 +217,7 @@
apply (erule conf_widen, assumption+)
done
-subsection {* oconf *}
+subsection \<open>oconf\<close>
lemma oconf_field_update:
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
@@ -238,7 +238,7 @@
apply (fastforce intro: approx_val_heap_update)
done
-subsection {* hconf *}
+subsection \<open>hconf\<close>
lemma hconf_newref:
"\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
@@ -255,7 +255,7 @@
simp add: obj_ty_def)
done
-subsection {* preallocated *}
+subsection \<open>preallocated\<close>
lemma preallocated_field_update:
"\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs);
@@ -285,7 +285,7 @@
with alloc show ?thesis by (simp add: preallocated_def)
qed
-subsection {* correct-frames *}
+subsection \<open>correct-frames\<close>
lemmas [simp del] = fun_upd_apply
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-section {* Effect of Instructions on the State Type *}
+section \<open>Effect of Instructions on the State Type\<close>
theory Effect
imports JVMType "../JVM/JVMExceptions"
@@ -11,7 +11,7 @@
type_synonym succ_type = "(p_count \<times> state_type option) list"
-text {* Program counter of successor instructions: *}
+text \<open>Program counter of successor instructions:\<close>
primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where
"succs (Load idx) pc = [pc+1]"
| "succs (Store idx) pc = [pc+1]"
@@ -226,10 +226,10 @@
lemmas [simp] = app_def xcpt_app_def
-text {*
+text \<open>
\medskip
simp rules for @{term app}
-*}
+\<close>
lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp
--- a/src/HOL/MicroJava/BV/EffectMono.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-section {* Monotonicity of eff and app *}
+section \<open>Monotonicity of eff and app\<close>
theory EffectMono
imports Effect
--- a/src/HOL/MicroJava/BV/JType.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* The Java Type System as Semilattice *}
+section \<open>The Java Type System as Semilattice\<close>
theory JType
imports "../DFA/Semilattices" "../J/WellForm"
--- a/src/HOL/MicroJava/BV/JVM.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* Kildall for the JVM \label{sec:JVM} *}
+section \<open>Kildall for the JVM \label{sec:JVM}\<close>
theory JVM
imports Typing_Framework_JVM
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* The JVM Type System as Semilattice *}
+section \<open>The JVM Type System as Semilattice\<close>
theory JVMType
imports JType
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* LBV for the JVM \label{sec:JVM} *}
+section \<open>LBV for the JVM \label{sec:JVM}\<close>
theory LBVJVM
imports Typing_Framework_JVM
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* The Typing Framework for the JVM \label{sec:JVM} *}
+section \<open>The Typing Framework for the JVM \label{sec:JVM}\<close>
theory Typing_Framework_JVM
imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
@@ -17,7 +17,7 @@
"opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
-subsection {* Executability of @{term check_bounded} *}
+subsection \<open>Executability of @{term check_bounded}\<close>
primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -46,7 +46,7 @@
by (simp add: list_all_iff check_bounded_def)
-subsection {* Connecting JVM and Framework *}
+subsection \<open>Connecting JVM and Framework\<close>
lemma check_bounded_is_bounded:
"check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Oct 07 23:28:49 2015 +0200
@@ -1276,7 +1276,7 @@
apply assumption
apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
- -- {* @{text "<=s"} *}
+ -- \<open>@{text "<=s"}\<close>
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply (simp add: max_spec_preserves_length [symmetric])
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2003 TUM
*)
-section {* Abstract Bytecode Verifier *}
+section \<open>Abstract Bytecode Verifier\<close>
(*<*)
theory Abstract_BV
--- a/src/HOL/MicroJava/DFA/Err.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* The Error Type *}
+section \<open>The Error Type\<close>
theory Err
imports Semilat
@@ -166,7 +166,7 @@
lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
by (auto simp add: err_def)
-subsection {* lift *}
+subsection \<open>lift\<close>
lemma lift_in_errI:
"\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
@@ -188,7 +188,7 @@
by (simp add: lift2_def plussub_def split: err.split)
-subsection {* sup *}
+subsection \<open>sup\<close>
lemma Err_sup_Err [simp]:
"Err +_(Err.sup f) x = Err"
@@ -217,7 +217,7 @@
apply (simp split: err.split)
done
-subsection {* semilat (err A) (le r) f *}
+subsection \<open>semilat (err A) (le r) f\<close>
lemma semilat_le_err_Err_plus [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
@@ -283,7 +283,7 @@
done
qed
-subsection {* semilat (err(Union AS)) *}
+subsection \<open>semilat (err(Union AS))\<close>
(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
@@ -301,11 +301,11 @@
apply fast
done
-text {*
+text \<open>
If @{term "AS = {}"} the thm collapses to
@{prop "order r & closed {Err} f & Err +_f Err = Err"}
which may not hold
-*}
+\<close>
lemma err_semilat_UnionI:
"\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {};
!A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk>
--- a/src/HOL/MicroJava/DFA/Kildall.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* Kildall's Algorithm \label{sec:Kildall} *}
+section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
theory Kildall
imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-section {* Completeness of the LBV *}
+section \<open>Completeness of the LBV\<close>
theory LBVComplete
imports LBVSpec Typing_Framework
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Correctness of the LBV *}
+section \<open>Correctness of the LBV\<close>
theory LBVCorrect
imports LBVSpec Typing_Framework
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* The Lightweight Bytecode Verifier *}
+section \<open>The Lightweight Bytecode Verifier\<close>
theory LBVSpec
imports SemilatAlg Opt
--- a/src/HOL/MicroJava/DFA/Listn.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* Fixed Length Lists *}
+section \<open>Fixed Length Lists\<close>
theory Listn
imports Err
--- a/src/HOL/MicroJava/DFA/Opt.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Opt.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* More about Options *}
+section \<open>More about Options\<close>
theory Opt
imports Err
--- a/src/HOL/MicroJava/DFA/Product.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Product.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* Products as Semilattices *}
+section \<open>Products as Semilattices\<close>
theory Product
imports Err
--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,9 +3,9 @@
Copyright 2000 TUM
*)
-chapter {* Bytecode Verifier \label{cha:bv} *}
+chapter \<open>Bytecode Verifier \label{cha:bv}\<close>
-section {* Semilattices *}
+section \<open>Semilattices\<close>
theory Semilat
imports Main "~~/src/HOL/Library/While_Combinator"
@@ -301,7 +301,7 @@
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
(*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
-subsection{*An executable lub-finder*}
+subsection\<open>An executable lub-finder\<close>
definition exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" where
"exec_lub r f x y \<equiv> while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2002 Technische Universitaet Muenchen
*)
-section {* More on Semilattices *}
+section \<open>More on Semilattices\<close>
theory SemilatAlg
imports Typing_Framework Product
--- a/src/HOL/MicroJava/DFA/Semilattices.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2003 TUM
*)
-section {* Semilattices *}
+section \<open>Semilattices\<close>
(*<*)
theory Semilattices
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,15 +3,15 @@
Copyright 2000 TUM
*)
-section {* Typing and Dataflow Analysis Framework *}
+section \<open>Typing and Dataflow Analysis Framework\<close>
theory Typing_Framework
imports Listn
begin
-text {*
+text \<open>
The relationship between dataflow analysis and a welltyped-instruction predicate.
-*}
+\<close>
type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-section {* Lifting the Typing Framework to err, app, and eff *}
+section \<open>Lifting the Typing Framework to err, app, and eff\<close>
theory Typing_Framework_err
imports Typing_Framework SemilatAlg
@@ -158,12 +158,12 @@
-text {*
+text \<open>
There used to be a condition here that each instruction must have a
successor. This is not needed any more, because the definition of
@{term error} trivially ensures that there is a successor for
the critical case where @{term app} does not hold.
-*}
+\<close>
lemma wt_err_imp_wt_app_eff:
assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
assumes b: "bounded (err_step (size ts) app step) (size ts)"
--- a/src/HOL/MicroJava/J/Conform.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Conformity Relations for Type Soundness Proof *}
+section \<open>Conformity Relations for Type Soundness Proof\<close>
theory Conform imports State WellType Exceptions begin
--- a/src/HOL/MicroJava/J/Decl.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Class Declarations and Programs *}
+section \<open>Class Declarations and Programs\<close>
theory Decl imports Type begin
--- a/src/HOL/MicroJava/J/Eval.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Operational Evaluation (big step) Semantics *}
+section \<open>Operational Evaluation (big step) Semantics\<close>
theory Eval imports State WellType begin
--- a/src/HOL/MicroJava/J/Example.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,11 +3,11 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Example MicroJava Program *}
+section \<open>Example MicroJava Program\<close>
theory Example imports SystemClasses Eval begin
-text {*
+text \<open>
The following example MicroJava program includes:
class declarations with inheritance, hiding of fields, and overriding of
methods (with refined result type),
@@ -34,15 +34,15 @@
}
}
\end{verbatim}
-*}
+\<close>
datatype cnam' = Base' | Ext'
datatype vnam' = vee' | x' | e'
-text {*
+text \<open>
@{text cnam'} and @{text vnam'} are intended to be isomorphic
to @{text cnam} and @{text vnam}
-*}
+\<close>
axiomatization cnam' :: "cnam' => cname"
where
@@ -378,7 +378,7 @@
apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;"
apply (rule t) -- "Expr"
apply (rule t) -- "LAss"
-apply simp -- {* @{text "e \<noteq> This"} *}
+apply simp -- \<open>@{text "e \<noteq> This"}\<close>
apply (rule t) -- "LAcc"
apply (simp (no_asm))
apply (simp (no_asm))
--- a/src/HOL/MicroJava/J/Exceptions.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy Wed Oct 07 23:28:49 2015 +0200
@@ -5,7 +5,7 @@
theory Exceptions imports State begin
-text {* a new, blank object with default values in all fields: *}
+text \<open>a new, blank object with default values in all fields:\<close>
definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where
"blank G C \<equiv> (C,init_vars (fields(G,C)))"
--- a/src/HOL/MicroJava/J/JBasis.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,9 +2,9 @@
Author: David von Oheimb, TU Muenchen
*)
-chapter {* Java Source Language \label{cha:j} *}
+chapter \<open>Java Source Language \label{cha:j}\<close>
-section {* Some Auxiliary Definitions *}
+section \<open>Some Auxiliary Definitions\<close>
theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin
--- a/src/HOL/MicroJava/J/JListExample.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: Stefan Berghofer
*)
-section {* Example for generating executable code from Java semantics *}
+section \<open>Example for generating executable code from Java semantics\<close>
theory JListExample
imports Eval
@@ -151,7 +151,7 @@
"test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
-ML_val {*
+ML_val \<open>
val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
locs @{code l1_name};
locs @{code l2_name};
@@ -177,6 +177,6 @@
val_field (Suc (Suc (Suc @{code "0 :: nat"})));
next_field (Suc (Suc (Suc @{code "0 :: nat"})));
-*}
+\<close>
end
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-section {* Type Safety Proof *}
+section \<open>Type Safety Proof\<close>
theory JTypeSafe imports Eval Conform begin
@@ -176,12 +176,12 @@
declare fun_upd_same [simp]
declare wf_prog_ws_prog [simp]
-ML{*
+ML\<open>
fun forward_hyp_tac ctxt =
ALLGOALS (TRY o (EVERY' [dresolve_tac ctxt [spec], mp_tac ctxt,
(mp_tac ctxt ORELSE' (dresolve_tac ctxt [spec] THEN' mp_tac ctxt)),
REPEAT o (eresolve_tac ctxt [conjE])]))
-*}
+\<close>
theorem eval_evals_exec_type_sound:
@@ -201,8 +201,8 @@
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
apply( simp_all)
apply( tactic "ALLGOALS (REPEAT o resolve_tac @{context} [impI, allI])")
-apply( tactic {* ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
- THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
+apply( tactic \<open>ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
+ THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context})))\<close>)
apply(tactic "ALLGOALS (EVERY' [REPEAT o (eresolve_tac @{context} [conjE]), REPEAT o hyp_subst_tac @{context}])")
-- "Level 7"
@@ -241,12 +241,12 @@
apply( fast elim: conforms_localD [THEN lconfD])
-- "for FAss"
-apply( tactic {* EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
- THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3*})
+apply( tactic \<open>EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
+ THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3\<close>)
-- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
- (asm_full_simp_tac @{context})) 7*})
+apply( tactic \<open>(Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
+ (asm_full_simp_tac @{context})) 7\<close>)
apply (tactic "forward_hyp_tac @{context}")
@@ -277,8 +277,8 @@
-- "7 LAss"
apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
- THEN_ALL_NEW (full_simp_tac @{context})) 1 *})
+apply( tactic \<open>(eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
+ THEN_ALL_NEW (full_simp_tac @{context})) 1\<close>)
apply (intro strip)
apply (case_tac E)
apply (simp)
--- a/src/HOL/MicroJava/J/State.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/State.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Program State *}
+section \<open>Program State\<close>
theory State
imports TypeRel Value
@@ -21,7 +21,7 @@
definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
"init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-type_synonym aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *}
+type_synonym aheap = "loc \<rightharpoonup> obj" -- \<open>"@{text heap}" used in a translation below\<close>
type_synonym locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents"
type_synonym state = "aheap \<times> locals" -- "heap, local parameter including This"
@@ -52,7 +52,7 @@
definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
"raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo"
-text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
+text \<open>Make @{text new_Addr} completely specified (at least for the code generator)\<close>
(*
definition new_Addr :: "aheap => loc \<times> val option" where
"new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None) | x = Some (Addr (XcptRef OutOfMemory))"
@@ -154,7 +154,7 @@
lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
by (simp add: c_hupd_def split_beta)
-text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
+text \<open>Naive implementation for @{term "new_Addr"} by exhaustive search\<close>
definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
"gen_new_Addr h n \<equiv>
--- a/src/HOL/MicroJava/J/SystemClasses.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,14 +3,14 @@
Copyright 2002 Technische Universitaet Muenchen
*)
-section {* System Classes *}
+section \<open>System Classes\<close>
theory SystemClasses imports Decl begin
-text {*
+text \<open>
This theory provides definitions for the @{text Object} class,
and the system exceptions.
-*}
+\<close>
definition ObjectC :: "'c cdecl" where
[code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
--- a/src/HOL/MicroJava/J/Term.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-section {* Expressions and Statements *}
+section \<open>Expressions and Statements\<close>
theory Term imports Value begin
--- a/src/HOL/MicroJava/J/Type.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Java types *}
+section \<open>Java types\<close>
theory Type imports JBasis begin
@@ -17,7 +17,7 @@
end
-text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
+text \<open>These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME\<close>
instantiation cnam :: typerep
begin
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-section {* Relations between Java Types *}
+section \<open>Relations between Java Types\<close>
theory TypeRel
imports Decl
@@ -74,7 +74,7 @@
-text {* Code generator setup *}
+text \<open>Code generator setup\<close>
code_pred
(modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
@@ -134,10 +134,10 @@
assume "(C, D, fs, ms) \<in> set G"
and "C \<noteq> Object"
and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
- from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms'
+ from \<open>(C, D, fs, ms) \<in> set G\<close> obtain D' fs' ms'
where "class": "class G C = Some (D', fs', ms')"
unfolding class_def by(auto dest!: weak_map_of_SomeI)
- hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
+ hence "G \<turnstile> C \<prec>C1 D'" using \<open>C \<noteq> Object\<close> ..
hence *: "(C, D') \<in> (subcls1 G)^+" ..
also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
@@ -154,20 +154,20 @@
case base
then obtain rest where "class G C = Some (C, rest)"
and "C \<noteq> Object" by cases
- from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
+ from \<open>class G C = Some (C, rest)\<close> have "(C, C, rest) \<in> set G"
unfolding class_def by(rule map_of_SomeD)
- with `C \<noteq> Object` `class G C = Some (C, rest)`
+ with \<open>C \<noteq> Object\<close> \<open>class G C = Some (C, rest)\<close>
have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
thus False by simp
next
case (step D)
- from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
+ from \<open>G \<turnstile> D \<prec>C1 C\<close> obtain rest where "class G D = Some (C, rest)"
and "D \<noteq> Object" by cases
- from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
+ from \<open>class G D = Some (C, rest)\<close> have "(D, C, rest) \<in> set G"
unfolding class_def by(rule map_of_SomeD)
- with `D \<noteq> Object` `class G D = Some (C, rest)`
+ with \<open>D \<noteq> Object\<close> \<open>class G D = Some (C, rest)\<close>
have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
- moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
+ moreover from \<open>(C, D) \<in> (subcls1 G)\<^sup>+\<close>
have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl)
ultimately show False by contradiction
qed
--- a/src/HOL/MicroJava/J/Value.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-section {* Java Values *}
+section \<open>Java Values\<close>
theory Value imports Type begin
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,13 +3,13 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Well-formedness of Java programs *}
+section \<open>Well-formedness of Java programs\<close>
theory WellForm
imports TypeRel SystemClasses
begin
-text {*
+text \<open>
for static checks on expressions and statements, see WellType.
\begin{description}
@@ -24,7 +24,7 @@
\item for uniformity, Object is assumed to be declared like any other class
\end{itemize}
\end{description}
-*}
+\<close>
type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
definition wf_syscls :: "'c prog => bool" where
--- a/src/HOL/MicroJava/J/WellType.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,11 +3,11 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Well-typedness Constraints *}
+section \<open>Well-typedness Constraints\<close>
theory WellType imports Term WellForm begin
-text {*
+text \<open>
the formulation of well-typedness of method calls given below (as well as
the Java Specification 1.0) is a little too restrictive: Is does not allow
methods of class Object to be called upon references of interface type.
@@ -19,7 +19,7 @@
e.g.\ definedness of names (of parameters, locals, fields, methods)
\end{itemize}
\end{description}
-*}
+\<close>
text "local variables, including method parameters and This:"
type_synonym lenv = "vname \<rightharpoonup> ty"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,15 +2,15 @@
Author: Gerwin Klein
*)
-section {* A Defensive JVM *}
+section \<open>A Defensive JVM\<close>
theory JVMDefensive
imports JVMExec
begin
-text {*
+text \<open>
Extend the state space by one element indicating a type error (or
- other abnormal termination) *}
+ other abnormal termination)\<close>
datatype 'a type_error = TypeError | Normal 'a
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-section {* Exception handling in the JVM *}
+section \<open>Exception handling in the JVM\<close>
theory JVMExceptions imports JVMInstructions begin
@@ -41,15 +41,15 @@
| Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
-text {*
+text \<open>
System exceptions are allocated in all heaps:
-*}
+\<close>
-text {*
+text \<open>
Only program counters that are mentioned in the exception table
can be returned by @{term match_exception_table}:
-*}
+\<close>
lemma match_exception_table_in_et:
"match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
by (induct et) (auto split: split_if_asm)
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Program Execution in the JVM *}
+section \<open>Program Execution in the JVM\<close>
theory JVMExec imports JVMExecInstr JVMExceptions begin
@@ -28,12 +28,12 @@
"G \<turnstile> s \<midarrow>jvm\<rightarrow> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-text {*
+text \<open>
The start configuration of the JVM: in the start heap, we call a
method @{text m} of class @{text C} in program @{text G}. The
@{text this} pointer of the frame is set to @{text Null} to simulate
a static method invokation.
-*}
+\<close>
definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where
"start_state G C m \<equiv>
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Oct 07 23:28:49 2015 +0200
@@ -4,7 +4,7 @@
*)
-section {* JVM Instruction Semantics *}
+section \<open>JVM Instruction Semantics\<close>
theory JVMExecInstr imports JVMInstructions JVMState begin
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
Author: Gerwin Klein, Technische Universitaet Muenchen
*)
-section {* Instructions of the JVM *}
+section \<open>Instructions of the JVM\<close>
theory JVMInstructions imports JVMState begin
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,16 +2,16 @@
Author: Stefan Berghofer
*)
-section {* Example for generating executable code from JVM semantics \label{sec:JVMListExample} *}
+section \<open>Example for generating executable code from JVM semantics \label{sec:JVMListExample}\<close>
theory JVMListExample
imports "../J/SystemClasses" JVMExec
begin
-text {*
+text \<open>
Since the types @{typ cnam}, @{text vnam}, and @{text mname} are
anonymous, we describe distinctness of names in the example by axioms:
-*}
+\<close>
axiomatization list_nam test_nam :: cnam
where distinct_classes: "list_nam \<noteq> test_nam"
@@ -136,7 +136,7 @@
definition
"test = exec (E, start_state E test_name makelist_name)"
-ML_val {*
+ML_val \<open>
@{code test};
@{code exec} (@{code E}, @{code the} it);
@{code exec} (@{code E}, @{code the} it);
@@ -191,6 +191,6 @@
@{code exec} (@{code E}, @{code the} it);
@{code exec} (@{code E}, @{code the} it);
@{code exec} (@{code E}, @{code the} it);
-*}
+\<close>
end
--- a/src/HOL/MicroJava/JVM/JVMState.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Wed Oct 07 23:28:49 2015 +0200
@@ -2,15 +2,15 @@
Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
*)
-chapter {* Java Virtual Machine \label{cha:jvm} *}
+chapter \<open>Java Virtual Machine \label{cha:jvm}\<close>
-section {* State of the JVM *}
+section \<open>State of the JVM\<close>
theory JVMState
imports "../J/Conform"
begin
-subsection {* Frame Stack *}
+subsection \<open>Frame Stack\<close>
type_synonym opstack = "val list"
type_synonym locvars = "val list"
type_synonym p_count = nat
@@ -29,16 +29,16 @@
-- "program counter within frame"
-subsection {* Exceptions *}
+subsection \<open>Exceptions\<close>
definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
"raise_system_xcpt b x \<equiv> raise_if b x None"
-subsection {* Runtime State *}
+subsection \<open>Runtime State\<close>
type_synonym
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
-subsection {* Lemmas *}
+subsection \<open>Lemmas\<close>
lemma new_Addr_OutOfMemory:
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"