(* Generated by gen-metatheory *)
theory cl
imports Pure
begin
typedecl bool
judgment
Trueprop :: "bool \ prop" ("(_)" 5)
axiomatization
implies :: "[bool, bool] \ bool" (infixr "-->" 25) and
conj :: "[bool, bool] \ bool" (infixr "&" 35) and
disj :: "[bool, bool] \ bool" (infixr "|" 30) and
Not :: "bool \ bool" ("~ _" [40] 40)
where
A1: "A --> (B --> A)" and
A2: "(A --> (B --> C)) --> ((A --> B) --> (A --> C))" and
A3: "A & B --> A" and
A4: "A & B --> B" and
A5: "A --> (B --> A & B)" and
A6: "A --> A | B" and
A7: "B --> A | B" and
A8: "(A --> C) --> ((B --> C) --> (A | B --> C))" and
A9: "(A --> B) --> ((A --> ~ B) --> ~ A)" and
A10: "~ ~ A --> A" and
MP: "\A --> B; A\ \ B"
theorem exam2_5:
shows "P | Q --> Q | P"
proof -
have s1: "P --> Q | P" by (rule A7)
have s2: "Q --> Q | P" by (rule A6)
have s3: "(P --> Q | P) --> ((Q --> Q | P) --> (P | Q --> Q | P))" by (rule A8)
have s4: "(Q --> Q | P) --> (P | Q --> Q | P)" using s3 and s1 by (rule MP)
have s5: "P | Q --> Q | P" using s4 and s2 by (rule MP)
thus ?thesis .
qed
theorem exam2_6:
shows "A --> A"
proof -
have s1: "(A --> ((A --> A) --> A)) --> ((A --> (A --> A)) --> (A --> A))" by (rule A2)
have s2: "A --> ((A --> A) --> A)" by (rule A1)
have s3: "(A --> (A --> A)) --> (A --> A)" using s1 and s2 by (rule MP)
have s4: "A --> (A --> A)" by (rule A1)
have s5: "A --> A" using s3 and s4 by (rule MP)
thus ?thesis .
qed
theorem exam2_11:
assumes h1: "P & Q"
shows "Q & P"
proof -
have s1: "P & Q --> P" by (rule A3)
have s2: "P" using s1 and h1 by (rule MP)
have s3: "P & Q --> Q" by (rule A4)
have s4: "Q" using s3 and h1 by (rule MP)
have s5: "Q --> (P --> Q & P)" by (rule A5)
have s6: "P --> Q & P" using s5 and s4 by (rule MP)
have s7: "Q & P" using s6 and s2 by (rule MP)
thus ?thesis .
qed
theorem for_exam2_19:
assumes h1: "A"
assumes h2: "A --> B"
assumes h3: "B --> C"
shows "C"
proof -
have s1: "B" using h2 and h1 by (rule MP)
have s2: "C" using h3 and s1 by (rule MP)
thus ?thesis .
qed
theorem for_exam2_20:
assumes not_b: "~ B"
assumes a_impl_b: "A --> B"
shows "~ A"
proof -
have s1: "(A --> B) --> ((A --> ~ B) --> ~ A)" by (rule A9)
have s2: "(A --> ~ B) --> ~ A" using s1 and a_impl_b by (rule MP)
have s3: "~ B --> (A --> ~ B)" by (rule A1)
have s4: "A --> ~ B" using s3 and not_b by (rule MP)
have s5: "~ A" using s2 and s4 by (rule MP)
thus ?thesis .
qed
theorem exam2_21:
assumes a: "A"
assumes not_a: "~ A"
shows "B"
proof -
have s1: "A --> (~ B --> A)" by (rule A1)
have s2: "~ A --> (~ B --> ~ A)" by (rule A1)
have s3: "~ B --> A" using s1 and a by (rule MP)
have s4: "~ B --> ~ A" using s2 and not_a by (rule MP)
have s5: "(~ B --> A) --> ((~ B --> ~ A) --> ~ ~ B)" by (rule A9)
have s6: "(~ B --> ~ A) --> ~ ~ B" using s5 and s3 by (rule MP)
have s7: "~ ~ B" using s6 and s4 by (rule MP)
have s8: "~ ~ B --> B" by (rule A10)
have s9: "B" using s8 and s7 by (rule MP)
thus ?thesis .
qed
theorem a_and_b_infers_a:
assumes h1: "A & B"
shows "A"
proof -
have s1: "A & B --> A" by (rule A3)
have s2: "A" using s1 and h1 by (rule MP)
thus ?thesis .
qed
theorem a_and_b_infers_b:
assumes h1: "A & B"
shows "B"
proof -
have s1: "A & B --> B" by (rule A4)
have s2: "B" using s1 and h1 by (rule MP)
thus ?thesis .
qed
theorem a_impl_false_infers_not_a:
assumes h1: "A --> B & ~ B"
shows "~ A"
proof -
have s1: "B & ~ B --> B" by (rule A3)
have s2: "B & ~ B --> ~ B" by (rule A4)
have s3: "(B & ~ B --> B) --> A --> (B & ~ B --> B)" by (rule A1)
have s4: "(B & ~ B --> ~ B) --> A --> (B & ~ B --> ~ B)" by (rule A1)
have s5: "A --> (B & ~ B --> B)" using s3 and s1 by (rule MP)
have s6: "A --> (B & ~ B --> ~ B)" using s4 and s2 by (rule MP)
have s7: "(A --> (B & ~ B --> B)) --> (A --> B & ~ B) --> (A --> B)" by (rule A2)
have s8: "(A --> (B & ~ B --> ~ B)) --> (A --> B & ~ B) --> (A --> ~ B)" by (rule A2)
have s9: "(A --> B & ~ B) --> (A --> B)" using s7 and s5 by (rule MP)
have s10: "(A --> B & ~ B) --> (A --> ~ B)" using s8 and s6 by (rule MP)
have s11: "A --> B" using s9 and h1 by (rule MP)
have s12: "A --> ~ B" using s10 and h1 by (rule MP)
have s13: "(A --> B) --> (A --> ~ B) --> ~ A" by (rule A9)
have s14: "(A --> ~ B) --> ~ A" using s13 and s11 by (rule MP)
have s15: "~ A" using s14 and s12 by (rule MP)
thus ?thesis .
qed
theorem a_b_infers_a_and_b:
assumes a: "A"
assumes b: "B"
shows "A & B"
proof -
have s1: "A --> B --> A & B" by (rule A5)
have s2: "B --> A & B" using s1 and a by (rule MP)
have s3: "A & B" using s2 and b by (rule MP)
thus ?thesis .
qed
theorem a_or_b_a_impl_c_b_impl_c_infers_c:
assumes ab: "A | B"
assumes a: "A --> C"
assumes b: "B --> C"
shows "C"
proof -
have s1: "(A --> C) --> (B --> C) --> (A | B --> C)" by (rule A8)
have s2: "(B --> C) --> (A | B --> C)" using s1 and a by (rule MP)
have s3: "A | B --> C" using s2 and b by (rule MP)
have s4: "C" using s3 and ab by (rule MP)
thus ?thesis .
qed
theorem a_infers_a_or_b:
assumes h1: "A"
shows "A | B"
proof -
have s1: "A --> A | B" by (rule A6)
have s2: "A | B" using s1 and h1 by (rule MP)
thus ?thesis .
qed
theorem b_infers_a_or_b:
assumes h1: "B"
shows "A | B"
proof -
have s1: "B --> A | B" by (rule A7)
have s2: "A | B" using s1 and h1 by (rule MP)
thus ?thesis .
qed
theorem mp:
assumes ab: "A --> B"
assumes a: "A"
shows "B"
proof -
have s1: "B" using ab and a by (rule MP)
thus ?thesis .
qed
theorem a_infers_b_impl_a:
assumes h1: "A"
shows "B --> A"
proof -
have s1: "A --> (B --> A)" by (rule A1)
have s2: "B --> A" using s1 and h1 by (rule MP)
thus ?thesis .
qed
theorem not_not_a_infers_a:
assumes h1: "~ ~ A"
shows "A"
proof -
have s1: "~ ~ A --> A" by (rule A10)
have s2: "A" using s1 and h1 by (rule MP)
thus ?thesis .
qed
end