tidying of HOL/Auth esp Guard lemmas
authorpaulson
Sun Dec 21 18:39:27 2003 +0100 (2003-12-21)
changeset 143071cbc24648cf7
parent 14306 1d40d90398eb
child 14308 c0489217deb2
tidying of HOL/Auth esp Guard lemmas
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Auth/ROOT.ML
     1.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Sun Dec 21 08:27:44 2003 +0100
     1.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Sun Dec 21 18:39:27 2003 +0100
     1.3 @@ -13,25 +13,11 @@
     1.4  
     1.5  theory Extensions = Event:
     1.6  
     1.7 -declare  insert_Diff_single [simp del]
     1.8 -
     1.9  subsection{*Extensions to Theory @{text Set}*}
    1.10  
    1.11  lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B"
    1.12  by auto
    1.13  
    1.14 -lemma Un_eq: "[| A=A'; B=B' |] ==> A Un B = A' Un B'"
    1.15 -by auto
    1.16 -
    1.17 -lemma insert_absorb_substI: "[| x:A; P (insert x A) |] ==> P A"
    1.18 -by (simp add: insert_absorb)
    1.19 -
    1.20 -lemma insert_Diff_substD: "[| x:A; P A |] ==> P (insert x (A - {x}))"
    1.21 -by (simp add: insert_Diff)
    1.22 -
    1.23 -lemma insert_Diff_substI: "[| x:A; P (insert x (A - {x})) |] ==> P A"
    1.24 -by (simp add: insert_Diff)
    1.25 -
    1.26  lemma insert_Un: "P ({x} Un A) ==> P (insert x A)"
    1.27  by simp
    1.28  
    1.29 @@ -201,11 +187,9 @@
    1.30  
    1.31  lemmas insert_commute_substI = insert_commute [THEN ssubst]
    1.32  
    1.33 -lemma analz_insertD: "[| Crypt K Y:H; Key (invKey K):H |]
    1.34 -==> analz (insert Y H) = analz H"
    1.35 -apply (rule_tac x="Crypt K Y" and P="%H. analz (insert Y H) = analz H"
    1.36 -in insert_absorb_substI, simp)
    1.37 -by (rule_tac insert_commute_substI, simp)
    1.38 +lemma analz_insertD:
    1.39 +     "[| Crypt K Y:H; Key (invKey K):H |] ==> analz (insert Y H) = analz H"
    1.40 +by (blast intro: analz.Decrypt analz_insert_eq)  
    1.41  
    1.42  lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==>
    1.43  X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)"
    1.44 @@ -367,19 +351,22 @@
    1.45  consts knows' :: "agent => event list => msg set"
    1.46  
    1.47  primrec
    1.48 -"knows' A [] = {}"
    1.49 -"knows' A (ev # evs) = (
    1.50 -  if A = Spy then (
    1.51 -    case ev of
    1.52 -      Says A' B X => insert X (knows' A evs)
    1.53 -    | Gets A' X => knows' A evs
    1.54 -    | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
    1.55 -  ) else (
    1.56 -    case ev of
    1.57 -      Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.58 -    | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.59 -    | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.60 -  ))"
    1.61 +knows'_Nil:
    1.62 + "knows' A [] = {}"
    1.63 +
    1.64 +knows'_Cons0:
    1.65 + "knows' A (ev # evs) = (
    1.66 +   if A = Spy then (
    1.67 +     case ev of
    1.68 +       Says A' B X => insert X (knows' A evs)
    1.69 +     | Gets A' X => knows' A evs
    1.70 +     | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
    1.71 +   ) else (
    1.72 +     case ev of
    1.73 +       Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.74 +     | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.75 +     | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    1.76 +   ))"
    1.77  
    1.78  translations "spies" == "knows Spy"
    1.79  
    1.80 @@ -408,7 +395,10 @@
    1.81  Un knows A evs"
    1.82  apply (simp only: knows_decomp)
    1.83  apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans)
    1.84 -by (rule Un_eq, rule knows'_Cons, simp, blast)
    1.85 +apply (simp only: knows'_Cons [of A ev evs] Un_ac)
    1.86 +apply blast
    1.87 +done
    1.88 +
    1.89  
    1.90  lemmas knows_Cons_substI = knows_Cons [THEN ssubst]
    1.91  lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst]
     2.1 --- a/src/HOL/Auth/Guard/Guard.thy	Sun Dec 21 08:27:44 2003 +0100
     2.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Sun Dec 21 18:39:27 2003 +0100
     2.3 @@ -168,10 +168,10 @@
     2.4  
     2.5  lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
     2.6  ==> Nonce n:analz (decrypt H K Y)"
     2.7 -by (drule_tac P="%H. Nonce n:analz H" in insert_Diff_substD, simp_all)
     2.8 -
     2.9 -lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)"
    2.10 -by auto
    2.11 +apply (drule_tac P="%H. Nonce n:analz H" in ssubst [OF insert_Diff])
    2.12 +apply assumption
    2.13 +apply (simp only: analz_Crypt_if, simp)
    2.14 +done
    2.15  
    2.16  lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
    2.17  by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
     3.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Sun Dec 21 08:27:44 2003 +0100
     3.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Dec 21 18:39:27 2003 +0100
     3.3 @@ -164,10 +164,10 @@
     3.4  
     3.5  lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
     3.6  ==> Key n:analz (decrypt H K Y)"
     3.7 -by (drule_tac P="%H. Key n:analz H" in insert_Diff_substD, simp_all)
     3.8 -
     3.9 -lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)"
    3.10 -by auto
    3.11 +apply (drule_tac P="%H. Key n:analz H" in ssubst [OF insert_Diff])
    3.12 +apply assumption 
    3.13 +apply (simp only: analz_Crypt_if, simp)
    3.14 +done
    3.15  
    3.16  lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
    3.17  by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
     4.1 --- a/src/HOL/Auth/ROOT.ML	Sun Dec 21 08:27:44 2003 +0100
     4.2 +++ b/src/HOL/Auth/ROOT.ML	Sun Dec 21 18:39:27 2003 +0100
     4.3 @@ -6,7 +6,6 @@
     4.4  Root file for protocol proofs.
     4.5  *)
     4.6  
     4.7 -goals_limit := 1;
     4.8  set timing;
     4.9  
    4.10  (*Shared-key protocols*)
    4.11 @@ -23,7 +22,6 @@
    4.12  time_use_thy "Yahalom_Bad";
    4.13  time_use_thy "ZhouGollmann";
    4.14  
    4.15 -
    4.16  (*Public-key protocols*)
    4.17  time_use_thy "NS_Public_Bad";
    4.18  time_use_thy "NS_Public";