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