# HG changeset patch
# User paulson
# Date 1072028367 -3600
# Node ID 1cbc24648cf71f555cadf7ed85f91436bd847b33
# Parent  1d40d90398eb89bbf82bf0654748b8574a803c8b
tidying of HOL/Auth esp Guard lemmas

diff -r 1d40d90398eb -r 1cbc24648cf7 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Sun Dec 21 08:27:44 2003 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Sun Dec 21 18:39:27 2003 +0100
@@ -13,25 +13,11 @@
 
 theory Extensions = Event:
 
-declare  insert_Diff_single [simp del]
-
 subsection{*Extensions to Theory @{text Set}*}
 
 lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B"
 by auto
 
-lemma Un_eq: "[| A=A'; B=B' |] ==> A Un B = A' Un B'"
-by auto
-
-lemma insert_absorb_substI: "[| x:A; P (insert x A) |] ==> P A"
-by (simp add: insert_absorb)
-
-lemma insert_Diff_substD: "[| x:A; P A |] ==> P (insert x (A - {x}))"
-by (simp add: insert_Diff)
-
-lemma insert_Diff_substI: "[| x:A; P (insert x (A - {x})) |] ==> P A"
-by (simp add: insert_Diff)
-
 lemma insert_Un: "P ({x} Un A) ==> P (insert x A)"
 by simp
 
@@ -201,11 +187,9 @@
 
 lemmas insert_commute_substI = insert_commute [THEN ssubst]
 
-lemma analz_insertD: "[| Crypt K Y:H; Key (invKey K):H |]
-==> analz (insert Y H) = analz H"
-apply (rule_tac x="Crypt K Y" and P="%H. analz (insert Y H) = analz H"
-in insert_absorb_substI, simp)
-by (rule_tac insert_commute_substI, simp)
+lemma analz_insertD:
+     "[| Crypt K Y:H; Key (invKey K):H |] ==> analz (insert Y H) = analz H"
+by (blast intro: analz.Decrypt analz_insert_eq)  
 
 lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==>
 X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)"
@@ -367,19 +351,22 @@
 consts knows' :: "agent => event list => msg set"
 
 primrec
-"knows' A [] = {}"
-"knows' A (ev # evs) = (
-  if A = Spy then (
-    case ev of
-      Says A' B X => insert X (knows' A evs)
-    | Gets A' X => knows' A evs
-    | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
-  ) else (
-    case ev of
-      Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
-    | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs
-    | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
-  ))"
+knows'_Nil:
+ "knows' A [] = {}"
+
+knows'_Cons0:
+ "knows' A (ev # evs) = (
+   if A = Spy then (
+     case ev of
+       Says A' B X => insert X (knows' A evs)
+     | Gets A' X => knows' A evs
+     | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
+   ) else (
+     case ev of
+       Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
+     | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs
+     | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
+   ))"
 
 translations "spies" == "knows Spy"
 
@@ -408,7 +395,10 @@
 Un knows A evs"
 apply (simp only: knows_decomp)
 apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans)
-by (rule Un_eq, rule knows'_Cons, simp, blast)
+apply (simp only: knows'_Cons [of A ev evs] Un_ac)
+apply blast
+done
+
 
 lemmas knows_Cons_substI = knows_Cons [THEN ssubst]
 lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst]
diff -r 1d40d90398eb -r 1cbc24648cf7 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Sun Dec 21 08:27:44 2003 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy	Sun Dec 21 18:39:27 2003 +0100
@@ -168,10 +168,10 @@
 
 lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
 ==> Nonce n:analz (decrypt H K Y)"
-by (drule_tac P="%H. Nonce n:analz H" in insert_Diff_substD, simp_all)
-
-lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)"
-by auto
+apply (drule_tac P="%H. Nonce n:analz H" in ssubst [OF insert_Diff])
+apply assumption
+apply (simp only: analz_Crypt_if, simp)
+done
 
 lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
 by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
diff -r 1d40d90398eb -r 1cbc24648cf7 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Sun Dec 21 08:27:44 2003 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Dec 21 18:39:27 2003 +0100
@@ -164,10 +164,10 @@
 
 lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
 ==> Key n:analz (decrypt H K Y)"
-by (drule_tac P="%H. Key n:analz H" in insert_Diff_substD, simp_all)
-
-lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)"
-by auto
+apply (drule_tac P="%H. Key n:analz H" in ssubst [OF insert_Diff])
+apply assumption 
+apply (simp only: analz_Crypt_if, simp)
+done
 
 lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
 by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
diff -r 1d40d90398eb -r 1cbc24648cf7 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Sun Dec 21 08:27:44 2003 +0100
+++ b/src/HOL/Auth/ROOT.ML	Sun Dec 21 18:39:27 2003 +0100
@@ -6,7 +6,6 @@
 Root file for protocol proofs.
 *)
 
-goals_limit := 1;
 set timing;
 
 (*Shared-key protocols*)
@@ -23,7 +22,6 @@
 time_use_thy "Yahalom_Bad";
 time_use_thy "ZhouGollmann";
 
-
 (*Public-key protocols*)
 time_use_thy "NS_Public_Bad";
 time_use_thy "NS_Public";