theory Tarski_Exercise1
imports Main
uses "/home/till/CASL/CASL-lib/Isabelle/prelude"
begin

ML "Header.initialize [\"Ax4\"]"

typedecl s

consts
Adjoins :: "s => s => bool" ("Adjoins'(_,/ _')" [10,10] 999)
BackOf :: "s => s => bool" ("BackOf'(_,/ _')" [10,10] 999)
Between :: "s => s => s => bool" ("Between'(_,/ _,/ _')" [10,10,10] 999)
Cube :: "s => bool" ("Cube'(_')" [10] 999)
Dodec :: "s => bool" ("Dodec'(_')" [10] 999)
FrontOf :: "s => s => bool" ("FrontOf'(_,/ _')" [10,10] 999)
Large :: "s => bool" ("Large'(_')" [10] 999)
Larger :: "s => s => bool" ("Larger'(_,/ _')" [10,10] 999)
LeftOf :: "s => s => bool" ("LeftOf'(_,/ _')" [10,10] 999)
Medium :: "s => bool" ("Medium'(_')" [10] 999)
RightOf :: "s => s => bool" ("RightOf'(_,/ _')" [10,10] 999)
SameCol :: "s => s => bool" ("SameCol'(_,/ _')" [10,10] 999)
SameRow :: "s => s => bool" ("SameRow'(_,/ _')" [10,10] 999)
SameShape :: "s => s => bool" ("SameShape'(_,/ _')" [10,10] 999)
SameSize :: "s => s => bool" ("SameSize'(_,/ _')" [10,10] 999)
Small :: "s => bool" ("Small'(_')" [10] 999)
Smaller :: "s => s => bool" ("Smaller'(_,/ _')" [10,10] 999)
Tet :: "s => bool" ("Tet'(_')" [10] 999)

instance s::type
by intro_classes

axioms
Ax1 : "ALL y. Cube(y) | Dodec(y)"

Ax2 : "ALL x. Cube(x) --> Large(x)"

Ax3 : "EX x. ~ Large(x)"

theorem Ax4 : "EX x. Dodec(x)"
apply(rule exE)
apply(rule Ax3)
apply(rule disjE)
apply(rule_tac x="x" in Ax1[THEN spec])
apply(drule Ax2[THEN spec, THEN mp])
apply(blast)
apply(rule exI)
apply(assumption)
done

(* schnellere Moeglichkeit:
   using Ax1 Ax2 Ax3 apply(blast) *)


ML "Header.record \"Ax4\""

end