Isabelle2025

.github/workflows/ci.yml

@@ -64,15 +64,6 @@ jobs:
             - name: Check library proofs
               run: |
                 find ./library -type f -iname "*_proofs.tla"            \
-                  \(                                                    \
-                         -not -name "BagsTheorems_proofs.tla"           \
-                    -and -not -name "FiniteSetTheorems_proofs.tla"      \
-                    -and -not -name "FunctionTheorems_proofs.tla"       \
-                    -and -not -name "NaturalsInduction_proofs.tla"      \
-                    -and -not -name "SequenceTheorems_proofs.tla"       \
-                    -and -not -name "SequencesExtTheorems_proofs.tla"   \
-                    -and -not -name "WellFoundedInduction_proofs.tla"   \
-                  \)                                                    \
                   -print0 | xargs --null --max-args=1 --no-run-if-empty \
                     ./_build/tlapm/bin/tlapm --cleanfp
             - name: Run tests

deps/isabelle/dune.mk

@@ -4,17 +4,17 @@
 OS_TYPE=$(patsubst CYGWIN%,Cygwin,$(shell uname))
 HOST_CPU=$(shell uname -m)
 
-ISABELLE_VSN=Isabelle2024
+ISABELLE_VSN=Isabelle2025
 
 ifeq ($(OS_TYPE),Linux)
-	ISABELLE_SHA256=603aaaf8abea36597af3b0651d2c162a86c0a0dd4420766f47e5724039639267
+	ISABELLE_SHA256=3d1d66de371823fe31aa8ae66638f73575bac244f00b31aee1dcb62f38147c56
 	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_linux.tar.gz
 	ISABELLE_ARCHIVE_TYPE=tgz
 	ISABELLE_ARCHIVE_DIR=$(ISABELLE_VSN)
 	FIND_EXEC=-executable
 endif
 ifeq ($(OS_TYPE),Darwin)
-	ISABELLE_SHA256=22035f996f71ea1f03063f6f144195eb6a04974d4d916ed0772cd79569a28bc7
+	ISABELLE_SHA256=ea5754c228857f5d9d3ae254ec9814797f2453ea290df20b2f6dcb2ef0e2e7f8
 	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_macos.tar.gz
 	ISABELLE_ARCHIVE_TYPE=tgz
 	ISABELLE_ARCHIVE_DIR=$(ISABELLE_VSN).app
@@ -64,12 +64,12 @@ ifeq ($(ISABELLE_ARCHIVE_TYPE),tgz)
 	tar -xzf $<
 	mv $(ISABELLE_ARCHIVE_DIR) $(ISABELLE_DIR)
 endif
-	cd $(ISABELLE_DIR) && rm -rf ./contrib/e-3.0.03-1/src/lib/
+	cd $(ISABELLE_DIR) && rm -rf ./contrib/e-3.1-1/src/lib/
 ifeq ($(OS_TYPE),Darwin)
-	cd $(ISABELLE_DIR) && cd contrib/jdk-21.0.3/arm64-darwin/ \
+	cd $(ISABELLE_DIR) && cd contrib/jdk-21.0.6/arm64-darwin/ \
 		&& (find . -type link | xargs rm) \
 		&& mv zulu-21.jdk/Contents/Home/* ./
-	cd $(ISABELLE_DIR) && cd contrib/jdk-21.0.3/x86_64-darwin/ \
+	cd $(ISABELLE_DIR) && cd contrib/jdk-21.0.6/x86_64-darwin/ \
 		&& (find . -type link | xargs rm) \
 		&& mv zulu-21.jdk/Contents/Home/* ./
 endif

isabelle/Constant.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/Constant.thy
     Author:     Stephan Merz, LORIA
-    Copyright (C) 2008-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2008-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open> Main theory for constant-level Isabelle/\tlaplus{} \<close>

isabelle/FixedPoints.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/FixedPoints.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2008-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2008-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open>Fixed points for set-theoretical constructions\<close>

isabelle/Functions.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/Functions.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2008-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2008-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open> \tlaplus{} Functions \<close>

isabelle/IntegerArithmetic.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/IntegerArithmetic.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2009-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2009-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open> Arithmetic (except division) for the integers \<close>
@@ -829,23 +829,8 @@ text \<open>
   From now on, we reduce the set @{text "Nat"} to the set of
   non-negative integers.
 \<close>
-lemma nat_iff_int_geq0' (*[simp]*) : "n \<in> Nat = (n \<in> Int \<and> 0 \<le> n)"
-  by (auto simp: int_leq_def)
-
-text \<open>
-We will use \<open>nat_is_int_geq0\<close> for simplification instead
-of \<open>nat_iff_int_geq0'\<close> for rewriting \<open>Nat\<close> to \<open>Int\<close> to
-handle also the cases where no \<open>Nat\<close> is used without
-the \<open>\<in>\<close> operator, e.g. in function sets.
-\<close>
 lemma nat_is_int_geq0 [simp] : "Nat = {x \<in> Int : 0 \<le> x}"
-proof
-  show "\<And>x. x \<in> Nat \<Longrightarrow> x \<in> {x \<in> Int : 0 \<le> x}"
-    using nat_iff_int_geq0' by auto
-next
-  show "\<And>x. x \<in> {x \<in> Int : 0 \<le> x} \<Longrightarrow> x \<in> Nat"
-    using nat_iff_int_geq0' by auto
-qed
+  by (auto simp: int_leq_def)
 
 
 declare natIsInt [simp del]
@@ -1717,13 +1702,26 @@ lemma trans_leq_diff_nat2 [simp]:
 
 lemma int_leq_iff_add:
   assumes "i \<in> Int" and "j \<in> Int"
-  shows "(i \<le> j) = (\<exists>k \<in> Nat: j = i + k)" (is "?lhs = ?rhs")
-  using assms by (auto intro: int_leq_imp_add simp del: nat_is_int_geq0 simp add: nat_iff_int_geq0')
+  shows "(i \<le> j) = (\<exists>k \<in> Nat: j = i + k)"
+  using assms by (auto intro: int_leq_imp_add simp: nat_zero_leq simp del: nat_is_int_geq0)
 
 lemma int_less_iff_succ_add:
   assumes "i \<in> Int" and "j \<in> Int"
   shows "(i < j) = (\<exists>k \<in> Nat: j = succ[i + k])" (is "?lhs = ?rhs")
-  using assms by (auto intro: int_less_imp_succ_add simp del: nat_is_int_geq0 simp add: nat_iff_int_geq0')
+proof -
+  {
+    assume ?lhs then have ?rhs
+      using assms by (blast dest: int_less_imp_succ_add)
+  }
+  moreover
+  {
+    assume ?rhs
+    then obtain k where k: "k \<in> Int" "0 \<le> k" "j = succ[i+k]" by auto
+    with assms have ?lhs by auto
+  }
+  ultimately 
+  show ?thesis by blast
+qed
 
 lemma leq_add_self1 [simp]:
   assumes "i \<in> Int" and "j \<in> Int"

isabelle/IntegerDivision.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/IntegerDivision.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2009-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2009-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open> The division operators div and mod on the integers \<close>

isabelle/Integers.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/Integers.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2008-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2008-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open> The set of integer numbers \<close>

isabelle/NewSMT.thy

@@ -107,7 +107,7 @@ subsection \<open>Integers\<close>
 lemma PlusTyping: "x \<in> Int \<and> y \<in> Int \<Rightarrow> x+y \<in> Int"
   by simp
 
-lemma UminusTyping: "x \<in> Int \<Rightarrow> -.x \<in> Int"
+lemma UminusTyping: "x \<in> Int \<Rightarrow> -x \<in> Int"
   by simp
 
 lemma MinusTyping: "x \<in> Int \<and> y \<in> Int \<Rightarrow> x-y \<in> Int"
@@ -116,33 +116,14 @@ lemma MinusTyping: "x \<in> Int \<and> y \<in> Int \<Rightarrow> x-y \<in> Int"
 lemma TimesTyping: "x \<in> Int \<and> y \<in> Int \<Rightarrow> x*y \<in> Int"
   by simp
 
-(* Isabelle currently provides integer division only for natural
-   numbers, so we cannot prove the following.
-
-lemma DivTyping: "x \<in> Int \<and> y \<in> Int \<and> y \<noteq> 0 \<Rightarrow> x \\div y \<in> Int"
-*)
+lemma DivTyping: "x \<in> Int \<and> y \<in> Int \<and> y > 0 \<Rightarrow> x div y \<in> Int"
+  by simp
 
 lemma NatDef: "x \<in> Nat \<Leftrightarrow> x \<in> Int \<and> 0 \<le> x"
-proof
-  assume "x \<in> Nat"
-  then show "x \<in> Int \<and> 0 \<le> x" by simp
-next
-  assume "x \<in> Int \<and> 0 \<le> x"
-  hence "x \<in> Int" "0 \<le> x" by blast+
-  from \<open>x \<in> Int\<close> show "x \<in> Nat"
-  proof (rule intCases)
-    fix m
-    assume "m \<in> Nat" "x = -.m"
-    with \<open>0 \<le> x\<close> show ?thesis
-      by (cases m) auto
-  qed
-qed
-
-(* Isabelle currently does not support integer intervals,
-   so we cannot prove the following.
+  by simp
 
 lemma RangeDef: "x \<in> a .. b \<Leftrightarrow> x \<in> Int \<and> a \<le> x \<and> x \<le> b"
-*)
+  by simp
 
 
 subsection \<open>Booleans\<close>
@@ -219,7 +200,16 @@ lemma SeqIntro:
      "\<forall>i : i \<in> DOMAIN s \<Leftrightarrow> i \<in> Nat \<and> 1 \<le> i \<and> i \<le> Len(s)"
      "\<forall>i \<in> Nat : 1 \<le> i \<and> i \<le> Len(s) \<Rightarrow> s[i] \<in> a"
    shows  "s \<in> Seq(a)"
-  using assms by auto
+proof
+  from assms show "isASeq(s)" by auto
+next
+  fix k
+  assume "k \<in> 1 .. Len(s)"
+  hence k: "k \<in> Int" "1 \<le> k" "k \<le> Len(s)" by auto
+  with \<open>Len(s) \<in> Nat\<close> have "k \<in> Nat" by auto
+  with \<open>\<forall>i \<in> Nat : 1 \<le> i \<and> i \<le> Len(s) \<Rightarrow> s[i] \<in> a\<close> k
+  show "s[k] \<in> a" by blast
+qed
 
 lemma SeqElim1:
   "s \<in> Seq(a) \<Rightarrow> isAFcn(s) \<and> Len(s) \<in> Nat \<and> DOMAIN s = 1 .. Len(s)"
@@ -258,14 +248,24 @@ text \<open>
 \<close>
 lemma AppendApp1:
   assumes "Len(s) \<in> Nat" (* missing from original formulation *)
-          "i \<in> Nat"  (* changed from Int because Isabelle doesn't support Int intervals *)
+          "i \<in> Int"
           "1 \<le> i" "i \<le> Len(s)"
   shows   "Append(s,x)[i] = s[i]"
   using assms unfolding Append_def by auto
 
 lemma AppendApp2:
-  "Len(s) \<in> Nat \<Rightarrow> Append(s,x)[Len(s)+1] = x"
-  unfolding Append_def by auto
+  assumes "Len(s) \<in> Nat"
+  shows "Append(s,x)[Len(s)+1] = x"
+proof -
+  from assms have "Len(s)+1 = succ[Len(s)]"
+    by simp
+  moreover
+  from assms have "Len(s)+1 \<in> DOMAIN Append(s,x)"
+    by (auto simp: Append_def)
+  ultimately
+  show ?thesis
+    using assms by (auto simp: Append_def)
+qed
 
 text \<open>
   Isabelle/TLA+ doesn't know about the remaining operations on sequences.

isabelle/PredicateLogic.thy

@@ -1,8 +1,8 @@
 (*  Title:      TLA+/PredicateLogic.thy
     Author:     Stephan Merz, Inria Nancy
-    Copyright (C) 2008-2024  INRIA and Microsoft Corporation
+    Copyright (C) 2008-2025  INRIA and Microsoft Corporation
     License:    BSD
-    Version:    Isabelle2024
+    Version:    Isabelle2025
 *)
 
 section \<open>First-Order Logic for TLA+\<close>
@@ -1355,8 +1355,6 @@ text \<open>
   development of FOL, we introduce a set of ``shadow connectives''
   that will only be used for this purpose.
 \<close>
-
-(* lemmas cases = case_split [case_names True False] *)
 context
 begin
 
@@ -1425,37 +1423,33 @@ ML \<open>
   )
 \<close>
 
+simproc_setup passive swap_cases_false ("cases_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q") =
+  \<open>fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      _ $ (P as _ $ \<^Const_>\<open>cases_false\<close>) $ (_ $ Q $ _) =>
+        if P <> Q then SOME Drule.swap_prems_eq else NONE
+    | _ => NONE)\<close>
+
+simproc_setup passive cases_equal_conj_curry ("cases_conj(P, Q) \<Longrightarrow> PROP R") =
+  \<open>fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      _ $ (_ $ P) $ _ =>
+        let
+          fun is_conj \<^Const_>\<open>cases_conj for P Q\<close> = is_conj P andalso is_conj Q
+            | is_conj \<^Const_>\<open>cases_equal\<close> = true
+            | is_conj \<^Const_>\<open>cases_true\<close> = true
+            | is_conj \<^Const_>\<open>cases_false\<close> = true
+            | is_conj _ = false
+        in if is_conj P then SOME @{thm cases_conj_curry} else NONE end
+      | _ => NONE)\<close>
+
 declaration \<open>
-  fn _ => Induct.map_simpset (fn ss => ss
-    addsimprocs
-      [Simplifier.make_simproc @{context}
-        {name = "swap_cases_false",
-         lhss = [@{term "cases_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"}],
-         proc = fn _ => fn _ => fn ct =>
-          (case Thm.term_of ct of
-            _ $ (P as _ $ @{const cases_false}) $ (_ $ Q $ _) =>
-              if P <> Q then SOME Drule.swap_prems_eq else NONE
-          | _ => NONE),
-         identifier = []},
-       Simplifier.make_simproc @{context}
-        {name = "cases_equal_conj_curry",
-         lhss = [@{term "cases_conj(P, Q) \<Longrightarrow> PROP R"}],
-         proc = fn _ => fn _ => fn ct =>
-          (case Thm.term_of ct of
-            _ $ (_ $ P) $ _ =>
-              let
-                fun is_conj (@{const cases_conj} $ P $ Q) =
-                      is_conj P andalso is_conj Q
-                  | is_conj (Const (@{const_name cases_equal}, _) $ _ $ _) = true
-                  | is_conj @{const cases_true} = true
-                  | is_conj @{const cases_false} = true
-                  | is_conj _ = false
-              in if is_conj P then SOME @{thm cases_conj_curry} else NONE end
-            | _ => NONE),
-         identifier = []}]
-    |> Simplifier.set_mksimps (fn ctxt =>
+  K (Induct.map_simpset
+     (Simplifier.add_proc \<^simproc>\<open>swap_cases_false\<close> #>
+      Simplifier.add_proc \<^simproc>\<open>cases_equal_conj_curry\<close> #>
+      Simplifier.set_mksimps (fn ctxt =>
         Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
-        map (rewrite_rule ctxt (map Thm.symmetric @{thms cases_rulify_fallback}))))
+        map (rewrite_rule ctxt (map Thm.symmetric @{thms cases_rulify_fallback})))))
 \<close>
 
 text \<open> Pre-simplification of induction and cases rules \<close>
@@ -1523,7 +1517,8 @@ subsection \<open> Propositional simplification \<close>
 subsubsection \<open> Conversion to Boolean values \<close>
 
 text \<open>
-  Because \tlaplus{} is untyped, equivalence is different from equality,
+  Because \tlaplus{} does not distinguish between terms and formulas, 
+  equivalence is different from equality,
   and one has to be careful about stating the laws of propositional
   logic. For example, although the equivalence @{text "(TRUE \<and> A) \<Leftrightarrow> A"}
   is valid, we cannot state the law @{text "(TRUE \<and> A) = A"}
@@ -1945,7 +1940,6 @@ struct
   (
     type T = ((term -> bool) * stamp) list;
     val empty = [];
-    val extend = I;
     fun merge data : T = Library.merge (eq_snd (op =)) data;
   );
   fun add m = Data.map (cons (m, stamp ()));

isabelle/SMT.thy

@@ -1,3 +1,5 @@
+(* This material is now obsolete but included because it may still become relevant. *)
+
 header {* Normalization rules used in the SMT backend  *}
 
 theory SMT