# HG changeset patch
# User paulson
# Date 1060947939 -7200
# Node ID b8bb6a6a2c46bf641373f7d568e8c4603619a904
# Parent  9a23e4eb5eb335f7fc627f94fb7234601c6bcb61
converting ex/If to Isar script

diff -r 9a23e4eb5eb3 -r b8bb6a6a2c46 src/FOL/IsaMakefile
--- 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	\
diff -r 9a23e4eb5eb3 -r b8bb6a6a2c46 src/FOL/ex/If.ML
--- 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));
diff -r 9a23e4eb5eb3 -r b8bb6a6a2c46 src/FOL/ex/If.thy
--- 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