(* Generated by gen-metatheory *)
theory metacl
imports Datatype List Set
begin
typedecl bool_var
datatype cl_bool =
bool_var bool_var
(* implies :: "[bool, bool] \ bool" (infixr "-->" 25) *)
| cl_implies cl_bool cl_bool
(* conj :: "[bool, bool] \ bool" (infixr "&" 35) *)
| cl_conj cl_bool cl_bool
(* disj :: "[bool, bool] \ bool" (infixr "|" 30) *)
| cl_disj cl_bool cl_bool
(* Not :: "bool \ bool" ("~ _" [40] 40) *)
| cl_Not cl_bool
definition
by_rule :: "[cl_bool list, cl_bool] \ bool"
where
"by_rule p c \
(* A1: A --> (B --> A) *)
(\ A B . p = [] \ c = (cl_implies A (cl_implies B A ) )) \
(* A2: (A --> (B --> C)) --> ((A --> B) --> (A --> C)) *)
(\ A B C . p = [] \ c = (cl_implies (cl_implies A (cl_implies B C ) ) (cl_implies (cl_implies A B ) (cl_implies A C ) ) )) \
(* A3: A & B --> A *)
(\ A B . p = [] \ c = (cl_implies (cl_conj A B ) A )) \
(* A4: A & B --> B *)
(\ A B . p = [] \ c = (cl_implies (cl_conj A B ) B )) \
(* A5: A --> (B --> A & B) *)
(\ A B . p = [] \ c = (cl_implies A (cl_implies B (cl_conj A B ) ) )) \
(* A6: A --> A | B *)
(\ A B . p = [] \ c = (cl_implies A (cl_disj A B ) )) \
(* A7: B --> A | B *)
(\ A B . p = [] \ c = (cl_implies B (cl_disj A B ) )) \
(* A8: (A --> C) --> ((B --> C) --> (A | B --> C)) *)
(\ A B C . p = [] \ c = (cl_implies (cl_implies A C ) (cl_implies (cl_implies B C ) (cl_implies (cl_disj A B ) C ) ) )) \
(* A9: (A --> B) --> ((A --> ~ B) --> ~ A) *)
(\ A B . p = [] \ c = (cl_implies (cl_implies A B ) (cl_implies (cl_implies A (cl_Not B ) ) (cl_Not A ) ) )) \
(* A10: ~ ~ A --> A *)
(\ A . p = [] \ c = (cl_implies (cl_Not (cl_Not A ) ) A )) \
(* MP: \A --> B; A\ \ B *)
(\ A B . p = [(cl_implies A B ), A] \ c = B) \
False"
datatype inference =
node "inference list" cl_bool
| hypothesis cl_bool
fun
conclusion :: "inference \ cl_bool"
where
"conclusion (node _ c) = c"
| "conclusion (hypothesis c) = c"
primrec
correct :: "[cl_bool set, inference] \ bool" and
correct_list :: "[cl_bool set, inference list] \ bool" (* This dirty correct_list trick (and not fun) to allow induction *)
where
"correct h (node p c) \ by_rule (map conclusion p) c \ correct_list h p"
| "correct h (hypothesis c) \ c \ h"
| "correct_list h [] \ True"
| "correct_list h (x # xs) \ correct h x \ correct_list h xs"
lemma whats_correct:
"correct h (node p c) \ by_rule (map conclusion p) c \ (\ x \ set p. correct h x)"
proof -
have "correct_list h p \ (\ x \ set p. correct h x)" by (induct p, auto)
thus ?thesis by auto
qed
lemma inference_induct [induct type: inference]:
assumes "\ p c. (\ x \ set p. pred x) \ pred (node p c)"
assumes "\ c. pred (hypothesis c)"
shows "pred p"
proof (induct p)
fix p and c
assume "\ x \ set p. pred x"
thus "pred (node p c)" using assms by auto
next
fix c
show "pred (hypothesis c)" using assms by auto
next
show "\ x \ set []. pred x" by auto
next
fix y and ys
assume "\ x \ set ys. pred x" and "pred y"
thus "\ x \ set (y # ys). pred x" by auto
qed
definition
infers :: "[cl_bool set, cl_bool] \ bool" (infix "|-" 55)
where
"\ |- A \ (\ p. correct \ p \ conclusion p = A)"
notation (xsymbols)
infers (infix "\" 55)
lemmas [iff] = infers_def
definition
provable :: "cl_bool \ bool" ("|- _" [55] 55)
where
"|- A \ {} \ A"
notation (xsymbols)
provable ("\ _" [55] 55)
lemmas [iff] = provable_def
(* P | Q --> Q | P *)
theorem exam2_5:
"{} \ (cl_implies (cl_disj P Q ) (cl_disj Q P ) )" (is "?left \ ?right")
proof -
(* P --> Q | P *)
let ?s1 = "node [] (cl_implies P (cl_disj Q P ) )"
(* Q --> Q | P *)
let ?s2 = "node [] (cl_implies Q (cl_disj Q P ) )"
(* (P --> Q | P) --> ((Q --> Q | P) --> (P | Q --> Q | P)) *)
let ?s3 = "node [] (cl_implies (cl_implies P (cl_disj Q P ) ) (cl_implies (cl_implies Q (cl_disj Q P ) ) (cl_implies (cl_disj P Q ) (cl_disj Q P ) ) ) )"
(* (Q --> Q | P) --> (P | Q --> Q | P) *)
let ?s4 = "node [?s3, ?s1] (cl_implies (cl_implies Q (cl_disj Q P ) ) (cl_implies (cl_disj P Q ) (cl_disj Q P ) ) )"
(* P | Q --> Q | P *)
let ?s5 = "node [?s4, ?s2] (cl_implies (cl_disj P Q ) (cl_disj Q P ) )"
have "correct ?left ?s5" and "conclusion ?s5 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A --> A *)
theorem exam2_6:
"{} \ (cl_implies A A )" (is "?left \ ?right")
proof -
(* (A --> ((A --> A) --> A)) --> ((A --> (A --> A)) --> (A --> A)) *)
let ?s1 = "node [] (cl_implies (cl_implies A (cl_implies (cl_implies A A ) A ) ) (cl_implies (cl_implies A (cl_implies A A ) ) (cl_implies A A ) ) )"
(* A --> ((A --> A) --> A) *)
let ?s2 = "node [] (cl_implies A (cl_implies (cl_implies A A ) A ) )"
(* (A --> (A --> A)) --> (A --> A) *)
let ?s3 = "node [?s1, ?s2] (cl_implies (cl_implies A (cl_implies A A ) ) (cl_implies A A ) )"
(* A --> (A --> A) *)
let ?s4 = "node [] (cl_implies A (cl_implies A A ) )"
(* A --> A *)
let ?s5 = "node [?s3, ?s4] (cl_implies A A )"
have "correct ?left ?s5" and "conclusion ?s5 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* P & Q \ Q & P *)
theorem exam2_11:
"{(cl_conj P Q )} \ (cl_conj Q P )" (is "?left \ ?right")
proof -
(* P & Q *)
let ?h1 = "hypothesis (cl_conj P Q )"
(* P & Q --> P *)
let ?s1 = "node [] (cl_implies (cl_conj P Q ) P )"
(* P *)
let ?s2 = "node [?s1, ?h1] P"
(* P & Q --> Q *)
let ?s3 = "node [] (cl_implies (cl_conj P Q ) Q )"
(* Q *)
let ?s4 = "node [?s3, ?h1] Q"
(* Q --> (P --> Q & P) *)
let ?s5 = "node [] (cl_implies Q (cl_implies P (cl_conj Q P ) ) )"
(* P --> Q & P *)
let ?s6 = "node [?s5, ?s4] (cl_implies P (cl_conj Q P ) )"
(* Q & P *)
let ?s7 = "node [?s6, ?s2] (cl_conj Q P )"
have "correct ?left ?s7" and "conclusion ?s7 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \A; A --> B; B --> C\ \ C *)
theorem for_exam2_19:
"{A, (cl_implies A B ), (cl_implies B C )} \ C" (is "?left \ ?right")
proof -
(* A *)
let ?h1 = "hypothesis A"
(* A --> B *)
let ?h2 = "hypothesis (cl_implies A B )"
(* B --> C *)
let ?h3 = "hypothesis (cl_implies B C )"
(* B *)
let ?s1 = "node [?h2, ?h1] B"
(* C *)
let ?s2 = "node [?h3, ?s1] C"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \~ B; A --> B\ \ ~ A *)
theorem for_exam2_20:
"{(cl_Not B ), (cl_implies A B )} \ (cl_Not A )" (is "?left \ ?right")
proof -
(* ~ B *)
let ?not_b = "hypothesis (cl_Not B )"
(* A --> B *)
let ?a_impl_b = "hypothesis (cl_implies A B )"
(* (A --> B) --> ((A --> ~ B) --> ~ A) *)
let ?s1 = "node [] (cl_implies (cl_implies A B ) (cl_implies (cl_implies A (cl_Not B ) ) (cl_Not A ) ) )"
(* (A --> ~ B) --> ~ A *)
let ?s2 = "node [?s1, ?a_impl_b] (cl_implies (cl_implies A (cl_Not B ) ) (cl_Not A ) )"
(* ~ B --> (A --> ~ B) *)
let ?s3 = "node [] (cl_implies (cl_Not B ) (cl_implies A (cl_Not B ) ) )"
(* A --> ~ B *)
let ?s4 = "node [?s3, ?not_b] (cl_implies A (cl_Not B ) )"
(* ~ A *)
let ?s5 = "node [?s2, ?s4] (cl_Not A )"
have "correct ?left ?s5" and "conclusion ?s5 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \A; ~ A\ \ B *)
theorem exam2_21:
"{A, (cl_Not A )} \ B" (is "?left \ ?right")
proof -
(* A *)
let ?a = "hypothesis A"
(* ~ A *)
let ?not_a = "hypothesis (cl_Not A )"
(* A --> (~ B --> A) *)
let ?s1 = "node [] (cl_implies A (cl_implies (cl_Not B ) A ) )"
(* ~ A --> (~ B --> ~ A) *)
let ?s2 = "node [] (cl_implies (cl_Not A ) (cl_implies (cl_Not B ) (cl_Not A ) ) )"
(* ~ B --> A *)
let ?s3 = "node [?s1, ?a] (cl_implies (cl_Not B ) A )"
(* ~ B --> ~ A *)
let ?s4 = "node [?s2, ?not_a] (cl_implies (cl_Not B ) (cl_Not A ) )"
(* (~ B --> A) --> ((~ B --> ~ A) --> ~ ~ B) *)
let ?s5 = "node [] (cl_implies (cl_implies (cl_Not B ) A ) (cl_implies (cl_implies (cl_Not B ) (cl_Not A ) ) (cl_Not (cl_Not B ) ) ) )"
(* (~ B --> ~ A) --> ~ ~ B *)
let ?s6 = "node [?s5, ?s3] (cl_implies (cl_implies (cl_Not B ) (cl_Not A ) ) (cl_Not (cl_Not B ) ) )"
(* ~ ~ B *)
let ?s7 = "node [?s6, ?s4] (cl_Not (cl_Not B ) )"
(* ~ ~ B --> B *)
let ?s8 = "node [] (cl_implies (cl_Not (cl_Not B ) ) B )"
(* B *)
let ?s9 = "node [?s8, ?s7] B"
have "correct ?left ?s9" and "conclusion ?s9 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A & B \ A *)
theorem a_and_b_infers_a:
"{(cl_conj A B )} \ A" (is "?left \ ?right")
proof -
(* A & B *)
let ?h1 = "hypothesis (cl_conj A B )"
(* A & B --> A *)
let ?s1 = "node [] (cl_implies (cl_conj A B ) A )"
(* A *)
let ?s2 = "node [?s1, ?h1] A"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A & B \ B *)
theorem a_and_b_infers_b:
"{(cl_conj A B )} \ B" (is "?left \ ?right")
proof -
(* A & B *)
let ?h1 = "hypothesis (cl_conj A B )"
(* A & B --> B *)
let ?s1 = "node [] (cl_implies (cl_conj A B ) B )"
(* B *)
let ?s2 = "node [?s1, ?h1] B"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A --> B & ~ B \ ~ A *)
theorem a_impl_false_infers_not_a:
"{(cl_implies A (cl_conj B (cl_Not B ) ) )} \ (cl_Not A )" (is "?left \ ?right")
proof -
(* A --> B & ~ B *)
let ?h1 = "hypothesis (cl_implies A (cl_conj B (cl_Not B ) ) )"
(* B & ~ B --> B *)
let ?s1 = "node [] (cl_implies (cl_conj B (cl_Not B ) ) B )"
(* B & ~ B --> ~ B *)
let ?s2 = "node [] (cl_implies (cl_conj B (cl_Not B ) ) (cl_Not B ) )"
(* (B & ~ B --> B) --> A --> (B & ~ B --> B) *)
let ?s3 = "node [] (cl_implies (cl_implies (cl_conj B (cl_Not B ) ) B ) (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) B ) ) )"
(* (B & ~ B --> ~ B) --> A --> (B & ~ B --> ~ B) *)
let ?s4 = "node [] (cl_implies (cl_implies (cl_conj B (cl_Not B ) ) (cl_Not B ) ) (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) (cl_Not B ) ) ) )"
(* A --> (B & ~ B --> B) *)
let ?s5 = "node [?s3, ?s1] (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) B ) )"
(* A --> (B & ~ B --> ~ B) *)
let ?s6 = "node [?s4, ?s2] (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) (cl_Not B ) ) )"
(* (A --> (B & ~ B --> B)) --> (A --> B & ~ B) --> (A --> B) *)
let ?s7 = "node [] (cl_implies (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) B ) ) (cl_implies (cl_implies A (cl_conj B (cl_Not B ) ) ) (cl_implies A B ) ) )"
(* (A --> (B & ~ B --> ~ B)) --> (A --> B & ~ B) --> (A --> ~ B) *)
let ?s8 = "node [] (cl_implies (cl_implies A (cl_implies (cl_conj B (cl_Not B ) ) (cl_Not B ) ) ) (cl_implies (cl_implies A (cl_conj B (cl_Not B ) ) ) (cl_implies A (cl_Not B ) ) ) )"
(* (A --> B & ~ B) --> (A --> B) *)
let ?s9 = "node [?s7, ?s5] (cl_implies (cl_implies A (cl_conj B (cl_Not B ) ) ) (cl_implies A B ) )"
(* (A --> B & ~ B) --> (A --> ~ B) *)
let ?s10 = "node [?s8, ?s6] (cl_implies (cl_implies A (cl_conj B (cl_Not B ) ) ) (cl_implies A (cl_Not B ) ) )"
(* A --> B *)
let ?s11 = "node [?s9, ?h1] (cl_implies A B )"
(* A --> ~ B *)
let ?s12 = "node [?s10, ?h1] (cl_implies A (cl_Not B ) )"
(* (A --> B) --> (A --> ~ B) --> ~ A *)
let ?s13 = "node [] (cl_implies (cl_implies A B ) (cl_implies (cl_implies A (cl_Not B ) ) (cl_Not A ) ) )"
(* (A --> ~ B) --> ~ A *)
let ?s14 = "node [?s13, ?s11] (cl_implies (cl_implies A (cl_Not B ) ) (cl_Not A ) )"
(* ~ A *)
let ?s15 = "node [?s14, ?s12] (cl_Not A )"
have "correct ?left ?s15" and "conclusion ?s15 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \A; B\ \ A & B *)
theorem a_b_infers_a_and_b:
"{A, B} \ (cl_conj A B )" (is "?left \ ?right")
proof -
(* A *)
let ?a = "hypothesis A"
(* B *)
let ?b = "hypothesis B"
(* A --> B --> A & B *)
let ?s1 = "node [] (cl_implies A (cl_implies B (cl_conj A B ) ) )"
(* B --> A & B *)
let ?s2 = "node [?s1, ?a] (cl_implies B (cl_conj A B ) )"
(* A & B *)
let ?s3 = "node [?s2, ?b] (cl_conj A B )"
have "correct ?left ?s3" and "conclusion ?s3 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \A | B; A --> C; B --> C\ \ C *)
theorem a_or_b_a_impl_c_b_impl_c_infers_c:
"{(cl_disj A B ), (cl_implies A C ), (cl_implies B C )} \ C" (is "?left \ ?right")
proof -
(* A | B *)
let ?ab = "hypothesis (cl_disj A B )"
(* A --> C *)
let ?a = "hypothesis (cl_implies A C )"
(* B --> C *)
let ?b = "hypothesis (cl_implies B C )"
(* (A --> C) --> (B --> C) --> (A | B --> C) *)
let ?s1 = "node [] (cl_implies (cl_implies A C ) (cl_implies (cl_implies B C ) (cl_implies (cl_disj A B ) C ) ) )"
(* (B --> C) --> (A | B --> C) *)
let ?s2 = "node [?s1, ?a] (cl_implies (cl_implies B C ) (cl_implies (cl_disj A B ) C ) )"
(* A | B --> C *)
let ?s3 = "node [?s2, ?b] (cl_implies (cl_disj A B ) C )"
(* C *)
let ?s4 = "node [?s3, ?ab] C"
have "correct ?left ?s4" and "conclusion ?s4 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A \ A | B *)
theorem a_infers_a_or_b:
"{A} \ (cl_disj A B )" (is "?left \ ?right")
proof -
(* A *)
let ?h1 = "hypothesis A"
(* A --> A | B *)
let ?s1 = "node [] (cl_implies A (cl_disj A B ) )"
(* A | B *)
let ?s2 = "node [?s1, ?h1] (cl_disj A B )"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* B \ A | B *)
theorem b_infers_a_or_b:
"{B} \ (cl_disj A B )" (is "?left \ ?right")
proof -
(* B *)
let ?h1 = "hypothesis B"
(* B --> A | B *)
let ?s1 = "node [] (cl_implies B (cl_disj A B ) )"
(* A | B *)
let ?s2 = "node [?s1, ?h1] (cl_disj A B )"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* \A --> B; A\ \ B *)
theorem mp:
"{(cl_implies A B ), A} \ B" (is "?left \ ?right")
proof -
(* A --> B *)
let ?ab = "hypothesis (cl_implies A B )"
(* A *)
let ?a = "hypothesis A"
(* B *)
let ?s1 = "node [?ab, ?a] B"
have "correct ?left ?s1" and "conclusion ?s1 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* A \ B --> A *)
theorem a_infers_b_impl_a:
"{A} \ (cl_implies B A )" (is "?left \ ?right")
proof -
(* A *)
let ?h1 = "hypothesis A"
(* A --> (B --> A) *)
let ?s1 = "node [] (cl_implies A (cl_implies B A ) )"
(* B --> A *)
let ?s2 = "node [?s1, ?h1] (cl_implies B A )"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
(* ~ ~ A \ A *)
theorem not_not_a_infers_a:
"{(cl_Not (cl_Not A ) )} \ A" (is "?left \ ?right")
proof -
(* ~ ~ A *)
let ?h1 = "hypothesis (cl_Not (cl_Not A ) )"
(* ~ ~ A --> A *)
let ?s1 = "node [] (cl_implies (cl_Not (cl_Not A ) ) A )"
(* A *)
let ?s2 = "node [?s1, ?h1] A"
have "correct ?left ?s2" and "conclusion ?s2 = ?right" using by_rule_def by auto
thus ?thesis by fast
qed
end