|
1 | 1 | (* Title: TLA+/PredicateLogic.thy |
2 | 2 | Author: Stephan Merz, Inria Nancy |
3 | | - Copyright (C) 2008-2024 INRIA and Microsoft Corporation |
| 3 | + Copyright (C) 2008-2025 INRIA and Microsoft Corporation |
4 | 4 | License: BSD |
5 | | - Version: Isabelle2024 |
| 5 | + Version: Isabelle2025 |
6 | 6 | *) |
7 | 7 |
|
8 | 8 | section \<open>First-Order Logic for TLA+\<close> |
@@ -1355,8 +1355,6 @@ text \<open> |
1355 | 1355 | development of FOL, we introduce a set of ``shadow connectives'' |
1356 | 1356 | that will only be used for this purpose. |
1357 | 1357 | \<close> |
1358 | | - |
1359 | | -(* lemmas cases = case_split [case_names True False] *) |
1360 | 1358 | context |
1361 | 1359 | begin |
1362 | 1360 |
|
@@ -1425,37 +1423,33 @@ ML \<open> |
1425 | 1423 | ) |
1426 | 1424 | \<close> |
1427 | 1425 |
|
| 1426 | +simproc_setup passive swap_cases_false ("cases_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q") = |
| 1427 | + \<open>fn _ => fn _ => fn ct => |
| 1428 | + (case Thm.term_of ct of |
| 1429 | + _ $ (P as _ $ \<^Const_>\<open>cases_false\<close>) $ (_ $ Q $ _) => |
| 1430 | + if P <> Q then SOME Drule.swap_prems_eq else NONE |
| 1431 | + | _ => NONE)\<close> |
| 1432 | + |
| 1433 | +simproc_setup passive cases_equal_conj_curry ("cases_conj(P, Q) \<Longrightarrow> PROP R") = |
| 1434 | + \<open>fn _ => fn _ => fn ct => |
| 1435 | + (case Thm.term_of ct of |
| 1436 | + _ $ (_ $ P) $ _ => |
| 1437 | + let |
| 1438 | + fun is_conj \<^Const_>\<open>cases_conj for P Q\<close> = is_conj P andalso is_conj Q |
| 1439 | + | is_conj \<^Const_>\<open>cases_equal\<close> = true |
| 1440 | + | is_conj \<^Const_>\<open>cases_true\<close> = true |
| 1441 | + | is_conj \<^Const_>\<open>cases_false\<close> = true |
| 1442 | + | is_conj _ = false |
| 1443 | + in if is_conj P then SOME @{thm cases_conj_curry} else NONE end |
| 1444 | + | _ => NONE)\<close> |
| 1445 | + |
1428 | 1446 | declaration \<open> |
1429 | | - fn _ => Induct.map_simpset (fn ss => ss |
1430 | | - addsimprocs |
1431 | | - [Simplifier.make_simproc @{context} |
1432 | | - {name = "swap_cases_false", |
1433 | | - lhss = [@{term "cases_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"}], |
1434 | | - proc = fn _ => fn _ => fn ct => |
1435 | | - (case Thm.term_of ct of |
1436 | | - _ $ (P as _ $ @{const cases_false}) $ (_ $ Q $ _) => |
1437 | | - if P <> Q then SOME Drule.swap_prems_eq else NONE |
1438 | | - | _ => NONE), |
1439 | | - identifier = []}, |
1440 | | - Simplifier.make_simproc @{context} |
1441 | | - {name = "cases_equal_conj_curry", |
1442 | | - lhss = [@{term "cases_conj(P, Q) \<Longrightarrow> PROP R"}], |
1443 | | - proc = fn _ => fn _ => fn ct => |
1444 | | - (case Thm.term_of ct of |
1445 | | - _ $ (_ $ P) $ _ => |
1446 | | - let |
1447 | | - fun is_conj (@{const cases_conj} $ P $ Q) = |
1448 | | - is_conj P andalso is_conj Q |
1449 | | - | is_conj (Const (@{const_name cases_equal}, _) $ _ $ _) = true |
1450 | | - | is_conj @{const cases_true} = true |
1451 | | - | is_conj @{const cases_false} = true |
1452 | | - | is_conj _ = false |
1453 | | - in if is_conj P then SOME @{thm cases_conj_curry} else NONE end |
1454 | | - | _ => NONE), |
1455 | | - identifier = []}] |
1456 | | - |> Simplifier.set_mksimps (fn ctxt => |
| 1447 | + K (Induct.map_simpset |
| 1448 | + (Simplifier.add_proc \<^simproc>\<open>swap_cases_false\<close> #> |
| 1449 | + Simplifier.add_proc \<^simproc>\<open>cases_equal_conj_curry\<close> #> |
| 1450 | + Simplifier.set_mksimps (fn ctxt => |
1457 | 1451 | Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> |
1458 | | - map (rewrite_rule ctxt (map Thm.symmetric @{thms cases_rulify_fallback})))) |
| 1452 | + map (rewrite_rule ctxt (map Thm.symmetric @{thms cases_rulify_fallback}))))) |
1459 | 1453 | \<close> |
1460 | 1454 |
|
1461 | 1455 | text \<open> Pre-simplification of induction and cases rules \<close> |
@@ -1523,7 +1517,8 @@ subsection \<open> Propositional simplification \<close> |
1523 | 1517 | subsubsection \<open> Conversion to Boolean values \<close> |
1524 | 1518 |
|
1525 | 1519 | text \<open> |
1526 | | - Because \tlaplus{} is untyped, equivalence is different from equality, |
| 1520 | + Because \tlaplus{} does not distinguish between terms and formulas, |
| 1521 | + equivalence is different from equality, |
1527 | 1522 | and one has to be careful about stating the laws of propositional |
1528 | 1523 | logic. For example, although the equivalence @{text "(TRUE \<and> A) \<Leftrightarrow> A"} |
1529 | 1524 | is valid, we cannot state the law @{text "(TRUE \<and> A) = A"} |
@@ -1945,7 +1940,6 @@ struct |
1945 | 1940 | ( |
1946 | 1941 | type T = ((term -> bool) * stamp) list; |
1947 | 1942 | val empty = []; |
1948 | | - val extend = I; |
1949 | 1943 | fun merge data : T = Library.merge (eq_snd (op =)) data; |
1950 | 1944 | ); |
1951 | 1945 | fun add m = Data.map (cons (m, stamp ())); |
|
0 commit comments