From c3c1cafaa3734e63bd7d32479dbca2eaf3ec2a4f Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Fri, 26 Feb 2021 11:42:58 +0000
Subject: [PATCH] Import of AFP for Isabelle 2021.

---
 Extended_Finite_State_Machines/EFSM.thy       | 19 ++++++++++---------
 Extended_Finite_State_Machines/FSet_Utils.thy |  2 +-
 .../document/root.tex                         |  6 ++----
 3 files changed, 13 insertions(+), 14 deletions(-)

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 |\<in>| 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 (\<lambda>(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) = (\<exists>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) \<Longrightarrow> \<forall>x |\<in>| xs. X x = Y x \<Longrightarrow> (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}