100 |
100 |
101 |
101 |
102 text{*This ML code does the inductions directly.*} |
102 text{*This ML code does the inductions directly.*} |
103 ML{* |
103 ML{* |
104 fun ns_constrains_tac ctxt i = |
104 fun ns_constrains_tac ctxt i = |
105 let |
105 SELECT_GOAL |
106 val cs = claset_of ctxt; |
106 (EVERY |
107 val ss = simpset_of ctxt; |
107 [REPEAT (etac @{thm Always_ConstrainsI} 1), |
108 in |
108 REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), |
109 SELECT_GOAL |
109 rtac @{thm ns_constrainsI} 1, |
110 (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1), |
110 full_simp_tac (simpset_of ctxt) 1, |
111 REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, |
111 REPEAT (FIRSTGOAL (etac disjE)), |
112 @{thm constrains_imp_Constrains}] 1), |
112 ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])), |
113 rtac @{thm ns_constrainsI} 1, |
113 REPEAT (FIRSTGOAL analz_mono_contra_tac), |
114 full_simp_tac ss 1, |
114 ALLGOALS (asm_simp_tac (simpset_of ctxt))]) i; |
115 REPEAT (FIRSTGOAL (etac disjE)), |
|
116 ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])), |
|
117 REPEAT (FIRSTGOAL analz_mono_contra_tac), |
|
118 ALLGOALS (asm_simp_tac ss)]) i |
|
119 end; |
|
120 |
115 |
121 (*Tactic for proving secrecy theorems*) |
116 (*Tactic for proving secrecy theorems*) |
122 fun ns_induct_tac ctxt = |
117 fun ns_induct_tac ctxt = |
123 let |
118 (SELECT_GOAL o EVERY) |
124 val cs = claset_of ctxt; |
119 [rtac @{thm AlwaysI} 1, |
125 val ss = simpset_of ctxt; |
120 force_tac ctxt 1, |
126 in |
121 (*"reachable" gets in here*) |
127 (SELECT_GOAL o EVERY) |
122 rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1, |
128 [rtac @{thm AlwaysI} 1, |
123 ns_constrains_tac ctxt 1]; |
129 force_tac (cs,ss) 1, |
|
130 (*"reachable" gets in here*) |
|
131 rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1, |
|
132 ns_constrains_tac ctxt 1] |
|
133 end; |
|
134 *} |
124 *} |
135 |
125 |
136 method_setup ns_induct = {* |
126 method_setup ns_induct = {* |
137 Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *} |
127 Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *} |
138 "for inductive reasoning about the Needham-Schroeder protocol" |
128 "for inductive reasoning about the Needham-Schroeder protocol" |