(*Smaus came up with this as paper-and-pencil example, Alex Schimpf
formalised it in Isabelle*)
use_thy "Nonconservative";
(*If you want to use "goal thy", you will need the following
line. Although use_thy sets the context correctly, it does not
automatically update the identifier "thy". Why this is so neither Jan
nor Alex know.*)
(*val thy = the_context();*)
(*As presented in the lecture:*)
Goal "False";
(*The following only works if thy has been set correctly, see above.
goal thy "False";*)
br False_neq_True 1;
by (res_inst_tac [("s","c"),("t","False")] subst 1);
by (res_inst_tac [("P","\\x. c = x")] spec 1);
br allI 1;
br define_const_by_variable 1;
by (res_inst_tac [("P","\\x. c = x")] spec 1);
br allI 1;
br define_const_by_variable 1;
qed "inconsistency";
(*simpler alternative*)
Goal "False";
br False_neq_True 1;
by (res_inst_tac [("s","c"),("t","False")] subst 1);
br define_const_by_variable 1;
br define_const_by_variable 1;
qed "inconsistency";
(*without explicit instantiation*)
Goal "False";
br False_neq_True 1;
br subst 1;back();back();
br define_const_by_variable 1;
br define_const_by_variable 1;
qed "inconsistency";