wneuper/isa: doc-src/ZF/If.thy@381fdcab0f36

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

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1991  University of Cambridge

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

     6 *)

     8 theory If imports FOL begin

    10 definition "if" :: "[o,o,o]=>o" where

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

    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

    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

    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

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

    44 declare ifI [intro!]

    45 declare ifE [elim!]

    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

    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

    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

    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

    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

    85 end

author	wenzelm
	Mon, 02 May 2011 22:31:46 +0200
changeset 43508	381fdcab0f36
parent 35413	d8d7d1b785af
child 49532	0f8c8ac6cc0e
permissions	-rw-r--r--