src/Doc/ZF/If.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 50530 6266e44b3396
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50530
6266e44b3396 updated some headers;
wenzelm
parents: 48985
diff changeset
     1
(*  Title:      Doc/ZF/If.thy
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     4
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     5
First-Order Logic: the 'if' example.
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     6
*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     7
48517
0f8c8ac6cc0e more precise imports;
wenzelm
parents: 42637
diff changeset
     8
theory If imports "~~/src/FOL/FOL" begin
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
     9
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 19792
diff changeset
    10
definition "if" :: "[o,o,o]=>o" where
19792
e8e3da6d3ff7 quoted "if";
wenzelm
parents: 16417
diff changeset
    11
  "if(P,Q,R) == P&Q | ~P&R"
14205
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    12
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    13
lemma ifI:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    14
    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    15
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    16
apply (simp add: if_def)
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 blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    19
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    20
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    21
lemma ifE:
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    22
   "[| 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
    23
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    24
apply (simp add: if_def)
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 blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    27
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    28
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    29
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
    30
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    31
apply (rule iffI)
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 (erule ifE)
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 (rule ifI)
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
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    42
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    43
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
    44
declare ifI [intro!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    45
declare ifE [elim!]
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    46
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    47
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
    48
by blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    49
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
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
    52
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    53
by blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    54
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    55
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
    56
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
    57
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    58
apply (simp add: if_def)
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 blast
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    61
done
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    62
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
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
    65
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
    66
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    67
apply auto
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
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    70
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    71
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    72
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    73
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
    74
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
    75
  --{* @{subgoals[display,indent=0,margin=65]} *}
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    76
apply (simp add: if_def)
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 (auto) 
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
(*The next step will fail unless subgoals remain*)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    81
apply (tactic all_tac)
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    82
oops
4ae8d65bc97c new example for the Isar version of the ZF manual
paulson
parents:
diff changeset
    83
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
end