diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6797264d..95b86003 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -73,9 +73,6 @@ jobs: rm "$DEPS_DIR/tlaps.tar.gz" mv $DEPS_DIR/tlaps* "$DEPS_DIR/tlapm-install" SKIP=( - # Missing operator ENABLEDrules; will be fixed after - # updated_enabled_cdot branch is merged. - "specifications/ewd998/AsyncTerminationDetection.tla" # General proof failure "specifications/Bakery-Boulangerie/Bakery.tla" "specifications/Bakery-Boulangerie/Boulanger.tla" @@ -88,12 +85,9 @@ jobs: "specifications/LoopInvariance/BinarySearch.tla" "specifications/LoopInvariance/Quicksort.tla" "specifications/LoopInvariance/SumSequence.tla" - "specifications/MisraReachability/ReachabilityProofs.tla" - "specifications/Paxos/Consensus.tla" - "specifications/PaxosHowToWinATuringAward/Consensus.tla" "specifications/lamport_mutex/LamportMutex_proofs.tla" "specifications/TeachingConcurrency/SimpleRegular.tla" - # Long-running + # Failing and long-running "specifications/byzpaxos/BPConProof.tla" # Takes about 30 minutes ) python "$SCRIPT_DIR/check_proofs.py" \ diff --git a/deps/isabelle/Makefile b/deps/isabelle/Makefile index 61dfa01f..524a2642 100644 --- a/deps/isabelle/Makefile +++ b/deps/isabelle/Makefile @@ -1,7 +1,7 @@ OS_TYPE=$(patsubst CYGWIN%,Cygwin,$(shell uname)) HOST_CPU=$(shell uname -m) -ISABELLE_VSN=Isabelle2023 +ISABELLE_VSN=Isabelle2024-RC3 ifeq ($(OS_TYPE),Linux) ISABELLE_ARCHIVE=$(ISABELLE_VSN)_linux.tar.gz @@ -76,14 +76,14 @@ $(ISABELLE_DIR)/src/TLA+: $(ISABELLE_DIR) .PRECIOUS: $(ISABELLE_DIR).no-links $(ISABELLE_DIR).no-links: $(ISABELLE_DIR) $(ISABELLE_DIR)/src/TLA+ rm -rf $@ - cd $< && rm -rf ./contrib/e-2.6-1/src/lib/ + cd $< && rm -rf ./contrib/e-3.0.03-1/src/lib/ ifeq ($(OS_TYPE),Darwin) - cd $< && cd contrib/jdk-17.0.7/arm64-darwin/ \ + cd $< && cd contrib/jdk-21.0.3/arm64-darwin/ \ && (find . -type link | xargs rm) \ - && mv zulu-17.jdk/Contents/Home/* ./ - cd $< && cd contrib/jdk-17.0.7/x86_64-darwin/ \ + && mv zulu-21.jdk/Contents/Home/* ./ + cd $< && cd contrib/jdk-21.0.3/x86_64-darwin/ \ && (find . -type link | xargs rm) \ - && mv zulu-17.jdk/Contents/Home/* ./ + && mv zulu-21.jdk/Contents/Home/* ./ cd $< && rm -rf contrib/vscodium-1.70.1 endif touch $@ diff --git a/deps/isabelle/README.md b/deps/isabelle/README.md new file mode 100644 index 00000000..692d4ad7 --- /dev/null +++ b/deps/isabelle/README.md @@ -0,0 +1,13 @@ +## Debugging Isabelle prover + +Run the `tlapm` with the `--debug=tempfiles` option, e.g.: + + (cd ../tlaplus-examples/specifications/MisraReachability/ \ + && rm -rf .tlacache/ && tlapm --toolbox 228 228 --debug=tempfiles ReachabilityProofs.tla) + +Then look for the corresponding `*.thy` files and open them with Isabelle, e.g. + + ./_build/default/deps/isabelle/Isabelle/bin/isabelle jedit \ + -d ./_build/default/deps/isabelle/Isabelle/src/TLA+/ \ + ../tlaplus-examples/specifications/MisraReachability/.tlacache/ReachabilityProofs.tlaps/tlapm_624cb2.thy + diff --git a/isabelle/Functions.thy b/isabelle/Functions.thy index ca831784..6ad4cf88 100644 --- a/isabelle/Functions.thy +++ b/isabelle/Functions.thy @@ -196,7 +196,7 @@ proof - proof auto fix x assume "x \ S" - with hyp have "\y : P(x,y)" .. + with hyp have "\y : P(x,y)" by auto thus "P(x, CHOOSE y : P(x,y))" by (rule chooseI_ex) qed thus ?thesis .. diff --git a/isabelle/IntegerArithmetic.thy b/isabelle/IntegerArithmetic.thy index 07aaf7a6..6002a476 100644 --- a/isabelle/IntegerArithmetic.thy +++ b/isabelle/IntegerArithmetic.thy @@ -1076,7 +1076,8 @@ proof - next fix n assume "n \ Nat" "\m \ Nat : m \ n \ P(m)" - with step show "\m \ Nat : m \ succ[n] \ P(m)" by auto + with step show "\m \ Nat : m \ succ[n] \ P(m)" + by (auto simp del: nat_iff_int_geq0) qed thus ?thesis by auto qed @@ -1398,7 +1399,7 @@ proof (rule int_leq_lessE[OF ij i j]) thus ?thesis by auto next assume "i = j" - with i f show ?thesis by simp + with i f show ?thesis by auto qed lemma nat_less_mono_imp_leq_mono: @@ -1412,7 +1413,7 @@ proof (rule int_leq_lessE[OF ij]) thus ?thesis by auto next assume "i = j" - with i f show ?thesis by simp + with i f show ?thesis by (auto simp del: nat_iff_int_geq0) qed (auto simp: i[simplified] j[simplified]) lemma int_succ_lessI: @@ -2070,7 +2071,7 @@ next { assume eq: "i..j = k..l" and idx: "i \ k \ j \ l" from eq \i \ i..j\ intvlIsEmpty[OF k l] have "\(k > l)" - by blast + by auto with k l have "k \ k..l" "l \ k..l" by simp+ from idx have "FALSE" proof diff --git a/isabelle/Integers.thy b/isabelle/Integers.thy index bfbefc7f..c33f40d9 100644 --- a/isabelle/Integers.thy +++ b/isabelle/Integers.thy @@ -118,7 +118,7 @@ proof - next fix n assume n: "n \ S" - with Sc have "Sc[n] \ S" .. + with Sc have "Sc[n] \ S" by (rule bspec) moreover from n sub have "n \ N" by auto hence "Sc[n] = ?sc(n)" by (simp add: Sc_def) @@ -149,15 +149,14 @@ proof - show "FALSE" proof (cases "k \ N") case True - with e \k \ Z\ have "e \ k \ cp(k) = k \ {e}" by (simp add: cp_def) - with \cp(k) = k\ show ?thesis by blast + with e \k \ Z\ \cp(k) = k\ show ?thesis + by (auto simp: cp_def) next case False with \k \ I\ obtain n where "n \ N" "k = cp(n)" by (auto simp: I_def) with \k \ Z\ have "n \ Z" by (auto simp: cp_def) - with e \n \ N\ \k = cp(n)\ \k \ Z\ - have "k = n \ {e}" "cp(k) = k \ {e}" by (auto simp: cp_def) - with \cp(k) = k\ show ?thesis by auto + with e \n \ N\ \k = cp(n)\ \k \ Z\ \cp(k) = k\ show ?thesis + by (auto simp: cp_def) qed qed @@ -178,7 +177,7 @@ proof - case False with \k \ I\ obtain n where "n \ N" "k = cp(n)" by (auto simp: I_def) - with \cp(k) = Z\ cpN have "n = Z" by simp + with \cp(k) = Z\ cpN have "n = Z" by auto with \k = cp(n)\ show ?thesis by (simp add: cp_def) qed } @@ -210,8 +209,7 @@ proof - assume "l \ N" with \l \ I\ obtain n where "n \ N" "l = cp(n)" by (auto simp: I_def) - with cpk cpN eq have "n = k \ {e}" by simp - with \n \ N\ e show "FALSE" by blast + with cpk eq cpN \n \ N\ e show "FALSE" by force qed have "l \ Z" proof @@ -219,28 +217,51 @@ proof - with eq cpZ dom kl cpisZ show "FALSE" by auto qed with \l \ N\ e have "e \ l" "cp(l) = l \ {e}" by (auto simp: cp_def) - with cpk eq have "k \ l" "l \ k" by auto + with cpk eq have "k \ l" "l \ k" by force+ with kl show ?thesis by (auto dest: setEqual) next case False with dom obtain nk where nk: "nk \ N" "k = cp(nk)" by (auto simp: I_def) - with cpN eq have cpl: "cp(l) \ N" by simp + with cpN eq have cpl: "cp(l) \ N" by auto have "l \ N" proof assume "l \ N" - with cpl cpNN have "l = Z" by simp - with eq dom cpZ cpisZ False 1 show "FALSE" by simp + with cpl cpNN have "l = Z" by auto + with eq dom cpZ cpisZ False 1 show "FALSE" by auto qed with dom obtain nl where "nl \ N" "l = cp(nl)" by (auto simp: I_def) - with nk eq kl cpN show ?thesis by simp + with nk eq have "cp(cp(nk)) = cp(cp(nl))" by simp + moreover + from \nk \ N\ cpN have "cp(cp(nk)) = nk" by auto + moreover + from \nl \ N\ cpN have "cp(cp(nl)) = nl" by auto + ultimately have "k = l" + using \k = cp(nk)\ \l = cp(nl)\ by simp + with kl show ?thesis .. qed } hence 10: "\k,l \ I : ?cp[k] = ?cp[l] \ k = l" by auto - from cpI cpN have 11: "\k \ I : ?cp[?cp[k]] = k" - by (auto simp: I_def) + have 11: "\k \ I : ?cp[?cp[k]] = k" + proof + fix k + assume "k \ I" + with cpI have "?cp[?cp[k]] = cp(cp(k))" + by force + moreover have "cp(cp(k)) = k" + proof (cases "k \ N") + case True + with cpN show ?thesis by auto + next + case False + with \k \ I\ obtain nk where "nk \ N" "k = cp(nk)" + by (auto simp: I_def) + with cpN show ?thesis by auto + qed + ultimately show "?cp[?cp[k]] = k" by simp + qed from 1 2 3 4 5 6 7 8 9 10 11 have "ExtendedPeano(I,N,Z,Sc,?cp)" unfolding ExtendedPeano_def by blast @@ -261,10 +282,10 @@ definition Nat :: "c" where "Nat \ DOMAIN Succ" definition zero :: "c" ("0") where - "0 \ CHOOSE Z : \cp,I : ExtendedPeano(I,Nat,Z,Succ,cp)" + "zero \ CHOOSE Z : \cp,I : ExtendedPeano(I,Nat,Z,Succ,cp)" definition intCplt :: "c" where - "intCplt \ CHOOSE cp : \I : ExtendedPeano(I,Nat,0,Succ,cp)" + "intCplt \ CHOOSE cp : \I : ExtendedPeano(I,Nat,zero,Succ,cp)" definition Int :: "c" where "Int \ DOMAIN intCplt" @@ -277,6 +298,10 @@ lemmas setEqualI [where B = "Nat", intro!] setEqualI [where A = "Int", intro!] setEqualI [where B = "Int", intro!] + setEqualE [where A = "Nat", elim] + setEqualE [where B = "Nat", elim] + setEqualE [where A = "Int", elim] + setEqualE [where B = "Int", elim] lemma intExtendedPeano: "ExtendedPeano(Int,Nat,0,Succ,intCplt)" proof - @@ -369,8 +394,11 @@ proof - from z have "0 \ ?P" by simp moreover from sc have "\n \ ?P : Succ[n] \ ?P" by simp - ultimately have "Nat \ ?P" + moreover + have "\S \ SUBSET Nat : 0 \ S \ (\n \ S : Succ[n] \ S) \ Nat \ S" using intExtendedPeano by (simp add: ExtendedPeano_def) + ultimately have "Nat \ ?P" + by blast thus ?thesis by auto qed @@ -411,8 +439,14 @@ lemma uminusInjIff [simp]: by auto lemma uminusUminus [simp]: - "a \ Int \ --a = a" - using intExtendedPeano by (simp add: ExtendedPeano_def uminus_def) + assumes "a \ Int" + shows "--a = a" +proof - + from intExtendedPeano have "\k \ Int : intCplt[intCplt[k]] = k" + by (simp add: ExtendedPeano_def) + with assms show ?thesis + by (auto simp add: uminus_def) +qed lemma uminusSwap: assumes "a \ Int" and "b \ Int" @@ -727,7 +761,7 @@ next fix n assume n: "n \ Nat" "a = -Succ[n]" hence "a = succ[-succ[Succ[n]]]" by simp - with n show ?thesis by blast + with n show ?thesis by auto qed definition pred where @@ -856,7 +890,7 @@ next fix n assume "n \ Nat" thus "P(succ[m],n)" proof (cases) - case 0 with b1 m show ?thesis by auto + case 0 with b1 m show ?thesis by force next case succ with step ih m show ?thesis by auto qed @@ -975,6 +1009,8 @@ where "upto(n) \ lfp(Nat, \S. {n} \ { k \ Nat : succ[k lemmas setEqualI [where A = "upto(n)" for n, intro!] setEqualI [where B = "upto(n)" for n, intro!] + setEqualE [where A = "upto(n)" for n, elim] + setEqualE [where B = "upto(n)" for n, elim] lemma uptoNat: "upto(n) \ Nat" unfolding upto_def by (rule lfpSubsetDomain) @@ -1082,7 +1118,7 @@ lemma uptoLimit: proof - from m uptoNat have mNat: "m \ Nat" by blast from n have "\m\Nat: m \ upto(n) \ succ[m] \ upto(n) \ m=n" (is "?P(n)") - by (induct, auto simp: uptoZero uptoSucc) + by (induct, (force simp add: uptoZero uptoSucc)+) with mNat m suc show ?thesis by blast qed @@ -1188,12 +1224,12 @@ proof - assume kNat: "k \ Nat" and ih: "k \ upto(m) \ f[k] = g[k]" and sk: "succ[k] \ upto(m)" from sk kNat g have "g[succ[k]] = step(k, g[k])" - unfolding primrec_nat_upto_def by simp + unfolding primrec_nat_upto_def by auto moreover from sk m n have "succ[k] \ upto(n)" by (rule uptoTrans) with kNat f have "f[succ[k]] = step(k, f[k])" - unfolding primrec_nat_upto_def by simp + unfolding primrec_nat_upto_def by auto moreover from sk kNat mNat have "k \ upto(m)" by (rule uptoPred) @@ -1256,7 +1292,7 @@ proof - unfolding g_def by (simp+) moreover from F have "g[0] = base" - by (simp add: primrec_nat_upto_def g_def) + by (auto simp: primrec_nat_upto_def g_def) moreover have "\n \ Nat : g[succ[n]] = step(n, g[n])" proof @@ -1363,14 +1399,14 @@ proof - from sk kNat g have "g[succ[k]] = pstep(k, g[k], g[-k]) \ g[-succ[k]] = nstep(k, g[k], g[-k])" - unfolding primrec_int_upto_def by simp + unfolding primrec_int_upto_def by auto moreover from sk m n have "succ[k] \ upto(n)" by (rule uptoTrans) with kNat f have "f[succ[k]] = pstep(k, f[k], f[-k]) \ f[-succ[k]] = nstep(k, f[k], f[-k])" - unfolding primrec_int_upto_def by simp + unfolding primrec_int_upto_def by auto moreover from sk kNat mNat have "k \ upto(m)" by (rule uptoPred) @@ -1448,7 +1484,7 @@ proof - unfolding g_def by (simp+) moreover from F have "g[0] = base" - by (simp add: primrec_int_upto_def g_def) + by (auto simp: primrec_int_upto_def g_def) moreover have "\n \ Nat : g[succ[n]] = pstep(n, g[n], g[-n]) \ g[-succ[n]] = nstep(n, g[n], g[-n])" @@ -1490,7 +1526,7 @@ proof - and 5: "\n\Nat : f[-succ[n]] = nstep(n, f[n], f[-n])" by blast from 3 4 5 base pstep nstep have "\n\Int : f[n] \ S" - by (intro intInduct) auto + by (intro intInduct) force+ with 1 2 3 4 5 show ?thesis by blast qed diff --git a/isabelle/PredicateLogic.thy b/isabelle/PredicateLogic.thy index cd9411a9..6aaf351d 100644 --- a/isabelle/PredicateLogic.thy +++ b/isabelle/PredicateLogic.thy @@ -1428,15 +1428,18 @@ ML \ declaration \ fn _ => Induct.map_simpset (fn ss => ss addsimprocs - [Simplifier.make_simproc @{context} "swap_cases_false" - {lhss = [@{term "cases_false \ PROP P \ PROP Q"}], + [Simplifier.make_simproc @{context} + {name = "swap_cases_false", + lhss = [@{term "cases_false \ PROP P \ 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)}, - Simplifier.make_simproc @{context} "cases_equal_conj_curry" - {lhss = [@{term "cases_conj(P, Q) \ PROP R"}], + | _ => NONE), + identifier = []}, + Simplifier.make_simproc @{context} + {name = "cases_equal_conj_curry", + lhss = [@{term "cases_conj(P, Q) \ PROP R"}], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of _ $ (_ $ P) $ _ => @@ -1448,7 +1451,8 @@ declaration \ | is_conj @{const cases_false} = true | is_conj _ = false in if is_conj P then SOME @{thm cases_conj_curry} else NONE end - | _ => NONE)}] + | _ => NONE), + identifier = []}] |> Simplifier.set_mksimps (fn ctxt => Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> map (rewrite_rule ctxt (map Thm.symmetric @{thms cases_rulify_fallback})))) @@ -1787,7 +1791,7 @@ simproc_setup neq ("x = y") = \fn _ => eq $ lhs $ rhs => (case find_first (is_neq eq lhs rhs) (Simplifier.prems_of ss) of SOME thm => SOME ((thm RS symEqLeft_to_symEQLeft) - handle _ => thm RS neq_to_EQ_False) + handle THM _ => thm RS neq_to_EQ_False) | NONE => NONE) | _ => NONE); in proc end diff --git a/isabelle/ROOT b/isabelle/ROOT index c4124c97..fb0a8202 100644 --- a/isabelle/ROOT +++ b/isabelle/ROOT @@ -7,6 +7,7 @@ session "TLA+" = "Pure" + Constant (global) Zenon (global) (* NewSMT (global) *) + Tests (* Test cases only. *) document_files "root.tex" diff --git a/isabelle/SetTheory.thy b/isabelle/SetTheory.thy index bbb6fbe0..9bfb1ac8 100644 --- a/isabelle/SetTheory.thy +++ b/isabelle/SetTheory.thy @@ -48,6 +48,7 @@ text \ axioms of set theory, in order to make them more readable. \ + text \ Concrete syntax: set comprehension \ (*** @@ -372,34 +373,26 @@ lemma bAllI [intro!]: shows "\x\A : P(x)" using assms unfolding bAll_def by blast -lemma bspec [dest?]: +lemma bspec: assumes "\x\A : P(x)" and "x \ A" shows "P(x)" using assms unfolding bAll_def by blast -(*** currently inactive -- causes several obscure warnings about renamed - variables and seems to slow down large examples such as AtomicBakery ***) -ML \ - structure Simpdata = - struct - - open Simpdata; - - val mksimps_pairs = [(@{const_name bAll}, (@{thms bspec}, false))] @ mksimps_pairs; +text \The following rule intentionally has single assumption (non-conditional), +because otherwise it interferes with how \Nat\ is reduced to \Int\.\ +lemma bspec' [dest]: + assumes "\x\A : P(x)" + shows "\x : (x\A) \ P(x)" + using assms unfolding bAll_def by blast - end; - - open Simpdata; -\ +lemma bAll_unb [simp] : "\T P. (\e : e \ T \ P(e)) \ (\e \ T : P(e))" + using bAll_def by simp -declaration \ - fn _ => Simplifier.map_ss (fn ss => ss - |> Simplifier.set_mksimps (fn ctxt => - Simpdata.mksimps Simpdata.mksimps_pairs ctxt)) +setup \ + map_theory_claset (fn ctxt => + ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt')) \ -(***) - lemma bAllE [elim]: assumes "\x\A : P(x)" and "x \ A \ Q" and "P(x) \ Q" shows "Q" @@ -491,6 +484,28 @@ unfolding bChoose_def proof (rule choose_det) from assms show "x \ A \ P(x) \ x \ B \ Q(x)" by blast qed +(*** currently inactive -- causes several obscure warnings about renamed + variables and seems to slow down large examples such as AtomicBakery *** +ML \ + structure Simpdata = + struct + + open Simpdata; + + val mksimps_pairs = [(@{const_name bAll}, (@{thms bspec}, false))] @ mksimps_pairs; + + end; + + open Simpdata; +\ + +declaration \ + fn _ => Simplifier.map_ss (fn ss => ss + |> Simplifier.set_mksimps (fn ctxt => + Simpdata.mksimps Simpdata.mksimps_pairs ctxt)) +\ +***) + (*** TYPE CHECKING CURRENTLY NOT INSTALLED @@ -689,17 +704,37 @@ lemma setEqualD1: "A = B \ A \ B" lemma setEqualD2: "A = B \ B \ A" by blast -text \ - We declare the elimination rule for set equations as an unsafe - rule to use with the classical reasoner, so it will be tried if - the more obvious uses of equality fail. -\ -lemma setEqualE [elim]: +lemma setEqualE: assumes "A = B" and "\ c \ A; c \ B \ \ P" and "\ c \ A; c \ B \ \ P" shows "P" using assms by (blast dest: setEqualD1 setEqualD2) +text \ + Again, we add instances of this theorem for obvious set constructors. +\ +lemmas + setEqualE [where A = "{}", elim] + setEqualE [where B = "{}", elim] + setEqualE [where A = "addElt(a,C)" for a C, elim] + setEqualE [where B = "addElt(a,C)" for a C, elim] + setEqualE [where A = "SUBSET C" for C, elim] + setEqualE [where B = "SUBSET C" for C, elim] + setEqualE [where A = "UNION C" for C, elim] + setEqualE [where B = "UNION C" for C, elim] + setEqualE [where A = "INTER C" for C, elim] + setEqualE [where B = "INTER C" for C, elim] + setEqualE [where A = "C \ D" for C D, elim] + setEqualE [where B = "C \ D" for C D, elim] + setEqualE [where A = "C \ D" for C D, elim] + setEqualE [where B = "C \ D" for C D, elim] + setEqualE [where A = "C \ D" for C D, elim] + setEqualE [where B = "C \ D" for C D, elim] + setEqualE [where A = "subsetOf(S,P)" for S P, elim] + setEqualE [where B = "subsetOf(S,P)" for S P, elim] + setEqualE [where A = "setOfAll(S,e)" for S e, elim] + setEqualE [where B = "setOfAll(S,e)" for S e, elim] + lemma setEqual_iff: "(A = B) = (\x : x \ A \ x \ B)" by (blast intro: setEqualI) @@ -1102,7 +1137,8 @@ lemma inAsym: shows "P" proof (rule contradiction) assume "\P" - with foundation[where A="{a,b}"] hyps show "FALSE" by blast + with foundation[where A="{a,b}"] hyps + show "FALSE" by blast qed lemma inIrrefl: @@ -1422,7 +1458,7 @@ lemma isEmptySimps [simp]: "({} = addElt(a,S)) = FALSE" "(SUBSET S = {}) = FALSE" "({} = SUBSET S) = FALSE" -by (blast+) +by blast+ subsection \ Generalized union: inclusions and equalities \ diff --git a/isabelle/Tests.thy b/isabelle/Tests.thy new file mode 100644 index 00000000..7ebe8ba3 --- /dev/null +++ b/isabelle/Tests.thy @@ -0,0 +1,51 @@ +theory Tests + imports Constant +begin +text \ +This theory only acts as a test suite to check for regressions. +The test cases should be proved by \auto\, because that's the +default method used by TLAPM. +\ + + +section \Interference of \Nat\ and \\\ elimination.\ + +text \After upgrading theories from Isabelle-2011 to Isabelle-202X +an interference of \x \ Nat \ x \ Int \ 0 \ x\ and \\\ elimination +was introduced. The former rule rewrites assumptions and then the +\bAllE\ elimination rule don't apply anymore.\ + +lemma + fixes P + assumes "\e : e \ Nat \ P(e)" + shows "\e. e \ Nat \ P(e)" + using assms + by auto + + +text \This lemma was passing with "blast" and failing with auto +until "lemma bspec' [dest]" was added. It was working with "auto" +in Isabelle-2011, so can be considered a regression.\ +lemma + fixes P Q e + assumes "e \ Nat" and "P(e)" and "\e \ Nat : (P(e) \ Q(e))" + shows "Q(e)" + using assms + by auto + + + +text \Only started to work after \bAll_unb [simp]\ was added.\ +lemma + assumes "RR (0)" + assumes "\ i :: c. i \ Nat \ RR(i) \ RR(F(i))" + assumes "\ PP :: c => c. + PP (0) \ + (\n\Nat : PP(n) \ PP(F(n))) \ + (\n\Nat : PP(n))" + shows "\ ii \ Nat : RR (ii)" + using assms + by auto + + +end diff --git a/isabelle/Tuples.thy b/isabelle/Tuples.thy index 5aa1bd04..1030ff1f 100644 --- a/isabelle/Tuples.thy +++ b/isabelle/Tuples.thy @@ -72,7 +72,13 @@ lemma isASeqE [elim]: assumes s: "isASeq(s)" and p: "\isAFcn(s); DOMAIN s = 1 .. Len(s); Len(s) \ Nat\ \ P" shows "P" - using assms unfolding isASeq_def by (blast dest: LenI) +proof - + from s obtain n where "isAFcn(s)" "n \ Nat" "DOMAIN s = 1 .. n" + unfolding isASeq_def by blast + with LenI have "isAFcn(s) \ DOMAIN s = 1 .. Len(s) \ Len(s) \ Nat" + by simp + thus ?thesis by (blast intro: p) +qed \ \The corresponding lemma for @{text "Seq(S)"} will be proved later.\ lemma SeqIsAFcn (*[elim!]*): @@ -156,7 +162,7 @@ lemma seqElt [elim]: lemma seqInSeqRange: assumes "isASeq(s)" shows "s \ Seq(Range(s))" - using assms by auto + using assms by force lemma isASeqInSeq: "isASeq(s) = (\S: s \ Seq(S))" by (auto elim: seqInSeqRange) @@ -273,8 +279,12 @@ lemmas appendElt1' [simp] = SeqIsASeq[THEN appendElt1] lemma appendElt2 [simp]: assumes "isASeq(s)" shows "Append(s,e)[succ[Len(s)]] = e" - using assms unfolding Append_def by force - +proof - + from assms have "succ[Len(s)] \ DOMAIN Append(s,e)" + by (auto simp: Append_def) + thus ?thesis by (auto simp: Append_def) +qed + lemmas appendElt2' [simp] = SeqIsASeq[THEN appendElt2] lemma isAppend [intro]: @@ -309,7 +319,7 @@ proof - fix k assume k: "k \ 1 .. Len(t)" with s ls have "s[k] = ?s1[k]" by (intro sym[OF appendElt1]) auto - also from k elt t have "\ = ?t1[k]" by auto + also from k elt t have "\ = ?t1[k]" by force also from t k have "... = t[k]" by (intro appendElt1) auto finally show "s[k] = t[k]" . qed @@ -413,10 +423,10 @@ proof - qed from sn n have 2: "so \ [1 .. n \ S]" unfolding so_def by force - with ih have 3: "P(so)" .. + with ih have 3: "P(so)" by blast from 2 n have 4: "so \ Seq(S)" unfolding Seq_def by auto - from sn n have "lst \ S" by (auto simp: lst_def) + from sn n have "lst \ S" by (force simp: lst_def) with 1 3 4 show "P(sn)" by (auto intro: step) qed qed @@ -690,11 +700,26 @@ lemma inProductLen: using assms unfolding Product_def by auto lemma inProductE [elim!]: - assumes "p \ Product(s)" and "isASeq(s)" - and "\isASeq(p); Len(p) = Len(s); p \ [1 .. Len(s) \ UNION Range(s)]; + assumes p: "p \ Product(s)" and s: "isASeq(s)" + and P: "\isASeq(p); Len(p) = Len(s); p \ [1 .. Len(s) \ UNION Range(s)]; \k \ 1 .. Len(s) : p[k] \ s[k] \ \ P" shows "P" - using assms unfolding Product_def by auto +proof - + from \p \ Product(s)\ have + 1: "p \ [1 .. Len(s) \ UNION {s[i] : i \ 1 .. Len(s)}]" and + 2: "\i \ 1 .. Len(s) : p[i] \ s[i]" + by (auto simp: Product_def) + from p s have "isASeq(p)" by (rule inProductIsASeq) + moreover + from p s have "Len(p) = Len(s)" by (rule inProductLen) + moreover + from s have "Range(s) = {s[i] : i \ 1 .. Len(s)}" + by auto + with 1 have "p \ [1 .. Len(s) \ UNION Range(s)]" + by simp + ultimately show ?thesis + using 2 by (rule P) +qed (*** examples *** lemma "Product(\\) = { \\ }" by auto @@ -1136,7 +1161,7 @@ lemma transitive_converse [simp]: lemma symmetric_iff_converse_eq: assumes r: "r \ A \ B" shows "symmetric(r) = (r^-1 = r)" - using assms by (auto simp: symmetric_def) + using assms by (auto simp: symmetric_def dest: converseI) subsubsection \ Identity relation over a set \ diff --git a/isabelle/Zenon.thy b/isabelle/Zenon.thy index 91cf9114..ebd642a7 100644 --- a/isabelle/Zenon.thy +++ b/isabelle/Zenon.thy @@ -19,7 +19,7 @@ proof thus "\ x \ S : P(x)" .. next assume "\ x \ S : P(x)" - thus "(\x. (x \ S \ P(x)))" .. + thus "(\x. (x \ S \ P(x)))" by blast qed lemma atomize_object_bAll [atomize]: @@ -2108,11 +2108,15 @@ next Append (zenon_seqify (es), e)[succ[Len(zenon_seqify(cs))]]) = CaseArm (c, e)" using h3 zenon_seqifyIsASeq by auto - with h5 + with h5 + have "x \\in CaseArm (Append (zenon_seqify (cs), c)[succ[Len(zenon_seqify(cs))]], + Append (zenon_seqify (es), e)[succ[Len(zenon_seqify(cs))]])" + by simp + with \succ[Len(zenon_seqify(cs))] \ DOMAIN Append (zenon_seqify (cs), c)\ have h6: "x \\in UNION {CaseArm (Append (zenon_seqify (cs), c)[i], Append (zenon_seqify (es), e)[i]) : i \\in DOMAIN Append (zenon_seqify (cs), c)}" - by blast + by blast show "?g" using h4 h6 by auto next @@ -2207,8 +2211,10 @@ proof (rule boolEqual, rule iffI) using h7 zenon_seqifyIsASeq by auto have h9: "zenon_seqify (cs) [i] = Append (zenon_seqify (cs), c)[i]" using zenon_case_append1 zenon_seqifyIsASeq h7 by auto - show "~ zenon_seqify(cs)[i]" - using h9 h8 h6 by auto + from h8 h6 have "~ Append(zenon_seqify(cs), c)[i]" + by blast + with h9 show "~ zenon_seqify(cs)[i]" + by simp qed next assume h6: "?f2" diff --git a/src/backend/isabelle.ml b/src/backend/isabelle.ml index 286d2a1d..6daefc2f 100644 --- a/src/backend/isabelle.ml +++ b/src/backend/isabelle.ml @@ -167,9 +167,8 @@ let rec pp_apply sd cx ff op args = match op.core with | B.Nat, [] -> atomic "Nat" | B.Int, [] -> atomic "Int" | B.Real, [] -> atomic (cook "Real") - | B.Plus, [e ; f] -> nonfix "arith_add" [e ; f] - | B.Minus, [e ; f] -> - nonfix "arith_add" [e ; Apply (Internal B.Uminus @@ f, [f]) @@ f] + | B.Plus, [e ; f] -> nonfix "addint" [e ; f] + | B.Minus, [e ; f] -> nonfix "subint" [e ; f] | B.Uminus, [e] -> nonfix "minus" [e] | B.Times, [e ; f] -> nonfix "mult" [e ; f] | B.Ratio, [e ; f] -> nonfix (cook "/") [e ; f] diff --git a/src/backend/prep.ml b/src/backend/prep.ml index c91a4f1e..097977c2 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -1193,7 +1193,7 @@ let compute_meth def args usept = Method.Zenon tmo | Some "isabelle" -> let tmo = Option.default Method.default_isabelle_timeout !timeout in - let tac = Option.default "auto" !tactic in + let tac = Option.default Method.default_isabelle_tactic !tactic in Method.Isabelle (tmo, tac) | Some "yices" -> let tmo = Option.default Method.default_yices_timeout !timeout in