src/HOL/Auth/Event.thy
changeset 27225 b316dde851f5
parent 27154 026f3db3f5c6
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Auth/Event.thy	Mon Jun 16 14:18:55 2008 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Mon Jun 16 17:54:35 2008 +0200
     1.3 @@ -278,16 +278,14 @@
     1.4      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
     1.5  
     1.6  
     1.7 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
     1.8 +
     1.9  ML
    1.10  {*
    1.11  val analz_mono_contra_tac = 
    1.12 -  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.13 -  in
    1.14 -    rtac analz_impI THEN' 
    1.15 -    REPEAT1 o 
    1.16 -      (dresolve_tac @{thms analz_mono_contra})
    1.17 -    THEN' mp_tac
    1.18 -  end
    1.19 +  rtac @{thm analz_impI} THEN' 
    1.20 +  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
    1.21 +  THEN' mp_tac
    1.22  *}
    1.23  
    1.24  method_setup analz_mono_contra = {*
    1.25 @@ -296,20 +294,19 @@
    1.26  
    1.27  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.28  
    1.29 +lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
    1.30 +
    1.31  ML
    1.32  {*
    1.33  val synth_analz_mono_contra_tac = 
    1.34 -  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.35 -  in
    1.36 -    rtac syan_impI THEN' 
    1.37 -    REPEAT1 o 
    1.38 -      (dresolve_tac 
    1.39 -       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.40 -       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.41 -       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.42 -    THEN'
    1.43 -    mp_tac
    1.44 -  end;
    1.45 +  rtac @{thm syan_impI} THEN'
    1.46 +  REPEAT1 o 
    1.47 +    (dresolve_tac 
    1.48 +     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.49 +      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.50 +      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.51 +  THEN'
    1.52 +  mp_tac
    1.53  *}
    1.54  
    1.55  method_setup synth_analz_mono_contra = {*