structure Spi_Redns = struct val thy = the_context () end ; val _ = use_legacy_bindings Spi_Redns.thy ; val tmk = InductivePackage.the_mk_cases Spi_Redns.thy ; val oth_red_mkc = tmk "Spi_Redns.oth_red" ; val oth_red_emptyE = oth_red_mkc "(x, {}) : oth_red" ; val oth_red_alt_mkc = tmk "Spi_Redns.oth_red_alt" ; val oth_red_alt_emptyE = oth_red_alt_mkc "(x, {}) : oth_red_alt" ; AddSEs [oth_red_emptyE, oth_red_alt_emptyE] ; val wfp_induct_pair = induct_inst_g [("xa", "(?G, ?Ss)"), ("P", "split ?Q")] wfp.induct ; val _ = qed_goal_spec_mp "oth_red_rev" Spi_Redns.thy "((G', G) : oth_red) --> ((rev_pair ` G', rev_pair ` G) : oth_red)" (fn _ => [ (safe_tac (ces [oth_red.elims])) , (ALLGOALS (EVERY' [Simp_tac, (resolve_tac oth_red.intros), (simp_tac (esimps [in_rp])) ])), (dtac indist_rev 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "oth_red_rtc_rev" Spi_Redns.thy "((G', G) : oth_red^*) --> ((rev_pair ` G', rev_pair ` G) : oth_red^*)" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), (rtac rtrancl_refl 1), (etac tct.rsr 1), (etac oth_red_rev 1) ]) ; val _ = qed_goal "oth_red_rev_iff" Spi_Redns.thy "((rev_pair ` G', rev_pair ` G) : oth_red) = ((G', G) : oth_red)" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac oth_red_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goal "oth_red_rev_iff_alt" Spi_Redns.thy "((rev_pair ` G', G) : oth_red) = ((G', rev_pair ` G) : oth_red)" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac oth_red_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goalw "rsmin_or_rev_iff" Spi_Redns.thy [rsmin_def] "(rev_pair ` G : rsmin oth_red UNIV) = (G : rsmin oth_red UNIV)" (fn _ => [ Clarsimp_tac 1, Safe_tac, (ALLGOALS (dtac oth_red_rev THEN' Force_tac)) ]) ; (** reduction of observer theories **) val _ = qed_goal "orkvs_orar" Spi_Redns.thy "(EX Vs. ((H, Vs), G) : orkvs & Ball Vs is_der_virt) = \ \ ((H, G) : oth_red_altr)" (fn _ => [ (safe_tac (ces ([orkvs.elims, oth_red_altr.elims] @ oth_red_altr.intros))), (TRYALL (dresolve_tac orkvs.intros)), (TRYALL (force_tac (cesimps [idv_Enc_equiv]))) ]) ; val _ = qed_goal "orkvs_or" Spi_Redns.thy "(EX Vs. ((H, Vs), G) : orkvs & Vs <= indist) = ((H, G) : oth_red)" (fn _ => [ (safe_tac (ces ([orkvs.elims, oth_red.elims] @ oth_red.intros))), Fast_tac 1, (REPEAT_FIRST (resolve_tac [exI, conjI])), (TRYALL (eresolve_tac orkvs.intros)), TRYALL Fast_tac ]) ; val orkvsD = tacsthm [rtac exI 1, rtac conjI 1] (orkvs_orar RS iffD1) ; val oth_red_altrE = tacthm (etac conjE 2) (orkvs_orar RS iffD2 RS exE) ; val _ = qed_goal_spec_mp "orkvs_k" Spi_Redns.thy "((H, Vs), G) : orkvs --> (H, G) : oth_red_k UNIV" (fn _ => [ (safe_tac (ces [orkvs.elims])), (ALLGOALS (eresolve_tac oth_red_k.intros)), rtac UNIV_I 1 ]) ; val _ = qed_goal_spec_mp "orkvss_k" Spi_Redns.thy "((H, Vs), (G, Us)) : orkvss --> (H, G) : oth_red_k UNIV" (fn _ => [ (safe_tac (ces [orkvss.elims, orkvs_k])) ]) ; val _ = qed_goal_spec_mp "orkvss_k_rtc" Spi_Redns.thy "((H, Vs), (G, Us)) : orkvss^* --> (H, G) : (oth_red_k UNIV)^*" (fn _ => [ rtac impI 1, etac rtip 1, Simp_tac 1, (fast_tac (ces [orkvss_k, tct.rsr]) 1) ]) ; val _ = qed_goal "oth_red_k" Spi_Redns.thy "oth_red_k UNIV >= oth_red" (fn _ => [ (safe_tac (ces [oth_red.elims])), (etac oth_red_k.plI 1), (etac oth_red_k.elI 1), rtac UNIV_I 1 ]) ; val _ = qed_goal "oth_red_alt" Spi_Redns.thy "oth_red_alt <= oth_red" (fn _ => [ (safe_tac (ces [oth_red_alt.elims])), (etac oth_red.plI 1), (etac oth_red.elI 1), (etac indist_wki 1) ]) ; val _ = qed_goal "oth_red_nkr" Spi_Redns.thy "oth_red_nkr <= oth_red_nk" (fn _ => [ (safe_tac (ces [oth_red_nkr.elims])), (etac oth_red_nk.plI 1), (etac oth_red_nk.elI 1), (etac virt_indist 1) ]) ; val _ = qed_goal "oth_red_altr" Spi_Redns.thy "oth_red_altr <= oth_red_alt" (fn _ => [ (safe_tac (ces [oth_red_altr.elims])), (etac oth_red_alt.plI 1), (etac oth_red_alt.elI 1), (etac virt_indist 1) ]) ; val _ = bind_thm ("oth_red_altr'", [oth_red_altr, oth_red_alt] MRS subset_trans) ; val oth_red_alt_rtc = oth_red_alt RS rtrancl_mono ; val oth_red_altr_rtc = oth_red_altr RS rtrancl_mono ; val oth_red_altr_rtc' = oth_red_altr' RS rtrancl_mono ; val _ = qed_goal_spec_mp "oth_red_alt_finite_iff" Spi_Redns.thy "(dtn, x) : oth_red_alt --> finite x = finite dtn" (fn _ => [ (strip_tac 1), (etac oth_red_alt.elims 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_alt_finite_rtc_iff" Spi_Redns.thy "(dtn, x) : oth_red_alt^* --> finite x = finite dtn" (fn _ => [ strip_tac 1, (etac converse_rtrancl_induct 1), (rtac refl 1), (dtac oth_red_alt_finite_iff 1), Clarsimp_tac 1 ]) ; val oth_red_alt_finite_rtc = oth_red_alt_finite_rtc_iff RS iffD1 ; val _ = qed_goal_spec_mp "oth_red_nk_finite_iff" Spi_Redns.thy "(dtn, x) : oth_red_nk --> finite x = finite dtn" (fn _ => [ (strip_tac 1), (etac oth_red_nk.elims 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_nk_finite_rtc_iff" Spi_Redns.thy "(dtn, x) : oth_red_nk^* --> finite x = finite dtn" (fn _ => [ strip_tac 1, (etac converse_rtrancl_induct 1), (rtac refl 1), (dtac oth_red_nk_finite_iff 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "oth_red_k_finite_iff" Spi_Redns.thy "(dtn, x) : oth_red_k K --> finite x = finite dtn" (fn _ => [ (strip_tac 1), (etac oth_red_k.elims 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_k_finite_rtc_iff" Spi_Redns.thy "(dtn, x) : (oth_red_k K)^* --> finite x = finite dtn" (fn _ => [ strip_tac 1, (etac converse_rtrancl_induct 1), (rtac refl 1), (dtac oth_red_k_finite_iff 1), Clarsimp_tac 1 ]) ; val oth_red_k_finite_rtc = oth_red_k_finite_rtc_iff RS iffD1 ; val _ = qed_goal_spec_mp "orkvs_finite_iff" Spi_Redns.thy "((H, Vs), G) : orkvs --> finite G = finite H" (fn _ => [ (strip_tac 1), (etac orkvs.elims 1), Auto_tac ]) ; (* easy proofs that oth_red_altr (sim oth_red_nkr) are wf because size of theory reduces *) val _ = qed_goal_spec_mp "wfp_oth_red_altr'" Spi_Redns.thy "c : wfp (measure (setsum (size o fst))) --> finite c --> \ \ c : wfp oth_red_altr" (fn _ => [ rtac impI 1, (etac wfp.induct 1), Clarify_tac 1, (rtac wfp.wfpI 1), Clarify_tac 1, (etac allE 1), (etac impE 1), (datac (oth_red_altr RS subsetD RS oth_red_alt_finite_iff RS iffD1) 1 2), Fast_tac 2, (etac oth_red_altr.elims 1), (TRYALL (force_tac (cis [setsum_insert2_le RSN (2, xt7)], esimps [measure_def, inv_image_def]))) ]) ; val wfp_oth_red_altr = wf_measure RS wf_ssI RS wfp_oth_red_altr' ; (* reduction doesn't change indistinguishability *) val red_nc_alt' = prove_goal Spi_Redns.thy "(oia, oib) : oth_red --> \ \ (ALL MN. ((oia, MN) : indist_alt) = ((oib, MN) : indist_alt))" (fn _ => [ (safe_tac (ces [oth_red.elims])), (etac indist_alt.plI 1), (etac (mk_alt pl_inv') 1), (fold_goals_tac [indist_alt]), (etac (insertI1 RS mk_alt indist.elI) 1), (etac (mk_alt indist_wk) 1), Fast_tac 1, (etac (mk_alt el_inv') 1) ]) RS mp ; val red_nc' = dest_alt red_nc_alt' ; val _ = bind_thm ("red_nc_alt", red_nc_alt' RS spec) ; val _ = bind_thm ("red_nc", dest_alt red_nc_alt) ; (* Tiu, Lemma 15 *) (* orkvs_idv_nc, orkvss_idv_nc have generalisations to substitution proved as subst_orkvs_idv_nc, subst_orkvss_idv_nc, also, stronger result subst_orkvs_iff *) val _ = bind_thm ("orkvs_orarI", conjI RS (exI RS (orkvs_orar RS iffD1))) ; val _ = bind_thm ("orkvs_orI", conjI RS (exI RS (orkvs_or RS iffD1))) ; val _ = bind_thm ("orkvs_oth_red", [oth_red_altr', orkvs_orarI] MRS subsetD) ; val _ = bind_thm ("orkvs_indist_nc", orkvs_orI RS red_nc) ; val _ = bind_thm ("orkvs_idv_nc", orkvs_oth_red RS red_nc) ; val _ = qed_goal_spec_mp "orkvss_oth_red" Spi_Redns.thy "((D, Vs), (C, Us)) : orkvss --> Ball Vs is_der_virt --> (D, C) : oth_red" (fn _ => [ (clarify_tac (ces [orkvss.elims]) 1), (etac orkvs_oth_red 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_indist_nc" Spi_Redns.thy "((D, Vs), (C, Us)) : orkvss --> Vs <= indist --> \ \ ((D, x) : indist) = ((C, x) : indist)" (fn _ => [ (clarify_tac (ces [orkvss.elims]) 1), (etac orkvs_indist_nc 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_idv_nc" Spi_Redns.thy "((D, Vs), (C, Us)) : orkvss --> Ball Vs is_der_virt --> \ \ ((D, x) : indist) = ((C, x) : indist)" (fn _ => [ (clarify_tac (ces [orkvss.elims]) 1), (etac orkvs_idv_nc 1), Fast_tac 1 ]) ; (* similarly a one-way result without assuming side constraints derivable *) val _ = qed_goal_spec_mp "orkvs_indist" Spi_Redns.thy "((H, Vs), G) : orkvs --> (G, MN) : indist --> (H, MN) : indist" (fn _ => [ (safe_tac (ces [orkvs.elims])), (ALLGOALS (EVERY' [(etac indist_ca1), rtac insert_mono, Fast_tac])), (rtac indist.erI 2), (rtac indist.prI 1), (ALLGOALS (rtac indist.id)), TRYALL Fast_tac ]) ; val _ = qed_goal_spec_mp "red_nc_rtc" Spi_Redns.thy "(oia, oib) : oth_red^* --> ((oia, MN) : indist) = ((oib, MN) : indist)" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), rtac refl 1, (etac trans 1), (etac red_nc 1) ]) ; val red_nk_nc_alt' = prove_goal Spi_Redns.thy "(G', G) : oth_red_nk --> \ \ (ALL MN. ((G', MN) : indist_nk_alt) = ((G, MN) : indist_nk_alt))" (fn _ => [ (safe_tac (ces [oth_red_nk.elims])), (etac indist_nk_alt.plI 1), (etac (mk_nk (mk_alt pl_inv')) 1), (fold_goals_tac [indist_nk_alt, indist_nk]), (eatac indist_nk_alt.elI 1 1), (rewrite_goals_tac [indist_nk_alt, indist_nk]), (dtac el_inv' 1), (etac indist_ca1 1), Fast_tac 1, (etac indist_wki 1) ]) RS mp ; val red_nk_nc' = dest_nk (dest_alt red_nk_nc_alt') ; val _ = bind_thm ("red_nk_nc_alt", red_nk_nc_alt' RS spec) ; val _ = bind_thm ("red_nk_nc", dest_nk (dest_alt red_nk_nc_alt)) ; val _ = bind_thm ("red_nkr_nc", oth_red_nkr RS subsetD RS red_nk_nc) ; val _ = qed_goal_spec_mp "red_nk_nc_rtc" Spi_Redns.thy "(G', G) : oth_red_nk^* --> ((G', MN) : indist) = ((G, MN) : indist)" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), rtac refl 1, (etac trans 1), (etac red_nk_nc 1) ]) ; val _ = qed_goal_spec_mp "red_nkr_idv_nc" Spi_Redns.thy "(G', G) : oth_red_nkr --> is_der_virt (G, MN) --> is_der_virt (G', MN)" (fn _ => [ (safe_tac (ces [oth_red_nkr.elims])), (etac idv_ca1 1), Fast_tac 1, Simp_tac 1, (fast_tac (cis [is_der_virt_id]) 1), (etac idv_ca1 1), Fast_tac 1, Simp_tac 1, Safe_tac, (etac notE 1 THEN etac idv_wki 1) ]) ; val _ = qed_goal_spec_mp "oth_red_k_ks" Spi_Redns.thy "(ALL ks : K. (oth, ks) : indist) --> \ \ (oth', oth) : oth_red_k K --> (oth', oth) : oth_red" (fn _ => [ (safe_tac (ces [oth_red_k.elims])), (etac oth_red.plI 1), (etac oth_red.elI 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "oth_red_k_ks_eq" Spi_Redns.thy "K = {k. (oth, k) : indist} --> \ \ ((oth', oth) : oth_red_k K) = ((oth', oth) : oth_red)" (fn _ => [ (safe_tac (ces [oth_red_k.elims, oth_red.elims])), (etac oth_red.plI 1), (etac oth_red.elI 1), Fast_tac 1, (etac oth_red_k.plI 1), (etac oth_red_k.elI 1), Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "oth_red_k_ks_rtc" Spi_Redns.thy "(ALL ks : K. (oth, ks) : indist) --> \ \ (oth', oth) : (oth_red_k K)^* --> (oth', oth) : oth_red^*" (fn _ => [ strip_tac 1, (etac converse_rtrancl_induct 1), Fast_tac 1, (rtac tct.srr 1), atac 2, (rtac oth_red_k_ks 1), atac 2, (etac ball_match 1), (eatac (red_nc_rtc RS iffD2) 1 1) ]) ; val _ = qed_goal_spec_mp "oth_red_k_ks_rtc_eq" Spi_Redns.thy "K = {k. (oth, k) : indist} --> \ \ ((oth', oth) : (oth_red_k K)^*) = ((oth', oth) : oth_red^*)" (fn _ => [ Safe_tac, (rtac oth_red_k_ks_rtc 1), atac 2, Fast_tac 1, (etac converse_rtrancl_induct 1), Fast_tac 1, (rtac tct.srr 1), atac 2, (rtac (oth_red_k_ks_eq RS iffD2) 1), atac 2, (rtac set_ext 1), Simp_tac 1, (etac (red_nc_rtc RS sym) 1) ]) ; fun asf simps th = asm_simplify (esimps simps) (#1 (freeze_thaw th)) ; (* reduction doesn't change the set of free names *) val _ = qed_goalw_spec_mp "fn_nc" Spi_Redns.thy [fn_oth_def] "(oia, oib) : oth_red --> fn_oth oia = fn_oth oib" (fn _ => [ (safe_tac (ces [oth_red.elims])), (TRYALL (eatac (insert_insertI2 RS UN_I) 1)), (TRYALL (eatac (insertI2 RS UN_I) 1)), Auto_tac ]) ; val _ = qed_goal_spec_mp "fn_nc_rtc" Spi_Redns.thy "(oia, oib) : oth_red^* --> fn_oth oia = fn_oth oib" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), rtac refl 1, (etac trans 1), (etac fn_nc 1) ]) ; (* changing definition of reduction from oth_red to oth_red_alt, show it doesn't make a difference ; note - we hypothesised that (insert (Enc Mp Mk, Enc Np Nk) oth, Mk, Nk) : indist ==> (oth, Mk, Nk) : indist but this isn't true, eg oth = {(Enc Mk (Enc Mp Mk), Enc Nk (Enc Np Nk))} *) fun mkI' th = rewrite_rule [mk_eq insert_Diff_single] (notindiffs RS th) ; val [orkvs_plI', oth_red_k_plI', oth_red_altr_plI', oth_red_alt_plI', oth_red_plI', oth_red_nkr_plI', oth_red_nk_plI', orkvs_elI', oth_red_k_elI', oth_red_altr_elI', oth_red_alt_elI', oth_red_elI', oth_red_nkr_elI', oth_red_nk_elI'] = map mkI' [orkvs.plI, oth_red_k.plI, oth_red_altr.plI, oth_red_alt.plI, oth_red.plI, oth_red_nkr.plI, oth_red_nk.plI, orkvs.elI, oth_red_k.elI, oth_red_altr.elI, oth_red_alt.elI, oth_red.elI, oth_red_nkr.elI, oth_red_nk.elI] ; val ins2 = [asm_rl, refl, insert_absorb] MRS mem_same_Pair ; val insx = [asm_rl, refl, insert_absorb, refl] MRS (Pair_eqI RSN (2, Pair_eqI) RSN (2, mem_same)) ; val [orkvs_plI'', oth_red_k_plI'', oth_red_altr_plI'', oth_red_alt_plI'', oth_red_plI'', oth_red_nkr_plI'', oth_red_nk_plI'', orkvs_elI'', oth_red_k_elI'', oth_red_altr_elI'', oth_red_alt_elI'', oth_red_nkr_elI'', oth_red_nk_elI''] = [orkvs_plI', oth_red_k_plI', oth_red_altr_plI', oth_red_alt_plI', oth_red_plI', oth_red_nkr_plI', oth_red_nk_plI', orkvs_elI', oth_red_k_elI', oth_red_altr_elI', oth_red_alt_elI', oth_red_nkr_elI', oth_red_nk_elI'] RL [ins2] ; local val (ore, thaw) = freeze_thaw (oth_red_elI' RS ins2) in val oth_red_elI'' = standard (thaw (asm_full_simplify (HOL_ss addsimps [insert_absorb]) ore)) end ; val oth_red_pl_not_min = oth_red_plI'' RSN (2, rsminE) ; val oth_red_el_not_min = oth_red_elI'' RSN (2, rsminE) ; val insDiff1 = [asm_rl, insert_Diff_single, refl] MRS mem_same_Pair ; val mk_i = (rewrite_rule (map mk_eq [Un_insert_right, Un_insert_left, Un_empty_right, Un_empty_left])) ; (* do we want the following ? *) val oth_red_plIi'' = mk_i oth_red_plI'' ; val oth_red_alt_plIi'' = mk_i oth_red_alt_plI'' ; val oth_red_elIi'' = mk_i oth_red_elI'' ; val oth_red_alt_elIi'' = mk_i oth_red_alt_elI'' ; val rtrancl_eq_refl = [rtrancl_refl, refl] MRS mem_same_Pair ; val _ = qed_goal_spec_mp "oth_red_nkr_sub" Spi_Redns.thy "(y, x) : oth_red_nkr --> x <= x' --> (EX y' >= y. (y', x') : oth_red_nkr)" (fn _ => [ (safe_tac (ces [oth_red_nkr.elims])), (REPEAT_FIRST (resolve_tac [exI, conjI])), (rtac oth_red_nkr_elI'' 4), (etac idv_wk 4), (rtac oth_red_nkr_plI'' 2), TRYALL Fast_tac ]) ; val _ = qed_goal_spec_mp "oth_red_altr_sub" Spi_Redns.thy "(y, x) : oth_red_altr --> x <= x' --> (EX y' >= y. (y', x') : oth_red_altr)" (fn _ => [ (safe_tac (ces [oth_red_altr.elims])), (REPEAT_FIRST (resolve_tac [exI, conjI])), (rtac oth_red_altr_elI'' 4), (etac idv_wk 4), (rtac oth_red_altr_plI'' 2), TRYALL Fast_tac ]) ; val _ = qed_goal_spec_mp "oth_red_alt_sub" Spi_Redns.thy "(y, x) : oth_red_alt --> x <= x' --> (EX y' >= y. (y', x') : oth_red_alt)" (fn _ => [ (safe_tac (ces [oth_red_alt.elims])), (REPEAT_FIRST (resolve_tac [exI, conjI])), (rtac oth_red_alt_elI'' 4), (etac indist_wk 4), (rtac oth_red_alt_plI'' 2), TRYALL Fast_tac ]) ; val _ = qed_goal_spec_mp "oth_red_sub" Spi_Redns.thy "(y, x) : oth_red --> x <= x' --> (EX y' >= y. (y', x') : oth_red)" (fn _ => [ (safe_tac (ces [oth_red.elims])), (REPEAT_FIRST (resolve_tac [exI, conjI])), (rtac oth_red_elI'' 4), (etac indist_wk 4), (rtac oth_red_plI'' 2), TRYALL Fast_tac ]) ; val _ = qed_goal_spec_mp "oth_red_Names'" Spi_Redns.thy "(y, x) : oth_red --> \ \ (EX y'. y' <= y & y' >= y - Ne & (y', x - Names ` S) : oth_red)" (fn _ => [ (safe_tac (ces [oth_red.elims])), (REPEAT_FIRST (resolve_tac [exI, conjI])), (rtac (oth_red_elI'') 6), (etac (Names_equivd RS iffD1) 6), (rtac (oth_red_plI'') 3), (TRYALL (rtac (insertI1 RS DiffI))), (ALLGOALS (clarsimp_tac (cesimps [Names_def, Ne_Names]))), Auto_tac ]) ; val _ = qed_goalw_spec_mp "diff_Names" Spi_Redns.thy [Ne_Names] "y' <= y --> y' >= y - Ne --> (EX S. y' = y - Names ` S & Names ` S <= y)" (fn _ => [ Safe_tac, (res_inst_tac [("x", "Names -` (y - y')")] exI 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_Names" Spi_Redns.thy "(y, x) : oth_red --> (EX S'. (y - Names ` S', x - Names ` S) : oth_red)" (fn _ => [ Safe_tac, (dtac oth_red_Names' 1), Safe_tac, (datac diff_Names 1 1), Safe_tac, (etac exI 1) ]) ; val _ = qed_goal_spec_mp "oth_red_Names_rtc" Spi_Redns.thy "(y, x) : oth_red^* --> \ \ (ALL S. EX S'. (y - Names ` S', x - Names ` S) : oth_red^*)" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), (Fast_tac 1), Clarify_tac 1, (dtac oth_red_Names 1), Clarify_tac 1, (etac allE 1), (etac ex_forward 1), (eatac tct.rsr 1 1) ]) ; val _ = qed_goal_spec_mp "oth_red_Un" Spi_Redns.thy "(y, x) : oth_red --> z Int x = {} --> (y Un z, x Un z) : oth_red" (fn _ => [ (safe_tac (ces [oth_red.elims])), (etac (indist_wk RS oth_red_elI'' RS mem_same_Pair1) 2), (rtac (oth_red_plI'' RS mem_same_Pair1) 1), (REPEAT (Fast_tac 1)) ]) ; val _ = qed_goal_spec_mp "oth_red_k_Un" Spi_Redns.thy "(y, x) : oth_red_k K --> z Int x = {} --> \ \ (y Un z, x Un z) : oth_red_k K" (fn _ => [ (safe_tac (ces [oth_red_k.elims])), (rtac (oth_red_k_elI'' RS mem_same_Pair1) 2), (rtac (oth_red_k_plI'' RS mem_same_Pair1) 1), (REPEAT (Fast_tac 1)) ]) ; val _ = qed_goalw_spec_mp "rsmin_oth_red_alt_sub" Spi_Redns.thy [rsmin_def] "oth : rsmin oth_red_alt UNIV --> oth' <= oth --> \ \ oth' : rsmin oth_red_alt UNIV" (fn _ => [ (safe_tac (cis [UNIV_I])), (datac oth_red_alt_sub 1 1), Fast_tac 1 ]); val _ = qed_goalw_spec_mp "rsmin_oth_red_sub" Spi_Redns.thy [rsmin_def] "oth : rsmin oth_red UNIV --> oth' <= oth --> oth' : rsmin oth_red UNIV" (fn _ => [ (safe_tac (cis [UNIV_I])), (datac oth_red_sub 1 1), Fast_tac 1 ]); val _ = qed_goal_spec_mp "oth_red_alt_nk" Spi_Redns.thy "(G', G) : oth_red_alt --> (EX H'. (H', G) : oth_red_nk & H' <= G')" (fn _ => [ (Clarify_tac 1), (etac oth_red_alt.elims 1), Safe_tac, (ALLGOALS (dresolve_tac oth_red_nk.intros)), atac 2, (ALLGOALS (rtac exI THEN' rtac conjI)), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_altr_nkr" Spi_Redns.thy "(G', G) : oth_red_altr --> (EX H'. (H', G) : oth_red_nkr & H' <= G')" (fn _ => [ (Clarify_tac 1), (etac oth_red_altr.elims 1), Safe_tac, (ALLGOALS (dresolve_tac oth_red_nkr.intros)), atac 2, (ALLGOALS (rtac exI THEN' rtac conjI)), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_nk_sup_alt" Spi_Redns.thy "(G', G) : oth_red_nk --> H >= G --> \ \ (EX H'. (H', H) : oth_red_alt & H' >= G')" (fn _ => [ (Clarify_tac 1), (etac oth_red_nk.elims 1), Safe_tac, (ALLGOALS (dresolve_tac oth_red_alt.intros)), atac 2, (ALLGOALS (datac oth_red_alt_sub 1)), Safe_tac, (ALLGOALS (rtac exI THEN' rtac conjI)), TRYALL atac, Fast_tac 1 ]) ; val _ = bind_thm ("oth_red_nk_alt", subset_refl RSN (2, oth_red_nk_sup_alt)) ; val _ = qed_goalw "rsmin_nk_alt_equiv" Spi_Redns.thy [rsmin_def] "rsmin oth_red_nk UNIV = rsmin oth_red_alt UNIV" (fn _ => [ Safe_tac, (fast_tac (cds [oth_red_alt_nk]) 1), (fast_tac (cds [oth_red_nk_alt]) 1) ]) ; val _ = qed_goal_spec_mp "oth_red_nkr_sup_altr" Spi_Redns.thy "(G', G) : oth_red_nkr --> H >= G --> \ \ (EX H'. (H', H) : oth_red_altr & H' >= G')" (fn _ => [ (Clarify_tac 1), (etac oth_red_nkr.elims 1), Safe_tac, (ALLGOALS (dresolve_tac oth_red_altr.intros)), atac 2, (ALLGOALS (datac oth_red_altr_sub 1)), Safe_tac, (ALLGOALS (rtac exI THEN' rtac conjI)), TRYALL atac, Fast_tac 1 ]) ; val _ = bind_thm ("oth_red_nkr_altr", subset_refl RSN (2, oth_red_nkr_sup_altr)) ; val _ = qed_goalw "rsmin_nkr_altr_equiv" Spi_Redns.thy [rsmin_def] "rsmin oth_red_nkr UNIV = rsmin oth_red_altr UNIV" (fn _ => [ Safe_tac, (fast_tac (cds [oth_red_altr_nkr]) 1), (fast_tac (cds [oth_red_nkr_altr]) 1) ]) ; (* oth_red_k finitely branching *) val _ = qed_goal_spec_mp "oth_red_k_lose1" Spi_Redns.thy "(G',G) : oth_red_k K --> (EX! g. g : G - G')" (fn _ => [ (fast_tac (ces [oth_red_k.elims]) 1) ]) ; val _ = qed_goal_spec_mp "ins_new_eq" HOL_Gen.thy "insert a B = insert a C --> B - {a} = C - {a}" (fn _ => [ (rtac impI 1), (rtac box_equals 1), (TRYALL (rtac (singletonI RS insert_Diff1))), Asm_simp_tac 1 ]) ; val th1' = (insert_eqD RS insertE) ; val th2' = (eq_insertD RS insertE) ; val th1 = (mk_dupE (insert_eqD RS insertE)) ; val th2 = (mk_dupE (eq_insertD RS insertE)) ; val thii2 = [equalityD2, insertI2 RS insertI2] MRS subsetD ; val _ = qed_goal_spec_mp "oth_red_k_unique_lose" Spi_Redns.thy "(G',G) : oth_red_k K --> (G'',G) : oth_red_k K --> \ \ g : G - G' --> g : G - G'' --> G' = G''" (fn _ => [ (strip_tac 1), (REPEAT_FIRST (etac oth_red_k.elims)), (ALLGOALS Clarsimp_tac), (* SEE IF THIS COULD BE SIMPLER *) (TRYALL (etac th1)), (TRYALL (etac th2)), (ALLGOALS Clarify_tac), (ALLGOALS (dtac ins_new_eq)), (ALLGOALS Clarsimp_tac) ]) ; val _ = qed_goal_spec_mp "oth_red_k_fb" Spi_Redns.thy "finite G --> finite {H. (H, G) : oth_red_k K}" (fn _ => [ (rtac impI 1), (res_inst_tac [("f", "%H. SOME g. g : G - H")] finite_imageD 1), (rtac finite_subset 1), atac 2, Clarsimp_tac 1, (rtac someI2_ex 1), (etac conjunct1 2), (dtac oth_red_k_lose1 1), Fast_tac 1, rewtac inj_on_def, Clarify_tac 1, (rtac oth_red_k_unique_lose 1), atac 1, atac 1, (rtac mem_same 1), atac 2, (ALLGOALS (rtac someI_ex)), (ALLGOALS (fast_tac (cds [oth_red_k_lose1]))) ]) ; val _ = qed_goal_spec_mp "orkvs_unique" Spi_Redns.thy "((H, Us), G) : orkvs --> ((H, Vs), G) : orkvs --> Us = Vs" (fn _ => [ (strip_tac 1), (REPEAT_FIRST (etac orkvs.elims)), (ALLGOALS Clarsimp_tac), (TRYALL (chop_last o (etac th1'))), (ALLGOALS Clarify_tac), Fast_tac 3, (ALLGOALS (datac thii2 1)), Safe_tac ]) ; val _ = qed_goal_spec_mp "ex_orkvs" Spi_Redns.thy "(H, G) : oth_red_k K --> (EX Vs. ((H, Vs), G) : orkvs)" (fn _ => [ (rtac impI 1), (etac oth_red_k.elims 1), (ALLGOALS Clarsimp_tac), (ALLGOALS (rtac exI)), (TRYALL (eresolve_tac orkvs.intros)) ]) ; val _ = qed_goal_spec_mp "orkvs_fb" Spi_Redns.thy "finite G --> finite {HVs. (HVs, G) : orkvs}" (fn _ => [ (rtac impI 1), (dtac oth_red_k_fb 1), (res_inst_tac [("f", "fst")] finite_imageD 1), (rtac finite_subset 1), atac 2, Clarsimp_tac 1, (etac orkvs_k 1), (rewtac inj_on_def), (Clarsimp_tac 1), (eatac orkvs_unique 1 1) ]) ; val _ = qed_goal_spec_mp "orkvss_unique" Spi_Redns.thy "((H, Vs), (G, Us)) : orkvss --> ((H, Ws), (G, Us)) : orkvss --> Vs = Ws" (fn _ => [ (strip_tac 1), (REPEAT (etac orkvss.elims 1)), Clarify_tac 1, (datac orkvs_unique 1 1), Clarify_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_fb" Spi_Redns.thy "finite G --> finite {HVs. (HVs, (G,Us)) : orkvss}" (fn _ => [ (rtac impI 1), (dtac orkvs_fb 1), (dres_inst_tac [("h", "%(H, Vs). (H, Vs Un Us)")] finite_imageI 1), (rtac finite_subset 1), atac 2, Clarsimp_tac 1, (etac orkvss.elims 1), Force_tac 1 ]) ; val psub_ex = [psubset_eq, reop rev conjI] MRS iffD2 RS psubset_imp_ex_mem ; val _ = qed_goal_spec_mp "oth_red_k_lem" Spi_Redns.thy "(G',G) : oth_red_k K --> p : D --> p : (G - G') --> \ \ (EX D'. (D', D) : oth_red_k K & D' >= D - {p} & D' <= D Un G')" (fn _ => [ Safe_tac, (etac oth_red_k.elims 1), (ALLGOALS Clarsimp_tac), (ALLGOALS (rtac exI)), (REPEAT_FIRST (resolve_tac [exI, conjI])), (etac oth_red_k_plI'' 1), (etac oth_red_k_elI'' 3), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_k_min" Spi_Redns.thy "T : wfp (oth_red_k K) --> \ \ (G',G) : oth_red_k K --> (D',D) : oth_red_k K --> \ \ T' = (G' Un D') - (G - G') - (D - D') --> \ \ (ALL k. T >= T' --> T <= G Un D Un G' Un D' --> \ \ (T', T) : (oth_red_k K)^*)" (fn _ => [ (REPEAT (rtac impI 1)), rtac allI 1, (etac wfp.induct 1), (case_tac "T' = dt" 1), Fast_tac 1, (strip_tac 1), (datac psub_ex 1 1), (etac exE 1), (etac DiffE 1), (subgoal_tac "b : (G - G') | b : (D - D')" 1), Force_tac 2, (etac disjE 1), (REPEAT1 (EVERY [ (datac oth_red_k_lem 2 1), Clarify_tac 1, (etac allE 1), mp_tac 1, (dtac conjunct2 1), (etac impE 1), (etac impE 2), (eatac tct.rsr 1 3), Force_tac 1, Force_tac 1 ])) ]) ; val _ = qed_goal_spec_mp "oth_red_k_smaller" Spi_Redns.thy "(a, b) : oth_red_k K --> finite a --> \ \ (SUM x:a. size (fst x)) < (SUM x:b. size (fst x))" (fn _ => [ (safe_tac (ces [oth_red_k.elims])), (REPEAT (EVERY [ Asm_simp_tac 1, (rtac xt7 1), (rtac setsum_insert2_le 2), Full_simp_tac 2, Asm_full_simp_tac 1 ])) ]) ; val _ = qed_goal "wf_oth_red_k_finite" Spi_Redns.thy "wf (oth_red_k K Int {(x, y). finite x})" (fn _ => [ (res_inst_tac [("f1", "setsum (size o fst)")] (wf_less_than RS wf_inv_image RS wf_subset) 1), Safe_tac, rewtac inv_image_def, Simp_tac 1, (eatac oth_red_k_smaller 1 1) ]) ; val _ = qed_goal "wf_oth_red_k_finite'" Spi_Redns.thy "wf (oth_red_k K Int {(x, y). finite x & finite y})" (fn _ => [ (rtac (wf_oth_red_k_finite RS wf_subset) 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_k_tc_smaller" Spi_Redns.thy "(a, b) : (oth_red_k K)^+ --> finite a --> \ \ (SUM x:a. size (fst x)) < (SUM x:b. size (fst x))" (fn _ => [ strip_tac 1, (etac trancl_induct 1), (eatac oth_red_k_smaller 1 1), (etac order_less_trans 1), (rtac oth_red_k_smaller 1), atac 1, (datac (trancl_into_rtrancl RS oth_red_k_finite_rtc_iff RS iffD2) 2 1) ]) ; val _ = bind_thm ("oth_red_smaller", oth_red_k RS subsetD RS oth_red_k_smaller) ; val _ = bind_thm ("oth_red_tc_smaller", oth_red_k RS mk_mono trancl_mono RS subsetD RS oth_red_k_tc_smaller) ; val _ = bind_thm ("oth_red_finite_rtc_iff", oth_red_k RS rtrancl_mono RS subsetD RS oth_red_k_finite_rtc_iff) ; val _ = bind_thm ("oth_red_finite_iff", oth_red_k RS subsetD RS oth_red_k_finite_iff) ; val oth_red_finite_rtc = oth_red_finite_rtc_iff RS iffD1 ; val oth_red_finite = oth_red_finite_iff RS iffD1 ; val oth_red_k_finite = oth_red_k_finite_iff RS iffD1 ; val _ = bind_thm ("wf_oth_red_finite", [wf_oth_red_k_finite, [oth_red_k, subset_refl] MRS Int_mono] MRS wf_subset) ; val _ = bind_thm ("wf_oth_red_finite'", [wf_oth_red_k_finite', [oth_red_k, subset_refl] MRS Int_mono] MRS wf_subset) ; (** showing that oth_red has a nf **) val _ = qed_goal_spec_mp "wfp_oth_red_k_finite" Spi_Redns.thy "finite x --> x : wfp (oth_red_k K)" (fn _ => [ (res_inst_tac [("a", "x")] (wf_oth_red_k_finite RS wf_induct) 1), (rtac impI 1), (rtac wfp.wfpI 1), strip_tac 1, (ftac oth_red_k_finite_iff 1), Force_tac 1 ]) ; val _ = bind_thm ("wfp_oth_red_finite", [wfp_oth_red_k_finite, oth_red_k] MRS wfp_mono') ; val wfp_oth_red_alt = [wfp_oth_red_finite, oth_red_alt] MRS wfp_mono' ; val _ = qed_goal_spec_mp "wfp_oth_red_nk'" Spi_Redns.thy "c : wfp oth_red_alt --> (ALL d. d <= c --> d : wfp oth_red_nk)" (fn _ => [ rtac impI 1, (etac wfp.induct 1), Clarify_tac 1, (rtac wfp.wfpI 1), (strip_tac 1), (datac oth_red_nk_sup_alt 1 1), Clarify_tac 1, (etac allE 1), mp_tac 1, Clarify_tac 1, (etac allE 1), etac mp 1, Fast_tac 1 ]) ; val wfp_oth_red_nk = [wfp_oth_red_alt, subset_refl] MRS wfp_oth_red_nk' ; val wfp_oth_red_altr = [wfp_oth_red_alt, oth_red_altr] MRS wfp_mono' ; val wfp_oth_red_nkr = [wfp_oth_red_nk, oth_red_nkr] MRS wfp_mono' ; val _ = qed_goal_spec_mp "oth_red_k_Un_confl" Spi_Redns.thy "finite (G Un D) --> (G',G) : oth_red_k K --> \ \ (D',D) : oth_red_k K --> \ \ (EX T. (T, D Un G') : (oth_red_k K)^* & \ \ (T, G Un D') : (oth_red_k K)^* )" (fn _ => [ Safe_tac, (forw_inst_tac [("z", "D' - G"), ("x", "G"), ("y", "G'")] oth_red_k_Un 1), Fast_tac 1, (forw_inst_tac [("z", "G' - D"), ("x", "D"), ("y", "D'")] oth_red_k_Un 1), Fast_tac 1, Clarsimp_tac 1, (rtac exI 1), (rtac conjI 1), (ALLGOALS (SELECT_GOAL (EVERY [ (rtac tct.rsr 1), (atac 2), (rtac (wfp_oth_red_k_finite RS oth_red_k_min) 1), atac 2, (chop_tac 1 (atac 2)), rtac refl 2, Fast_tac 2, Fast_tac 2 ]))), (safe_tac (ces [oth_red_k_finite] addSIs [finite_Diff])) ]) ; val insert_not = tacsthm [ atac 2, etac rev_notE 2, etac thin_rl 2 ] insertE ; val insert_eqD1 = [insertI2, transfer Main.thy order_eq_refl] MRS rev_subsetD RS insert_not ; val insert_eqD2 = sym RSN (2, insert_eqD1) ; val _ = qed_goal_spec_mp "inserts_eq" Main.thy "insert a A = insert b B --> a ~: A --> b ~: B --> \ \ a = b & A = B | a ~= b & a : B & b : A & \ \ (EX f x. B - {a} = f x & A - {b} = f x)" (fn _ => [ (case_tac "a = b" 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "inserts_eq_ff" Main.thy "insert a A = insert b B --> finite A = finite B" (fn _ => [ (rtac impI 1), (dres_inst_tac [("f", "%x. finite x") ] arg_cong 1), Auto_tac ]) ; val dulem = prove_goal Main.thy "A - {a} = B --> A Un B = A" fn_ft1 RS mp ; val inserts_eq' = read_instantiate [("'b", "nat")] inserts_eq ; val epi = read_instantiate [("P", "?y : ?S")] prod.exhaust ; val _ = qed_goal_spec_mp "oth_red_k_confl" Spi_Redns.thy "finite G --> (D, G) : oth_red_k K --> (D', G) : oth_red_k K --> \ \ (EX T. (T, D) : (oth_red_k K)^* & (T, D') : (oth_red_k K)^* )" (fn _ => [ (safe_tac (ces [oth_red_k.elims])), (ALLGOALS (fatac inserts_eq' 2)), (REPEAT_SOME (eresolve_tac [disjE, conjE])), (ALLGOALS Clarsimp_tac), (* deal with cases where both reductions are the same *) (TRYALL (rtac exI THEN' rtac rtrancl_refl)), (* now get oth Un otha as disjoint union of two reducible theories *) (ALLGOALS (forw_inst_tac [ ("G", "otha"), ("D", "oth")] (thin_rl RS oth_red_k_Un_confl))), (TRYALL (etac oth_red_k_plI'')), (TRYALL (eatac oth_red_k_elI'' 1)), (TRYALL (ftac inserts_eq_ff THEN' Asm_simp_tac)), (ALLGOALS (etac ex_forward THEN' etac conj_forward)), (ALLGOALS (etac mem_same THEN' asm_simp_tac (esimps [dulem]))) ]) ; val _ = qed_goal_spec_mp "oth_red_confl" Spi_Redns.thy "finite G --> (D, G) : oth_red --> (D', G) : oth_red --> \ \ (EX T. (T, D) : (oth_red)^* & (T, D') : (oth_red)^* )" (fn _ => [ (strip_tac 1), (full_simp_tac (esimps [refl RS oth_red_k_ks_eq RS sym, refl RS oth_red_k_ks_rtc_eq RS sym]) 1), (datac oth_red_k_confl 1 1), (chop_last (atac 1)), ((etac ex_forward THEN' etac conj_forward) 1), (ALLGOALS (EVERY' [ (etac (transfer Main.thy order_eq_refl RSN (2, rev_subsetD))), cong_tac, rtac ext, (full_simp_tac (esimps [refl RS oth_red_k_ks_eq])), (etac (red_nc RS sym)) ])) ]) ; val _ = qed_goal_spec_mp "oth_red_confl_rtc" Spi_Redns.thy "finite G --> (ALL D D'. (D, G) : oth_red^* --> (D', G) : oth_red^* --> \ \ (EX T. (T, D) : (oth_red)^* & (T, D') : (oth_red)^* ))" (fn _ => [ (rtac impI 1), (ftac wfp_oth_red_finite 1), (etac rev_mp 1), (etac wfp.induct 1), Clarify_tac 1, (etac (mk_dupE rtranclE) 1), Fast_tac 1, (etac (mk_dupE rtranclE) 1), Fast_tac 1, (fatac oth_red_confl 1 1), (chop_tac 1 (atac 1)), Clarify_tac 1, (etac all_dupE 1), mp_tac 1, (etac conjE 1), (etac impE 1), (eatac oth_red_finite 1 1), (etac allE2 1), mp_tac 1, (chop_tac 1 (mp_tac 1)), Clarify_tac 1, (etac allE 1), (chop_tac 1 (mp_tac 1)), (etac conjE 1), (etac impE 1), (eatac oth_red_finite 1 1), (eres_inst_tac [("xa", "Ta"), ("x", "D'")] allE2 1), (etac impE 1), (eatac rtrancl_trans 1 1), mp_tac 1, Clarify_tac 1, (res_inst_tac [("x", "Tb")] exI 1), (rtac conjI 1), atac 2, (eatac rtrancl_trans 1 1) ]) ; (* following implies similar results for other relations, once the relevant results are proved, ie [ indist_norm, oth_red_alt, oth_red_altr, oth_red_nk_alt, oth_red_nkr ] and results relating oth_red_altr to oth_red_nkr corresponding to oth_red_nk_alt *) (* apart from the finiteness condition, idv_red_nkr_not_ctg would follow from idv_red_nkr_not_idv *) val _ = qed_goal_spec_mp "idv_red_nkr_not_ctg" Spi_Redns.thy "(G, MN) : indist_norm --> ~ is_der_virt (G, MN) --> \ \ (EX G'. (G', G) : oth_red_nkr & Not (G' <= G))" (fn _ => [ (rtac impI 1), (etac indist_norm_induct_pair 1), ALLGOALS Clarify_tac, (case_tac "{(Ma, Na), (Mb, Nb)} <= oth" 1), (force_tac (cesimps [insert_absorb]) 1), (rtac exI 1), (rtac conjI 1), (etac oth_red_nkr_plI'' 1), Force_tac 1, (case_tac "(Mp, Np) : oth" 1), (force_tac (cesimps [insert_absorb]) 1), (rtac exI 1), (rtac conjI 1), (rtac oth_red_nkr_elI'' 1), atac 2, (simp_tac (esimps [idv_Enc_equiv_d]) 1), Fast_tac 1 ]) ; val _ = qed_goal "rsmin_names" Spi_Redns.thy "(oth - Ne : rsmin oth_red UNIV) = (oth : rsmin oth_red UNIV)" (fn _ => [ (rtac iffI 1), (etac rsmin_oth_red_sub 2), (rtac Diff_subset 2), (clarsimp_tac (cesimps [rsmin_def]) 1), (safe_tac (ces [oth_red.elims])), (ALLGOALS (etac allE)), (ALLGOALS (chop_last o etac notE)), (rtac oth_red_plI'' 1), (rtac oth_red_elI'' 2), (etac (name_equivd RS iffD1) 2), Safe_tac, (TRYALL (rtac refl)), (ALLGOALS (etac Ne.elims)), Auto_tac ]) ; (* effect of oth_red_alt on pairs of Names *) val _ = qed_goal_spec_mp "oth_red_alt_aug_Name" Spi_Redns.thy "(othr, oth) : oth_red_alt --> \ \ (insert (Name i, m) othr, insert (Name i, m) oth) : oth_red_alt" (fn _ => [ (safe_tac (ces [oth_red_alt.elims])), (rtac (oth_red_alt.plI RS rev_iffD1) 1), cong_tac 2, Clarsimp_tac 2, (rtac conjI 2), (rtac insert_commute 3), (simp_tac (esimps [insert_commute]) 2), Asm_simp_tac 1, (rtac (oth_red_alt.elI RS rev_iffD1) 1), cong_tac 3, Clarsimp_tac 3, (rtac conjI 3), (rtac insert_commute 4), (simp_tac (esimps [insert_commute]) 3), (etac indist_wki 2), Asm_simp_tac 1 ]) ; val _ = qed_goal_spec_mp "oth_red_alt_Name" Spi_Redns.thy "(othr, oth) : oth_red_alt --> \ \ (ALL oth'. oth' - Ne = oth - Ne --> \ \ (EX othr'. (othr', oth') : oth_red_alt & \ \ othr' - Ne = othr - Ne))" (fn _ => [ (rtac impI 1), (etac oth_red_alt.elims 1), Safe_tac, (REPEAT_FIRST (resolve_tac [exI, conjI])), (subgoal_tac "(Mpair Ma Mb, Mpair Na Nb) : oth'" 1), (force_tac (cesimps [Ne.defs]) 2), (rtac oth_red_alt_plI'' 1), atac 1, (subgoal_tac "(Enc Mp Mk, Enc Np Nk) : oth'" 2), (force_tac (cesimps [Ne.defs]) 3), (rtac oth_red_alt_elI'' 2), atac 3, (dtac (name_equivd RS iffD1) 2), (etac indist_wk 2), Fast_tac 2, (* could replace this lot by ALLGOALS Fast_tac, but slower *) (ALLGOALS (rtac equalityI')), (REPEAT_FIRST (eresolve_tac [insertE, DiffE])), TRYALL hyp_subst_tac, (TRYALL (rtac (reop rev DiffI) THEN' atac)), (TRYALL (resolve_tac insertIs)), (dtac equalityD2' 4), (dtac equalityD1' 3), (dtac equalityD2' 2), (dtac equalityD1' 1), (REPEAT (Fast_tac 1)) ]) ; val _ = qed_goal_spec_mp "oth_red_alt_Name_rtc" Spi_Redns.thy "(othr, oth) : oth_red_alt^* --> \ \ (ALL oth'. oth' - Ne = oth - Ne --> \ \ (EX othr'. (othr', oth') : oth_red_alt^* & \ \ othr' - Ne = othr - Ne))" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), Fast_tac 1, Clarify_tac 1, (datac oth_red_alt_Name 1 1), Clarify_tac 1, (etac allE 1), mp_tac 1, Clarify_tac 1, (rtac exI 1), (rtac conjI 1), atac 2, (eatac tct.rsr 1 1) ]) ; val _ = qed_goal_spec_mp "orkvs_con_eq" Spi_Redns.thy "((G', Cs), G) : orkvs --> (H, MN) : Cs --> H = G" (fn _ => [ (strip_tac 1), (etac orkvs.elims 1), Auto_tac ]) ; val orkvs_con_sub = orkvs_con_eq RS equalityD1 ; val _ = qed_goal_spec_mp "orkvs_pair" Spi_Redns.thy "((G', Cs), G) : orkvs --> G <= range pair --> G' <= range pair" (fn _ => [ (strip_tac 1), (etac orkvs.elims 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "orkvss_pair" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss --> G <= range pair --> G' <= range pair" (fn _ => [ (strip_tac 1), (etac orkvss.elims 1), Clarsimp_tac 1, (datac orkvs_pair 1 1), (datac subsetD 1 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_rtc_pair" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss^* --> G <= range pair --> G' <= range pair" (fn _ => [ (strip_tac 1), (etac crtip 1), Fast_tac 1, (etac orkvss.elims 1), (fast_tac (cds [orkvs_pair]) 1) ]) ; val _ = qed_goal_spec_mp "orkvss_rtc_kc_pair" Spi_Redns.thy "((G', Vs), (G, Cs)) : orkvss^* --> G <= range pair --> \ \ (H, MN) : Vs - Cs --> insert MN H <= range pair" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac crtip 1), Simp_tac 1, Clarify_tac 1, (etac orkvss.elims 1), (etac orkvs.elims 1), Force_tac 1, Clarsimp_tac 1, (etac disjE 1), Force_tac 2, (datac orkvss_rtc_pair 1 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_rtc_sub" Spi_Redns.thy "((G', Vs), (G, Cs)) : orkvss^* --> Cs <= Vs" (fn _ => [ (rtac impI 1), (etac rtrancl_induct_pair 1), Simp_tac 1, (etac orkvss.elims 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_exp" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss --> \ \ ((G', Cs' Un Es), (G, Cs Un Es)) : orkvss" (fn _ => [ (strip_tac 1), (etac orkvss.elims 1), (clarsimp_tac (cesimps [Un_assoc]) 1), (etac orkvss.I 1) ]) ; val _ = qed_goal_spec_mp "orkvss_rtc_exp" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss^* --> \ \ ((G', Cs' Un Es), (G, Cs Un Es)) : orkvss^*" (fn _ => [ (strip_tac 1), (etac rtip 1), Simp_tac 1, (etac tct.rsr 1), (etac orkvss_exp 1) ]) ; val SOME orkvss_expr = Conv.cvt (Conv.eqc [Un_commute]) orkvss_exp ; val SOME orkvss_rtc_expr = Conv.cvt (Conv.eqc [Un_commute]) orkvss_rtc_exp ; val _ = qed_goal_spec_mp "orkvss_exs" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss --> \ \ (EX S. ((G', S), G) : orkvs & Cs' = S Un Cs)" (fn _ => [ (strip_tac 1), (etac orkvss.elims 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_rtc_exs" Spi_Redns.thy "((G', Cs'), (G, Cs)) : orkvss^* --> \ \ (EX S. ((G', S), (G, {})) : orkvss^* & Cs' = S Un Cs)" (fn _ => [ (strip_tac 1), (etac rtrancl_induct_pair 1), Fast_tac 1, (dtac orkvss_exs 1), Clarify_tac 1, rtac exI 1, rtac conjI 1, (rtac tct.rsr 1), (etac orkvss.I 2), (etac orkvss_rtc_expr 1), (simp_tac (esimps Un_ac) 1) ]) ; val _ = qed_goal "orkvss_fif" Spi_Redns.thy "fwd_image orkvss fst <= oth_red_k UNIV" (fn _ => [ (safe_tac (ces fwd_image.elims)), Simp_tac 1, (etac orkvss_k 1) ]) ; val _ = bind_thm ("wfp_orkvss'", wfp_oth_red_k_finite RS (orkvss_fif RS wfp_mono RS subsetD RS wfp_fwd_image)) ; val _ = bind_thm ("wfp_orkvss", rewrite_rule [mk_eq fst_conv] (read_instantiate [("x", "(?G, ?Us)")] wfp_orkvss')) ; val _ = qed_goal_spec_mp "orkvss_rtc_fb'" Spi_Redns.thy "(G, Us) : wfp orkvss --> (finite G --> \ \ finite {HVs. (HVs, G, Us) : orkvss^*})" (fn _ => [ (rtac impI 1), (etac wfp_induct_pair 1), Clarify_tac 1, (stac rtc_alt 1), Simp_tac 1, (rtac finite_UN_I 1), (etac orkvss_fb 1), Clarify_tac 1, (etac allE 1), mp_tac 1, etac conjE 1, Clarsimp_tac 1, (dtac orkvss_k 1), (datac oth_red_k_finite 1 1), contr_tac 1 ]) ; val _ = bind_thm ("orkvss_rtc_fb", reop tl (wfp_orkvss RS orkvss_rtc_fb')) ; val _ = qed_goal_spec_mp "oth_red_paired" Spi_Redns.thy "G <= range pair --> (H, G) : oth_red --> H <= range pair" (fn _ => [ (safe_tac (ces [oth_red.elims])), (TRYALL (eatac (insertI2 RS rev_subsetD) 1)), (TRYALL (dtac (insertI1 RS rev_subsetD) THEN' Clarsimp_tac)) ]) ; val _ = qed_goal_spec_mp "oth_red_rtc_paired" Spi_Redns.thy "G <= range pair --> (H, G) : oth_red^* --> H <= range pair" (fn _ => [ strip_tac 1, (eatac converse_rtrancl_induct 1 1), (eatac oth_red_paired 1 1) ]) ; val memswap = swap RS (refl RS set_cong RS iffD1) ; val _ = qed_goalw_spec_mp "fn_orkvs_eq" Spi_Redns.thy [fn_oth_def] "((H, Ts), G) : orkvs --> fn_oth H = fn_oth G" (fn _ => [ (safe_tac (ces [orkvs.elims])), (TRYALL Fast_tac), (ALLGOALS Full_simp_tac), (TRYALL Fast_tac) ]) ; val _ = qed_goal_spec_mp "fn_orkvss_rtc_eq" Spi_Redns.thy "((H, Ts), (G, Ss)) : orkvss^* --> fn_oth H = fn_oth G" (fn _ => [ Clarify_tac 1, (etac rtip 1), Simp_tac 1, (etac orkvss.elims 1), Clarsimp_tac 1, etac fn_orkvs_eq 1 ]) ; val fn_orkvss_rtc = fn_orkvss_rtc_eq RS equalityD1 ; (* val _ = qed_goal_spec_mp "fn_orkvss_rtc" Spi_Redns.thy "((H, Ts), (G, Ss)) : orkvss^* --> fn_oth H <= fn_oth G" (fn _ => [ Clarify_tac 1, (etac rtip 1), Simp_tac 1, (etac orkvss.elims 1), Clarsimp_tac 1, (eatac (fn_orkvs RS subsetD) 1 1) ]) ; *) val _ = qed_goal_spec_mp "fn_orkvss_kc_rtc" Spi_Redns.thy "((H, Ts), (G, Ss)) : orkvss^* --> (K, X) : Ts - Ss --> \ \ fn_oth (insert X K) <= fn_oth G" (fn _ => [ (rtac impI 1), (etac crtip 1), Simp_tac 1, (etac orkvss.elims 1), Clarsimp_tac 1, (etac disjE 1), Fast_tac 2, (etac orkvs.elims 1), ALLGOALS Clarsimp_tac, (dtac fn_orkvss_rtc 1), (asm_full_simp_tac (esimps [fn_oth_insert]) 1), Safe_tac, (TRYALL (eatac rev_subsetD 1)) ]) ; val _ = bind_thm ("orkvss_finite_rtc", orkvss_k_rtc RS oth_red_k_finite_rtc) ; val _ = qed_goal_spec_mp "orkvss_rtc_in_kc_finite" Spi_Redns.thy "((H, Ts), (G, Ss)) : orkvss^* --> (K, X) : Ts - Ss --> \ \ finite G --> finite K" (fn _ => [ (rtac impI 1), (etac crtip 1), Simp_tac 1, Clarify_tac 1, (etac impCE 1), Fast_tac 2, (etac orkvss.elims 1), Clarsimp_tac 1, (etac orkvs.elims 1), ALLGOALS Clarsimp_tac, (datac orkvss_finite_rtc 1 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "orkvss_kc_rtc_finite" Spi_Redns.thy "((H, Ts), (G, Ss)) : orkvss^* --> finite Ss --> finite Ts" (fn _ => [ strip_tac 1, etac crtip 1, Simp_tac 1, (safe_tac (ces [orkvs.elims, orkvss.elims])) ]) ;