wneuper/isa: doc-src/ZF/If.thy@4ae8d65bc97c

     1 (*  Title:      FOL/ex/If.ML

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1991  University of Cambridge

     6 First-Order Logic: the 'if' example.

     7 *)

     9 theory If = FOL:

    11 constdefs

    12   if :: "[o,o,o]=>o"

    13    "if(P,Q,R) == P&Q | ~P&R"

    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

    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

    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

    45 text{*Trying again from the beginning in order to use @{text blast}*}

    46 declare ifI [intro!]

    47 declare ifE [elim!]

    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

    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

    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

    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

    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

    87 end

author	paulson
	Wed, 24 Sep 2003 10:44:41 +0200
changeset 14205	4ae8d65bc97c
child 16417	9bc16273c2d4
permissions	-rw-r--r--