(* CS567, MP 0 Solutions *)
(*
I thought for this mp, I would amalgamate all the answers given by each of you.
*)
theory mp0_sol
imports Main
begin
lemma "(a \ b) = (b \ a)"
by auto
lemma "((a \ b) \ a) \ b"
by auto
lemma "((a \ b) \ \ b) \ \ a"
by auto
lemma sample1: "(2::nat)+2=4"
by auto
lemma sample2: "f=g \ (\ x. f x = g x)"
by auto
lemma sample3: "f x = u \ (\ x. P x \ g (f x) = x) \ P x \ x = g u"
by auto
lemma "(\(a \ b)) = ((\b) \ (\a))"
by auto
lemma "(\(a \ b)) = ((\a) \ (\b))"
by auto
lemma "a \ b \ ((a \ b) = a)"
by auto
lemma "(P x y \ (y = z)) \ P x z"
by auto
lemma "(x = y) \ (y = z) \ x = z"
by auto
lemma "(b :: nat) * (a div b) + (a mod b) = a"
by auto
lemma "\ x. P(x) \ \ x. P(x)"
by auto
(* consensus theorem *)
lemma "((x \ y) \ (~ x \ z) \ (y \ z)) = ((x \ y) \ (~ x \ z))"
by auto
(* triangle inequality *)
lemma "\ x. \ y. abs((x::int) + y) <= (abs(x) + abs(y))"
by auto
lemma " a=a"
apply (auto)
done
lemma "a=b\b=a"
apply (auto)
done
lemma " (a=b) & (b=c)\a=c"
apply (auto)
done
lemma "\x. x = x" by auto
lemma "\y. P y \ (\y. P y)" by auto
lemma "\x::nat. x > y" by auto
lemma "((a \ b) \ c) = ((a \ c) \ (b \ c))"
apply (auto)
done
lemma "((a \ b) \ \ a) \ b"
apply (auto)
done
lemma "(a \ (b \ c)) = ((a \ b) \ c)"
apply (auto)
done
lemma "a \ \a"
by auto
lemma "(a \ \(b \ c)) = (a \ \b \ \c)"
by auto
lemma "(\a. a) \ a"
by auto
lemma "\a. (a \ a)"
by auto
lemma "((a \ b) \ c) = ((a \ c) \ (b \ c))"
apply(auto)
done
lemma "((a \ b) \ c) = (a \ (b \ c))"
apply(auto)
done
lemma "((a \ b) \ c) = (a \ (b \ c))"
apply(auto)
done
end