src/HOL/Auth/Event.thy
changeset 24122 fc7f857d33c8
parent 21588 cd0dc678a205
child 27154 026f3db3f5c6
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Aug 01 19:59:12 2007 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Aug 01 20:25:16 2007 +0200
     1.3 @@ -258,18 +258,6 @@
     1.4         knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
     1.5         knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 -val analz_mono_contra_tac = 
    1.10 -  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.11 -  in
    1.12 -    rtac analz_impI THEN' 
    1.13 -    REPEAT1 o 
    1.14 -      (dresolve_tac (thms"analz_mono_contra"))
    1.15 -    THEN' mp_tac
    1.16 -  end
    1.17 -*}
    1.18 -
    1.19  
    1.20  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    1.21  by (induct e, auto simp: knows_Cons)
    1.22 @@ -289,6 +277,19 @@
    1.23             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.24      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
    1.25  
    1.26 +
    1.27 +ML
    1.28 +{*
    1.29 +val analz_mono_contra_tac = 
    1.30 +  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.31 +  in
    1.32 +    rtac analz_impI THEN' 
    1.33 +    REPEAT1 o 
    1.34 +      (dresolve_tac @{thms analz_mono_contra})
    1.35 +    THEN' mp_tac
    1.36 +  end
    1.37 +*}
    1.38 +
    1.39  method_setup analz_mono_contra = {*
    1.40      Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    1.41      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.42 @@ -297,51 +298,15 @@
    1.43  
    1.44  ML
    1.45  {*
    1.46 -val knows_Cons     = thm "knows_Cons"
    1.47 -val used_Nil       = thm "used_Nil"
    1.48 -val used_Cons      = thm "used_Cons"
    1.49 -
    1.50 -val Notes_imp_used = thm "Notes_imp_used";
    1.51 -val Says_imp_used = thm "Says_imp_used";
    1.52 -val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
    1.53 -val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
    1.54 -val knows_Spy_partsEs = thms "knows_Spy_partsEs";
    1.55 -val spies_partsEs = thms "spies_partsEs";
    1.56 -val Says_imp_spies = thm "Says_imp_spies";
    1.57 -val parts_insert_spies = thm "parts_insert_spies";
    1.58 -val Says_imp_knows = thm "Says_imp_knows";
    1.59 -val Notes_imp_knows = thm "Notes_imp_knows";
    1.60 -val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
    1.61 -val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
    1.62 -val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
    1.63 -val usedI = thm "usedI";
    1.64 -val initState_into_used = thm "initState_into_used";
    1.65 -val used_Says = thm "used_Says";
    1.66 -val used_Notes = thm "used_Notes";
    1.67 -val used_Gets = thm "used_Gets";
    1.68 -val used_nil_subset = thm "used_nil_subset";
    1.69 -val analz_mono_contra = thms "analz_mono_contra";
    1.70 -val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
    1.71 -val initState_subset_knows = thm "initState_subset_knows";
    1.72 -val keysFor_parts_insert = thm "keysFor_parts_insert";
    1.73 -
    1.74 -
    1.75 -val synth_analz_mono = thm "synth_analz_mono";
    1.76 -
    1.77 -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
    1.78 -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
    1.79 -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
    1.80 -
    1.81 -
    1.82  val synth_analz_mono_contra_tac = 
    1.83    let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.84    in
    1.85      rtac syan_impI THEN' 
    1.86      REPEAT1 o 
    1.87        (dresolve_tac 
    1.88 -       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
    1.89 -        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
    1.90 -	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
    1.91 +       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.92 +       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.93 +       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.94      THEN'
    1.95      mp_tac
    1.96    end;