tuned proofs;

--- a/src/HOL/HOLCF/IOA/TL.thy	Sun Jan 05 21:17:36 2025 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy	Sun Jan 05 22:28:05 2025 +0100
@@ -57,34 +57,53 @@
 subsection \<open>TLA Axiomatization by Merz\<close>
 
 lemma suffix_refl: "suffix s s"
-  apply (simp add: suffix_def)
-  apply (rule_tac x = "nil" in exI)
-  apply auto
-  done
+proof -
+  have "Finite nil \<and> s = nil @@ s" by simp
+  then show ?thesis unfolding suffix_def ..
+qed
+
+lemma suffix_trans:
+  assumes "suffix y x"
+    and "suffix z y"
+  shows "suffix z x"
+proof -
+  from assms obtain s1 s2
+    where "Finite s1 \<and> x = s1 @@ y"
+      and "Finite s2 \<and> y = s2 @@ z"
+    unfolding suffix_def by iprover
+  then have "Finite (s1 @@ s2) \<and> x = (s1 @@ s2) @@ z"
+    by (simp add: Conc_assoc)
+  then show ?thesis unfolding suffix_def ..
+qed
 
 lemma reflT: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
-  apply (simp add: satisfies_def IMPLIES_def Box_def)
-  apply (rule impI)+
-  apply (erule_tac x = "s" in allE)
-  apply (simp add: tsuffix_def suffix_refl)
-  done
-
-lemma suffix_trans: "suffix y x \<Longrightarrow> suffix z y \<Longrightarrow> suffix z x"
-  apply (simp add: suffix_def)
-  apply auto
-  apply (rule_tac x = "s1 @@ s1a" in exI)
-  apply auto
-  apply (simp add: Conc_assoc)
-  done
+proof
+  assume s: "s \<noteq> UU \<and> s \<noteq> nil"
+  have "F s" if box_F: "\<forall>s2. tsuffix s2 s \<longrightarrow> F s2"
+  proof -
+    from s and suffix_refl [of s] have "tsuffix s s"
+      by (simp add: tsuffix_def)
+    also from box_F have "?this \<longrightarrow> F s" ..
+    finally show ?thesis .
+  qed
+  then show "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F"
+    by (simp add: satisfies_def IMPLIES_def Box_def)
+qed
 
 lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"
-  apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def)
-  apply auto
-  apply (drule suffix_trans)
-  apply assumption
-  apply (erule_tac x = "s2a" in allE)
-  apply auto
-  done
+proof -
+  have "F s2" if *: "tsuffix s1 s" "tsuffix s2 s1"
+    and **: "\<forall>s'. tsuffix s' s \<longrightarrow> F s'"
+    for s1 s2
+  proof -
+    from * have "tsuffix s2 s"
+      by (auto simp: tsuffix_def elim: suffix_trans)
+    also from ** have "?this \<longrightarrow> F s2" ..
+    finally show ?thesis .
+  qed
+  then show ?thesis
+    by (simp add: satisfies_def IMPLIES_def Box_def)
+qed
 
 lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"
   by (simp add: satisfies_def IMPLIES_def Box_def)
@@ -98,10 +117,11 @@
 lemma STL1b: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (Init P)"
   by (simp add: valid_def validT_def satisfies_def Init_def)
 
-lemma STL1: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P))"
-  apply (rule STL1a)
-  apply (erule STL1b)
-  done
+lemma STL1: assumes "\<TTurnstile> P" shows "\<^bold>\<TTurnstile> (\<box>(Init P))"
+proof -
+  from assms have "\<^bold>\<TTurnstile> (Init P)" by (rule STL1b)
+  then show ?thesis by (rule STL1a)
+qed
 
 (*Note that unlift and HD is not at all used!*)
 lemma STL4: "\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"