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