structure Spi_Reduce = struct val thy = the_context () end ; val _ = use_legacy_bindings Spi_Reduce.thy ; val ratacs = [ (etac allE3), (etac allE3), (REPEAT1 o (eres_inst_tac [("xc", "Qp"), ("xb", "Qk"), ("xa", "Rp"), ("x", "Rk")] allE4)), (REPEAT1 o dtac (refl RS rev_mp)), (REPEAT1 o (etac impE THEN' etac xt6 THEN' Force_tac)), Clarsimp_tac ] ; (* keep red_alt_lem and oth_red_alt_lem - in TPHOLs 2009 paper *) val _ = qed_goal_spec_mp "red_alt_lem'" Spi_Reduce.thy "(othe, MN) : indist --> (ALL oth M N Qp Qk Rp Rk. \ \ oth = othe - {(Enc Qp Qk, Enc Rp Rk)} --> MN = (M, N) --> \ \ size M <= size Qk --> (oth, M, N) : indist | \ \ (EX oth'. (oth', othe) : oth_red_alt))" (fn _ => [ (rtac impI 1), (etac indist.induct 1), Safe_tac, (rtac indist.id 1), Force_tac 1, (EVERY' ratacs 1), (eatac indist.prI 1 1), (EVERY' ratacs 1), (eatac indist.erI 1 1), (* pl rule - not applicable to normal form *) (thin_tac "All ?P" 1), (etac notE 1), (rtac exI 1), (etac oth_red_alt_plI'' 1), (* el rule - not applicable to normal form *) (chop_tac 1 (thin_tac "All ?P" 1)), (etac notE 1), (eres_inst_tac [("xa", "Mk"), ("x", "Nk")] allE3 1), (eres_inst_tac [("xc", "Mp"), ("xb", "Mk"), ("xa", "Np"), ("x", "Nk")] allE4 1), (dtac (refl RS rev_mp) 1), (Clarsimp_tac 1), (rtac exI 1), (eatac oth_red_alt_elI'' 1 1) ]) ; val red_alt_lem = tacthm (TRYALL (resolve_tac [refl, order_refl])) red_alt_lem' ; (* above proved more easily using version of indist where principal formula required not to be in the el, pl rules, because then the derivation of keys used in the el rule matches the derivation of keys required for oth_red_alt, but is such a set of rules correct ? *) val _ = qed_goal_spec_mp "oth_red_alt_lem" Spi_Reduce.thy "(D, G) : oth_red --> (EX D'. (D', G) : oth_red_alt)" (fn _ => [ (safe_tac (ces [oth_red.elims])), (rtac exI 1), (etac oth_red_alt.plI 1), (dtac red_alt_lem 1), (etac disjE 1), atac 2, (rtac exI 1), (rtac oth_red_alt_elI' 1), (etac mem_same 1), (cong_tac 1), (rtac (singletonI RS insert_Diff1) 1) ]) ; val _ = qed_goalw "rsmin_or_alt" Spi_Reduce.thy [rsmin_def] "rsmin oth_red_alt UNIV = rsmin oth_red UNIV" (fn _ => [ Safe_tac, (dtac (oth_red_alt RS subsetD) 2), Fast_tac 2, (dtac oth_red_alt_lem 1), Fast_tac 1 ]) ; val _ = bind_thm ("rsmin_nk_equiv", [rsmin_nk_alt_equiv, rsmin_or_alt] MRS trans) ; (** alternate, simpler, proof of indist_norm, independent of red_alt_lem **) val _ = qed_goal_spec_mp "idv_red_nkr_ns" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX G'. (G', G) : oth_red_nkr & Not (G' <= G))" (fn _ => [ (rtac impI 1), (etac (dest_nk indist_nk.induct) 1), (ALLGOALS Clarsimp_tac), (dtac is_der_virt_id 1), contr_tac 1, (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), (etac allE 1), (thin_tac "?P --> ?Q" 1), (etac impE 1), (rtac oth_red_nkr_elI'' 1), (etac idv_Enc_equiv_dI 1), atac 1, Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "idv_red_altr_ns" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX G'. (G', G) : oth_red_altr & Not (G' <= G))" (fn _ => [ Clarify_tac 1, (datac idv_red_nkr_ns 1 1), Clarify_tac 1, (dtac oth_red_nkr_altr 1), Fast_tac 1 ]) ; val _= bind_thm ("idv_red_nkr", idv_red_nkr_ns RS tacthm (etac conjunct1 2) ex_forward) ; val _= bind_thm ("idv_red_altr", idv_red_altr_ns RS tacthm (etac conjunct1 2) ex_forward) ; val _ = qed_goal_spec_mp "idv_orkvs" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX G' Cs. ((G', Cs), G) : orkvs & satvss (G', Cs) MN)" (fn _ => [ Safe_tac, (fatac idv_red_altr 1 1), Safe_tac, (ftac (orkvs_orar RS iffD2) 1), Clarsimp_tac 1, (REPEAT_FIRST (ares_tac [exI, conjI])), (dtac (oth_red_altr' RS subsetD) 1), (eatac (red_nc RS iffD2) 1 1) ]) ; val _ = qed_goal_spec_mp "idv_orkvss" Spi_Reduce.thy "satvss (S, Us) MN --> ~ is_der_virt (S, MN) --> (EX S' Us'. \ \ ((S', Us'), (S, Us)) : orkvss & satvss (S', Us') MN)" (fn _ => [ Clarsimp_tac 1, (datac idv_orkvs 1 1), Clarsimp_tac 1, (REPEAT_FIRST (resolve_tac [exI, conjI])), (eatac orkvss.I 1 1), Fast_tac 1 ]) ; (* orkvss takes you to S' which is oth_red_altr-minimal *) val _ = qed_goal_spec_mp "ex_orkvss_idv_ea_min'" Spi_Reduce.thy "(S, Us) : wfp orkvss --> (EX S' Us'. ((S', Us'), (S, Us)) : orkvss^* & \ \ S' : rsmin oth_red_altr UNIV & \ \ (ALL MN. satvss (S, Us) MN --> is_der_virt (S', MN) & \ \ satvss (S', Us') MN))" (fn _ => [ (rtac impI 1), (etac wfp_induct_pair 1), (case_tac "a : rsmin oth_red_altr UNIV" 1), (etac thin_rl 1), (rtac exI 1), (rtac exI 1), (rtac conjI 1), (rtac rtrancl_refl 1), Clarsimp_tac 1, (etac contrapos_pp 1), (datac idv_red_altr 1 1), (force_tac (cesimps [rsmin_def]) 1), (clarsimp_tac (cesimps [rsmin_def]) 1), (dtac (orkvs_orar RS iffD2) 1), Clarify_tac 1, (etac allE2 1), (etac impE 1), etac orkvss.I 1, Clarify_tac 1, (rtac exI 1), (rtac exI 1), (rtac conjI 1), (rtac tct.rsr 1), (etac orkvss.I 2), atac 1, etac conjI 1, (etac all_forward 1), (etac all_forward 1), (rtac impI 1), etac mp 1, (clarsimp_tac (cesimps [ball_Un]) 1), (eatac (orkvs_idv_nc RS iffD2) 2 1) ]) ; val _ = qed_goal_spec_mp "ex_orkvss_idv'" Spi_Reduce.thy "(S, Us) : wfp orkvss --> satvss (S, Us) MN --> \ \ (EX S' Us'. is_der_virt (S', MN) & \ \ ((S', Us'), (S, Us)) : orkvss^* & satvss (S', Us') MN)" (fn _ => [ (rtac impI 1), (etac wfp_induct_pair 1), (rtac impI 1), (case_tac "?P :: bool" 1), (datac idv_orkvss 1 2), Clarify_tac 2, (etac allE 2), mp_tac 2, Clarsimp_tac 2, (REPEAT_FIRST (resolve_tac [exI, conjI])), (SOMEGOAL (eatac tct.rsr 1)), (REPEAT_FIRST atac), (rtac rtrancl_refl 1) ]) ; val ex_orkvss_idv_ea_min = wfp_orkvss RS ex_orkvss_idv_ea_min' ; (* also, ex_orkvss_idv(') easily follows from ex_orkvss_idv_ea(') *) val ex_orkvss_idv = wfp_orkvss RS ex_orkvss_idv' ; (* orkvss is characterised by the fact that if a set of constraints is satisfiable, then it can be reduced repeatedly until you get a set of constraints which are all right-satisfiable ; the converse is also true, by subst_orkvss_if_rtc *) val _ = qed_goal_spec_mp "idv_red_nkr_wfp" Spi_Reduce.thy "G : wfp oth_red_nkr --> (G, MN) : indist --> \ \ (EX H. (H, G) : oth_red_nkr^* & is_der_virt (H, MN))" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), rtac impI 1, (case_tac "?P :: bool" 1), (fatac idv_red_nkr 1 2), Fast_tac 1, (etac exE 1), (etac allE 1), mp_tac 1, (etac conjE 1), (etac impE 1), (eatac (red_nkr_nc RS iffD2) 1 1), (REPEAT_SOME (eresolve_tac [ex_forward, conj_forward, asm_rl])), (eatac tct.rsr 1 1) ]) ; val _ = qed_goal_spec_mp "wfp_indist_norm_excl" Spi_Reduce.thy "G : wfp oth_red_nkr --> (G, MN) : indist --> (G, MN) : indist_norm_excl" (fn _ => [ Clarify_tac 1, (datac idv_red_nkr_wfp 1 1), Clarify_tac 1, (etac rtrancl_induct 1), (etac indist_norm_excl.virt 1), (etac oth_red_nkr.elims 1), ALLGOALS Clarsimp_tac, (eatac indist_norm_excl.plI 1 1), (eatac indist_norm_excl.elI 1 1), (etac indist_norm_excl_wk 1), Fast_tac 1 ]) ; (* don't yet have indist_norm_excl <= indist_norm, requires cut-elimination for indist_norm (because indist_norm, but not indist_norm_excl, does without keys in major premise of plI rule), so do the same for indist_norm *) val _ = qed_goal_spec_mp "wfp_indist_norm" Spi_Reduce.thy "G : wfp oth_red_nkr --> (G, MN) : indist --> (G, MN) : indist_norm" (fn _ => [ Clarify_tac 1, (datac idv_red_nkr_wfp 1 1), Clarify_tac 1, (etac rtrancl_induct 1), (etac indist_norm.virt 1), (etac oth_red_nkr.elims 1), ALLGOALS Clarsimp_tac, (rtac (insertI1 RS indist_norm.plI) 1), (rtac (insertI1 RS indist_norm.elI) 2), (etac idv_wki 2), (TRYALL (etac indist_norm_wk THEN' Fast_tac)) ]) ; val _ = bind_thm ("finite_ine", wfp_oth_red_nkr RS wfp_indist_norm_excl) ; val _ = bind_thm ("finite_in", wfp_oth_red_nkr RS wfp_indist_norm) ; val _ = qed_goal_spec_mp "ind_ine" Spi_Reduce.thy "indist <= indist_norm_excl" (fn _ => [ Safe_tac, (dtac indist_finite_char 1), Clarify_tac 1, (datac finite_ine 1 1), (eatac indist_norm_excl_wk 1 1) ]) ; val _ = qed_goal_spec_mp "ind_in" Spi_Reduce.thy "indist <= indist_norm" (fn _ => [ Safe_tac, (dtac indist_finite_char 1), Clarify_tac 1, (datac finite_in 1 1), (eatac indist_norm_wk 1 1) ]) ; val _ = bind_thm ("indist_norm", mk_eq ([indist_norm_le, ind_in] MRS subset_antisym)) ; fun dest_norm th = rewrite_rule [indist_norm] th ; fun mk_norm th = fold_rule [indist_norm] th ; val _ = qed_goal_spec_mp "ine_in" Spi_Reduce.thy "indist_norm_excl <= indist_norm" (fn _ => [ rtac subsetI 1, (etac indist_norm_excl.induct 1), (etac indist_norm.virt 1), (rtac (insertI1 RS indist_norm.plI) 1), (rtac (insertI1 RS indist_norm.elI) 2), (etac idv_wki 2), (etac indist_norm_wk 1), Fast_tac 1, (SELECT_GOAL (rewtac indist_norm) 1), (rtac indist_wki' 1), (etac indist_ca1 1), Fast_tac 1, (etac (virt_indist RS indist_wki) 1) ]) ; val _ = bind_thm ("indist_norm_excl", mk_eq ([ine_in, mk_norm ind_ine] MRS subset_antisym)) ; val dest_ne = rewrite_rule [indist_norm_excl] ; val mk_ne = fold_rule [indist_norm_excl] ; val _ = qed_goal_spec_mp "nkr_not_idv_lem" Spi_Reduce.thy "(H, G') : oth_red_nkr --> h:H --> ~ is_der_virt (G, h) --> \ \ (ALL g':G'. is_der_virt (G, g')) --> \ \ (EX K. (K, G) : oth_red_nkr & (EX k:K. ~ is_der_virt (G, k)))" (fn _ => [ (safe_tac (ces [oth_red_nkr.elims])), Fast_tac 5, Fast_tac 3, (ALLGOALS (EVERY' [ ftac (insertI1 RSN (2, bspec)), Clarsimp_tac, rtac exI, rtac conjI])), (TRYALL (etac bexI)), (TRYALL (etac oth_red_nkr_plI'' THEN' Fast_tac)), (rtac oth_red_nkr_elI'' 1), atac 2, Fast_tac 2, (rtac idv_Enc_equiv_dI 1), (etac idv_ca 1), (rtac Un_upper2 1), atac 1 ]) ; val _ = qed_goal_spec_mp "idv_red_nkr_not_idv_wfp" Spi_Reduce.thy "G : wfp oth_red_nkr --> (G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX H. (H, G) : oth_red_nkr & (EX h:H. ~ is_der_virt (G, h)))" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), Clarify_tac 1, (fatac idv_red_nkr 1 1), etac exE 1, (case_tac "?P :: bool" 1), (rtac exI 1), (eatac conjI 1 1), Clarsimp_tac 1, (etac allE 1), mp_tac 1, (etac conjE 1), (etac impE 1), (eatac (red_nkr_nc RS iffD2) 1 1), (etac impE 1), (etac contrapos_nn 1), (etac idv_ca 1), (rtac Un_upper2 1), (atac 1), (Clarify_tac 1), (rtac nkr_not_idv_lem 1), atac 4, atac 1, atac 1, (etac contrapos_nn 1 THEN eatac red_nkr_idv_nc 1 1) ]) ; val _ = qed_goal_spec_mp "idv_red" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> (EX G'. (G', G) : oth_red)" (fn _ => [ (rtac impI 1), (etac indist.induct 1), (ALLGOALS Clarsimp_tac), (dtac is_der_virt_id 1), contr_tac 1, (dtac oth_red_plI'' 1), etac exI 1, (datac oth_red_elI'' 1 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "idv_red_alt" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX G'. (G', G) : oth_red_alt)" (fn _ => [ Safe_tac, (datac idv_red 1 1), etac exE 1, (etac oth_red_alt_lem 1) ]) ; val _ = qed_goal_spec_mp "idv_red_nk" Spi_Reduce.thy "(G, MN) : indist --> ~ is_der_virt (G, MN) --> \ \ (EX G'. (G', G) : oth_red_nk)" (fn _ => [ Safe_tac, (datac idv_red_alt 1 1), etac exE 1, (dtac oth_red_alt_nk 1), etac ex_forward 1, etac conjunct1 1 ]) ; val _ = qed_goal_spec_mp "oth_red_altr_lems" Spi_Reduce.thy "(D, G) : oth_red --> (EX D'. (D', G) : oth_red_altr)" (fn _ => [ (safe_tac (ces [oth_red.elims])), (dtac oth_red_altr.plI 1), (etac exI 1), (case_tac "?P :: bool" 1), (datac oth_red_altr.elI 1 1), (etac exI 1), (etac (idv_red_altr RS exE) 1), (simp_tac (esimps [idv_Enc_equiv]) 1), etac exI 1 ]) ; val oth_red_altr_lem = oth_red_alt RS subsetD RS oth_red_altr_lems ; (* an alternative proof, requiring finiteness, using red_alt_lem ; a less elegant approach, but keep this as it is in TPHOLs 2009 paper *) val _ = qed_goal_spec_mp "oth_red_altr_lem'" Spi_Reduce.thy "ALL D G. card G < n --> finite G --> (D, G) : oth_red_alt --> \ \ (EX D'. (D', G) : oth_red_altr)" (fn _ => [ (induct_tac "n" 1), Simp_tac 1, (safe_tac (ces [oth_red_alt.elims])), (rtac exI 1), (etac oth_red_altr.plI 1), (case_tac "is_der_virt (oth, Mk, Nk)" 1), (rtac exI 1), (eatac oth_red_altr.elI 1 1), (datac idv_red_alt 1 1), Clarsimp_tac 1, (etac allE2 1), (REPEAT (mp_tac 1)), etac exE 1, (dtac oth_red_altr_sub 1), (rtac subset_insertI 1), Fast_tac 1 ]) ; val oth_red_altr_lemf = lessI RS oth_red_altr_lem' ; val _ = qed_goal_spec_mp "oth_red_nkr_lem" Spi_Reduce.thy "(D, G) : oth_red_nk --> (EX D'. (D', G) : oth_red_nkr)" (fn _ => [ (safe_tac (ces [oth_red_nk.elims])), (dtac oth_red_nkr.plI 1), (etac exI 1), (case_tac "?P :: bool" 1), (datac oth_red_nkr.elI 1 1), (etac exI 1), (eatac (idv_red_nkr RS exE) 1 1), (dtac oth_red_nkr_sub 1), (rtac subset_insertI 1), Fast_tac 1 ]) ; val _ = qed_goalw_spec_mp "rsmin_or_altr" Spi_Reduce.thy [rsmin_def] "(G : rsmin oth_red_altr UNIV) = (G : rsmin oth_red_alt UNIV)" (fn _ => [ Safe_tac, (dtac (oth_red_altr RS subsetD) 2), Fast_tac 2, (dtac oth_red_altr_lem 1), Fast_tac 1 ]) ; val _ = bind_thm ("nf_props_orar", [wfp_oth_red_altr, oth_red_altr, tacthm (etac (rsmin_or_altr RS iffD1) 1) subsetI] MRS transfer Spi_Reduce.thy nf_sub_lem) ; val _ = bind_thm ("nf_props_ora", [wfp_oth_red_alt, oth_red_alt, rsmin_or_alt RS equalityD1] MRS transfer Spi_Reduce.thy nf_sub_lem) ; val _ = qed_goalw_spec_mp "rsmin_or_nkr" Spi_Reduce.thy [rsmin_def] "finite G --> (G : rsmin oth_red_nkr UNIV) = (G : rsmin oth_red_nk UNIV)" (fn _ => [ Safe_tac, (dtac (oth_red_nkr RS subsetD) 2), Fast_tac 2, (dtac oth_red_nkr_lem 1), Fast_tac 1 ]) ; val _ = qed_goalw_spec_mp "nf_oth_red" Spi_Reduce.thy [nf_def, nf_props_def] "finite x --> nf_props oth_red x (nf oth_red x)" (fn _ => [ (rtac impI 1), (rtac someI_ex 1), (ftac wfp_oth_red_finite 1), (dtac snwfp_rsmin_rtc 1), (rtac UNIV_I 1), (etac ex_forward 1), Asm_simp_tac 1, (rewtac tri_prop_def), Clarify_tac 1, (datac oth_red_confl_rtc 1 1), (chop_tac 1 (atac 1)), Clarify_tac 1, (etac mem_same_Pair1 1), (eatac rtranclE 1 1), (eatac rsminE 1 1) ]) ; val [nf_or_rtc, nf_or_min, nf_or_tp] = [nf_oth_red] RL nf_propsDs ; val _ = qed_goalw_spec_mp "nf_oth_red_alt" Spi_Reduce.thy [nf_def] "finite G --> nf_props oth_red_alt G (nf oth_red_alt G)" (fn _ => [ (rtac impI 1), (rtac someI 1), (rtac nf_props_ora 1), (etac nf_oth_red 2), atac 1 ]) ; val [nf_ora_rtc, nf_ora_min, nf_ora_tp] = [nf_oth_red_alt] RL nf_propsDs ; val _ = bind_thm ("nf_or_ora", reop tl (nf_oth_red RSN (2, nf_props_ora) RS nf_unique)) ; val _ = bind_thm ("nf_ora_orar", reop tl (nf_oth_red_alt RSN (2, nf_props_orar) RS nf_unique)) ; val _ = qed_goal_spec_mp "nf_nc" Spi_Reduce.thy "finite oia --> ((nf oth_red oia, MN) : indist) = ((oia, MN) : indist)" (fn _ => [ (rtac impI 1), (rtac red_nc_rtc 1), (etac nf_or_rtc 1) ]) ; val _ = qed_goal_spec_mp "nf_fn_nc" Spi_Reduce.thy "finite oia --> fn_oth (nf oth_red oia) = fn_oth oia" (fn _ => [ (rtac impI 1), (rtac fn_nc_rtc 1), (etac nf_or_rtc 1) ]) ; val _ = bind_thm ("oth_red_finite_nf", reop (fn [x, y] => [x]) (nf_or_rtc RS oth_red_finite_rtc)) ; val _ = bind_thm ("finite_nf_or_of", finite_oth_of RS oth_red_finite_nf) ; AddIffs [finite_nf_or_of] ; val _ = qed_goal_spec_mp "finite_red_pe" Spi_Reduce.thy "finite (red_pair y S) = finite S & finite (red_enc y S) = finite S" (fn _ => [ (case_tac "y" 1), (case_tac "a" 1), (ALLGOALS (case_tac "b")), Auto_tac ]) ; Addsimps [finite_red_pe] ; val _ = qed_goal_spec_mp "is_der_virt_red'" Spi_Reduce.thy "oth : rsmin oth_red UNIV --> \ \ (ALL MN N. MN = (M, N) --> \ \ is_der_virt (oth, MN) = is_der_virt_red (oth, MN))" (fn _ => [ (rtac impI 1), (induct_tac "M" 1), (ALLGOALS Clarify_tac), (ALLGOALS (case_tac "N")), (ALLGOALS Clarsimp_tac), (ALLGOALS (rtac iffI)), (TRYALL (etac disjI2)), (ALLGOALS (etac disjE)), (TRYALL atac), (ALLGOALS (EVERY' [clarsimp_tac (cesimps [rsmin_def]), (etac allE), (etac notE)] )), (etac oth_red_plI'' 1), (rtac oth_red_elI'' 1), atac 2, (etac allE 1 THEN datac iffD2 1 1), (etac virt_indist 1) ]) ; val is_der_virt_red = surjective_pairing RSN (2, is_der_virt_red') ; (* reduction as a function *) (* fix up permissive recdef definition *) val reduce_induct' = tacsthm [ Clarify_tac 1, (eatac setsum_diff1_less_nat 1 1), (etac Encs.elims 1), Asm_simp_tac 1 ] reduce.induct ; val reduce_simps' = tacsthm [ Clarify_tac 1, (eatac setsum_diff1_less_nat 1 1), (etac Encs.elims 1), Clarsimp_tac 1 ] reduce.simps ; fun smtacsf _ = [ (safe_tac (ces [Encs.elims, Mpairs.elims])), (simp_tac (esimps [measure_def, inv_image_def]) 1), (rtac xt7 1), (rtac setsum_insert2_le 2), (rtac xt1 1), (etac ssd1 1), ALLGOALS Simp_tac ] ; val _ = qed_goal_spec_mp "red_enc_smaller" Spi_Reduce.thy "x : Encs <*> Encs --> x : S --> finite S --> \ \ (red_enc x (S - {x}), S) : measure (setsum (size o fst))" smtacsf ; val _ = qed_goal_spec_mp "red_pair_smaller" Spi_Reduce.thy "x : Mpairs <*> Mpairs --> x : S --> finite S --> \ \ (red_pair x (S - {x}), S) : measure (setsum (size o fst))" smtacsf ; val [red_pair_smaller', red_enc_smaller'] = map (simplify (esimps [measure_def, inv_image_def])) [red_pair_smaller, red_enc_smaller] ; val sf = prove_goal Main.thy "((a & b --> c) & a & b) = (a & b & c)" fn_ft1 ; val _ = qed_goal "reduce_simps" Spi_Reduce.thy "reduce S = (if infinite S then S \ \ else let P = %x. x : Mpairs <*> Mpairs & x : S; \ \ Q = %x. x : Encs <*> Encs & x : S \ \ & is_der_virt_red (reduce (S - {x}), keys x) \ \ in if Ex P then reduce (red_pair (Eps P) (S - {Eps P})) \ \ else if Ex Q then reduce (red_enc (Eps Q) (S - {Eps Q})) else S)" (fn _ => [ (rtac trans 1), (rtac reduce_simps' 1), Clarsimp_tac 1, (rewtac Let_def), (REPEAT_FIRST (resolve_tac [refl, if_cong])), Fast_tac 2, Clarsimp_tac 1, (etac notE 1), (rtac red_pair_smaller 1), (rtac someI2 1), Fast_tac 1, Fast_tac 1, (rtac someI2 1), Fast_tac 1, Fast_tac 1, atac 1, (simp_tac (esimps [sf]) 1), (etac someI2_ex 1), Clarify_tac 1, (etac notE 1), (etac notE 1), (rtac red_enc_smaller 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "infinite_reduce" Spi_Reduce.thy "infinite S --> reduce S = S" (fn _ => [ (clarsimp_tac (cesimps [reduce_simps]) 1) ]) ; (* corresponding result for red_enc needs an inductive proof *) val _ = qed_goal_spec_mp "red_pair_oth_red_alt" Spi_Reduce.thy "x : Mpairs <*> Mpairs --> x : S --> \ \ (red_pair x (S - {x}), S) : oth_red_alt" (fn _ => [ (clarsimp_tac (ces [Mpairs.elims], esimps []) 1), (etac oth_red_alt_plIi'' 1) ]) ; val _ = qed_goal_spec_mp "reduce_ora" Spi_Reduce.thy "(reduce S, S) : oth_red_alt^*" (fn _ => [ (res_inst_tac [("a", "S")] (wf_measure RS wf_induct) 1), (stac reduce_simps 1), rewtac Let_def, (simp_tac (HOL_basic_ss addsimps (rtrancl_refl :: simp_thms) addsplits [split_if]) 1), (REPEAT_FIRST (resolve_tac [conjI, impI])), (TRYALL (rtac someI2_ex THEN' atac)), (TRYALL (EVERY' [rtac tct.rsr, etac allE, etac mp])), (REPEAT_FIRST (etac conjE)), (TRYALL (eatac red_pair_oth_red_alt 1)), (TRYALL (eatac red_pair_smaller 2)), (TRYALL (eatac red_enc_smaller 2)), (* now the proof for red_enc, for which the first premise requires the induction *) (clarsimp_tac (ces [Encs.elims], esimps []) 1), (rtac oth_red_alt_elIi'' 1), atac 2, (dtac virt_red_indist 1), (rtac (oth_red_alt_rtc RS subsetD RS red_nc_rtc RS iffD1) 1), atac 2, (etac allE 1), (etac mp 1), (simp_tac (esimps [measure_def, inv_image_def]) 1), (rtac setsum_diff1_less_nat 1), Auto_tac ]) ; val _ = bind_thm ("reduce_oth_red", reduce_ora RS (oth_red_alt_rtc RS subsetD)) ; val _ = bind_thm ("reduce_finite", reduce_oth_red RS oth_red_finite_rtc) ; val _ = bind_thm ("reduce_nc", reduce_oth_red RS red_nc_rtc) ; val _ = qed_goal "reduce_finite_iff" Spi_Reduce.thy "finite (reduce G) = finite G" (fn _ => [ (rtac iffI 1), (etac reduce_finite 2), (etac contrapos_pp 1), (stac reduce_simps 1), Asm_simp_tac 1 ]) ; val _ = qed_goal "reduce_empty" Spi_Reduce.thy "reduce {} = {}" (fn _ => [ (rtac trans 1), (rtac reduce_simps 1), Auto_tac ]) ; Addsimps [reduce_empty, reduce_finite_iff] ; val _ = qed_goal_spec_mp "reduce_smaller" Spi_Reduce.thy "finite S --> (SUM x: reduce S. size (fst x)) <= (SUM x:S. size (fst x))" (fn _ => [ (rtac impI 1), (cut_inst_tac [("S", "S")] reduce_oth_red 1), (dtac (rtrancl_eq_or_trancl RS iffD1) 1), (etac disjE 1), Asm_simp_tac 1, (etac conjE 1), (dtac oth_red_tc_smaller 1), (Asm_simp_tac 2), (etac reduce_finite 1) ]) ; val suml_ne = prove_goal Main.thy "setsum f A < (setsum f B :: nat) --> A ~= B" fn_ft1 RS mp ; val rrpne = [red_pair_smaller', reduce_smaller] MRS xt7 RS suml_ne ; val rrene = [red_enc_smaller', reduce_smaller] MRS xt7 RS suml_ne ; (* characterising reduced observer theories *) val _ = qed_goal_spec_mp "reduce_same'" Spi_Reduce.thy "finite S --> (reduce S = S) = (let P = %x. x : Mpairs <*> Mpairs & x : S; \ \ Q = %x. x : Encs <*> Encs & x : S \ \ & is_der_virt_red (reduce (S - {x}), keys x) in Not (Ex P) & Not (Ex Q))" (fn _ => [ (rtac impI 1), (stac reduce_simps 1), rewtac Let_def, (asm_simp_tac (HOL_basic_ss addsimps (simp_thms) addsplits [split_if]) 1), (REPEAT_FIRST (resolve_tac [iffI, conjI, impI])), TRYALL atac, (REPEAT_FIRST (etac conjE)), TRYALL contr_tac, (ALLGOALS (etac contrapos_pn THEN' resolve_tac [rrene, rrpne])), (TRYALL atac), (ALLGOALS Simp_tac), (TRYALL (etac someI2_ex THEN' Fast_tac)) ]) ; val reduce_same = rewrite_rule [Let_def] reduce_same' ; val _ = qed_goal_spec_mp "nf_no_lefte" Spi_Reduce.thy "seq : derrec indpsc {} --> (ALL G MN. seq = (G, MN) --> \ \ G : rsmin oth_red UNIV --> seq : derrec indpsc_virt {})" (fn _ => [ (rtac impI 1), (etac drs.inductre 1), (safe_tac (ces [indpsc.elims])), (rtac drs.derI' 1), atac 1, Clarify_tac 1, (datac bspec 1 1), (datac virt_nc 1 1), Force_tac 1, (rewtac rsmin_def), (ALLGOALS Clarsimp_tac), (ALLGOALS (etac allE THEN' etac notE)), (etac oth_red_plI'' 1), (eatac (mk_der oth_red_elI'') 1 1) ]) ; val nf_no_left = refl RSN (2, nf_no_lefte) ; val _ = bind_thm ("nf_no_left'", rewrite_rule [mk_eq virt_dec, symmetric indist_derrec] nf_no_left) ; val _ = bind_thm ("nf_no_left_red", reop (fn [x,y,z] => [x,y]) (rewrite_rule [mk_eq fst_conv] ([is_der_virt_red, nf_no_left'] MRS iffD1))) ; val nf_no_left_redr = reop rev nf_no_left_red ; val lnef = arg_cong RSN (2, less_imp_neq RS notE) ; val flne = tacthm (etac (reop rev lnef) 1) notI ; val _ = qed_goal_spec_mp "reduce_ora_min" Spi_Reduce.thy "finite S --> reduce S : rsmin oth_red_alt UNIV" (fn _ => [ (res_inst_tac [("a", "S")] (wf_measure RS wf_induct) 1), (rtac impI 1), (stac reduce_simps 1), rewtac Let_def, (asm_simp_tac (HOL_basic_ss addsimps simp_thms addsplits [split_if]) 1), (REPEAT_FIRST (resolve_tac [conjI, impI])), (TRYALL (rtac someI2_ex THEN' atac)), (TRYALL (EVERY' [ etac allE, etac impE, etac mp o incr, REPEAT o etac conjE, resolve_tac [red_pair_smaller, red_enc_smaller ], atac, atac, atac, Simp_tac ])), (simp_tac (esimps [rsmin_def]) 1), (safe_tac (ces [oth_red_alt.elims])), (chop_tac 1 (etac notE 1)), (REPEAT (etac thin_rl 1)), Fast_tac 1, (etac notE 1), (REPEAT_FIRST (resolve_tac [exI, conjI, insertI1, SigmaI, Encs.I])), Simp_tac 1, (rtac nf_no_left_red 1), (asm_simp_tac (esimps [reduce_nc]) 2), (simp_tac (esimps [rsmin_or_alt RS sym]) 1), (etac allE 1), (etac impE 1), (etac mp 2), Full_simp_tac 2, (asm_simp_tac (esimps [measure_def, inv_image_def]) 1), (stac setsum_insert 1), atac 2, Simp_tac 2, Full_simp_tac 1 ]) ; val _ = bind_thm ("reduce_or_min", asf [rsmin_or_alt] reduce_ora_min) ; val _ = bind_thm ("is_der_virt_reduce", reduce_or_min RS is_der_virt_red) ; Addsimps [reduce_or_min] ; val _ = bind_thm ("red_orE", (simplify (esimps [rsmin_def]) reduce_or_min RS spec RS notE)) ; val _ = qed_goal_spec_mp "virt_reduce" Spi_Reduce.thy "finite oth --> is_der_virt (reduce oth, MN) = ((oth, MN) : indist)" (fn _ => [ (rtac impI 1), (rtac iffI 1), (full_simp_tac (esimps [indist_derrec, virt_dec RS sym]) 1), (dtac der_mono 1), (rtac (mk_mono indpsc.virt) 1), (rtac empty_subsetI 1), (etac (mk_der reduce_nc RS iffD1) 1), (rtac nf_no_left' 1), (etac (reduce_nc RS iffD2) 1), (Asm_simp_tac 1) ]) ; val _ = qed_goal_spec_mp "virt_reduce_sub" Spi_Reduce.thy "finite oth --> oth >= reduce oth --> \ \ is_der_virt (oth, MN) = ((oth, MN) : indist)" (fn _ => [ Safe_tac, (etac virt_indist 1), (datac (virt_reduce RS iffD2) 1 1), (eatac idv_wk 1 1) ]) ; val _ = qed_goal_spec_mp "virt_reduce_sub_Ne" Spi_Reduce.thy "finite oth --> oth >= reduce oth - Ne --> \ \ is_der_virt (oth, MN) = ((oth, MN) : indist)" (fn _ => [ Safe_tac, (etac virt_indist 1), (datac ([idv_Ne, virt_reduce] MRS trans RS iffD2) 1 1), (eatac idv_wk 1 1) ]) ; val _ = bind_thm ("idvr_reduce", rdp ([virt_reduce RS sym, reduce_or_min RS is_der_virt_red] MRS trans)) ; val _ = bind_thm ("reduce_Ne_nc", [reduce_nc RS sym, name_equivd] MRS trans) ; val _ = bind_thm ("idv_sets_reduce", [virt_reduce RS sym, idv_sets] MRS trans) ; val _ = qed_goal_spec_mp "virt_reduce_sub_Ne_inv" Spi_Reduce.thy "(ALL MN. ((oth, MN) : indist) --> is_der_virt (oth, MN)) --> \ \ finite oth --> oth >= reduce oth - Ne" (fn _ => [ (Clarify_tac 1), (etac allE 1), (etac impE 1), (rtac (reduce_nc RS iffD1) 1), (etac indist.id 1), (dtac (virt_dec RS iffD2) 1), (etac (hd drs.elims) 1), Safe_tac, (etac indpsc_virt.elims 1), Safe_tac, (dtac oth_red_plI'' 1), (eatac red_orE 1 1), (full_simp_tac (esimps [virt_dec]) 1), (REPEAT (dtac virt_indist 1)), (dtac (reop rev oth_red_elI'') 1), (simp_tac (esimps [reduce_nc]) 1), (eatac red_orE 1 1) ]) ; val _ = qed_goal_spec_mp "idv_sets_reduce_le" Spi_Reduce.thy "finite G --> G >= reduce G --> \ \ ((G, MN) : indist) = (EX sp:idv_sets MN. sp <= G)" (fn _ => [ Safe_tac, (clarsimp_tac (cesimps [idv_sets_reduce]) 1), (etac rev_bexI 1), (eatac subset_trans 1 1), (eatac ([idv_sets, bexI] MRS iffD2 RS virt_indist) 1 1) ]) ; val thfr = [oth_red_nk_finite_iff RS iffD1 RS wfp_oth_red_nkr, UNIV_I] MRS snwfp_rsmin_rtc ; val _ = qed_goal_spec_mp "or_nkr_Un_lemw'" Spi_Reduce.thy "finite G --> (H, G) : oth_red_nkr --> (K, G Un H) : oth_red_nk^* --> \ \ (K, k) : indist --> \ \ (EX K'. (K', G) : oth_red_nkr^+ & is_der_virt (K', k))" (fn _ => [ Safe_tac, (ftac (oth_red_nkr RS subsetD) 1), (datac (red_nk_nc_rtc RS iffD1) 1 1), (dtac indist_extra 1), Clarify_tac 1, (eatac (red_nk_nc RS iffD1) 1 1), Full_simp_tac 1, (fatac (red_nk_nc RS iffD2) 1 1), (fatac thfr 1 1), (etac ex_forward 1), Safe_tac, (eatac tct.rst 1 1), (ftac (oth_red_nkr RSN (2, rtrancl_mono')) 1), (rtac nf_no_left' 1), (eatac (red_nk_nc_rtc RS iffD2) 1 1), (rtac ([rsmin_or_nkr, rsmin_nk_equiv RS set_cong] MRS trans RS iffD1) 1), atac 2, (etac (oth_red_nk_finite_rtc_iff RS iffD1) 1), (eatac (oth_red_nk_finite_iff RS iffD1) 1 1) ]) ; val or_nkr_Un_lemw = [asm_rl, asm_rl, ([trancl_into_rtrancl, oth_red_nkr] MRS rtrancl_mono'), indist.id] MRS or_nkr_Un_lemw' ; val _ = bind_thm ("smder_norm", [ dest_norm smder_norm_alt, indist_smpsc_eq RS sym] MRS trans) ; val _ = bind_thm ("idv_red_nkr_not_idv", reop (fn [a,b,c] => [b,c,a]) (wfp_oth_red_nkr RS idv_red_nkr_not_idv_wfp)) ; (* set show_sorts ; reset show_sorts ; set trace_simp ; reset trace_simp ; *) val _ = bind_thm ("nf_acc_alt'", [wfp_oth_red_alt, oth_red_alt, rsmin_or_alt RS equalityD1] MRS nf_or_lem) ; val _ = qed_goalw_spec_mp "nf_acc_altp" Spi_Reduce.thy [nf_props_def] "finite G --> nf_props oth_red G D --> (D, G) : oth_red_alt^*" (fn _ => [ Clarify_tac 1, (eatac nf_acc_alt' 2 1) ]) ; val _ = bind_thm ("nf_acc_alt", reop tl (nf_oth_red RSN (2, nf_acc_altp))) ; (* TO FINISH - use rsmin_or_altr but cope with finiteness ; aim is to prove reduce_orar, "(reduce ?S, ?S) : oth_red_altr^*" [oth_red_altr, asm_rl, wfp_oth_red_altr] MRS nf_sub_lem1 ; *) val _ = bind_thm ("nf_or_char", nf_oth_red RSN (2, nf_extg)) ; (* REDUNDANT now done as nf_props_ora val _ = qed_goalw_spec_mp "nf_alt" Spi_Reduce.thy [nf_props_def] "finite G --> nf_props oth_red G D --> nf_props oth_red_alt G D" (fn _ => [ Safe_tac, (eatac nf_acc_alt' 2 1), (force_tac (cds [oth_red_alt RS subsetD], esimps [rsmin_def]) 1), (simp_tac (esimps [tri_prop_def]) 1), Clarify_tac 1, (dtac (oth_red_alt RSN (2, rtrancl_mono')) 1), (thin_tac "?p : ?S^*" 1), (fatac tri_propD 1 1), (datac tri_ext 1 1), (rtac nf_acc_alt' 1), (eatac oth_red_finite_rtc 3 1) ]) ; *) val _ = qed_goal_spec_mp "nf_props_same" Spi_Reduce.thy "finite G --> nf_props oth_red G D --> nf_props oth_red_alt G D' --> D = D'" (fn _ => [ Clarify_tac 1, (fatac nf_props_ora 1 1), (eatac (rtrancl_refl RS nf_ext) 1 1) ]) ; val _ = qed_goal_spec_mp "nf_same" Spi_Reduce.thy "finite G --> nf oth_red_alt G = nf oth_red G" (fn _ => [ (rtac impI 1), (rtac (nf_props_same RS sym) 1), atac 1, (etac nf_oth_red 1), (etac nf_oth_red_alt 1) ]) ; val _ = qed_goal_spec_mp "rsmin_ora_nf" Spi_Reduce.thy "finite G --> (G : rsmin oth_red_alt UNIV) = (nf oth_red_alt G = G)" (fn _ => [ (rtac impI 1), (rtac iffI 1), (rtac mem_same 2), atac 3, (etac nf_ora_min 2), (full_simp_tac (esimps [rsmin_def]) 1), (rtac (nf_ora_rtc RS rtranclE) 1), Auto_tac ]) ; val _ = bind_thm ("rsmin_or_nf", asf [nf_same, rsmin_or_alt] rsmin_ora_nf) ; val _ = qed_goal_spec_mp "nf_ext_same" Spi_Reduce.thy "finite G --> (D, G) : oth_red^* --> nf oth_red D = nf oth_red G" (fn _ => [ Clarify_tac 1, (rtac (nf_ext RS sym) 1), atac 1, (etac nf_oth_red 1), (rtac nf_oth_red 1), (dtac oth_red_finite_rtc_iff 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "nf_ext_alt_same" Spi_Reduce.thy "finite G --> (D, G) : oth_red_alt^* --> nf oth_red_alt D = nf oth_red_alt G" (fn _ => [ Clarify_tac 1, (rtac (nf_ext RS sym) 1), atac 1, (etac nf_oth_red_alt 1), (rtac nf_oth_red_alt 1), (dtac oth_red_alt_finite_rtc_iff 1), Clarsimp_tac 1 ]) ; val nf_ext_same1 = r_into_rtrancl RSN (2, nf_ext_same) ; val nf_ext_alt_same1 = r_into_rtrancl RSN (2, nf_ext_alt_same) ; val _ = bind_thm ("nf_nf", reop tl (nf_or_rtc RSN (2, nf_ext_same))) ; (* alternative proof below *) val _ = bind_thm ("reduce_nf_alt", reop tl ([reduce_ora, nf_oth_red_alt, reduce_ora_min] MRS nf_extg)) ; val _ = bind_thm ("reduce_nf", asf [nf_same] reduce_nf_alt) ; val _ = bind_thm ("reduce_nf_alt", reop tl ([nf_or_ora RS sym, reduce_nf] MRS trans)) ; val _ = bind_thm ("reduce_nf_altr", reop tl ([nf_ora_orar RS sym, reduce_nf_alt] MRS trans)) ; val _ = bind_thm ("reduce_char", reop tl ([reduce_nf RS sym, nf_or_char] MRS trans)) ; val _ = qed_goal "reduce_rev" Spi_Reduce.thy "reduce (rev_pair ` G) = rev_pair ` reduce G" (fn _ => [ (case_tac "finite G" 1), (asm_simp_tac (esimps [reduce_simps, finite_rp]) 2), (rtac reduce_char 1), (rtac (reduce_oth_red RS oth_red_rtc_rev) 1), (asm_simp_tac (esimps [finite_rp]) 1), (asm_simp_tac (esimps [rsmin_or_rev_iff]) 1) ]) ; (* these next two combine with reduce_same *) val _ = bind_thm ("or_min_reduce", asf [reduce_nf] rsmin_or_nf) ; val _ = bind_thm ("ora_min_reduce", asf [reduce_nf_alt] rsmin_ora_nf) ; val _ = bind_thm ("orar_min_reduce", [rsmin_or_altr, ora_min_reduce] MRS trans) ; (* simplifying using reduce_nf requires frozen - why ?? *) fun mk_ft simps th = let val (fr, thaw) = freeze_thaw th ; in thaw (asm_full_simplify (HOL_basic_ss addsimps simps) fr) end ; val mk_red = mk_ft [reduce_finite_iff, oth_red_finite_nf, finite_oth_of, finite_Diff, reduce_nf] ; val _ = qed_goal "reduce_reduce" Spi_Reduce.thy "reduce (reduce G) = reduce G" (fn _ => [ (case_tac "finite G" 1), (etac (mk_red nf_nf) 1), (asm_simp_tac (esimps [infinite_reduce]) 1) ]) ; Addsimps [reduce_reduce] ; val _ = bind_thm ("reduce_fn_nc", mk_red nf_fn_nc) ; val _ = bind_thm ("reduce_or_char", mk_red nf_or_char) ; val _ = bind_thm ("reduce_not_or", simplify (esimps [rsmin_def]) ([reduce_finite RS or_min_reduce, reduce_reduce] MRS iffD2) RS spec) ; val _ = qed_goal_spec_mp "reduce_diff_Names" Spi_Reduce.thy "finite x --> (EX S'. reduce x - Names ` S' = reduce (x - Names ` S))" (fn _ => [ (rtac impI 1), (rtac (reduce_oth_red RS oth_red_Names_rtc RS ex_forward) 1), (etac (reduce_or_char RS sym) 1), Asm_simp_tac 1, (etac ([reduce_or_min, Diff_subset] MRS rsmin_oth_red_sub) 1) ]) ; val _ = qed_goal_spec_mp "reduce_diff_Names_le" Spi_Reduce.thy "finite x --> reduce (x - Names ` S) <= reduce x" (fn _ => [ (rtac impI 1), (dtac reduce_diff_Names 1), Clarify_tac 1, (dtac equalityD2 1), (datac subsetD 1 1), Fast_tac 1 ]) ; (* suggested by Boreale, Definition 10 *) val _ = qed_goal_spec_mp "reduce_alt" Spi_Reduce.thy "finite G --> MN : reduce G - Ne = ((G, MN) : indist & MN ~: Ne & \ \ MN ~: Mpairs <*> Mpairs & \ \ (MN : Encs <*> Encs --> (G, keys MN) ~: indist))" (fn _ => [ (rtac impI 1), (rtac iffI 1), (clarsimp_tac (cesimps [idvr_reduce]) 2), (case_tac "MN" 2), ((case_tac "a" THEN_ALL_NEW case_tac "b") 2), (ALLGOALS Clarsimp_tac), (REPEAT_FIRST (rtac conjI)), (etac ([reduce_nc, indist.id] MRS iffD1) 1), (clarsimp_tac (ces [Mpairs.elims], esimps []) 1), (dtac oth_red_plI'' 1), (clarsimp_tac (ces [Encs.elims], esimps []) 2), (datac (reduce_nc RS iffD2 RS oth_red_elI'') 1 2), (ALLGOALS (dtac reduce_not_or THEN' contr_tac)) ]) ; val _ = qed_goal_spec_mp "nf_Un" Spi_Reduce.thy "finite x --> finite y --> (x', x) : oth_red --> \ \ nf oth_red (x Un y) = nf oth_red (x' Un y)" (fn _ => [ strip_tac 1, (etac oth_red.elims 1), (ALLGOALS Clarsimp_tac), (* pl rule *) (case_tac "(Mpair Ma Mb, Mpair Na Nb) : y" 1), (rtac (nf_ext_same1 RS sym) 2), Asm_simp_tac 2, (rtac (oth_red.plI RS mem_same_Pair1) 2), Asm_simp_tac 2, Asm_simp_tac 2, (rtac (sym RS trans) 1), (rtac nf_ext_same1 2), Asm_simp_tac 2, (rtac nf_ext_same1 1), Asm_simp_tac 1, (rtac oth_red_plI' 1), (rtac (oth_red_plI'' RS mem_same_Pair1) 1), Fast_tac 1, Force_tac 1, (* el rule *) (subgoal_tac "(insert (Enc Mp Mk, Enc Np Nk) (oth Un y), Mk, Nk) : indist" 1), (etac indist_wk 2), Fast_tac 2, (case_tac "(Enc Mp Mk, Enc Np Nk) : y" 1), (rtac (nf_ext_same1 RS sym) 2), Asm_simp_tac 2, (rtac (oth_red.elI RS mem_same_Pair1) 2), Asm_simp_tac 2, Asm_simp_tac 3, atac 2, (rtac (sym RS trans) 1), (rtac nf_ext_same1 2), Asm_simp_tac 2, (rtac nf_ext_same1 1), Asm_simp_tac 1, (rtac oth_red_elI' 1), atac 1, (rtac (oth_red_elI'' RS mem_same_Pair1) 1), Fast_tac 2, Force_tac 2, (etac indist_wk 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "nf_Un_rtc" Spi_Reduce.thy "finite x --> finite y --> (x', x) : oth_red^* --> \ \ nf oth_red (x Un y) = nf oth_red (x' Un y)" (fn _ => [ strip_tac 1, (etac converse_rtrancl_induct 1), (rtac refl 1), (etac trans 1), (rtac nf_Un 1), (eatac (oth_red_finite_rtc) 1 1), atac 1, atac 1 ]) ; val _ = bind_thm ("nf_nf_Un", reop (fn [x,y,z] => [x,y]) (nf_or_rtc RSN (3, nf_Un_rtc)) RS sym) ; val _ = bind_thm ("nf_ins_nf", simplify (esimps []) (Finites.emptyI RS Finites.insertI RSN (2, nf_nf_Un))) ; (* corollary to nf_no_left *) val _ = qed_goalw_spec_mp "rigid_ind" Spi_Reduce.thy [nf_props_def] "(oth, Rigid a, Rigid b) : indist --> \ \ nf_props oth_red oth othr --> (Rigid a, Rigid b) : othr" (fn _ => [ (Safe_tac), (datac (red_nc_rtc RS iffD2) 1 1), (dtac (dest_der nf_no_left) 1 THEN Force_tac 1), (eresolve_tac drs.elims 1), etac emptyE 1, Clarify_tac 1, (etac indpsc_virt.elims 1), Auto_tac ]) ; val _ = bind_thm ("rsmin_names_alt", fold_rule [mk_eq rsmin_or_alt] rsmin_names) ; val _ = qed_goal_spec_mp "reduce_Names" Spi_Reduce.thy "finite G --> (reduce (G - Ne) = G - Ne) = (reduce G = G)" (fn _ => [ (rtac impI 1), (rtac box_equals 1), (TRYALL (rtac or_min_reduce)), rtac rsmin_names 1, Auto_tac ]) ; val _ = qed_goal_spec_mp "oth_red_alt_Name_nf'" Spi_Reduce.thy "finite oth --> oth' - Ne = oth - Ne --> \ \ oth' : rsmin oth_red_alt UNIV --> \ \ nf oth_red_alt oth - Ne = oth' - Ne" (fn _ => [ Clarify_tac 1, (datac (nf_ora_rtc RS oth_red_alt_Name_rtc) 1 1), Clarify_tac 1, (etac rtranclE 1), Force_tac 1, (eatac rsminE 1 1) ]) ; val oth_red_alt_Name_nf = nf_ora_min RSN (3, oth_red_alt_Name_nf') ; val sub_same = prove_goal Main.thy "(a = b) --> a - n = b - n" fn_at RS mp ; val _ = qed_goal_spec_mp "oth_red_alt_Name_nfs" Spi_Reduce.thy "finite oth --> finite oth' --> oth' - Ne = oth - Ne --> \ \ nf oth_red_alt oth - Ne = nf oth_red_alt oth' - Ne" (fn _ => [ Clarify_tac 1, (fatac (nf_ora_rtc RS oth_red_alt_Name_rtc) 1 1), Clarify_tac 1, (ftac (thin_rl RS oth_red_alt_Name_nf) 1), etac sym 2, atac 2, (eatac oth_red_alt_finite_rtc 1 1), (chop_last (etac (sym RS trans) 1)), (rtac sub_same 1), (eatac nf_ext_alt_same 1 1) ]) ; val _ = bind_thm ("nf_alt_Ne", reop (fn [x,y] => [x]) ([asm_rl, finite_Diff, Diff_idemp] MRS oth_red_alt_Name_nfs RS sym)) ; val nf_ext_alt_same1_sub = nf_ext_alt_same1 RS sub_same ; (* irreducible theories characterised by their indistinguishable pairs *) val _ = qed_goal_spec_mp "same_nf" Spi_Reduce.thy "seq : derrec indpsc_virt {} --> (ALL oth MN del. seq = (oth, MN) --> \ \ finite oth --> finite del --> nf oth_red_alt (oth Un del) - Ne = \ \ nf oth_red_alt (insert MN (oth Un del)) - Ne)" (fn _ => [ (rtac impI 1), (etac drs.inductre 1), (etac indpsc_virt.elims 1), (ALLGOALS Clarify_tac), (rtac box_equals 1), rtac nf_alt_Ne 3, rtac nf_alt_Ne 2, Asm_simp_tac 2, Asm_simp_tac 2, (rtac sub_same 1), (cong1_tac 1), (force_tac (cesimps [Ne.defs]) 1), (rtac sub_same 1), (cong1_tac 1), (Fast_tac 1), ALLGOALS Full_simp_tac, ALLGOALS Clarify_tac, (* pr rule *) (case_tac "(Mpair Ma Mb, Mpair Na Nb) : (otha Un del)" 1), (stac insert_absorb 1), atac 1, rtac refl 1, (etac allE 1), (eatac (mp RS trans) 1 1), (eres_inst_tac [("x", "insert (Ma, Na) del")] allE 1), Clarsimp_tac 1, (rtac nf_ext_alt_same1_sub 1), Asm_simp_tac 1, (rtac (oth_red_alt.plI RS mem_same_Pair1) 1), Asm_simp_tac 1, (simp_tac (esimps [insert_commute]) 1), (* er rule *) (case_tac "(Enc Mp Mk, Enc Np Nk) : (otha Un del)" 1), (stac insert_absorb 1), atac 1, rtac refl 1, (etac allE 1), (eatac (mp RS trans) 1 1), (eres_inst_tac [("x", "insert (Mp, Np) del")] allE 1), Clarsimp_tac 1, (rtac nf_ext_alt_same1_sub 1), Asm_simp_tac 1, (rtac (oth_red_alt.elI RS mem_same_Pair1) 1), Asm_simp_tac 1, (simp_tac (esimps [insert_commute]) 2), (rtac (Un_upper1 RSN (2, indist_wk)) 1), (simp_tac (esimps [indist_derrec]) 1), (etac der_mono 1), (safe_tac (ces [indpsc.virt])) ]) ; val nf_same_nf = (simplify (esimps []) ([nf_no_left, asm_rl, asm_rl, Finites.emptyI] MRS same_nf)) ; val nfs1 = full_simplify (esimps []) (refl RSN (3, nf_same_nf)) ; val nfs2 = (nf_or_min) RSN (2, nfs1) ; val (nfs2', thaw) = freeze_thaw nfs2 ; val nfs3 = asm_simplify (esimps [nf_same, nf_ins_nf, nf_nf]) nfs2' ; val _ = bind_thm ("nf_same_der'", reop (fn [x,y,z] => [x,y]) (oth_red_finite_nf RSN (3, thaw nfs3))) ; val _ = bind_thm ("nf_same_der", reop (fn [x,y,z] => [y,z]) (mk_der nf_nc RS iffD2 RS nf_same_der')) ; val _ = qed_goal_spec_mp "nf_same_der_union" Spi_Reduce.thy "finite othb --> finite otha --> \ \ (ALL MN : othb. (otha, MN) : indist) --> \ \ nf oth_red (otha Un othb) - Ne = nf oth_red otha - Ne" (fn _ => [ rtac impI 1, rtac impI 1, (etac finite_induct 1), Simp_tac 1, (Clarify_tac 1), (etac impE 1), Fast_tac 1, (rtac trans 1), atac 2, (Simp_tac 1), (rtac (dest_der nf_same_der RS sym) 1), Force_tac 2, (dtac (insertI1 RS rev_bspec) 1), (etac indist_wk 1), (rtac Un_upper1 1) ]) ; val _ = qed_goal_spec_mp "nf_equiv_der" Spi_Reduce.thy "finite otha --> finite othb --> \ \ (ALL MN. ((otha, MN) : indist) = ((othb, MN) : indist)) = \ \ (nf oth_red otha - Ne = nf oth_red othb - Ne)" (fn _ => [ (strip_tac 1), (rtac iffI 1), rtac allI 2, (dres_inst_tac [("f", "%oth. (oth, MN) : indist")] arg_cong 2), (asm_full_simp_tac (esimps [nf_nc, name_equivd RS sym]) 2), (rtac box_equals 1), (TRYALL (rtac nf_same_der_union)), (stac Un_commute 1), rtac refl 1, (ALLGOALS Clarsimp_tac), (etac allE2 1), (etac iffD1 1), (etac indist.id 1) ]) ; val nf_equiv_derD1 = [nf_equiv_der, allI] MRS iffD1 ; val nf_equiv_derD2 = nf_equiv_der RS iffD2 RS spec ; val _ = qed_goal_spec_mp "nf_Ne_equiv" Spi_Reduce.thy "finite oth --> nf oth_red (oth - Ne) - Ne = \ \ nf oth_red oth - Ne" (fn _ => [ (rtac impI 1), (rtac nf_equiv_derD1 1), (ALLGOALS Clarsimp_tac), (rtac (name_equivd RS sym) 1) ]) ; val _ = bind_thm ("reduce_equiv_der", mk_red nf_equiv_der) ; val _ = bind_thm ("reduce_Ne_equiv", mk_red nf_Ne_equiv) ; val reduce_equiv_derD1 = [reduce_equiv_der, allI] MRS iffD1 ; val reduce_equiv_derD2 = reduce_equiv_der RS iffD2 RS spec ; val _ = qed_goal_spec_mp "red_nk_same_ex_Ne" Spi_Reduce.thy "(D, G) : oth_red_nk^* --> D : rsmin oth_red_nk UNIV --> \ \ finite G --> D - Ne = reduce G - Ne" (fn _ => [ Clarify_tac 1, (ftac oth_red_nk_finite_rtc_iff 1), (rtac trans 1), (rtac reduce_equiv_derD1 2), (etac red_nk_nc_rtc 4), atac 3, Fast_tac 2, (clarsimp_tac (cesimps [rsmin_nk_equiv, or_min_reduce]) 1) ]) ; val _= qed_goalw_spec_mp "ka_oth_red" Spi_Reduce.thy [ka_oth_def] "ka_oth oth --> (oth', oth) : oth_red --> ka_oth oth'" (fn _ => [ Clarify_tac 1, (etac oth_red.elims 1), (ALLGOALS Clarsimp_tac), (REPEAT_FIRST (etac disjE)), (ALLGOALS Clarify_tac), (TRYALL (datac bspec 1 THEN' Fast_tac)), (fast_tac (cds [atomic_ka]) 1) ]) ; val _= qed_goal_spec_mp "ka_oth_red_rtc" Spi_Reduce.thy "ka_oth oth --> (oth', oth) : oth_red^* --> ka_oth oth'" (fn _ => [ strip_tac 1, (eatac converse_rtrancl_induct 1 1), (eatac ka_oth_red 1 1) ]) ; val _ = bind_thm ("ka_oth_reduce", reduce_oth_red RSN (2, ka_oth_red_rtc)) ; Addsimps [ka_oth_reduce] ; (* single-sided *) val _ = qed_goal_spec_mp "red_pair_paired" Spi_Reduce.thy "x : range pair --> oth <= range pair --> red_pair x oth <= range pair" (fn _ => [ (Clarify_tac 1), (case_tac "x" 1), Auto_tac ]) ; val _ = qed_goal_spec_mp "red_enc_paired" Spi_Reduce.thy "x : range pair --> oth <= range pair --> red_enc x oth <= range pair" (fn _ => [ (Clarify_tac 1), (case_tac "x" 1), Auto_tac ]) ; val [red_pair_paired', red_enc_paired'] = map (rewrite_rule [pair_def]) [red_pair_paired, red_enc_paired] ; val _ = bind_thm ("reduce_paired", reduce_oth_red RSN (2, oth_red_rtc_paired)) ; val _ = bind_thm ("reduce_pair", fold_rule [reduce_ss_def] (subset_UNIV RS image_mono RS reduce_paired RS im_pair_fst RS sym)) ; val _ = qed_goalw_spec_mp "reduce_pairD" Spi_Reduce.thy [mk_eq reduce_pair] "(a, b) : reduce (pair ` S) --> a = b" fn_at ; val _ = qed_goalw "reduce_pair_same" Spi_Reduce.thy [reduce_ss_def] "(reduce_ss S = S) = (reduce (pair ` S) = pair ` S)" (fn _ => [ (rtac iffI 1), (ALLGOALS (clarsimp_tac (cesimps [reduce_pair]))) ]) ; val _ = qed_goalw "reduce_pair_le_iff" Spi_Reduce.thy [reduce_ss_def] "(reduce_ss S <= S) = (reduce (pair ` S) <= pair ` S)" (fn _ => [ (rtac iffI 1), (ALLGOALS (force_tac (cesimps [reduce_pair]))) ]) ; val _ = qed_goalw "reduce_pair_Ne_le_iff" Spi_Reduce.thy [reduce_ss_def] "(reduce_ss S - range Name <= S) = (reduce (pair ` S) - Ne <= pair ` S)" (fn _ => [ Safe_tac, (ALLGOALS (ftac reduce_pairD)), (auto_tac (cesimps [Ne.defs])) ]) ; val _ = bind_thm ("reduce_ss_fn_nc", simplify (esimps [fn_oth_def, mk_eq reduce_pair]) (finite_pair RS iffD2 RS reduce_fn_nc)) ; val _ = qed_goal_spec_mp "reduce_ss_Names" Spi_Reduce.thy "finite S --> (reduce_ss (S - range Name) = S - range Name) = \ \ (reduce_ss S = S)" (fn _ => [ (clarsimp_tac (cesimps [reduce_pair_same]) 1), (rtac trans 1), (rtac reduce_Names 2), (clarsimp_tac (cesimps [pair_Name, pair_diff]) 1), Asm_simp_tac 1 ]) ; val _ = bind_thm ("or_min_reduce_ss", [finite_imageI RS or_min_reduce, reduce_pair_same RS sym] MRS trans) ; val _ = qed_goalw_spec_mp "idv_reduce_ss" Spi_Reduce.thy [idv_ss_def, reduce_ss_def, mk_eq derrec_smpsc_eq] "finite S --> ((S, M) : derrec smpsc {}) = idv_ss (reduce_ss S, M)" (fn _ => [ Clarsimp_tac 1, (stac (rewrite_rule [indist_derrec] (virt_reduce RS sym)) 1), (etac finite_imageI 1), (rtac (im_pair_fst RS arg_cong RS sym) 1), (rtac reduce_paired 1), Fast_tac 1 ]) ; val _ = bind_thm ("idv_reduce_ss_sets", [idv_reduce_ss, idv_ss_sets] MRS trans) ; val _ = qed_goalw_spec_mp "idv_r_ss" Spi_Reduce.thy [idvr_ss_def, idv_ss_def] "finite S --> idvr_ss (reduce_ss S, M) = idv_ss (reduce_ss S, M)" (fn _ => [ (clarsimp_tac (cesimps [reduce_pair RS sym, is_der_virt_reduce]) 1) ]) ; val _ = bind_thm ("idvr_reduce_ss", reop (fn [x,y] => [x]) ([idv_reduce_ss, idv_r_ss RS sym] MRS trans)) ; (* so get a set of constraints such that the requirement is, for each constraint, instead of G |- MN, (EX sp:idv_sets MN. sp <= G)") by idv_sets *) (* but how about substitution ?? *) (* [subst_idv_sets, subst_idv_sets_rev] ; bt_resp_constrs_idv ; bt_resp_constrs_idv_alt ; (* depends on atomic keys *) *) val _ = qed_goal_spec_mp "ine_ora_elim" Spi_Reduce.thy "[| a : indist_norm_excl; !!seq. [| a = seq; is_der_virt seq |] ==> P; \ \ !!MN G G'. [| a = (G, MN); (G', G) : oth_red_altr |] ==> P |] ==> P" (fn [p, pv, po] => [ (rtac (p RS indist_norm_excl.elims) 1), (eatac pv 1 1), ALLGOALS (etac po), (etac oth_red_altr.plI 1), (eatac oth_red_altr.elI 1 1) ]) ; val _ = qed_goal_spec_mp "ine_ora_induct" Spi_Reduce.thy "[| xa : indist_norm_excl; !!seq. [| is_der_virt seq |] ==> P seq ; \ \ !!G MN. [| EX G'. (G', G) : oth_red_altr & P (G', MN) |] \ \ ==> P (G, MN) |] ==> P xa" (fn [p, pv, po] => [ (rtac (p RS indist_norm_excl.induct) 1), (etac pv 1), (ALLGOALS (EVERY' [rtac po, rtac exI, rtac conjI, atac o incr])), (etac oth_red_altr.plI 1), (eatac oth_red_altr.elI 1 1) ]) ; val _ = qed_goal_spec_mp "ine_ora_intro" Spi_Reduce.thy "(G', MN) : indist_norm_excl --> (G', G) : oth_red_altr --> \ \ (G, MN) : indist_norm_excl" (fn _ => [ (safe_tac (ces [oth_red_altr.elims])), (eatac indist_norm_excl.plI 1 1), (eatac indist_norm_excl.elI 2 1) ]) ; val _ = qed_goal_spec_mp "ine_ora_rtc_intro" Spi_Reduce.thy "(G', MN) : indist_norm_excl --> (G', G) : oth_red_altr^* --> \ \ (G, MN) : indist_norm_excl" (fn _ => [ (strip_tac 1), (eatac rtrancl_induct 1 1), (eatac ine_ora_intro 1 1) ]) ; (* indist_alt possible, smaller premises as you go up *) val _ = qed_goal_spec_mp "idv_indist_alt_smaller" Spi_Reduce.thy "is_der_virt (oth, Mk, Nk) --> (oth, Mk, Nk) : derrec (indpsc_alt \ \ Int {(ps, c). ALL p:set ps. seq_fst_size p < seq_fst_size c}) {}" (fn _ => [ (rtac impI 1), (dtac (virt_dec RS iffD2) 1), (etac drs.inductr 1), (ALLGOALS Clarsimp_tac), (etac indpsc_virt.elims 1), (ALLGOALS Clarsimp_tac), (rtac (IntI RS drs.derI) 1), (rtac indpsc_alt.var 1), Force_tac 1, Force_tac 1, (rtac (IntI RS drs.derI) 1), (etac indpsc_alt.id 1), Force_tac 1, Force_tac 1, (rtac (IntI RS drs.derI) 1), (rtac indpsc_alt.prI 1), Force_tac 1, Force_tac 1, (rtac (IntI RS drs.derI) 1), (rtac indpsc_alt.erI 1), Force_tac 1, Force_tac 1 ]) ; val _ = qed_goal_spec_mp "indist_alt_smaller" Spi_Reduce.thy "seq : indist_norm_excl --> finite (fst seq) --> \ \ seq : derrec (indpsc_alt Int {(ps, c). ALL p : set ps. \ \ seq_fst_size p < seq_fst_size c}) {}" (fn _ => [ (rtac impI 1), (etac indist_norm_excl.induct 1), ALLGOALS Clarsimp_tac, (etac idv_indist_alt_smaller 1), (* plI rule *) (rtac (IntI RS drs.derI) 1), (rtac indpsc_alt.plI 1), Clarsimp_tac 1, (rtac (setsum_insert2_le RSN (2, xt7)) 1), Simp_tac 1, Simp_tac 1, (simp_tac (esimps [drs.all]) 1), (* elI rule *) (rtac (IntI RS drs.derI) 1), (rtac indpsc_alt.elI 1), Clarsimp_tac 1, (rtac (setsum_insert2_le RSN (2, xt7)) 1), Simp_tac 1, Simp_tac 1, (asm_simp_tac (esimps [drs.all]) 1), (etac idv_indist_alt_smaller 1) ]) ;