doc-src/TutorialI/Sets/Relations.thy
author bulwahn
Mon, 22 Mar 2010 08:30:12 +0100
changeset 35876 ac44e2312f0a
parent 26806 40b411ec05aa
child 36745 403585a89772
permissions -rw-r--r--
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10341
6eb91805a012 added the $Id:$ line
paulson
parents: 10294
diff changeset
     1
(* ID:         $Id$ *)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12489
diff changeset
     2
theory Relations imports Main begin
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     3
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     4
ML "Pretty.setmargin 64"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     5
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     6
(*Id is only used in UNITY*)
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     7
(*refl, antisym,trans,univalent,\<dots> ho hum*)
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     8
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     9
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    10
@{thm[display] Id_def[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    11
\rulename{Id_def}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    12
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    13
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    14
text{*
12489
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    15
@{thm[display] rel_comp_def[no_vars]}
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    16
\rulename{rel_comp_def}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    17
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    18
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    19
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    20
@{thm[display] R_O_Id[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    21
\rulename{R_O_Id}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    22
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    23
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    24
text{*
12489
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    25
@{thm[display] rel_comp_mono[no_vars]}
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    26
\rulename{rel_comp_mono}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    27
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    28
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    29
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    30
@{thm[display] converse_iff[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    31
\rulename{converse_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    32
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    33
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    34
text{*
12489
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    35
@{thm[display] converse_rel_comp[no_vars]}
c92e38c3cbaa *** empty log message ***
nipkow
parents: 11330
diff changeset
    36
\rulename{converse_rel_comp}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    37
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    38
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    39
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    40
@{thm[display] Image_iff[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    41
\rulename{Image_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    42
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    43
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    44
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    45
@{thm[display] Image_UN[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    46
\rulename{Image_UN}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    47
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    48
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    49
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    50
@{thm[display] Domain_iff[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    51
\rulename{Domain_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    52
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    53
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    54
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    55
@{thm[display] Range_iff[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    56
\rulename{Range_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    57
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    58
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    59
text{*
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    60
@{thm[display] relpow.simps[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    61
\rulename{relpow.simps}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    62
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    63
@{thm[display] rtrancl_refl[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    64
\rulename{rtrancl_refl}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    65
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    66
@{thm[display] r_into_rtrancl[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    67
\rulename{r_into_rtrancl}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    68
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    69
@{thm[display] rtrancl_trans[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    70
\rulename{rtrancl_trans}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    71
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    72
@{thm[display] rtrancl_induct[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    73
\rulename{rtrancl_induct}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    74
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    75
@{thm[display] rtrancl_idemp[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    76
\rulename{rtrancl_idemp}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    77
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    78
@{thm[display] r_into_trancl[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    79
\rulename{r_into_trancl}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    80
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    81
@{thm[display] trancl_trans[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    82
\rulename{trancl_trans}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    83
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    84
@{thm[display] trancl_into_rtrancl[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    85
\rulename{trancl_into_rtrancl}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    86
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    87
@{thm[display] trancl_converse[no_vars]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    88
\rulename{trancl_converse}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    89
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    90
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    91
text{*Relations.  transitive closure*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    92
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
    93
lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    94
apply (erule rtrancl_induct)
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    95
txt{*
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    96
@{subgoals[display,indent=0,margin=65]}
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    97
*};
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    98
 apply (rule rtrancl_refl)
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
    99
apply (blast intro: rtrancl_trans)
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   100
done
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   101
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   102
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
   103
lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   104
apply (erule rtrancl_induct)
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   105
 apply (rule rtrancl_refl)
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
   106
apply (blast intro: rtrancl_trans)
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   107
done
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   108
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
   109
lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   110
by (auto intro: rtrancl_converseI dest: rtrancl_converseD)
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   111
11080
22855d091249 various revisions in response to comments from Tobias
paulson
parents: 10864
diff changeset
   112
lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   113
apply (intro equalityI subsetI)
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   114
txt{*
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   115
after intro rules
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   116
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   117
@{subgoals[display,indent=0,margin=65]}
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   118
*};
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   119
apply clarify
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   120
txt{*
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   121
after splitting
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   122
@{subgoals[display,indent=0,margin=65]}
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   123
*};
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   124
oops
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   125
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   126
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   127
lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id"
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   128
apply (rule subsetI)
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   129
txt{*
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   130
@{subgoals[display,indent=0,margin=65]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   131
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   132
after subsetI
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   133
*};
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   134
apply clarify
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   135
txt{*
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   136
@{subgoals[display,indent=0,margin=65]}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   137
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   138
subgoals after clarify
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   139
*};
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   140
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   141
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   142
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   143
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   144
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   145
text{*rejects*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   146
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   147
lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   148
apply (blast)
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   149
done
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   150
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   151
text{*Pow, Inter too little used*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   152
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   153
lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 16417
diff changeset
   154
apply (simp add: psubset_eq)
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   155
done
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   156
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   157
end