| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Sequents/LK/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 2 kB |
|
Quelle Nat.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Sequents/LK/Nat.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge *) section ‹ Nat "../LK" nat nat :: "term" .. Zero :: nat (‹0›) and Suc :: "nat ==> nat" and rec :: "[nat, 'a, [nat,'a] ==> 'a] ==> 'a" induct: "[$H ⊨ $E, P(0), $F; ∧x. $H, P(x) ⊨ $E, P(Suc(x)), $F] ==> $H ⊨ $E, P(n), $F" and Suc_inject: "⊨ Suc(m) = Suc(n) ⟶ m = n" and Suc_neq_0: "⊨ Suc(m) ≠ 0" and rec_0: "⊨ rec(0,a,f) = a" and rec_Suc: "⊨ rec(Suc(m), a, f) = f(m, rec(m,a,f))" add :: "[nat, nat] ==> nat" (infixl ‹+› 60) where "m + n == rec(m, n, λx y. Suc(y))" Suc_neq_0 [simp] Suc_inject_rule: "$H, $G, m = n ⊨ $E ==> $H, Suc(m) = Suc(n), $G ⊨ $E" by (rule L_of_imp [OF Suc_inject]) Suc_n_not_n: "⊨ Suc(k) ≠ k" apply (rule_tac n = k in induct) apply simp apply (fast add!: Suc_inject_rule) done add_0: "⊨ 0 + n = n" apply (unfold add_def) apply (rule rec_0) done add_Suc: "⊨ Suc(m) + n = Suc(m + n)" apply (unfold add_def) apply (rule rec_Suc) done add_0 [simp] add_Suc [simp] add_assoc: "⊨ (k + m) + n = k + (m + n)" apply (rule_tac n = "k" in induct) apply simp_all done add_0_right: "⊨ m + 0 = m" apply (rule_tac n = "m" in induct) apply simp_all done add_Suc_right: "⊨ m + Suc(n) = Suc(m + n)" apply (rule_tac n = "m" in induct) apply simp_all done "(∧n. ⊨ f(Suc(n)) = Suc(f(n))) ==> ⊨ f(i + j) = i + f(j)" apply (rule_tac n = "i" in induct) apply simp_all done
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09