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
```