doc-src/ZF/If.thy
author boehmes
Tue, 07 Dec 2010 15:44:38 +0100
changeset 41064 0c447a17770a
parent 35416 d8d7d1b785af
child 42637 381fdcab0f36
permissions -rw-r--r--
updated SMT certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     1
(*  Title:      FOL/ex/If.ML
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     2
    ID:         $Id$
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     5
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     6
First-Order Logic: the 'if' example.
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     7
*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14205
diff changeset
     9
theory If imports FOL begin
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    10
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 19792
diff changeset
    11
definition "if" :: "[o,o,o]=>o" where
19792
e8e3da6d3ff7 quoted "if";
wenzelm
parents: 16417
diff changeset
    12
  "if(P,Q,R) == P&Q | ~P&R"
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    13
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    14
lemma ifI:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    15
    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    16
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    17
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    18
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    19
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    20
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    21
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    22
lemma ifE:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    23
   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    24
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    25
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    26
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    27
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    28
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    29
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    30
lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    31
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    32
apply (rule iffI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    33
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    34
apply (erule ifE)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    35
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    36
apply (erule ifE)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    37
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    38
apply (rule ifI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    39
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    40
apply (rule ifI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    41
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    42
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    43
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    44
text{*Trying again from the beginning in order to use @{text blast}*}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    45
declare ifI [intro!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    46
declare ifE [elim!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    47
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    48
lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    49
by blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    50
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    51
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    52
lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    53
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    54
by blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    55
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    56
text{*Trying again from the beginning in order to prove from the definitions*}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    57
lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    58
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    59
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    60
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    61
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    62
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    63
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    64
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    65
text{*An invalid formula.  High-level rules permit a simpler diagnosis*}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    66
lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    67
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    68
apply auto
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    69
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    70
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    71
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    72
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    73
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    74
text{*Trying again from the beginning in order to prove from the definitions*}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    75
lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    76
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    77
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    78
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    79
apply (auto) 
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    80
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    81
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    82
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    83
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    84
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    85
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    86
end