# HG changeset patch
# User paulson
# Date 1064393081 -7200
# Node ID 4ae8d65bc97cff92219995b99e6d30df26776ad3
# Parent  2fa6ecb87d4725cf5ea6cf0f9cb86c29dfc4cb27
new example for the Isar version of the ZF manual

diff -r 2fa6ecb87d47 -r 4ae8d65bc97c doc-src/ZF/If.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/If.thy	Wed Sep 24 10:44:41 2003 +0200
@@ -0,0 +1,87 @@
+(*  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)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (simp add: if_def)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply blast
+done
+
+lemma ifE:
+   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (simp add: if_def)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply 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))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule iffI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule ifE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule ifE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule ifI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule ifI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+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))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+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))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (simp add: if_def)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply blast
+done
+
+
+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))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply auto
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+(*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))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (simp add: if_def)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (auto) 
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+(*The next step will fail unless subgoals remain*)
+apply (tactic all_tac)
+oops
+
+
+end