wneuper/isa: doc-src/ZF/If.thy@20e3616b2d9c

     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 imports FOL begin

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

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

    14 lemma ifI:

    15     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"

    16   --{* @{subgoals[display,indent=0,margin=65]} *}

    17 apply (simp add: if_def)

    18   --{* @{subgoals[display,indent=0,margin=65]} *}

    19 apply blast

    20 done

    22 lemma ifE:

    23    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"

    24   --{* @{subgoals[display,indent=0,margin=65]} *}

    25 apply (simp add: if_def)

    26   --{* @{subgoals[display,indent=0,margin=65]} *}

    27 apply blast

    28 done

    30 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"

    31   --{* @{subgoals[display,indent=0,margin=65]} *}

    32 apply (rule iffI)

    33   --{* @{subgoals[display,indent=0,margin=65]} *}

    34 apply (erule ifE)

    35   --{* @{subgoals[display,indent=0,margin=65]} *}

    36 apply (erule ifE)

    37   --{* @{subgoals[display,indent=0,margin=65]} *}

    38 apply (rule ifI)

    39   --{* @{subgoals[display,indent=0,margin=65]} *}

    40 apply (rule ifI)

    41   --{* @{subgoals[display,indent=0,margin=65]} *}

    42 oops

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

    45 declare ifI [intro!]

    46 declare ifE [elim!]

    48 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"

    49 by blast

    52 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"

    53   --{* @{subgoals[display,indent=0,margin=65]} *}

    54 by blast

    56 text{*Trying again from the beginning in order to prove from the definitions*}

    57 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"

    58   --{* @{subgoals[display,indent=0,margin=65]} *}

    59 apply (simp add: if_def)

    60   --{* @{subgoals[display,indent=0,margin=65]} *}

    61 apply blast

    62 done

    65 text{*An invalid formula.  High-level rules permit a simpler diagnosis*}

    66 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"

    67   --{* @{subgoals[display,indent=0,margin=65]} *}

    68 apply auto

    69   --{* @{subgoals[display,indent=0,margin=65]} *}

    70 (*The next step will fail unless subgoals remain*)

    71 apply (tactic all_tac)

    72 oops

    74 text{*Trying again from the beginning in order to prove from the definitions*}

    75 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"

    76   --{* @{subgoals[display,indent=0,margin=65]} *}

    77 apply (simp add: if_def)

    78   --{* @{subgoals[display,indent=0,margin=65]} *}

    79 apply (auto)

    80   --{* @{subgoals[display,indent=0,margin=65]} *}

    81 (*The next step will fail unless subgoals remain*)

    82 apply (tactic all_tac)

    83 oops

    86 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 35413	d8d7d1b785af
child 43508	381fdcab0f36
permissions	-rw-r--r--