--- a/src/HOL/Bali/AxCompl.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxCompl.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb and Norbert Schirmer
*)
-header {*
+subsection {*
Completeness proof for Axiomatic semantics of Java expressions and statements
*}
@@ -18,7 +18,7 @@
-section "set of not yet initialzed classes"
+subsubsection "set of not yet initialzed classes"
definition
nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
@@ -93,7 +93,7 @@
done
-section "init-le"
+subsubsection "init-le"
definition
init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50)
@@ -113,7 +113,7 @@
apply (rule card_nyinitcls_bound)
done
-section "Most General Triples and Formulas"
+subsubsection "Most General Triples and Formulas"
definition
remember_init_state :: "state assn" ("\<doteq>")
@@ -265,7 +265,7 @@
apply blast
done
-section "main lemmas"
+subsubsection "main lemmas"
lemma MGFn_Init:
assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
@@ -1355,7 +1355,7 @@
apply assumption (* wf_prog G *)
done
-section "nested version"
+subsubsection "nested version"
lemma nesting_lemma' [rule_format (no_asm)]:
assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts"
@@ -1425,7 +1425,7 @@
done
-section "simultaneous version"
+subsubsection "simultaneous version"
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>
G,A \<union> (\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms
@@ -1460,7 +1460,7 @@
done
-section "corollaries"
+subsubsection "corollaries"
lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk>
\<Longrightarrow> \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
--- a/src/HOL/Bali/AxExample.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-header {* Example of a proof based on the Bali axiomatic semantics *}
+subsection {* Example of a proof based on the Bali axiomatic semantics *}
theory AxExample
imports AxSem Example
--- a/src/HOL/Bali/AxSem.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxSem.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-header {* Axiomatic semantics of Java expressions and statements
+subsection {* Axiomatic semantics of Java expressions and statements
(see also Eval.thy)
*}
theory AxSem imports Evaln TypeSafe begin
@@ -72,7 +72,7 @@
done
-section "assertion transformers"
+subsubsection "assertion transformers"
subsection "peek-and"
@@ -369,7 +369,7 @@
apply (simp (no_asm))
done
-section "validity"
+subsubsection "validity"
definition
type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
@@ -644,7 +644,7 @@
where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
-section "rules derived by induction"
+subsubsection "rules derived by induction"
lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
apply (unfold ax_valids_def)
@@ -715,7 +715,7 @@
oops (* dead end, Methd is to blame *)
-section "rules derived from conseq"
+subsubsection "rules derived from conseq"
text {* In the following rules we often have to give some type annotations like:
@{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
@@ -914,7 +914,7 @@
done
-section "alternative axioms"
+subsubsection "alternative axioms"
lemma ax_Lit2:
"G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
@@ -945,7 +945,7 @@
done
-section "misc derived structural rules"
+subsubsection "misc derived structural rules"
(* unused *)
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms.
@@ -1019,7 +1019,7 @@
lemmas ax_SkipI = ax_Skip [THEN conseq1]
-section "derived rules for methd call"
+subsubsection "derived rules for methd call"
lemma ax_Call_known_DynT:
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT;
@@ -1084,7 +1084,7 @@
apply clarsimp
done
-section "rules derived from Init and Done"
+subsubsection "rules derived from Init and Done"
lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
@@ -1139,7 +1139,7 @@
done
-section "introduction rules for Alloc and SXAlloc"
+subsubsection "introduction rules for Alloc and SXAlloc"
lemma ax_SXAlloc_Normal:
"G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q}
--- a/src/HOL/Bali/AxSound.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxSound.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
(* Title: HOL/Bali/AxSound.thy
Author: David von Oheimb and Norbert Schirmer
*)
-header {* Soundness proof for Axiomatic semantics of Java expressions and
+subsection {* Soundness proof for Axiomatic semantics of Java expressions and
statements
*}
theory AxSound imports AxSem begin
-section "validity"
+subsubsection "validity"
definition
triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
@@ -100,7 +100,7 @@
oops
-section "soundness"
+subsubsection "soundness"
lemma Methd_sound:
assumes recursive: "G,A\<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
--- a/src/HOL/Bali/Basis.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
(* Title: HOL/Bali/Basis.thy
Author: David von Oheimb
*)
-header {* Definitions extending HOL as logical basis of Bali *}
+subsection {* Definitions extending HOL as logical basis of Bali *}
theory Basis
imports Main "~~/src/HOL/Library/Old_Recdef"
begin
-section "misc"
+subsubsection "misc"
ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
@@ -109,7 +109,7 @@
done
-section "pairs"
+subsubsection "pairs"
lemma surjective_pairing5:
"p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
@@ -125,7 +125,7 @@
by (induct l) auto
-section "quantifiers"
+subsubsection "quantifiers"
lemma All_Ex_refl_eq2 [simp]: "(\<forall>x. (\<exists>b. x = f b \<and> Q b) \<longrightarrow> P x) = (\<forall>b. Q b \<longrightarrow> P (f b))"
by auto
@@ -143,7 +143,7 @@
by auto
-section "sums"
+subsubsection "sums"
notation case_sum (infixr "'(+')" 80)
@@ -186,7 +186,7 @@
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
-section "quantifiers for option type"
+subsubsection "quantifiers for option type"
syntax
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3! _:_:/ _)" [0,0,10] 10)
@@ -201,7 +201,7 @@
"\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
-section "Special map update"
+subsubsection "Special map update"
text{* Deemed too special for theory Map. *}
@@ -218,7 +218,7 @@
by (auto simp: chg_map_def)
-section "unique association lists"
+subsubsection "unique association lists"
definition unique :: "('a \<times> 'b) list \<Rightarrow> bool"
where "unique = distinct \<circ> map fst"
@@ -250,7 +250,7 @@
by (induct l) auto
-section "list patterns"
+subsubsection "list patterns"
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
where "lsplit = (\<lambda>f l. f (hd l) (tl l))"
--- a/src/HOL/Bali/Conform.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Conform.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-header {* Conformance notions for the type soundness proof for Java *}
+subsection {* Conformance notions for the type soundness proof for Java *}
theory Conform imports State begin
@@ -19,7 +19,7 @@
type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
-section "extension of global store"
+subsubsection "extension of global store"
definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70) where
@@ -94,7 +94,7 @@
done
-section "value conformance"
+subsubsection "value conformance"
definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70)
where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. map_option obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
@@ -175,7 +175,7 @@
done
-section "value list conformance"
+subsubsection "value list conformance"
definition
lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
@@ -248,7 +248,7 @@
apply force
done
-section "weak value list conformance"
+subsubsection "weak value list conformance"
text {* Only if the value is defined it has to conform to its type.
This is the contribution of the definite assignment analysis to
@@ -338,7 +338,7 @@
"G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
by (force simp add: lconf_def wlconf_def)
-section "object conformance"
+subsubsection "object conformance"
definition
oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) where
@@ -373,7 +373,7 @@
apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
done
-section "state conformance"
+subsubsection "state conformance"
definition
conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ("_\<Colon>\<preceq>_" [71,71] 70) where
@@ -383,7 +383,7 @@
(\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
(fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
-section "conforms"
+subsubsection "conforms"
lemma conforms_globsD:
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
--- a/src/HOL/Bali/Decl.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Decl.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Decl.thy
Author: David von Oheimb and Norbert Schirmer
*)
-header {* Field, method, interface, and class declarations, whole Java programs
+subsection {* Field, method, interface, and class declarations, whole Java programs
*}
theory Decl
@@ -367,7 +367,7 @@
by (simp add: cbody_def)
-section "standard classes"
+subsubsection "standard classes"
consts
Object_mdecls :: "mdecl list" --{* methods of Object *}
@@ -399,7 +399,7 @@
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
-section "programs"
+subsubsection "programs"
record prog =
ifaces ::"idecl list"
@@ -426,7 +426,7 @@
where "is_class G C == class G C \<noteq> None"
-section "is type"
+subsubsection "is type"
primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
@@ -445,7 +445,7 @@
by auto
-section "subinterface and subclass relation, in anticipation of TypeRel.thy"
+subsubsection "subinterface and subclass relation, in anticipation of TypeRel.thy"
definition
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
@@ -516,7 +516,7 @@
apply (auto intro: no_subcls1_Object)
done
-section "well-structured programs"
+subsubsection "well-structured programs"
definition
ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
@@ -562,7 +562,7 @@
done
-section "well-foundedness"
+subsubsection "well-foundedness"
lemma finite_is_iface: "finite {I. is_iface G I}"
apply (fold dom_def)
@@ -765,7 +765,7 @@
qed
qed
-section "general recursion operators for the interface and class hiearchies"
+subsubsection "general recursion operators for the interface and class hiearchies"
function iface_rec :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
where
--- a/src/HOL/Bali/DeclConcepts.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,12 +1,12 @@
(* Title: HOL/Bali/DeclConcepts.thy
Author: Norbert Schirmer
*)
-header {* Advanced concepts on Java declarations like overriding, inheritance,
+subsection {* Advanced concepts on Java declarations like overriding, inheritance,
dynamic method lookup*}
theory DeclConcepts imports TypeRel begin
-section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
+subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
"is_public G qn = (case class G qn of
@@ -1389,7 +1389,7 @@
qed
qed
-section "fields and methods"
+subsubsection "fields and methods"
type_synonym
@@ -2282,7 +2282,7 @@
apply assumption
done
-section "calculation of the superclasses of a class"
+subsubsection "calculation of the superclasses of a class"
definition
superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,4 +1,4 @@
-header {* Definite Assignment *}
+subsection {* Definite Assignment *}
theory DefiniteAssignment imports WellType begin
@@ -39,7 +39,7 @@
\end{itemize}
*}
-section {* Correct nesting of jump statements *}
+subsubsection {* Correct nesting of jump statements *}
text {* For definite assignment it becomes crucial, that jumps (break,
continue, return) are nested correctly i.e. a continue jump is nested in a
@@ -111,7 +111,7 @@
-section {* Calculation of assigned variables for boolean expressions*}
+subsubsection {* Calculation of assigned variables for boolean expressions*}
subsection {* Very restricted calculation fallback calculation *}
@@ -495,7 +495,7 @@
by (unfold all_union_ts_def) blast
-section "The rules of definite assignment"
+subsubsection "The rules of definite assignment"
type_synonym breakass = "(label, lname) tables"
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,4 +1,4 @@
-header {* Correctness of Definite Assignment *}
+subsection {* Correctness of Definite Assignment *}
theory DefiniteAssignmentCorrect imports WellForm Eval begin
--- a/src/HOL/Bali/Eval.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Eval.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Eval.thy
Author: David von Oheimb
*)
-header {* Operational evaluation (big-step) semantics of Java expressions and
+subsection {* Operational evaluation (big-step) semantics of Java expressions and
statements
*}
@@ -157,7 +157,7 @@
by (simp add: undefined3_def)
-section "exception throwing and catching"
+subsubsection "exception throwing and catching"
definition
throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
@@ -233,7 +233,7 @@
-section "misc"
+subsubsection "misc"
definition
assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
@@ -385,7 +385,7 @@
apply auto
done
-section "variables"
+subsubsection "variables"
definition
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
@@ -467,7 +467,7 @@
AccessViolation)
s)"
-section "evaluation judgments"
+subsubsection "evaluation judgments"
inductive
halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
@@ -1123,7 +1123,7 @@
qed
-section "single valued"
+subsubsection "single valued"
lemma unique_halloc [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>halloc oi\<succ>a' \<rightarrow> s'' \<longrightarrow> a' = a \<and> s'' = s'"
--- a/src/HOL/Bali/Evaln.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Evaln.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Evaln.thy
Author: David von Oheimb and Norbert Schirmer
*)
-header {* Operational evaluation (big-step) semantics of Java expressions and
+subsection {* Operational evaluation (big-step) semantics of Java expressions and
statements
*}
@@ -401,7 +401,7 @@
-section {* evaln implies eval *}
+subsubsection {* evaln implies eval *}
lemma evaln_eval:
assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
@@ -510,7 +510,7 @@
declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
-section {* eval implies evaln *}
+subsubsection {* eval implies evaln *}
lemma eval_evaln:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
--- a/src/HOL/Bali/Example.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Example.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Example.thy
Author: David von Oheimb
*)
-header {* Example Bali program *}
+subsection {* Example Bali program *}
theory Example
imports Eval WellForm
@@ -63,7 +63,7 @@
declare wf_fdecl_def2 [iff]
-section "type and expression names"
+subsubsection "type and expression names"
(** unfortunately cannot simply instantiate tnam **)
datatype tnam' = HasFoo' | Base' | Ext' | Main'
@@ -141,7 +141,7 @@
lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
by (simp add: SXcpt_def)
-section "classes and interfaces"
+subsubsection "classes and interfaces"
defs
@@ -266,7 +266,7 @@
apply (simp (no_asm) add: Object_def SXcpt_def)
done
-section "program"
+subsubsection "program"
abbreviation
tprg :: prog where
@@ -281,7 +281,7 @@
(Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
-section "well-structuredness"
+subsubsection "well-structuredness"
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
apply (auto dest!: tranclD subcls1D)
@@ -378,7 +378,7 @@
done
-section "misc program properties (independent of well-structuredness)"
+subsubsection "misc program properties (independent of well-structuredness)"
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
apply (unfold Ifaces_def)
@@ -421,7 +421,7 @@
-section "fields and method lookup"
+subsubsection "fields and method lookup"
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
by (rule ws_tprg [THEN fields_emptyI], force+)
@@ -531,7 +531,7 @@
apply (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
done
-section "accessibility"
+subsubsection "accessibility"
lemma classesDefined:
"\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
@@ -881,7 +881,7 @@
done
-section "well-formedness"
+subsubsection "well-formedness"
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
@@ -1059,7 +1059,7 @@
apply auto
done
-section "max spec"
+subsubsection "max spec"
lemma appl_methds_Base_foo:
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =
@@ -1076,7 +1076,7 @@
, [Class Base])}"
by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
-section "well-typedness"
+subsubsection "well-typedness"
schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
@@ -1128,7 +1128,7 @@
apply (rule wtIs (* Skip *))
done
-section "definite assignment"
+subsubsection "definite assignment"
schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
@@ -1171,7 +1171,7 @@
done
-section "execution"
+subsubsection "execution"
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>
new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
--- a/src/HOL/Bali/Name.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Name.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Name.thy
Author: David von Oheimb
*)
-header {* Java names *}
+subsection {* Java names *}
theory Name imports Basis begin
--- a/src/HOL/Bali/State.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/State.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/State.thy
Author: David von Oheimb
*)
-header {* State for evaluation of Java expressions and statements *}
+subsection {* State for evaluation of Java expressions and statements *}
theory State
imports DeclConcepts
@@ -17,7 +17,7 @@
\end{itemize}
*}
-section "objects"
+subsubsection "objects"
datatype obj_tag = --{* tag for generic object *}
CInst qtname --{* class instance *}
@@ -128,7 +128,7 @@
apply (auto dest: widen_Array_Class)
done
-section "object references"
+subsubsection "object references"
type_synonym oref = "loc + qtname" --{* generalized object reference *}
syntax
@@ -211,7 +211,7 @@
done
-section "stores"
+subsubsection "stores"
type_synonym globs --{* global variables: heap and static variables *}
= "(oref , obj) table"
@@ -459,7 +459,7 @@
done
-section "abrupt completion"
+subsubsection "abrupt completion"
@@ -577,7 +577,7 @@
by (simp add: absorb_def)
-section "full program state"
+subsubsection "full program state"
type_synonym
state = "abopt \<times> st" --{* state including abruption information *}
@@ -687,7 +687,7 @@
apply (simp (no_asm))
done
-section "initialisation test"
+subsubsection "initialisation test"
definition
inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
@@ -727,7 +727,7 @@
apply (simp (no_asm))
done
-section {* @{text error_free} *}
+subsubsection {* @{text error_free} *}
definition
error_free :: "state \<Rightarrow> bool"
--- a/src/HOL/Bali/Table.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Table.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Table.thy
Author: David von Oheimb
*)
-header {* Abstract tables and their implementation as lists *}
+subsection {* Abstract tables and their implementation as lists *}
theory Table imports Basis begin
@@ -35,7 +35,7 @@
= "'a \<Rightarrow> 'b set"
-section "map of / table of"
+subsubsection "map of / table of"
abbreviation
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
@@ -49,7 +49,7 @@
by (simp add: map_add_def)
-section {* Conditional Override *}
+subsubsection {* Conditional Override *}
definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
@@ -95,7 +95,7 @@
by (rule finite_UnI)
-section {* Filter on Tables *}
+subsubsection {* Filter on Tables *}
definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
where
@@ -179,7 +179,7 @@
by (auto simp add: fun_eq_iff cond_override_def filter_tab_def )
-section {* Misc *}
+subsubsection {* Misc *}
lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y"
apply (erule rev_mp)
@@ -289,7 +289,7 @@
where "(t hiding s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
-section "Untables"
+subsubsection "Untables"
lemma Un_tablesI [intro]: "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k"
by (auto simp add: Un_tables_def)
@@ -301,7 +301,7 @@
by (simp add: Un_tables_def)
-section "overrides"
+subsubsection "overrides"
lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
by (simp add: overrides_t_def)
@@ -322,7 +322,7 @@
by (simp add: overrides_t_def)
-section "hiding entails"
+subsubsection "hiding entails"
lemma hiding_entailsD:
"t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y"
@@ -335,7 +335,7 @@
by (simp add: hiding_entails_def)
-section "cond hiding entails"
+subsubsection "cond hiding entails"
lemma cond_hiding_entailsD:
"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
--- a/src/HOL/Bali/Term.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Term.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-header {* Java expressions and statements *}
+subsection {* Java expressions and statements *}
theory Term imports Value Table begin
@@ -427,7 +427,7 @@
apply auto
done
-section {* Evaluation of unary operations *}
+subsubsection {* Evaluation of unary operations *}
primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
where
"eval_unop UPlus v = Intg (the_Intg v)"
@@ -435,7 +435,7 @@
| "eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
| "eval_unop UNot v = Bool (\<not> the_Bool v)"
-section {* Evaluation of binary operations *}
+subsubsection {* Evaluation of binary operations *}
primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
where
"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
--- a/src/HOL/Bali/Type.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Type.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-header {* Java types *}
+subsection {* Java types *}
theory Type imports Name begin
--- a/src/HOL/Bali/TypeRel.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/TypeRel.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/TypeRel.thy
Author: David von Oheimb
*)
-header {* The relations between Java types *}
+subsection {* The relations between Java types *}
theory TypeRel imports Decl begin
@@ -55,7 +55,7 @@
implmt1_syntax ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
-section "subclass and subinterface relations"
+subsubsection "subclass and subinterface relations"
(* direct subinterface in Decl.thy, cf. 9.1.3 *)
(* direct subclass in Decl.thy, cf. 8.1.3 *)
@@ -327,7 +327,7 @@
qed
qed
-section "implementation relation"
+subsubsection "implementation relation"
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)
@@ -366,7 +366,7 @@
done
-section "widening relation"
+subsubsection "widening relation"
inductive
--{*widening, viz. method invocation conversion, cf. 5.3
@@ -583,7 +583,7 @@
done
-section "narrowing relation"
+subsubsection "narrowing relation"
(* all properties of narrowing and casting conversions we actually need *)
(* these can easily be proven from the definitions below *)
@@ -643,7 +643,7 @@
lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
-section "casting relation"
+subsubsection "casting relation"
inductive --{* casting conversion, cf. 5.5 *}
cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
--- a/src/HOL/Bali/TypeSafe.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
(* Title: HOL/Bali/TypeSafe.thy
Author: David von Oheimb and Norbert Schirmer
*)
-header {* The type soundness proof for Java *}
+subsection {* The type soundness proof for Java *}
theory TypeSafe
imports DefiniteAssignmentCorrect Conform
begin
-section "error free"
+subsubsection "error free"
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
@@ -90,7 +90,7 @@
by (cases s) (simp add: throw_def)
-section "result conformance"
+subsubsection "result conformance"
definition
assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
@@ -163,7 +163,7 @@
apply (simp (no_asm))
done
-section "fits and conf"
+subsubsection "fits and conf"
(* unused *)
lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
@@ -188,7 +188,7 @@
-section "gext"
+subsubsection "gext"
lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
@@ -242,7 +242,7 @@
done
-section "Lemmas"
+subsubsection "Lemmas"
lemma obj_ty_obj_class1:
"\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
@@ -809,7 +809,7 @@
done
-section "Call"
+subsubsection "Call"
lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;
wf_mhead G P sig mh;
@@ -1699,7 +1699,7 @@
thus ?thesis ..
qed
-section "main proof of type safety"
+subsubsection "main proof of type safety"
lemma eval_type_sound:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
--- a/src/HOL/Bali/Value.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Value.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Value.thy
Author: David von Oheimb
*)
-header {* Java values *}
+subsection {* Java values *}
--- a/src/HOL/Bali/WellForm.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/WellForm.thy Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb and Norbert Schirmer
*)
-header {* Well-formedness of Java programs *}
+subsection {* Well-formedness of Java programs *}
theory WellForm imports DefiniteAssignment begin
text {*
@@ -27,7 +27,7 @@
\end{itemize}
*}
-section "well-formed field declarations"
+subsubsection "well-formed field declarations"
text {* well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3) *}
@@ -42,7 +42,7 @@
-section "well-formed method declarations"
+subsubsection "well-formed method declarations"
(*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
(* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
@@ -202,7 +202,7 @@
apply auto
done
-section "well-formed interface declarations"
+subsubsection "well-formed interface declarations"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
text {*
@@ -273,7 +273,7 @@
apply auto
done
-section "well-formed class declarations"
+subsubsection "well-formed class declarations"
(* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
@@ -500,7 +500,7 @@
done
-section "well-formed programs"
+subsubsection "well-formed programs"
(* well-formed program, cf. 8.1, 9.1 *)
text {*
--- a/src/HOL/Bali/WellType.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/WellType.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/WellType.thy
Author: David von Oheimb
*)
-header {* Well-typedness of Java programs *}
+subsection {* Well-typedness of Java programs *}
theory WellType
imports DeclConcepts
@@ -47,7 +47,7 @@
pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
where "pkg e == pid (cls e)"
-section "Static overloading: maximally specific methods "
+subsubsection "Static overloading: maximally specific methods "
type_synonym
emhead = "ref_ty \<times> mhead"
@@ -174,7 +174,7 @@
apply (clarsimp simp add: invmode_IntVir_eq)
done
-section "Typing for unary operations"
+subsubsection "Typing for unary operations"
primrec unop_type :: "unop \<Rightarrow> prim_ty"
where
@@ -190,7 +190,7 @@
| "wt_unop UBitNot t = (t = PrimT Integer)"
| "wt_unop UNot t = (t = PrimT Boolean)"
-section "Typing for binary operations"
+subsubsection "Typing for binary operations"
primrec binop_type :: "binop \<Rightarrow> prim_ty"
where
@@ -242,7 +242,7 @@
| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
| "wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-section "Typing for terms"
+subsubsection "Typing for terms"
type_synonym tys = "ty + ty list"
translations
--- a/src/HOL/Bali/document/root.tex Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/document/root.tex Sun Nov 02 18:16:19 2014 +0100
@@ -19,8 +19,7 @@
%subsection instead of section to make the toc readable
\renewcommand{\thesubsection}{\arabic{subsection}}
-\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
-\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
+\renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}}
%remove spaces from the isabelle environment (trivlist makes them too large)
\renewenvironment{isabelle}