# HG changeset patch
# User wenzelm
# Date 1729262582 -7200
# Node ID 60f46822a22cc4c750e5cf55cf86e959d701c6b2
# Parent  60fedd5b7c5813621ae4a6d026aa3dcca88ecf49
tuned proofs;

diff -r 60fedd5b7c58 -r 60f46822a22c src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Fri Oct 18 16:42:53 2024 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Fri Oct 18 16:43:02 2024 +0200
@@ -136,33 +136,30 @@
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q"
 proof -                             
-  {
-    fix s n
-    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
-    proof (induction "n" arbitrary: s rule: less_induct)
-      fix n :: nat
-      fix s :: 'a
-      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
-      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
-      proof (rule impI, cases "s \<in> b")
-        assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
-        hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
-          using assms(1) by auto
-        hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
-          by (metis assms(2) ValidTC_def)
-        from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
-          by auto
-        hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q"
-          using 1 by auto
-        thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
-          using 2 3 Sem.intros(6) by force
-      next
-        assume "s \<notin> b" and "s \<in> i \<and> v s = n"
-        thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
-          using Sem.intros(5) assms(3) by fastforce
-      qed
+  have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)" for s n
+  proof (induction "n" arbitrary: s rule: less_induct)
+    fix n :: nat
+    fix s :: 'a
+    assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
+    show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
+    proof (rule impI, cases "s \<in> b")
+      assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
+      hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
+        using assms(1) by auto
+      hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
+        by (metis assms(2) ValidTC_def)
+      from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
+        by auto
+      hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q"
+        using 1 by auto
+      thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
+        using 2 3 Sem.intros(6) by force
+    next
+      assume "s \<notin> b" and "s \<in> i \<and> v s = n"
+      thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
+        using Sem.intros(5) assms(3) by fastforce
     qed
-  }
+  qed
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
diff -r 60fedd5b7c58 -r 60f46822a22c src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Oct 18 16:42:53 2024 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Oct 18 16:43:02 2024 +0200
@@ -140,33 +140,30 @@
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b c) (Awhile i v A) q"
 proof -
-  {
-    fix s n
-    have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
-    proof (induction "n" arbitrary: s rule: less_induct)
-      fix n :: nat
-      fix s :: 'a
-      assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
-      show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
-      proof (rule impI, cases "s \<in> b")
-        assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
-        hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
-          using assms(1) by auto
-        hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
-          by (metis assms(2) ValidTC_def)
-        from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
-          by auto
-        hence "\<exists>u . Sem (While b c) (Some t) (Some u) \<and> u \<in> q"
-          using 1 by auto
-        thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
-          using 2 3 Sem.intros(10) by force
-      next
-        assume "s \<notin> b" and "s \<in> i \<and> v s = n"
-        thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
-          using Sem.intros(9) assms(3) by fastforce
-      qed
+  have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)" for s n
+  proof (induction "n" arbitrary: s rule: less_induct)
+    fix n :: nat
+    fix s :: 'a
+    assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
+    show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q)"
+    proof (rule impI, cases "s \<in> b")
+      assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
+      hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
+        using assms(1) by auto
+      hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
+        by (metis assms(2) ValidTC_def)
+      from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
+        by auto
+      hence "\<exists>u . Sem (While b c) (Some t) (Some u) \<and> u \<in> q"
+        using 1 by auto
+      thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
+        using 2 3 Sem.intros(10) by force
+    next
+      assume "s \<notin> b" and "s \<in> i \<and> v s = n"
+      thus "\<exists>t . Sem (While b c) (Some s) (Some t) \<and> t \<in> q"
+        using Sem.intros(9) assms(3) by fastforce
     qed
-  }
+  qed
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed