equal
deleted
inserted
replaced
749 (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN |
749 (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN |
750 (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN |
750 (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN |
751 (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN |
751 (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN |
752 (*Base*) (force_tac ctxt) 1 |
752 (*Base*) (force_tac ctxt) 1 |
753 |
753 |
754 val analz_prepare_tac = |
754 fun analz_prepare_tac ctxt = |
755 prepare_tac THEN |
755 prepare_tac THEN |
756 dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN |
756 dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN |
757 (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN |
757 (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN |
758 REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac) |
758 REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt) |
759 |
759 |
760 end |
760 end |
761 *} |
761 *} |
762 |
762 |
763 method_setup prepare = {* |
763 method_setup prepare = {* |
767 method_setup parts_prepare = {* |
767 method_setup parts_prepare = {* |
768 Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} |
768 Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} |
769 "additional facts to reason about parts" |
769 "additional facts to reason about parts" |
770 |
770 |
771 method_setup analz_prepare = {* |
771 method_setup analz_prepare = {* |
772 Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *} |
772 Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.analz_prepare_tac ctxt)) *} |
773 "additional facts to reason about analz" |
773 "additional facts to reason about analz" |
774 |
774 |
775 |
775 |
776 (*Treatment of pins is here for completeness. This protocol doesn't use pins*) |
776 (*Treatment of pins is here for completeness. This protocol doesn't use pins*) |
777 lemma Spy_parts_keys [simp]: "evs \<in> sr \<Longrightarrow> |
777 lemma Spy_parts_keys [simp]: "evs \<in> sr \<Longrightarrow> |