--- a/src/FOL/IsaMakefile Fri Aug 15 13:07:01 2003 +0200
+++ b/src/FOL/IsaMakefile Fri Aug 15 13:45:39 2003 +0200
@@ -42,7 +42,7 @@
FOL-ex: FOL $(LOG)/FOL-ex.gz
-$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.ML \
+$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy \
ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \
ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML ex/document/root.tex \
--- a/src/FOL/ex/If.ML Fri Aug 15 13:07:01 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: FOL/ex/If.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-First-Order Logic: the 'if' example.
-*)
-
-open Cla; (*in case structure IntPr is open!*)
-
-val prems = Goalw [if_def]
- "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
-by (blast_tac (claset() addIs prems) 1);
-qed "ifI";
-
-val major::prems = Goalw [if_def]
- "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
-by (cut_facts_tac [major] 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "ifE";
-
-
-Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-by (rtac iffI 1);
-by (etac ifE 1);
-by (etac ifE 1);
-by (rtac ifI 1);
-by (rtac ifI 1);
-
-choplev 0;
-AddSIs [ifI];
-AddSEs [ifE];
-by (Blast_tac 1);
-qed "if_commute";
-
-
-Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
-by (Blast_tac 1);
-qed "nested_ifs";
-
-choplev 0;
-by (rewtac if_def);
-by (blast_tac FOL_cs 1);
-qed "";
-
-
-(*An invalid formula. High-level rules permit a simpler diagnosis*)
-Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
-by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
-(*Check that subgoals remain: proof failed.*)
-getgoal 1;
-by (REPEAT (Step_tac 1));
-
-choplev 0;
-by (rewtac if_def);
-by (blast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
-(*Check that subgoals remain: proof failed.*)
-getgoal 1;
-by (REPEAT (step_tac FOL_cs 1));
--- a/src/FOL/ex/If.thy Fri Aug 15 13:07:01 2003 +0200
+++ b/src/FOL/ex/If.thy Fri Aug 15 13:45:39 2003 +0200
@@ -1,5 +1,64 @@
-If = FOL +
-consts if :: [o,o,o]=>o
-rules
- if_def "if(P,Q,R) == P&Q | ~P&R"
+(* Title: FOL/ex/If.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+First-Order Logic: the 'if' example.
+*)
+
+theory If = FOL:
+
+constdefs
+ if :: "[o,o,o]=>o"
+ "if(P,Q,R) == P&Q | ~P&R"
+
+lemma ifI:
+ "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
+apply (simp add: if_def, blast)
+done
+
+lemma ifE:
+ "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
+apply (simp add: if_def, blast)
+done
+
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+apply (rule iffI)
+apply (erule ifE)
+apply (erule ifE)
+apply (rule ifI)
+apply (rule ifI)
+oops
+
+text{*Trying again from the beginning in order to use @{text blast}*}
+declare ifI [intro!]
+declare ifE [elim!]
+
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+by blast
+
+
+lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
+by blast
+
+text{*Trying again from the beginning in order to prove from the definitions*}
+lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
+by (simp add: if_def, blast)
+
+
+text{*An invalid formula. High-level rules permit a simpler diagnosis*}
+lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
+apply auto
+(*The next step will fail unless subgoals remain*)
+apply (tactic all_tac)
+oops
+
+text{*Trying again from the beginning in order to prove from the definitions*}
+lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
+apply (simp add: if_def, auto)
+(*The next step will fail unless subgoals remain*)
+apply (tactic all_tac)
+oops
+
+
end