Logik - Listen-Induktion

Mit folgender CASL-Spezifikation von natürlichen Zahlen und Listen, beweise die beiden Beweisziele am Ende per Induktion. Note: 1

sort Nat op 0 : Nat op suc : Nat -> Nat op __+__ : Nat * Nat -> Nat generated type Nat ::= 0 | suc(Nat) %% induction axiom forall X1 : Nat; Y1 : Nat . suc(X1) = suc(Y1) => X1 = Y1 %(ga_injective_suc)% forall Y1 : Nat . not 0 = suc(Y1) %(ga_disjoint_0_suc)% forall m : Nat . 0 + m = m %(add_0_Nat)% forall m, n : Nat . suc(n) + m = suc(n + m) %(add_suc_Nat)% forall m : Nat . m + 0 = m %(add_0_Nat_right)% forall m, n, k : Nat . m + (n + k) = (m + n) + k %(add_assoc_Nat)% forall m, n : Nat . m + suc(n) = suc(m + n) %(add_suc_Nat_1)% forall m, n : Nat . m + n = n + m %(add_comm_Nat)% sort List op [] : List op cons : Nat * List -> List op __++__ : List * List -> List op length : List -> Nat generated type List ::= [] | cons(Nat; List) %% induction axiom forall X1 : Nat; X2 : List; Y1 : Nat; Y2 : List . cons(X1, X2) = cons(Y1, Y2) => X1 = Y1 /\ X2 = Y2 %(ga_injective_cons)% forall Y1 : Nat; Y2 : List . not [] = cons(Y1, Y2) %(ga_disjoint_[]_cons)% forall L : List . [] ++ L = L forall e : Nat; L1, L2 : List . cons(e, L1) ++ L2 = cons(e, L1 ++ L2) . length([]) = 0 forall e : Nat; L : List . length(cons(e, L)) = suc(length(L)) %% to prove forall L1, L2, L3 : List . L1 ++ (L2 ++ L3) = (L1 ++ L2) ++ L3 %implied forall L1, L2 : List . length(L1 ++ L2) = length(L1) + length(L2) %implied

Autor: Dr. Till Mossakowski

AG BKB

Zuletzt geändert am: 14. Januar 2008