doc-src/ZF/If.thy
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 14205 4ae8d65bc97c
child 16417 9bc16273c2d4
permissions -rw-r--r--
aded comment
     1 (*  Title:      FOL/ex/If.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 First-Order Logic: the 'if' example.
     7 *)
     8 
     9 theory If = FOL:
    10 
    11 constdefs
    12   if :: "[o,o,o]=>o"
    13    "if(P,Q,R) == P&Q | ~P&R"
    14 
    15 lemma ifI:
    16     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
    17   --{* @{subgoals[display,indent=0,margin=65]} *}
    18 apply (simp add: if_def)
    19   --{* @{subgoals[display,indent=0,margin=65]} *}
    20 apply blast
    21 done
    22 
    23 lemma ifE:
    24    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
    25   --{* @{subgoals[display,indent=0,margin=65]} *}
    26 apply (simp add: if_def)
    27   --{* @{subgoals[display,indent=0,margin=65]} *}
    28 apply blast
    29 done
    30 
    31 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    32   --{* @{subgoals[display,indent=0,margin=65]} *}
    33 apply (rule iffI)
    34   --{* @{subgoals[display,indent=0,margin=65]} *}
    35 apply (erule ifE)
    36   --{* @{subgoals[display,indent=0,margin=65]} *}
    37 apply (erule ifE)
    38   --{* @{subgoals[display,indent=0,margin=65]} *}
    39 apply (rule ifI)
    40   --{* @{subgoals[display,indent=0,margin=65]} *}
    41 apply (rule ifI)
    42   --{* @{subgoals[display,indent=0,margin=65]} *}
    43 oops
    44 
    45 text{*Trying again from the beginning in order to use @{text blast}*}
    46 declare ifI [intro!]
    47 declare ifE [elim!]
    48 
    49 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    50 by blast
    51 
    52 
    53 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    54   --{* @{subgoals[display,indent=0,margin=65]} *}
    55 by blast
    56 
    57 text{*Trying again from the beginning in order to prove from the definitions*}
    58 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    59   --{* @{subgoals[display,indent=0,margin=65]} *}
    60 apply (simp add: if_def)
    61   --{* @{subgoals[display,indent=0,margin=65]} *}
    62 apply blast
    63 done
    64 
    65 
    66 text{*An invalid formula.  High-level rules permit a simpler diagnosis*}
    67 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
    68   --{* @{subgoals[display,indent=0,margin=65]} *}
    69 apply auto
    70   --{* @{subgoals[display,indent=0,margin=65]} *}
    71 (*The next step will fail unless subgoals remain*)
    72 apply (tactic all_tac)
    73 oops
    74 
    75 text{*Trying again from the beginning in order to prove from the definitions*}
    76 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
    77   --{* @{subgoals[display,indent=0,margin=65]} *}
    78 apply (simp add: if_def)
    79   --{* @{subgoals[display,indent=0,margin=65]} *}
    80 apply (auto) 
    81   --{* @{subgoals[display,indent=0,margin=65]} *}
    82 (*The next step will fail unless subgoals remain*)
    83 apply (tactic all_tac)
    84 oops
    85 
    86 
    87 end