doc-src/ZF/If.thy
author wenzelm
Thu, 15 May 2008 20:14:10 +0200
changeset 26913 67040326ab7a
parent 19792 e8e3da6d3ff7
child 35416 d8d7d1b785af
permissions -rw-r--r--
use Isabelle sty files from Doc/;
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
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    11
constdefs
19792
e8e3da6d3ff7 quoted "if";
wenzelm
parents: 16417
diff changeset
    12
  "if" :: "[o,o,o]=>o"
e8e3da6d3ff7 quoted "if";
wenzelm
parents: 16417
diff changeset
    13
  "if(P,Q,R) == P&Q | ~P&R"
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    14
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    15
lemma ifI:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    16
    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    17
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    18
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    19
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    20
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    21
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    22
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    23
lemma ifE:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    24
   "[| 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
    25
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    26
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    27
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    28
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    29
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    30
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    31
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
    32
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    33
apply (rule iffI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    34
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    35
apply (erule ifE)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    36
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    37
apply (erule ifE)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    38
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    39
apply (rule ifI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    40
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    41
apply (rule ifI)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    42
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    43
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    44
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    45
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
    46
declare ifI [intro!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    47
declare ifE [elim!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    48
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    49
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
    50
by blast
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
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    53
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
    54
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    55
by blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    56
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    57
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
    58
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
    59
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    60
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    61
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    62
apply blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    63
done
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
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    66
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
    67
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
    68
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    69
apply auto
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    70
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    71
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    72
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    73
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    74
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    75
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
    76
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
    77
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    78
apply (simp add: if_def)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    79
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    80
apply (auto) 
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    81
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    82
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    83
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    84
oops
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
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    87
end