Quelle Nat.thy

Sprache: 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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.