diff --git a/Extended_Finite_State_Machines/EFSM.thy b/Extended_Finite_State_Machines/EFSM.thy index 85ca22d..1d96bef 100644 --- a/Extended_Finite_State_Machines/EFSM.thy +++ b/Extended_Finite_State_Machines/EFSM.thy @@ -586,8 +586,7 @@ lemma observe_execution_step: apply simp subgoal for a b apply (case_tac "SOME x. x |\| possible_steps e s r a b") - apply (simp add: random_member_def) - by auto + by (simp add: random_member_def) done lemma observe_execution_possible_step: @@ -949,7 +948,7 @@ next apply simp apply simp apply clarsimp - subgoal for _ _ i o l + subgoal for l o _ _ i apply (case_tac "ffilter (\(s1', t1). evaluate_outputs t1 i r1 = map Some o) (possible_steps e1 s1 r1 l i) = {||}") apply auto[1] by fastforce @@ -1129,7 +1128,7 @@ proof(induct t arbitrary: s1 s2 r1 r2) apply simp apply clarsimp apply standard - subgoal for p l i + subgoal for i p l apply (rule accepts_trace.cases) apply simp apply simp @@ -1145,11 +1144,13 @@ proof(induct t arbitrary: s1 s2 r1 r2) apply simp apply simp apply clarsimp - apply (rule accepts_trace.step) - apply (erule_tac x="(aa, b)" in fBallE) - defer apply simp - apply simp - by fastforce + subgoal for _ _ _ aa b + apply (rule accepts_trace.step) + apply (erule_tac x="(aa, b)" in fBallE) + defer apply simp + apply simp + by fastforce + done qed auto lemma executionally_equivalent_acceptance: diff --git a/Extended_Finite_State_Machines/FSet_Utils.thy b/Extended_Finite_State_Machines/FSet_Utils.thy index 2ebf6a5..1e8eb7a 100644 --- a/Extended_Finite_State_Machines/FSet_Utils.thy +++ b/Extended_Finite_State_Machines/FSet_Utils.thy @@ -296,7 +296,7 @@ lemma size_fsingleton: "(size f = 1) = (\e. f = {|e|})" apply clarify apply (simp only: size_fset_of_list) apply (simp add: fset_of_list_def fset_both_sides Abs_fset_inverse) - by (metis List.card_set One_nat_def card.insert card_1_singletonE card_empty empty_iff finite.intros(1)) + by (metis List.card_set One_nat_def card.insert card_1_singletonE card.empty empty_iff finite.intros(1)) lemma ffilter_mono: "(ffilter X xs = f) \ \x |\| xs. X x = Y x \ (ffilter Y xs = f)" by auto diff --git a/Extended_Finite_State_Machines/document/root.tex b/Extended_Finite_State_Machines/document/root.tex index 67ffd27..bc1c425 100644 --- a/Extended_Finite_State_Machines/document/root.tex +++ b/Extended_Finite_State_Machines/document/root.tex @@ -1,5 +1,5 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt} -\usepackage[USenglish]{babel} +\usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym} \usepackage{booktabs} @@ -30,8 +30,6 @@ \begingroup% \def\isacharunderscore{\textunderscore}% \section{#1 (\thy)}% - \def\isacharunderscore{-}% - \expandafter\label{sec:\isabellecontext}% \endgroup% } @@ -128,7 +126,7 @@ formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}): -\nocite{foster.ea:efsm:2018} +\nocite{foster2018} \clearpage % \chapter{Theories}