src/HOL/Metis_Examples/Message.thy
author blanchet
Wed, 28 Apr 2010 22:36:39 +0200
changeset 36553 95bdfa572cee
parent 35416 d8d7d1b785af
child 36580 d23a3a4d1849
permissions -rw-r--r--
redo some of the metis proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     1
(*  Title:      HOL/MetisTest/Message.thy
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     3
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32864
diff changeset
     4
Testing the metis method.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     5
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
     7
theory Message
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
     8
imports Main
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
     9
begin
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    10
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    11
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    12
by (metis Un_ac(2) Un_ac(3))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    14
types 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    15
  key = nat
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
consts
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
  all_symmetric :: bool        --{*true if all keys are symmetric*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
specification (invKey)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
  invKey [simp]: "invKey (invKey K) = K"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
  invKey_symmetric: "all_symmetric --> invKey = id"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    24
by (metis id_apply)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    25
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    26
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    27
text{*The inverse of a symmetric key is itself; that of a public key
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    28
      is the private key and vice versa*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    29
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35109
diff changeset
    30
definition symKeys :: "key set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
  "symKeys == {K. invKey K = K}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    32
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    33
datatype  --{*We allow any number of friendly agents*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    34
  agent = Server | Friend nat | Spy
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    36
datatype
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32864
diff changeset
    37
     msg = Agent  agent     --{*Agent names*}
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    38
         | Number nat       --{*Ordinary integers, timestamps, ...*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    39
         | Nonce  nat       --{*Unguessable nonces*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    40
         | Key    key       --{*Crypto keys*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32864
diff changeset
    41
         | Hash   msg       --{*Hashing*}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32864
diff changeset
    42
         | MPair  msg msg   --{*Compound messages*}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32864
diff changeset
    43
         | Crypt  key msg   --{*Encryption, public- or shared-key*}
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    44
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    45
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    46
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    47
syntax
35109
0015a0a99ae9 modernized syntax/translations;
wenzelm
parents: 35095
diff changeset
    48
  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    50
syntax (xsymbols)
35109
0015a0a99ae9 modernized syntax/translations;
wenzelm
parents: 35095
diff changeset
    51
  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    52
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    53
translations
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    54
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
35054
a5db9779b026 modernized some syntax translations;
wenzelm
parents: 33027
diff changeset
    55
  "{|x, y|}"      == "CONST MPair x y"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    56
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35109
diff changeset
    58
definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    59
    --{*Message Y paired with a MAC computed with the help of X*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    60
    "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35109
diff changeset
    62
definition keysFor :: "msg set => key set" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    63
    --{*Keys useful to decrypt elements of a message set*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    64
  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    65
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    66
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    67
subsubsection{*Inductive Definition of All Parts" of a Message*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    68
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    69
inductive_set
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    70
  parts :: "msg set => msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    71
  for H :: "msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    72
  where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    73
    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    74
  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    75
  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
    76
  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    77
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    78
lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    79
apply auto
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    80
apply (erule parts.induct)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    81
   apply (metis parts.Inj set_rev_mp)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    82
  apply (metis parts.Fst)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    83
 apply (metis parts.Snd)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    84
by (metis parts.Body)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    85
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    86
text{*Equations hold because constructors are injective.*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    87
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    88
by (metis agent.inject imageI image_iff)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    89
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    90
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    91
by (metis image_iff msg.inject(4))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    92
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    93
lemma Nonce_Key_image_eq [simp]: "Nonce x \<notin> Key`A"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    94
by (metis image_iff msg.distinct(23))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    95
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    96
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    97
subsubsection{*Inverse of keys *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    98
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
    99
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   100
by (metis invKey)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   101
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   102
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   103
subsection{*keysFor operator*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   104
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   105
lemma keysFor_empty [simp]: "keysFor {} = {}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   106
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   107
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   108
lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   109
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   110
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   111
lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   112
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   113
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   114
text{*Monotonicity*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   115
lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   116
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   117
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   118
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   119
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   120
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   121
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   122
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   123
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   124
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   125
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   126
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   127
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   128
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   129
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   130
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   131
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   132
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   133
lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   134
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   135
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   136
lemma keysFor_insert_Crypt [simp]: 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   137
    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   138
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   139
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   140
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   141
by (unfold keysFor_def, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   142
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   143
lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   144
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   145
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   146
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   147
subsection{*Inductive relation "parts"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   148
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
lemma MPair_parts:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   150
     "[| {|X,Y|} \<in> parts H;        
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   151
         [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   152
by (blast dest: parts.Fst parts.Snd) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   153
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   154
declare MPair_parts [elim!] parts.Body [dest!]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   155
text{*NB These two rules are UNSAFE in the formal sense, as they discard the
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   156
     compound message.  They work well on THIS FILE.  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   157
  @{text MPair_parts} is left as SAFE because it speeds up proofs.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   158
  The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   159
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   160
lemma parts_increasing: "H \<subseteq> parts(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   161
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   162
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   163
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   164
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   165
lemma parts_empty [simp]: "parts{} = {}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   166
apply safe
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   167
apply (erule parts.induct)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   168
apply blast+
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   169
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   170
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   171
lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   172
by simp
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   173
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   175
lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   176
apply (erule parts.induct)
26807
4cd176ea28dc Replaced blast by fast in proof of parts_singleton, since blast looped
berghofe
parents: 25710
diff changeset
   177
apply fast+
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   179
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   180
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   181
subsubsection{*Unions *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   182
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   183
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   184
by (intro Un_least parts_mono Un_upper1 Un_upper2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   186
lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   187
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   188
apply (erule parts.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   189
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   190
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   191
lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   192
by (intro equalityI parts_Un_subset1 parts_Un_subset2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   193
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   194
lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   195
apply (subst insert_is_Un [of _ H])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   196
apply (simp only: parts_Un)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   197
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   198
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   199
lemma parts_insert2:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   200
     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
25710
4cdf7de81e1b Replaced refs by config params; finer critical section in mets method
paulson
parents: 25457
diff changeset
   201
by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   202
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   203
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   204
lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   205
by (intro UN_least parts_mono UN_upper)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   206
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   207
lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   208
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   209
apply (erule parts.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   210
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   211
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   212
lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   213
by (intro equalityI parts_UN_subset1 parts_UN_subset2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   214
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   215
text{*Added to simplify arguments to parts, analz and synth.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   216
  NOTE: the UN versions are no longer used!*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   217
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   218
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   219
text{*This allows @{text blast} to simplify occurrences of 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   220
  @{term "parts(G\<union>H)"} in the assumption.*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   221
lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   222
declare in_parts_UnE [elim!]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   223
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   224
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   225
by (blast intro: parts_mono [THEN [2] rev_subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   226
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   227
subsubsection{*Idempotence and transitivity *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   228
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   229
lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   230
by (erule parts.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   231
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   232
lemma parts_idem [simp]: "parts (parts H) = parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   233
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   234
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   235
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   236
apply (rule iffI) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   237
apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
25710
4cdf7de81e1b Replaced refs by config params; finer critical section in mets method
paulson
parents: 25457
diff changeset
   238
apply (metis parts_idem parts_mono)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   239
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   240
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   241
lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   242
by (blast dest: parts_mono); 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   243
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   244
lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
35095
6cdf9bbd0342 minor metis proof tuning
haftmann
parents: 35054
diff changeset
   245
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   246
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   247
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   248
subsubsection{*Rewrite rules for pulling out atomic messages *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   249
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   250
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   251
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   252
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   253
lemma parts_insert_Agent [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   254
     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   255
apply (rule parts_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   256
apply (erule parts.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   257
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   258
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   259
lemma parts_insert_Nonce [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   260
     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   261
apply (rule parts_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   262
apply (erule parts.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   263
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   264
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   265
lemma parts_insert_Number [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   266
     "parts (insert (Number N) H) = insert (Number N) (parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   267
apply (rule parts_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   268
apply (erule parts.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   269
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   270
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   271
lemma parts_insert_Key [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   272
     "parts (insert (Key K) H) = insert (Key K) (parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   273
apply (rule parts_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   274
apply (erule parts.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   275
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   276
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   277
lemma parts_insert_Hash [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   278
     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   279
apply (rule parts_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   280
apply (erule parts.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   281
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   282
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   283
lemma parts_insert_Crypt [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   284
     "parts (insert (Crypt K X) H) =  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   285
          insert (Crypt K X) (parts (insert X H))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   286
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   287
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   288
apply (erule parts.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   289
apply (blast intro: parts.Body)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   290
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   291
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   292
lemma parts_insert_MPair [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   293
     "parts (insert {|X,Y|} H) =  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   294
          insert {|X,Y|} (parts (insert X (insert Y H)))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   295
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   296
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   297
apply (erule parts.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   298
apply (blast intro: parts.Fst parts.Snd)+
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   299
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   300
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   301
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   302
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   303
apply (erule parts.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   304
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   305
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   306
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   307
apply (induct_tac "msg") 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   308
apply (simp_all add: parts_insert2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   309
apply (metis Suc_n_not_le_n)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   310
apply (metis le_trans linorder_linear)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   311
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   312
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   313
subsection{*Inductive relation "analz"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   314
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   315
text{*Inductive definition of "analz" -- what can be broken down from a set of
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   316
    messages, including keys.  A form of downward closure.  Pairs can
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   317
    be taken apart; messages decrypted with known keys.  *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   318
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   319
inductive_set
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   320
  analz :: "msg set => msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   321
  for H :: "msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   322
  where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   323
    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   324
  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   325
  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   326
  | Decrypt [dest]: 
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   327
             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   328
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   329
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   330
text{*Monotonicity; Lemma 1 of Lowe's paper*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   331
lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   332
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   333
apply (erule analz.induct) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   334
apply (auto dest: analz.Fst analz.Snd) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   335
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   336
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   337
text{*Making it safe speeds up proofs*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   338
lemma MPair_analz [elim!]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   339
     "[| {|X,Y|} \<in> analz H;        
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   340
             [| X \<in> analz H; Y \<in> analz H |] ==> P   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   341
          |] ==> P"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   342
by (blast dest: analz.Fst analz.Snd)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   343
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   344
lemma analz_increasing: "H \<subseteq> analz(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   345
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   346
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   347
lemma analz_subset_parts: "analz H \<subseteq> parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   348
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   349
apply (erule analz.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   350
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   351
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   352
lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   353
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   354
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   355
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   356
lemma parts_analz [simp]: "parts (analz H) = parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   357
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   358
apply (metis analz_subset_parts parts_subset_iff)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   359
apply (metis analz_increasing parts_mono)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   360
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   361
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   362
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   363
lemma analz_parts [simp]: "analz (parts H) = parts H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   364
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   365
apply (erule analz.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   366
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   367
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   368
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   369
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   370
subsubsection{*General equational properties *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   371
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   372
lemma analz_empty [simp]: "analz{} = {}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   373
apply safe
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   374
apply (erule analz.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   375
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   376
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   377
text{*Converse fails: we can analz more from the union than from the 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   378
  separate parts, as a key in one might decrypt a message in the other*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   379
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   380
by (intro Un_least analz_mono Un_upper1 Un_upper2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   381
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   382
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   383
by (blast intro: analz_mono [THEN [2] rev_subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   384
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   385
subsubsection{*Rewrite rules for pulling out atomic messages *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   386
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   387
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   388
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   389
lemma analz_insert_Agent [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   390
     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   391
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   392
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   393
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   394
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   395
lemma analz_insert_Nonce [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   396
     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   397
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   398
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   399
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   400
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   401
lemma analz_insert_Number [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   402
     "analz (insert (Number N) H) = insert (Number N) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   403
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   404
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   405
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   406
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   407
lemma analz_insert_Hash [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   408
     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   409
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   410
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   411
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   412
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   413
text{*Can only pull out Keys if they are not needed to decrypt the rest*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   414
lemma analz_insert_Key [simp]: 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   415
    "K \<notin> keysFor (analz H) ==>   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   416
          analz (insert (Key K) H) = insert (Key K) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   417
apply (unfold keysFor_def)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   418
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   419
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   420
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   421
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   422
lemma analz_insert_MPair [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   423
     "analz (insert {|X,Y|} H) =  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   424
          insert {|X,Y|} (analz (insert X (insert Y H)))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   425
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   426
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   427
apply (erule analz.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   428
apply (erule analz.induct)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   429
apply (blast intro: analz.Fst analz.Snd)+
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   430
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   431
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   432
text{*Can pull out enCrypted message if the Key is not known*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   433
lemma analz_insert_Crypt:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   434
     "Key (invKey K) \<notin> analz H 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   435
      ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   436
apply (rule analz_insert_eq_I) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   437
apply (erule analz.induct, auto) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   438
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   439
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   440
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   441
lemma lemma1: "Key (invKey K) \<in> analz H ==>   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   442
               analz (insert (Crypt K X) H) \<subseteq>  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   443
               insert (Crypt K X) (analz (insert X H))" 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   444
apply (rule subsetI)
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   445
apply (erule_tac x = x in analz.induct, auto)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   446
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   447
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   448
lemma lemma2: "Key (invKey K) \<in> analz H ==>   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   449
               insert (Crypt K X) (analz (insert X H)) \<subseteq>  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   450
               analz (insert (Crypt K X) H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   451
apply auto
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   452
apply (erule_tac x = x in analz.induct, auto)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   453
apply (blast intro: analz_insertI analz.Decrypt)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   454
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   455
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   456
lemma analz_insert_Decrypt:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   457
     "Key (invKey K) \<in> analz H ==>   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   458
               analz (insert (Crypt K X) H) =  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   459
               insert (Crypt K X) (analz (insert X H))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   460
by (intro equalityI lemma1 lemma2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   461
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   462
text{*Case analysis: either the message is secure, or it is not! Effective,
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   463
but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   464
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   465
(Crypt K X) H)"} *} 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   466
lemma analz_Crypt_if [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   467
     "analz (insert (Crypt K X) H) =                 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   468
          (if (Key (invKey K) \<in> analz H)                 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   469
           then insert (Crypt K X) (analz (insert X H))  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   470
           else insert (Crypt K X) (analz H))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   471
by (simp add: analz_insert_Crypt analz_insert_Decrypt)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   472
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   473
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   474
text{*This rule supposes "for the sake of argument" that we have the key.*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   475
lemma analz_insert_Crypt_subset:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   476
     "analz (insert (Crypt K X) H) \<subseteq>   
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   477
           insert (Crypt K X) (analz (insert X H))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   478
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   479
apply (erule analz.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   480
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   481
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   482
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   483
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   484
apply auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   485
apply (erule analz.induct, auto)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   486
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   487
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   488
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   489
subsubsection{*Idempotence and transitivity *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   490
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   491
lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   492
by (erule analz.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   493
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   494
lemma analz_idem [simp]: "analz (analz H) = analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   495
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   496
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   497
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   498
apply (rule iffI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   499
apply (iprover intro: subset_trans analz_increasing)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   500
apply (frule analz_mono, simp) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   501
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   502
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   503
lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   504
by (drule analz_mono, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   505
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   506
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   507
declare analz_trans[intro]
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   508
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   509
lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   510
(*TOO SLOW
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   511
by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   512
??*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   513
by (erule analz_trans, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   514
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   515
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   516
text{*This rewrite rule helps in the simplification of messages that involve
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   517
  the forwarding of unknown components (X).  Without it, removing occurrences
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   518
  of X can be very complicated. *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   519
lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   520
by (blast intro: analz_cut analz_insertI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   521
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   522
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   523
text{*A congruence rule for "analz" *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   524
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   525
lemma analz_subset_cong:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   526
     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   527
      ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   528
apply simp
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   529
apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   530
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   531
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   532
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   533
lemma analz_cong:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   534
     "[| analz G = analz G'; analz H = analz H'  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   535
               |] ==> analz (G \<union> H) = analz (G' \<union> H')"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   536
by (intro equalityI analz_subset_cong, simp_all) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   537
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   538
lemma analz_insert_cong:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   539
     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   540
by (force simp only: insert_def intro!: analz_cong)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   541
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   542
text{*If there are no pairs or encryptions then analz does nothing*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   543
lemma analz_trivial:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   544
     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   545
apply safe
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   546
apply (erule analz.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   547
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   548
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   549
text{*These two are obsolete (with a single Spy) but cost little to prove...*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   550
lemma analz_UN_analz_lemma:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   551
     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   552
apply (erule analz.induct)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   553
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   554
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   555
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   556
lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   557
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   558
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   559
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   560
subsection{*Inductive relation "synth"*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   561
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   562
text{*Inductive definition of "synth" -- what can be built up from a set of
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   563
    messages.  A form of upward closure.  Pairs can be built, messages
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   564
    encrypted with known keys.  Agent names are public domain.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   565
    Numbers can be guessed, but Nonces cannot be.  *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   566
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   567
inductive_set
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   568
  synth :: "msg set => msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   569
  for H :: "msg set"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   570
  where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   571
    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   572
  | Agent  [intro]:   "Agent agt \<in> synth H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   573
  | Number [intro]:   "Number n  \<in> synth H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   574
  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   575
  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 23449
diff changeset
   576
  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   577
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   578
text{*Monotonicity*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   579
lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   580
  by (auto, erule synth.induct, auto)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   581
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   582
text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   583
  The same holds for @{term Number}*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   584
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   585
inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   586
inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   587
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   588
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   589
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   590
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   591
lemma synth_increasing: "H \<subseteq> synth(H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   592
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   593
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   594
subsubsection{*Unions *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   595
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   596
text{*Converse fails: we can synth more from the union than from the 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   597
  separate parts, building a compound message using elements of each.*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   598
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   599
by (intro Un_least synth_mono Un_upper1 Un_upper2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   600
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   601
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   602
by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   603
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   604
subsubsection{*Idempotence and transitivity *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   605
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   606
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   607
by (erule synth.induct, blast+)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   608
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   609
lemma synth_idem: "synth (synth H) = synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   610
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   611
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   612
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   613
apply (rule iffI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   614
apply (iprover intro: subset_trans synth_increasing)  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   615
apply (frule synth_mono, simp add: synth_idem) 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   616
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   617
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   618
lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   619
by (drule synth_mono, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   620
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   621
lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   622
(*TOO SLOW
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   623
by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   624
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   625
by (erule synth_trans, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   626
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   627
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   628
lemma Agent_synth [simp]: "Agent A \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   629
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   630
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   631
lemma Number_synth [simp]: "Number n \<in> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   632
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   633
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   634
lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   635
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   636
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   637
lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   638
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   639
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   640
lemma Crypt_synth_eq [simp]:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   641
     "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   642
by blast
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   643
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   644
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   645
lemma keysFor_synth [simp]: 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   646
    "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   647
by (unfold keysFor_def, blast)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   648
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   649
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   650
subsubsection{*Combinations of parts, analz and synth *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   651
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   652
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   653
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   654
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   655
apply (erule parts.induct)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   656
apply (metis UnCI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   657
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   658
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   659
apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   660
apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   661
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   662
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   663
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   664
apply (rule equalityI);
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   665
apply (metis analz_idem analz_subset_cong order_eq_refl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   666
apply (metis analz_increasing analz_subset_cong order_eq_refl)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   667
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   668
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   669
declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   670
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   671
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   672
apply (rule equalityI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   673
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   674
apply (erule analz.induct)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   675
apply (metis UnCI UnE Un_commute analz.Inj)
35095
6cdf9bbd0342 minor metis proof tuning
haftmann
parents: 35054
diff changeset
   676
apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
6cdf9bbd0342 minor metis proof tuning
haftmann
parents: 35054
diff changeset
   677
apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   678
apply (blast intro: analz.Decrypt)
24759
b448f94b1c88 fixed metis proof (Why did it stop working?);
wenzelm
parents: 23755
diff changeset
   679
apply blast
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   680
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   681
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   682
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   683
proof -
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   684
  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   685
    by (metis Un_commute analz_synth_Un)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   686
  hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   687
    by (metis UN_extend_simps(3))
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   688
  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   689
    by (metis UN_extend_simps(3))
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   690
  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   691
    by (metis Un_commute)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   692
  thus "analz (synth H) = analz H \<union> synth H" by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   693
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   694
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   695
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   696
subsubsection{*For reasoning about the Fake rule in traces *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   697
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   698
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   699
proof -
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   700
  assume "X \<in> G"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   701
  hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   702
  hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   703
    by (metis Un_upper2)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   704
  hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   705
  hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   706
    by (metis parts_mono)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   707
  thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   708
    by (metis parts_Un)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   709
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   710
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   711
lemma Fake_parts_insert:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   712
     "X \<in> synth (analz H) ==>  
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   713
      parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   714
sledgehammer
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   715
proof -
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   716
  assume A1: "X \<in> synth (analz H)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   717
  have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   718
    by (metis analz_idem analz_synth)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   719
  have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   720
    by (metis parts_analz parts_synth)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   721
  have F3: "synth (analz H) X" using A1 by (metis mem_def)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   722
  have "\<forall>x\<^isub>2 x\<^isub>1\<Colon>msg set. x\<^isub>1 \<le> sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3))
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   723
  hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   724
  have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   725
  have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   726
         \<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   727
    using F1 by (metis subset_Un_eq)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   728
  hence F6: "\<forall>x\<^isub>1. analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   729
    by (metis synth_increasing)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   730
  have "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" using F4 by (metis analz_subset_iff)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   731
  hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth (analz x\<^isub>1))" by (metis analz_subset_iff)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   732
  hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)" using F6 by metis
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   733
  hence "H \<subseteq> synth (analz H)" by metis
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   734
  hence "H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)" using F5 by metis
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   735
  hence "insert X H \<subseteq> synth (analz H)" by (metis insert_subset)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   736
  hence "parts (insert X H) \<subseteq> parts (synth (analz H))" by (metis parts_mono)
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   737
  hence "parts (insert X H) \<subseteq> parts H \<union> synth (analz H)" using F2 by metis
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   738
  thus "parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" by (metis Un_commute)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   739
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   740
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   741
lemma Fake_parts_insert_in_Un:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   742
     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   743
      ==> Z \<in>  synth (analz H) \<union> parts H";
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   744
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   745
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   746
declare analz_mono [intro] synth_mono [intro] 
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   747
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   748
lemma Fake_analz_insert:
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   749
     "X \<in> synth (analz G) ==>
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   750
      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   751
by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   752
          analz_mono analz_synth_Un insert_absorb)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   753
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   754
(* Simpler problems?  BUT METIS CAN'T PROVE THE LAST STEP
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   755
lemma Fake_analz_insert_simpler:
36553
95bdfa572cee redo some of the metis proofs
blanchet
parents: 35416
diff changeset
   756
     "X \<in> synth (analz G) ==>  
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   757
      analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   758
apply (rule subsetI)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   759
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   760
apply (metis Un_commute analz_analz_Un analz_synth_Un)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   761
apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   762
done
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   763
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   764
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   765
end