structure Spi_CC = struct val thy = the_context () end ; val _ = use_legacy_bindings Spi_CC.thy ; val _ = bind_thm ("R1_intros'", [notindiffs RS R1.intros, insert_Diff] MRS mem_same_Pair3l) ; val wf_cc_Ds' as [wf_ccDval, wf_ccDfte, wf_ccDcons, wf_ccDfn, wf_ccDred, wf_ccDidv] = conjs (wf_cc.simps RS iffD1) ; val _ = qed_goal_spec_mp "wf_cc_DsN" Spi_CC.thy "wf_cc (h, G) --> bt_sameNs h" (fn _ => [ (rtac impI 1), (rtac bt_fn_same_Ns 1), (TRYALL (eresolve_tac wf_cc_Ds')) ]) ; val wf_cc_Ds = (wf_ccDfte RS finite_imageI) :: wf_cc_DsN :: wf_cc_Ds' ; val _ = qed_goal_spec_mp "wf_cc_Ne" Spi_CC.thy "Ns <= Ne --> wf_cc (h, G) --> wf_cc (h, G - Ns)" (fn _ => [ Clarsimp_tac 1, (REPEAT_FIRST (rtac conjI)), ALLGOALS Clarsimp_tac, (etac subsetD 1), (force_tac (cesimps [fn_oth_def]) 1), (clarsimp_tac (cesimps [or_min_reduce RS sym, rsmin_def]) 1), (dtac (Diff_subset RSN (2, oth_red_sub)) 1), Fast_tac 1, (datac bspec 1 1), (dtac (idv_Ne RS iffD2) 1), (etac idv_wk 1), (fast_tac (ces [Ne.elims]) 1) ]) ; val _ = qed_goal_spec_mp "wf_cc_take" Spi_CC.thy "wf_cc (ha @ hb, G) --> Gb = G - oth_ctg_fns (- fn_oth (oth_of hb)) --> \ \ wf_cc (hb, Gb)" (fn _ => [ Clarsimp_tac 1, (REPEAT_FIRST (rtac conjI)), (rtac (finite_Diff RS or_min_reduce RS sym RS iffD2) 4), atac 4, (rtac (diff_ocf RS subset_trans) 3), Fast_tac 3, (rtac rsmin_oth_red_sub 3), (eatac (or_min_reduce RS iffD2) 1 3), (etac validbt_take 1), (etac bt_cons_take 1), (rtac Diff_subset 1), Clarify_tac 1, (dtac bspec 1), (force_tac (cesimps [oth_of_append]) 1), (etac idv_ctg_fn 1), (fast_tac (cis [fn_othI]) 1) ]) ; val _ = qed_goal_spec_mp "wf_cc_take_ex" Spi_CC.thy "wf_cc (ha @ hb, G) --> (EX Gb. wf_cc (hb, Gb))" (fn _ => [ (rtac impI 1), (dtac wf_cc_take 1), (rtac refl 1), (etac exI 1) ]) ; val _ = qed_goal_spec_mp "wf_cc_tcrI" Spi_CC.thy "wf_cc (h, G) --> thy_cons G --> thy_cons_red G" (fn _ => [ Clarsimp_tac 1, (fatac (tc_red_iff RS iffD1) 1 1), Clarsimp_tac 1]) ; val _ = qed_goal_spec_mp "rev_rev_cc'" Spi_CC.thy "cc = (h, G) --> rev_cc (rev_cc cc) = cc" fn_at ; val rev_rev_cc = surjective_pairing RS rev_rev_cc' ; Addsimps [rev_rev_cc] ; val _ = qed_goal_spec_mp "wf_cc_rev'" Spi_CC.thy "cc = (h, G) --> wf_cc cc --> wf_cc (rev_cc cc)" (fn _ => [ (clarsimp_tac (cesimps [validbt_rev_iff, bt_cons_rev_iff, or_min_reduce RS sym, rsmin_def, oth_red_rev_iff_alt RS sym, fn_rp, rev_oth_of, idv_rev_iff', oth_red_rev]) 1) ]) ; val wf_cc_rev = surjective_pairing RS wf_cc_rev' ; val _ = qed_goal_spec_mp "wf_cc_rev_iff" Spi_CC.thy "wf_cc (rev_cc cc) = wf_cc cc" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac wf_cc_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goal_spec_mp "wf_cc_rev_iff'" Spi_CC.thy "wf_cc (rev_bt h, rev_pair ` G) = wf_cc (h, G)" (fn _ => [ (rtac trans 1), (rtac wf_cc_rev_iff 2), Simp_tac 1 ]) ; (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac wf_cc_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goal_spec_mp "valid_cc_rev'" Spi_CC.thy "cc = (h, G) --> valid_cc cc --> valid_cc (rev_cc cc)" (fn _ => [ (clarsimp_tac (cesimps [thy_cons_rev_iff, bt_resp_rev_iff, subst_oth_rev' RS sym]) 1) ]) ; val valid_cc_rev = surjective_pairing RS valid_cc_rev' ; val _ = qed_goal_spec_mp "valid_cc_rev_iff" Spi_CC.thy "valid_cc (rev_cc cc) = valid_cc cc" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac valid_cc_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goal "r_lcompat" Spi_CC.thy "rcompat (S, M) h = lcompat (S, M) (rev_bt h)" (fn _ => [ (simp_tac (esimps [rev_oth_of, fn_rp]) 1), Safe_tac, (ALLGOALS (etac subsetD)), (REPEAT_FIRST (ares_tac [image_eqI, refl])), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal "RC2_RC1" Spi_CC.thy "((f,g) : RC2 h C) = ((g,f) : RC1 (rev_bt h) C)" (fn _ => [ (safe_tac (ces [RC1.elims, RC2.elims])), (simp_tac (HOL_ss addsimps [CS2_CS1]) 1), (rtac RC1.intros 1), (simp_tac (HOL_ss addsimps [CS2_CS1 RS sym]) 4), (rtac RC2.intros 4), (rewtac (mk_eq rev_bt_12)), (TRYALL (ares_tac [refl])) ]) ; val _ = qed_goal "RS2_RS1" Spi_CC.thy "((f,g) : RS2 h theta) = ((g,f) : RS1 (rev_bt h) theta)" (fn _ => [ (safe_tac (ces [RS1.elims, RS2.elims])), (simp_tac (HOL_ss addsimps [CS2_CS1]) 1), (rtac RS1.intros 1), (simp_tac (HOL_ss addsimps [CS2_CS1 RS sym]) 4), (rtac RS2.intros 4), (rewtac (mk_eq rev_bt_12)), (TRYALL (ares_tac [refl])) ]) ; val _ = qed_goal_spec_mp "R2_rev" Spi_CC.thy "(theta, cc', cc) : R2 --> (rev_pair theta, rev_cc cc', rev_cc cc) : R2" (fn _ => [ (clarsimp_tac (ces [R2.elims], esimps [subst_bt_rev RS sym, reduce_rev RS sym, subst_oth_rev']) 1), (rtac R2.intros 1), (simp_tac (esimps [in_rp]) 1) , rtac refl 1, rtac refl 1, (full_simp_tac (esimps [RC2_RC1, rev_oth_of, image_Un RS sym, image_compose RS sym, snd_o_rp, fst_o_rp]) 1) , (etac (disj_commute RS iffD1) 1) ]) ; val _ = qed_goal_spec_mp "R3_rev" Spi_CC.thy "(theta, cc', cc) : R3 --> (rev_pair theta, rev_cc cc', rev_cc cc) : R3" (fn _ => [ (safe_tac (ces [R3.elims])), (ALLGOALS (clarsimp_tac (cesimps [subst_bt_rev RS sym, reduce_rev RS sym, subst_oth_rev']))), (rtac R3.I1 2), (rtac R3.I2 1), (TRYALL (resolve_tac ([RS2_RS1] RL iffDs) THEN' Simp_tac)), (TRYALL atac), (TRYALL (simp_tac (esimps [in_rp]))) ]) ; val _ = qed_goalw_spec_mp "ps_cc_red_rev" Spi_CC.thy [ps_cc_red_def] "(theta, cc', cc) : ps_cc_red --> \ \ (rev_pair theta, rev_cc cc', rev_cc cc) : ps_cc_red" (fn _ => [ Safe_tac, Simp_tac 1, (TRYALL (dresolve_tac [R2_rev, R3_rev] THEN' contr_tac)), (etac R1.elims 1), (clarsimp_tac (cesimps [Names_rp]) 1), (rtac R1.intros 1), (simp_tac (esimps [Names_in_rp]) 1) ]) ; val _ = qed_goalw "cc_red_alt" Spi_CC.thy [cc_red_def, ps_cc_red_def, meta_eq_def] "cc_red == snd ` ps_cc_red" (fn _ => [ Safe_tac, ALLGOALS Clarsimp_tac, (TRYALL (etac notE)), (TRYALL (rtac rev_image_eqI THEN' Fast_tac THEN' Simp_tac)) ]) ; val _ = qed_goalw_spec_mp "ps_cc_redD" Spi_CC.thy [cc_red_alt] "(theta, red) : ps_cc_red --> red : cc_red" (fn _ => [ Force_tac 1 ]) ; val _ = qed_goalw_spec_mp "cc_red_rev" Spi_CC.thy [cc_red_alt] "(cc', cc) : cc_red --> (rev_cc cc', rev_cc cc) : cc_red" (fn _ => [ Clarsimp_tac 1, (dtac ps_cc_red_rev 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "cc_red_rtc_rev" Spi_CC.thy "(cc', cc) : cc_red^* --> (rev_cc cc', rev_cc cc) : cc_red^*" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), (rtac rtrancl_refl 1), (etac tct.rsr 1), (etac cc_red_rev 1) ]) ; val _ = qed_goal_spec_mp "cc_red_rtc_rev_iff" Spi_CC.thy "((rev_cc cc', rev_cc cc) : cc_red^*) = ((cc', cc) : cc_red^*)" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac cc_red_rtc_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goal_spec_mp "wfp_cc_red_rev" Spi_CC.thy "cc : wfp cc_red --> rev_cc cc : wfp cc_red" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (rtac wfp.wfpI 1), strip_tac 1, (dtac cc_red_rev 1) , (etac allE 1), (etac impE 1), Full_simp_tac 1, Asm_full_simp_tac 1 ]) ; val _ = qed_goal_spec_mp "wfp_cc_red_rev_iff" Spi_CC.thy "(rev_cc cc : wfp cc_red) = (cc : wfp cc_red)" (fn _ => [ (rtac iffI 1), (ALLGOALS (dtac wfp_cc_red_rev THEN' Full_simp_tac)) ]) ; val _ = qed_goalw_spec_mp "cc_red_sub" Spi_CC.thy [ps_cc_red_def] "(theta, (h', G'), (h, G)) : ps_cc_red --> h' = subst_bt theta h" (fn _ => [ (safe_tac (ces [R1.elims, R2.elims, R3.elims])), Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "cc_red_rtc_sub" Spi_CC.thy "(theta, hG', hG) : psig_rtc ps_cc_red --> fst hG' = subst_bt theta (fst hG)" (fn _ => [ rtac impI 1, (etac psig_rtc.induct 1), ALLGOALS Clarsimp_tac, (dtac cc_red_sub 1), (Clarsimp_tac 1), (rtac (comp_bt' RS sym RS trans) 1), Simp_tac 1 ]) ; AddIffs [psig_rtc.refl, psig_rtc'.refl] ; val psig_rtc_comp_Name = simplify (esimps []) (read_instantiate [("psig", "(Name, Name)")] psig_rtc.comp) ; val _ = bind_thm ("psig_rtc_single", simplify (esimps []) (psig_rtc.refl RS psig_rtc.comp)) ; val _ = qed_goalw "psig_rtc_equiv" Spi_CC.thy [meta_eq_def] "psig_rtc' == psig_rtc" (fn _ => [ (rtac ext 1), Safe_tac, (etac psig_rtc'.induct 1), (rtac psig_rtc.refl 1), (etac thin_rl 1), (chop_last (etac rev_mp 1)), (etac psig_rtc.induct 1), Clarsimp_tac 1, (dtac psig_rtc_single 1), Full_simp_tac 1, Clarify_tac 1, (chop_tac 1 (datac psig_rtc.comp 1 1)), (full_simp_tac (esimps [comp_subst_assoc]) 1), (etac psig_rtc.induct 1), (rtac psig_rtc'.refl 1), (etac thin_rl 1), (chop_last (etac rev_mp 1)), (etac psig_rtc'.induct 1), Clarsimp_tac 1, (dtac (psig_rtc'.refl RS psig_rtc'.comp) 1), Full_simp_tac 1, Clarify_tac 1, (chop_tac 1 (datac psig_rtc'.comp 1 1)), (full_simp_tac (esimps [comp_subst_assoc]) 1) ]) ; val _ = qed_goal_spec_mp "valid_cc_alt" Spi_CC.thy "wf_cc (h, G) --> valid_cc (h, G) = \ \ (ALL fl fr. domain fl Un domain fr <= fn_oth (oth_of h) --> \ \ h : bt_resp (fl, fr) --> thy_cons (subst_pr (fl, fr) ` G))" (fn _ => [ Clarsimp_tac 1, Safe_tac, Fast_tac 1, (etac allE2 1), (etac impE 1), (REPEAT_FIRST (resolve_tac [conjI, dom_dom_restr_sub])), (etac (tacthm (etac rev_iffD1 3) impE) 1), (freeze_tac (cong1_tac 2)), (* why is this needed *) (etac dom_restr_oth 2), (fatac bt_resp_v 1 1), (rtac bt_resp_vr 1), (etac (subset_refl RS dom_restr_respv RS iffD1) 1) ]) ; (* Lemma 42 as in the paper *) val _ = qed_goal_spec_mp "wf_cc_indist" Spi_CC.thy "wf_cc (h, Gamma) --> h : bt_resp theta --> \ \ (ALL x : fn_oth (oth_of h). \ \ (subst_pr theta ` Gamma, subst_nat theta x) : indist) & \ \ (ALL MN : oth_of h. (subst_pr theta ` Gamma, subst_pr theta MN) : indist)" (fn _ => [ Clarsimp_tac 1, (rtac conjI 1), (eatac wf_cc_indist_fn 2 1), (eatac wf_cc_indist_bt 2 1) ]) ; val _ = qed_goalw_spec_mp "wf_cc_resp" Spi_CC.thy [thy_resp_def'] "wf_cc (h, Gamma) --> h : bt_resp theta --> thy_resp theta Gamma" (fn _ => [ (strip_tac 1), (fatac (wf_cc_indist RS conjunct1) 1 1), (Clarsimp_tac 1), (datac subsetD 1 1), (eatac bspec 1 1) ]) ; (* remark following definition of left-/right-compatible *) val _ = qed_goal_spec_mp "lcompat_is_fnrf" Spi_CC.thy "h : bt_cons --> validbt h --> lcompat (S, M) h --> \ \ fnrf ((f, S, M) # st_dcs (fst_bt h))" (fn _ => [ Clarify_tac 1, (simp_tac (HOL_ss addsimps fnrf.simps) 1), (datac bt_fn_same_Ns 1 1), rtac conjI 1, (eatac (valid_fst_bt RS st_dcs_fnrf) 1 1), Clarsimp_tac 1, (dtac subsetD 1 THEN eatac UN_I 1 1), (rtac st_dcs_fnrf_lem 1), (eatac valid_fst_bt 1 1), (datac bt_sameNs_in1 1 1), (clarsimp_tac (cesimps [fst_bt_def, rem_map_io']) 1) ]) ; val _ = qed_goalw_spec_mp "lcompat_is_sac" Spi_CC.thy [fst_bt_def] "h : bt_cons --> validbt h --> lcompat (S, M) h --> \ \ lhs_sacond ((f, S, M) # st_dcs (fst_bt h))" (fn _ => [ (clarsimp_tac (cesimps [st_dcs_sac, lhs_acond1_def]) 1), (rtac smder_id 1), (rtac imageI 1), (rtac DiffI 1), (dtac st_dcs_lhs_sub 1), (datac subsetD 1 1), (etac subsetD 1), (clarsimp_tac (cesimps [oth_of_def, rem_map_io']) 1), (clarsimp_tac (cesimps [ms_ctg_fns_def]) 1) ]) ; (* Lemma 44 *) val _ = qed_goal_spec_mp "compat_resp1" Spi_CC.thy "validbt h --> h : bt_cons --> lcompat (S, M) h --> \ \ theta : RC1 h (f, S, M) --> h : bt_resp theta" (fn _ => [ (safe_tac (ces [RC1.elims])), Full_simp_tac 1, Safe_tac, (rtac second_sub' 1), (TRYALL atac), (rtac sat_st_dcs_resp 1), (eatac valid_fst_bt_cons 1 1), (dtac ndcr_rtc_sound 1), (etac rsolved_sat 1), Clarsimp_tac 1 ]); val _ = qed_goal_spec_mp "compat_resp2" Spi_CC.thy "validbt h --> h : bt_cons --> rcompat (S, M) h --> \ \ theta : RC2 h (f, S, M) --> h : bt_resp theta" (fn _ => [ (safe_tac (ces [RC2.elims])), Full_simp_tac 1, Safe_tac, (rtac second_sub_rev 1), (TRYALL atac), (rtac sat_st_dcs_resp 1), (eatac valid_snd_bt_cons 1 1), (dtac ndcr_rtc_sound 1), (etac rsolved_sat 1), Clarsimp_tac 1 ]); val _ = bind_thm ("cr_sat_st_dcs", [asm_rl, refl RS bt_sm_resp, btc_st1_sf] MRS rc_sat_st_dcs) ; val l47b = [satldcs_comp, fold_rule [fst_bt_def] cr_sat_st_dcs] MRS iffD1 ; val l47c = [st_dcs_sac RS lhs_sacond_sub, asm_rl, st_dcs_fnrf RS fnrf_sub, subst_st_dcs_finite] MRS ndcr_vars_der_subst ; val _ = bind_thm ("sub_dcs_resp", ndcr_rtc_rsf RS (satldcs_comp RS iffD2) RSN (2, sat_st_dcs_resp)) ; val _ = qed_goal_spec_mp "RS1_resp" Spi_CC.thy "validbt h --> h : bt_cons --> theta : RS1 h beta --> h : bt_resp theta" (fn _ => [ (clarify_tac (ces [RS1.elims]) 1), (rtac CS1_resp 1), (rtac sub_dcs_resp 1), TRYALL atac, (rtac valid_fst_bt_cons 1), TRYALL atac ]) ; val _ = qed_goal_spec_mp "RS2_resp" Spi_CC.thy "validbt h --> h : bt_cons --> theta : RS2 h beta --> h : bt_resp theta" (fn _ => [ (clarify_tac (ces [RS2.elims]) 1), (rtac CS2_resp 1), (rtac sub_dcs_resp 1), TRYALL atac, (rtac valid_snd_bt_cons 1), TRYALL atac ]) ; (* reduction of consistency constraints *) val cltacs = [ Clarsimp_tac 1, Safe_tac, (Fast_tac 1), (etac subsetD 2), (TRYALL (etac fn_othI THEN' Clarsimp_tac)), rtac imageI 1, etac UnI1 1 ] ; val _ = qed_goal_spec_mp "lcompat_lem" Spi_CC.thy "fn_oth G <= fn_oth (oth_of h) --> fn_msg M <= fn_oth G --> \ \ lcompat (fst ` (oth_of h Un G), M) h" (fn _ => cltacs) ; val _ = qed_goal_spec_mp "rcompat_lem" Spi_CC.thy "fn_oth G <= fn_oth (oth_of h) --> fn_msg M <= fn_oth G --> \ \ rcompat (snd ` (oth_of h Un G), M) h" (fn _ => cltacs) ; val _ = qed_goal_spec_mp "R2_lcompat" Spi_CC.thy "wf_cc (h, G) --> (Enc Mp Mk, Enc Np Nk) : G --> \ \ lcompat (fst ` (oth_of h Un G), Mk) h" (fn _ => [ Clarify_tac 1, (rtac lcompat_lem 1), Asm_full_simp_tac 1, Clarify_tac 1, (etac fn_othI 1), Asm_simp_tac 1 ]) ; val _ = qed_goal_spec_mp "R2_rcompat" Spi_CC.thy "wf_cc (h, G) --> (Enc Mp Mk, Enc Np Nk) : G --> \ \ rcompat (snd ` (oth_of h Un G), Nk) h" (fn _ => [ Clarify_tac 1, (rtac rcompat_lem 1), Asm_full_simp_tac 1, Clarify_tac 1, (etac fn_othI 1), Asm_simp_tac 1 ]) ; (* TODO - SOME FOLLOWING RESULTS EASIER USING THIS *) val _ = qed_goalw_spec_mp "cc_red_resp" Spi_CC.thy [ps_cc_red_def] "wf_cc (h, G) --> (theta, H', (h, G)) : ps_cc_red --> h : bt_resp theta" (fn _ => [ Clarsimp_tac 1, (safe_tac (ces [R2.elims, R3.elims])), (ALLGOALS (eresolve_tac (map (reop rev) [RS1_resp, RS2_resp, compat_resp1, compat_resp2]))), (ALLGOALS (ares_tac [R2_lcompat, R2_rcompat])), TRYALL atac, ALLGOALS Asm_simp_tac ]) ; val _ = qed_goalw_spec_mp "pres_wf'" Spi_CC.thy [cc_red_alt] "H = (h, G) --> H' = (h', G') --> wf_cc H --> (H', H) : cc_red --> wf_cc H'" (fn _ => [ (clarsimp_tac init_css 1), (fatac cc_red_resp 1 1), ftac cc_red_sub 1, rewtac ps_cc_red_def, Clarsimp_tac 1, (REPEAT_FIRST (rtac conjI)), (eatac valid_subst 1 1), (eatac cons_subs_bt 2 2), (REPEAT_FIRST (eresolve_tac [disjE, conjE, R1.elims, R2.elims, R3.elims])), (ALLGOALS (clarsimp_tac (cesimps [fn_oth_insert]))), (TRYALL (eatac idv_rs_lem 4)), (TRYALL (eatac (bt_fn_same_Ns RSN (2, fn_red_lem) RS subsetD) 4)), (clarsimp_tac (cesimps [or_min_reduce RS sym, rsmin_def]) 1), (dtac (subset_insertI RSN (2, oth_red_sub)) 1), Fast_tac 1, (datac bspec 1 1), (etac (subset_refl RSN (2, idv_ca1)) 1), (simp_tac (esimps [Names_def]) 1) ]) ; val pres_wf = [ surjective_pairing, surjective_pairing] MRS pres_wf' ; val _ = qed_goal_spec_mp "rtc_pres_wf" Spi_CC.thy "(H', H) : cc_red^* --> wf_cc H --> wf_cc H'" (fn _ => [ (Clarify_tac 1), (eatac converse_rtrancl_induct 1 1), (eatac pres_wf 1 1) ]) ; val _ = qed_goal_spec_mp "cc_red_rtc_resp" Spi_CC.thy "(theta, H', H) : psig_rtc ps_cc_red --> wf_cc H --> \ \ fst H : bt_resp theta" (fn _ => [ rtac impI 1, (etac psig_rtc.induct 1), ALLGOALS Clarify_tac, (etac impE 1), (etac pres_wf 1), (etac ps_cc_redD 1), (rtac bt_resp_comp 1), (full_simp_tac init_ss 1), (eatac cc_red_resp 1 1), (dtac cc_red_sub 2), Auto_tac ]) ; val _ = qed_goal_spec_mp "cc_red_comp_resp" Spi_CC.thy "(theta, (h', G'), (h, G)) : psig_rtc ps_cc_red --> wf_cc (h, G) --> \ \ h' : bt_resp rho --> h : bt_resp (comp_psub rho theta)" (fn _ => [ Clarify_tac 1, (rtac bt_resp_comp 1), (datac cc_red_rtc_resp 1 1), (dtac cc_red_rtc_sub 3), Auto_tac ]) ; val _ = qed_goal_spec_mp "decomp_resp_subst1" Spi_CC.thy "theta = (thl, thr) --> \ \ validbt h --> h : bt_cons --> h : bt_resp theta --> \ \ finite S --> aCs = ((f, S, M) # st_dcs (fst_bt h)) --> \ \ satldcs (fst theta) aCs --> lcompat (S, M) h --> \ \ (EX rho gamma. rho : RC1 h (f, S, M) & \ \ (ALL n : fn_oth (oth_of h). subst_pr theta (Names n) = \ \ subst_pr (comp_psub gamma rho) (Names n)) & \ \ subst_bt rho h : bt_resp gamma)" (fn _ => [ Clarify_tac 1, (fatac valid_fst_bt_cons 1 1), (fatac lcompat_is_sac 2 1), (fatac ndcr_vars_der_subst 1 1), (eatac lcompat_is_fnrf 2 1), (Clarsimp_tac 1), Clarify_tac 1, (rtac exI 1), (res_inst_tac [("x", "(gamma, CS1 (subst_bt (rho, CS1 (h, rho)) h, gamma))")] exI 1), (subgoal_tac "map (map_io (subst_msg rho)) (fst_bt h) : sm_resp gamma" 1), (rtac dcrs1lem4 2), (REPEAT_FIRST (eresolve_tac [all_forward, imp_forward2, asm_rl])), Clarsimp_tac 2, (thin_tac "All ?P" 1), (* level 15 *) (rtac (mk_dupE conjI) 1), (eatac (refl RS RC1.intros) 1 1), (fatac compat_resp1 3 1), (rtac ([conj_commute, (mk_dupE conjI)] MRS iffD1) 1), (rtac CS1_resp 1), (simp_tac (esimps [fst_subst_bt]) 1), (eatac cons_subs_bt 2 1), (eatac valid_subst 1 1), (asm_full_simp_tac (init_ss addsimps [subst_pr_simps, comp_psub_simps, hd subst_msg.simps, Names_def]) 1), (rtac (subst_unique_alt RS iffD1) 1), TRYALL atac, Fast_tac 2, (* level 27 *) (simp_tac (init_ss addsimps [comp_psub_simps RS sym]) 1), (rtac bt_resp_comp 1), TRYALL atac ]) ; val _ = qed_goal_spec_mp "decomp_resp_subst2" Spi_CC.thy "wf_cc (h, G) --> theta = (thl, thr) --> h : bt_resp theta --> \ \ subst_msg thl M = subst_msg thl N --> mgu {(M,N)} = Some beta --> \ \ (EX rho gamma. rho : RS1 h beta & h : bt_resp rho & \ \ (ALL n : fn_oth (oth_of h). subst_pr theta (Names n) = \ \ subst_pr (comp_psub gamma rho) (Names n)) & \ \ subst_bt rho h : bt_resp gamma)" (fn _ => [ Clarsimp_tac 1, (fatac valid_fst_bt_cons 1 1), (dtac (mguI1 RS iffD1) 1), Clarsimp_tac 1, (rename_tac "delta" 1), (fatac l47b 2 1), (datac l47c 1 1), (Clarsimp_tac 1), (rename_tac "sigma gamma1 C" 1), (fatac sub_dcs_resp 2 1), (ftac dcrs1lem4 1), Simp_tac 1, (REPEAT_FIRST (eresolve_tac [all_forward, imp_forward2, asm_rl])), (simp_tac (esimps ([apsnd_o, image_compose, comp_con] RL [sym])) 1), (thin_tac "All ?P" 1), (fatac CS1_resp 2 1), (* so h respects \rho_1 *) (rtac exI 1), (rtac exI 1), (rtac conjI 1), (eatac RS1.intros 1 1), rtac refl 1, (rtac conjI 1), atac 1, (rtac exI 1), (rtac exI 1), (rtac ([conj_commute, (mk_dupE conjI)] MRS iffD1) 1), (rtac CS1_resp 1), (eatac valid_subst 1 3), (rtac cons_subs_bt 2), TRYALL atac, (simp_tac (esimps [fst_subst_bt]) 1), (clarsimp_tac (cesimps [Names_def, comp_subst_assoc]) 1), (etac (subst_unique_alt RS iffD1 RS bspec) 1), Clarify_tac 4, rtac refl 4, TRYALL atac, (rewtac (mk_eq (comp_psub_simps RS sym))), (rtac bt_resp_comp 1), TRYALL atac ]) ; val _ = qed_goal_spec_mp "fn_oth_subst_lem'" Spi_Bitrace_defs.thy "theta = (thl, thr) --> fn_oth G <= fn_oth (oth_of h) --> \ \ bt_sameNs h --> n : fn_oth (subst_pr theta ` G) --> \ \ n:fn_oth (subst_pr theta ` oth_of h)" (fn _ => [ (clarsimp_tac (ces [fn_othE], esimps [fn_subst_msg_iff]) 1), Safe_tac, (ALLGOALS (EVERY' [ (dtac subsetD), (etac fn_othI), Force_tac ])), (datac bt_sameNs_in1 1 1), (datac bt_sameNs_in2 1 2), Safe_tac, (ALLGOALS (EVERY' [ (etac (rem_oth RS imageI RS fn_othI)), (case_tac "rem_io x"), (force_tac (cesimps [fn_subst_msg_iff])) ])) ]) ; val fn_oth_subst_lem = surjective_pairing RS fn_oth_subst_lem' ; val _ = qed_goal_spec_mp "cc_subst_resp" Spi_Bitrace_defs.thy "fn_oth G <= fn_oth (oth_of h) --> validbt h --> bt_sameNs h --> \ \ h : bt_resp (comp_psub rho sigma) --> \ \ (ALL MN:oth_of h. is_der_virt (G, MN)) --> \ \ thy_resp rho (subst_pr sigma ` oth_of h) --> \ \ thy_resp rho (subst_pr sigma ` G)" (fn _ => [ (clarsimp_tac (cesimps [subst_oth_bt', thy_resp_def]) 1), (fatac fn_oth_subst_lem 2 1), (datac bspec 1 1), (etac indist_ca_all 1), (clarsimp_tac (cesimps [subst_oth_def]) 1), (simp_tac (HOL_ss addsimps [image_compose RS sym, comp_pr RS sym, comp_pr' RS sym]) 1), (eatac (wf_cc_indist_bt RS bspec) 3 1) ]) ; val _ = qed_goal_spec_mp "pvlem'" Spi_CC.thy "sigma = (sigl, sigr) --> rho = (rhol, rhor) --> h : bt_resp sigma --> \ \ (ALL a b. h : bt_resp (a, b) --> thy_cons (subst_pr (a, b) ` G)) --> \ \ validbt h --> finite G --> h : bt_cons --> bt_sameNs h --> \ \ fn_oth G <= fn_oth (oth_of h) --> \ \ subst_bt sigma h : bt_resp rho --> \ \ (ALL MN:oth_of h. is_der_virt (G, MN)) --> \ \ thy_cons (subst_pr rho ` reduce (subst_pr sigma ` G))" (fn _ => [ Clarify_tac 1, (fatac bt_resp_comp 3 1), Full_simp_tac 1, (etac allE2 1), (chop_last (mp_tac 1)), (rtac (thy_cons_reduce' RS iffD1) 1), (etac finite_imageI 1), (full_simp_tac (HOL_ss addsimps [comp_psub_simps RS sym, comp_pr, image_compose]) 2), (fatac (valid_subst RS bt_thy_resp) 2 1), (full_simp_tac (HOL_ss addsimps [subst_oth_bt', comp_psub_simps RS sym]) 1), (eatac cc_subst_resp 5 1) ]) ; val pvlem = [ surjective_pairing, surjective_pairing] MRS pvlem' ; val _ = qed_goalw_spec_mp "pres_valid'" Spi_CC.thy [cc_red_alt] "H = (h, G) --> H' = (h', G') --> wf_cc H --> valid_cc H --> \ \ (H', H) : cc_red --> valid_cc H'" (fn _ => [ (clarsimp_tac init_css 1), (fatac cc_red_resp 1 1), (Clarsimp_tac 1), (fatac bt_fn_same_Ns 1 1), (rewtac ps_cc_red_def), (safe_tac (ces [R1.elims, R2.elims, R3.elims])), (* R1 *) Full_simp_tac 1, (etac allE2 1), mp_tac 1, (etac (subset_insertI RSN (2, cons_mono)) 1), (* R2 and R3 *) (ALLGOALS (eatac pvlem 8)) ]); val pres_valid = [ surjective_pairing, surjective_pairing] MRS pres_valid' ; val _ = qed_goal_spec_mp "rtc_pres_valid" Spi_CC.thy "(H', H) : cc_red^* --> wf_cc H --> valid_cc H --> valid_cc H'" (fn _ => [ (Clarify_tac 1), (eatac converse_rtrancl_induct 1 1), (rtac pres_valid 1), TRYALL atac, (eatac rtc_pres_wf 1 1) ]) ; val l51a = reop (tl o tl o tl) ([compat_resp1 RSN (2, bt_resp_v), bt_fn_same_Ns] MRS bt_same_Ns_subst) ; (* Lemma 51, <= part, still need ~= *) val _ = qed_goal_spec_mp "compat_fn1" Spi_CC.thy "validbt h --> h : bt_cons --> lcompat (S, M) h --> \ \ theta : RC1 h (f, S, M) --> \ \ fn_oth (oth_of (subst_bt theta h)) <= fn_oth (oth_of h)" (fn _ => [ Clarify_tac 1, (fatac (l51a RS bt_sameNs_in1) 4 1), (thin_tac "x : ?s" 1), (clarsimp_tac (ces [RC1.elims, fn_othE], esimps [subst_bt_def, rem_map_io']) 1), (dtac rem_oth 1), (case_tac "rem_io a" 1), (clarsimp_tac (cesimps [fn_subst_msg_iff]) 1), (ALLGOALS (dres_inst_tac [("x", "n'")] ndcr_rtc_sub_fn)), (datac subsetD 1 2), (clarsimp_tac (cesimps [fn_ldcs_Cons]) 2), (REPEAT (etac disjE 2 THEN Fast_tac 2)), (clarsimp_tac (cesimps [fn_ldcs_def]) 2), (dtac (st_dcs_fn RS subsetD) 2), Force_tac 2, (clarsimp_tac (cesimps [fst_bt_def, oth_of_def, rem_map_io']) 2), (rtac fn_othI 2), (chop_last (etac imageI 2)), (case_tac "rem_io ab" 2), Force_tac 2, (datac (valid_fst_bt_cons RS st_dcs_fnrf_lem) 1 1), (simp_tac (esimps [rem_io_fst]) 1), (etac rev_bexI 1), MSSG Simp_tac 1, (force_tac (cesimps [fn_ldcs_def]) 1) ]) ; val _ = qed_goal_spec_mp "compat_fn2'" Spi_CC.thy "theta = (thl, thr) --> validbt h --> h : bt_cons --> rcompat (S, M) h --> \ \ theta : RC2 h (f, S, M) --> \ \ fn_oth (oth_of (subst_bt theta h)) <= fn_oth (oth_of h)" (fn _ => [ (Clarify_tac 1), (dtac (RC2_RC1 RS iffD1 RS (reop rev compat_fn1)) 1), (etac (r_lcompat RS iffD1) 1), (etac bt_cons_rev 1), (etac validbt_rev 1), (full_simp_tac (esimps [subst_bt_rev, rev_oth_of, fn_rp]) 1), (eatac subsetD 1 1) ]) ; val _ = qed_goal_spec_mp "compat_fn_ne1'" Spi_CC.thy "theta = (thl, thr) --> validbt h --> h : bt_cons --> \ \ lcompat (S, M) h --> theta : RC1 h (f, S, M) --> \ \ (S, M) ~: derrec smpsc {} --> \ \ fn_oth (oth_of (subst_bt theta h)) ~= fn_oth (oth_of h)" (fn _ => [ Clarify_tac 1, (fatac l51a 3 1), (clarsimp_tac (ces [RC1.elims, fn_othE], esimps []) 1), (dtac rsolved_sat 1), (fatac ndcr_rtc_sound 1 1), (Full_simp_tac 1), (case_tac "ALL x : fn_oth (oth_of h). thl x = Name x" 1), (subgoal_tac "subst_con thl (S, M) = (S, M)" 1), (clarsimp_tac (claset (), esimps [] addsplits [split_if_asm]) 1), (dtac idv_ss_smpsc 1 THEN contr_tac 1), Simp_tac 1, (rtac conjI 1), (rtac image_id_eq' 1), (TRYALL (rtac (domain_disj_id RS iffD1))), rewtac domain_def, (TRYALL (rtac (subset_empty RS iffD1) THEN' Fast_tac)), Clarsimp_tac 1, (datac equalityD2' 1 1), (datac bt_sameNs_in1 1 1), (clarsimp_tac (cesimps [subst_bt_def, rem_map_io']) 1), (case_tac "rem_io a" 1), Clarsimp_tac 1, (datac (ndcr_rtc_dr_disj RS dr_disj_subst_lem) 1 1), (clarsimp_tac (cesimps [domain_def]) 1) ]) ; val compat_fn2 = surjective_pairing RS compat_fn2' ; val compat_fn_ne1 = surjective_pairing RS compat_fn_ne1' ; val _ = qed_goal_spec_mp "compat_fn_ne2'" Spi_CC.thy "theta = (thl, thr) --> validbt h --> h : bt_cons --> \ \ rcompat (S, M) h --> theta : RC2 h (f, S, M) --> \ \ (S, M) ~: derrec smpsc {} --> \ \ fn_oth (oth_of (subst_bt theta h)) ~= fn_oth (oth_of h)" (fn _ => [ Clarify_tac 1, (datac (RC2_RC1 RS iffD1 RSN (2, reop rev compat_fn_ne1)) 1 1), (etac (r_lcompat RS iffD1) 1), (etac bt_cons_rev 1), (etac validbt_rev 1), (full_simp_tac (esimps [subst_bt_rev, rev_oth_of, fn_rp]) 1) ]) ; val compat_fn_ne2 = surjective_pairing RS compat_fn_ne2' ; val _ = bind_thm ("l52a", reop (tl o tl o tl) ([RS1_resp RSN (2, bt_resp_v), bt_fn_same_Ns] MRS bt_same_Ns_subst)) ; (* Lemma 52 *) val _ = qed_goal_spec_mp "RS1_fn" Spi_CC.thy "validbt h --> h : bt_cons --> rho : RS1 h theta --> \ \ UNION (subst_msg theta ` fst ` oth_of h) fn_msg < fn_oth (oth_of h) --> \ \ fn_oth (oth_of (subst_bt rho h)) < fn_oth (oth_of h)" (fn _ => [ strip_tac 1, (etac xt7 1), Clarify_tac 1, (datac (reop rev (l52a RS bt_sameNs_in1)) 3 1), (clarsimp_tac (ces [RS1.elims, fn_othE], esimps [subst_bt_def, rem_map_io']) 1), (dtac rem_oth 1), (case_tac "rem_io a" 1), (clarsimp_tac (cesimps [fn_subst_msg_iff, comp_subst_def]) 1), (dres_inst_tac [("x", "n'a")] ndcr_rtc_sub_fn 1), (datac subsetD 1 2), (clarsimp_tac (cesimps [fn_ldcs_subst_iff]) 2), (clarsimp_tac (cesimps [fn_ldcs_def]) 2), (dtac (st_dcs_fn RS subsetD) 2), Force_tac 2, (clarsimp_tac (cesimps [fst_bt_def, oth_of_def, rem_map_io']) 2), (rtac bexI 2), (etac bexI 2), atac 2, atac 2, (clarsimp_tac (cesimps [fn_ldcs_subst_iff]) 1), (clarsimp_tac (cesimps [fn_ldcs_def]) 1), (datac (valid_fst_bt_cons RS st_dcs_fnrf_lem) 1 1), Clarify_tac 2, (etac rev_bexI 2), (clarsimp_tac (cesimps [rem_io_fst]) 1), (etac rev_bexI 1), MSSG Simp_tac 1, (etac bexI 1), Simp_tac 1, Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "RS2_fn'" Spi_CC.thy "rho = (rho1, rho2) --> validbt h --> h : bt_cons --> rho : RS2 h theta --> \ \ UNION (subst_msg theta ` snd ` oth_of h) fn_msg < fn_oth (oth_of h) --> \ \ fn_oth (oth_of (subst_bt rho h)) < fn_oth (oth_of h)" (fn _ => [ strip_tac 1, hyp_subst_tac 1, (ftac (thin_rl RS (RS2_RS1 RS iffD1 RSN (3, RS1_fn))) 1), atac 3, (etac validbt_rev 1), (etac bt_cons_rev 1), (full_simp_tac (esimps [subst_bt_rev, rev_oth_of, fn_rp]) 2), (full_simp_tac (esimps [rev_oth_of, fn_rp, fst_rp]) 1) ]) ; val RS2_fn = refl RS RS2_fn' ; val [tcd1, tcd2] = [disjI1, disjI2] RL [reop rev tcdes] ; val _ = qed_goal_spec_mp "R2_non_triv" Spi_CC.thy "(rho, (h', G'), (h, G)) : R2 --> wf_cc (h, G) --> thy_cons G --> \ \ fn_oth (oth_of h') < fn_oth (oth_of h)" (fn _ => [ (clarify_tac (ces [R2.elims]) 1), (fatac R2_lcompat 1 1), (fatac R2_rcompat 1 1), (clarsimp_tac (HOL_cs, HOL_ss addsimps [wf_cc.simps]) 1), (subgoal_tac "thy_cons (oth_of h Un G)" 1), (etac cons_der_ca 2), Clarify_tac 2, (etac UnE 2 THEN etac indist.id 3), (datac bspec 1 2), (etac virt_indist 2), (etac UnE 1), (ALLGOALS (rtac psubsetI)), (eatac compat_fn1 3 1), (eatac compat_fn_ne1 3 1), (eatac compat_fn2 3 2), (eatac compat_fn_ne2 3 2), (REPEAT_FIRST (thin_tac "?a <= ?b")), (REPEAT_FIRST (thin_tac "lcompat ?a ?b")), (REPEAT_FIRST (thin_tac "rcompat ?a ?b")), Safe_tac, (TRYALL (forward_tac [tcd1, tcd2])), TRYALL atac, (TRYALL (etac (UnI2 RS indist.id))), (TRYALL (subgoal_tac "(G, Mk, Nk) : indist")), (TRYALL (etac indist_ca_all)), Safe_tac, (TRYALL (datac bspec 1 THEN' etac virt_indist)), (ALLGOALS (clarsimp_tac (cesimps [rsmin_def, or_min_reduce RS sym]))), (ALLGOALS (datac oth_red_elI'' 1)), ALLGOALS Fast_tac ]) ; val _ = qed_goal_spec_mp "R3_non_triv'" Spi_CC.thy "rho = (rho1, rho2) --> (rho, (h', G'), (h, G)) : R3 --> wf_cc (h, G) --> \ \ fn_oth (oth_of h') < fn_oth (oth_of h)" (fn _ => [ Clarify_tac 1, (etac R3.elims 1), (ALLGOALS (REPEAT o (etac Pair_inject))), ALLGOALS hyp_subst_tac, (rtac RS2_fn 2), (rtac RS1_fn 1), ALLGOALS Clarsimp_tac, TRYALL atac, (REPEAT1 (EVERY [ (subgoal_tac "domain beta ~= {}" 1), etac contrapos_nn 2, eatac mgu_domain_empty 1 2, rtac singletonI 2, etac nonemptyE 1, (fatac (domain_mgu RS subsetD) 1 1), (subgoal_tac "x : fn_oth (oth_of h)" 1), (etac subsetD 2), (etac fn_othE 2), (clarsimp_tac (cesimps [fn_oth_def]) 2), (etac disjE 2), ((REPEAT o (etac rev_bexI THEN' MSSG Asm_simp_tac)) 2), (rtac psubsetI 1), (clarify_tac (ces []) 1), (dtac (fn_sub_lem RS subsetD) 1), etac UnE 1, (etac fn_othI 1), Force_tac 1, (dtac range_mgu 1), (etac subsetD 1), (datac subsetD 1 1), (rotate_tac 2 1), (EVERY (replicate 12 (etac thin_rl 1))), (force_tac (cesimps [fn_oth_def]) 1), (rtac notI 1), (chop_last (datac equalityD2' 1 1)), Clarify_tac 1, (datac (mgu_dr_disj RS dr_disj_subst_lem) 1 1), contr_tac 1 ])) ]) ; val R3_non_triv = refl RS R3_non_triv' ; val _ = qed_goal_spec_mp "cc_cwf_red_measl" Spi_CC.thy "cc_cwf_red <= lex_rel [%(h, G). card (fn_oth (oth_of h)), %(h, G). card G]" (fn _ => [ (safe_tac (ces [cc_cwf_red.elims, cc_cons_red.elims, R1.elims] addSss (esimps [cc_red_def] delsimps [wf_cc.simps]))), Force_tac 1, (ALLGOALS (etac (finite_fn_oth_of RS psubset_card_mono RSN (2, notE)))), (ALLGOALS (eresolve_tac [R2_non_triv, R3_non_triv])), ALLGOALS atac ]) ; (* Theorem 53, modified to require that reductions have Gamma consistent and consistency constraints well-founded ; note, the latter requirement is preserved by reductions (without that requirement) anyway *) val _ = bind_thm ("wf_cc_cwf_red", [wf_lex_rel, cc_cwf_red_measl] MRS wf_subset) ; val _ = qed_goal_spec_mp "wfp_cc_cons_red'" Spi_CC.thy "H : wfp cc_cwf_red --> wf_cc H --> H : wfp cc_cons_red" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), Clarify_tac 1, (rtac wfp.wfpI 1), Clarify_tac 1, (etac allE 1), (etac impE 1), (eatac cc_cwf_red.I 1 1), Clarify_tac 1, (etac notE 1), (etac pres_wf 1), (etac cc_cons_red.elims 1) , Fast_tac 1 ]) ; val _ = bind_thm ("wfp_cc_cons_red", wf_cc_cwf_red RS wf_ssI RS wfp_cc_cons_red') ; (* Theorem 54 - Completeness *) val _ = qed_goal_spec_mp "cc_red_complete" Spi_CC.thy "(H', H) : cc_red^* --> wf_cc H --> valid_cc H --> thy_cons (snd H')" (fn _ => [ (Clarify_tac 1), (datac rtc_pres_valid 2 1), (case_tac "H'" 1), Clarsimp_tac 1, (eres_inst_tac [("x", "Name"), ("xa", "Name")] allE2 1), Clarsimp_tac 1 ]) ; val _ = qed_goal_spec_mp "R1_valid" Spi_CC.thy "fn_oth G <= fn_oth (oth_of h) --> \ \ (ALL MN:oth_of h. is_der_virt (G, MN)) --> validbt h --> \ \ valid_cc (h, G - {Names x}) --> valid_cc (h, G)" (fn _ => [ Clarsimp_tac 1, (etac allE2 1), mp_tac 1, (etac cons_der_ca 1), Clarsimp_tac 1, (case_tac "?p : ?t" 1), (etac indist.id 1), (subgoal_tac "(aa, ba) = Names x" 1), (etac swap 2), (rtac image_eqI 2), Fast_tac 3, Simp_tac 2, (clarsimp_tac (cesimps [Names_def]) 1), (thin_tac "~?P" 1), (ftac wf_cc_indist_fn 1), atac 2, Clarsimp_tac 2, (etac bspec 2), (etac subsetD 2), (etac fn_othI 2), Simp_tac 2, (etac ball_match 1), (dtac (idv_Ne RS iffD2) 1), (etac idv_wk 1), (fast_tac (ces [Ne.elims]) 1) ]) ; (* Soundness of Consistency Constraint Reduction *) val str_ccrs' = "(ALL dtn. (dtn, h, G) : cc_red --> dtn : wfp cc_red & (wf_cc dtn --> \ \ (ALL h' G'. ((h', G'), dtn) : cc_red^* --> thy_cons G') --> \ \ valid_cc dtn)) --> \ \ (ALL G' G'a. ((G', G'a), h, G) : cc_red^* --> thy_cons G'a) --> \ \ thy_cons_red G --> ~ (EX x. Names x : G) --> wf_cc (h, G) --> \ \ h : bt_resp (fl, fr) " ; val str_ccrs = str_ccrs' ^ "--> subst_pr (fl, fr) ` G : rsmin oth_red UNIV" ; val str_ccrs_b = str_ccrs ^ " --> (M, N) : subst_pr (fl, fr) ` G --> \ \ (M', N') : subst_pr (fl, fr) ` G --> "; val _ = qed_goal_spec_mp "lem_ccrs_f" Spi_CC.thy "(ALL n:fn_oth G. subst_pr (fl, fr) (Names n) = \ \ subst_pr (comp_psub (gl, gr) (rhol, rhor)) (Names n)) --> \ \ (subst_pr (gl, gr) ` subst_pr (rhol, rhor) ` G) = subst_pr (fl, fr) ` G" (fn _ => [ (clarsimp_tac (init_cs, init_ss addsimps [image_compose RS sym, comp_pr RS sym, comp_psub_simps]) 1), (rtac (refl RS image_cong) 1), Clarsimp_tac 1, rtac conjI 1, (TRYALL (EVERY' [(rtac subst_msg_eqI), etac (ball_match_set RS ball_match), Clarify_tac, etac fn_othI, MSSG Asm_simp_tac, (clarsimp_tac (cesimps [Names_def])) ])) ]) ; val lem_ccrs_fw = (wf_ccDfn RSN (2, ball_match_set) RS lem_ccrs_f) ; val _ = qed_goal_spec_mp "lem_ccrs_g" Spi_CC.thy "valid_cc (subst_bt (rhol, rhor) h, reduce (subst_pr (rhol, rhor) ` G)) --> \ \ wf_cc (h, G) --> subst_bt (rhol, rhor) h : bt_resp (gammal, gammar) --> \ \ h : bt_resp (comp_subst gammal rhol, comp_subst gammar rhor) --> \ \ thy_cons (subst_pr (gammal, gammar) ` subst_pr (rhol, rhor) ` G)" (fn _ => [ Clarify_tac 1, (dtac (valid_cc.simps RS iffD1 RS spec) 1), mp_tac 1, (etac (reop rev (thy_cons_reduce' RS iffD2)) 1), (etac (wf_ccDfte RS finite_imageI) 2), (clarsimp_tac (init_cs, init_ss addsimps [thy_resp_def, subst_oth_def, image_compose RS sym, comp_pr RS sym]) 1), (rtac wf_cc_indist_sub_fn 1), (TRYALL (ares_tac [refl])), (TRYALL (eresolve_tac wf_cc_Ds)), Simp_tac 1, (rtac (fn_oth_sub_lem RS subsetD) 1), (TRYALL (eresolve_tac (asm_rl :: wf_cc_Ds))) ]) ; val _ = qed_goal_spec_mp "lem_ccrs_e" Spi_CC.thy (str_ccrs_b ^ " M' = M --> N' = N | thy_cons (subst_pr (fl, fr) ` G)") (fn _ => [ Clarify_tac 1, (clarsimp_tac (claset (), HOL_ss addsimps [subst_pr_simps]) 1), (ftac (mguI1 RS iffD1) 1), Clarify_tac 1, (fatac (reop rev decomp_resp_subst2) 2 1), rtac refl 1, atac 1, Clarify_tac 1, (rename_tac "M N R T g m rho1 rho2 gamma1 gamma2" 1), (case_tac "M = R" 1), Clarsimp_tac 1, (datac (reop rev thy_cons_redDee) 2 1), Force_tac 1, (* level 13 *) (fatac (reop rev (hd R3.intros)) 4 1), (subgoal_tac "?c : cc_red" 1), (simp_tac (esimps [cc_red_def]) 2), (rtac disjI2 2), (etac (UnI2 RS rev_image_eqI) 2), Simp_tac 2, (etac allE 1), (mp_tac 1), (etac conjE 1), (etac impE 1), (eatac pres_wf 1 1), (etac impE 1), (REPEAT (eresolve_tac [all_forward, imp_forward2] 1)), atac 2, (eatac tct.rsr 1 1), (* level 28 *) (datac lem_ccrs_g 2 1), (etac (wf_ccDval RS bt_resp_equiv RS iffD1) 1), atac 2, (etac ball_match 1), (full_simp_tac (esimps [Names_def]) 1), (datac lem_ccrs_fw 1 1), (clarsimp_tac HOL_css 1) ]) ; val str_ccrs_d = str_ccrs' ^ " --> (Enc Mp Mk, Enc Np Nk) : subst_pr (fl, fr) ` G --> \ \ is_der_virt (subst_pr (fl, fr) ` G, M', N')" ; val _ = qed_goal_spec_mp "lem_ccrs_d" Spi_CC.thy (str_ccrs_d ^ " --> Mk = M' --> thy_cons (subst_pr (fl, fr) ` G)") (fn _ => [ Clarify_tac 1, (clarsimp_tac (claset (), HOL_ss addsimps [subst_pr_simps]) 1), (fatac thy_cons_redDst 1 1), (etac same_type.elims 1), (ALLGOALS (clarsimp_tac (claset (), simpset_of Spi_Subst_defs.thy addsimps [Names_def]))), (fatac R2_lcompat 1 1), (ftac (reop rev decomp_resp_subst1) 1), TRYALL (ares_tac [refl, finite_imageI, satldc_idv RS conjI RS (satldcs_Cons RS iffD2)]), Simp_tac 3, (TRYALL (eresolve_tac wf_cc_Ds)), (rtac rc_sat_st_dcs 2), (rtac valid_fst_bt 2), (rtac (refl RS bt_sm_resp') 4), Simp_tac 4, (rtac btc_st1_sf' 4), (TRYALL (eresolve_tac wf_cc_Ds)), Simp_tac 1, (dtac slice_idv1 1), (etac idv_ss_wk 1), Clarsimp_tac 1, (etac (UnI2 RS rev_image_eqI RS imageI) 1 THEN MSSG Simp_tac 1), (* level 21, now make use of Lemma 45 *) Clarify_tac 1, (ftac R2.intros 1), (REPEAT (rtac refl 1)), (etac UnI1 1), (subgoal_tac "?c : cc_red" 1), (simp_tac (esimps [cc_red_def]) 2), (rtac disjI2 2), (etac (UnI1 RS rev_image_eqI) 2), Simp_tac 2, (etac allE2 1), (mp_tac 1), (etac conjE 1), (etac impE 1), (eatac pres_wf 1 1), (etac impE 1), (REPEAT (eresolve_tac [all_forward, imp_forward2] 1)), atac 2, (eatac tct.rsr 1 1), (* level 39 *) (rename_tac "rho1 rho2 gamma1 gamma2" 1), (datac lem_ccrs_g 2 1), (etac (wf_ccDval RS bt_resp_equiv RS iffD1) 1), atac 2, (etac ball_match 1), (full_simp_tac (esimps [Names_def]) 1), (datac lem_ccrs_fw 1 1), (clarsimp_tac HOL_css 1) ]) ; val l_ccrs_dr = read_instantiate [("G", "rev_pair ` G"), ("h", "rev_bt h")] lem_ccrs_d ; val l_ccrs_er = read_instantiate [("G", "rev_pair ` G"), ("h", "rev_bt h")] lem_ccrs_e ; val ri_simps = [Names_in_rp, in_rp, subst_oth_rev' RS sym, thy_cons_red_rev_iff, thy_cons_rev_iff, bt_resp_rev_iff, wf_cc_rev_iff', rsmin_or_rev_iff, idvr_rev_iff, idv_rev_iff] ; val l_ccrs_drs = full_simplify (HOL_ss addsimps ri_simps) l_ccrs_dr ; val l_ccrs_ers = full_simplify (HOL_ss addsimps ri_simps) l_ccrs_er ; fun rtacs th = [ strip_tac 1, (rtac th 1), TRYALL atac, Full_simp_tac 3, Clarify_tac 2, (etac allE2 2), (etac impE 2), (etac (thy_cons_rev_iff RS iffD1) 3), (dtac cc_red_rtc_rev 2), Full_simp_tac 2, (Clarify_tac 1), (etac allE 1), (etac impE 1), (dtac cc_red_rev 1), Full_simp_tac 1, (etac conj_forward 1), (etac imp_forward2 2), (simp_tac (HOL_ss addsimps [rev_cc.simps RS sym]) 2), (etac wf_cc_rev 2), (etac imp_forward2 2), (full_simp_tac (HOL_ss addsimps [rev_cc.simps RS sym]) 3), (etac (valid_cc_rev_iff RS iffD1) 3), Clarify_tac 2, (chop_last (etac allE2 2)), (etac impE 2), (etac (thy_cons_rev_iff RS iffD1) 3), (dtac cc_red_rtc_rev 2), Full_simp_tac 2, (full_simp_tac (HOL_ss addsimps [wfp_cc_red_rev_iff, rev_cc.simps RS sym]) 1) ] ; val _ = qed_goal_spec_mp "lem_ccrs_d2" Spi_CC.thy (str_ccrs_d ^ " --> Nk = N' --> thy_cons (subst_pr (fl, fr) ` G)") (fn _ => rtacs l_ccrs_drs) ; val _ = qed_goal_spec_mp "lem_ccrs_e2" Spi_CC.thy (str_ccrs_b ^ " N' = N --> M' = M | thy_cons (subst_pr (fl, fr) ` G)") (fn _ => rtacs l_ccrs_ers) ; val lem_ccrs_da = tacthm (SOMEGOAL (rtac (reop rev (is_der_virt_red RS iffD2)))) lem_ccrs_d ; val lem_ccrs_d2a = tacthm (SOMEGOAL (rtac (reop rev (is_der_virt_red RS iffD2)))) lem_ccrs_d2 ; val _ = qed_goal_spec_mp "cc_red_sound_wfp" Spi_CC.thy "H : wfp cc_red --> wf_cc H --> \ \ (ALL h' G'. ((h', G'), H) : cc_red^* --> thy_cons G') --> valid_cc H" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (Clarify_tac 1), (rename_tac "h G" 1), (etac (mk_dupE allE2) 1), (etac impE 1), (rtac rtrancl_refl 1), (case_tac "EX x. Names x : G" 1), Clarify_tac 1, (etac allE 1), (subgoal_tac "?p : ?c" 1), mp_tac 1, (etac conjE 1), (etac impE 1), (eatac pres_wf 1 1), (etac impE 1), (REPEAT (etac all_forward 1)), (etac imp_forward2 1), (eatac tct.rsr 1 1), atac 1, (simp_tac (esimps [cc_red_def]) 2), (etac (R1_intros' RS disjI1) 2), (rtac R1_valid 1), (TRYALL (eresolve_tac (asm_rl :: wf_cc_Ds))), (* level 24 *) (fatac wf_cc_tcrI 1 1), (Simp_tac 1), Clarify_tac 1, (case_tac "subst_pr (a, b) ` G : rsmin oth_red UNIV" 1), (rtac classical 1), (rtac cons_redD 1), atac 1, (simp_tac (esimps [thy_cons_red_def]) 1) , (REPEAT_FIRST (resolve_tac [conjI, allI, impI, notI])), Clarsimp_tac 1, (fatac thy_cons_redDst 1 1), (etac same_type.elims 1), Clarsimp_tac 1, Clarsimp_tac 1, Clarsimp_tac 1, (clarsimp_tac (cesimps [Names_def]) 1), (* level 39, 4 subgoals *) (rtac iffI 1), (datac lem_ccrs_e 9 1), Fast_tac 1, (datac lem_ccrs_e2 9 1), Fast_tac 1, (datac lem_ccrs_da 9 1), contr_tac 1, (datac lem_ccrs_d2a 9 1),contr_tac 1, (* case where Gamma theta is reducible, although Gamma is not *) (fold_tac [mk_eq rsmin_or_alt]), (fold_tac [mk_eq rsmin_or_altr]), (fatac (wf_ccDfte RS subst_red_lem) 1 1), TRYALL atac, (etac wf_ccDred 1), Clarify_tac 1, (dtac lem_ccrs_d 1), (TRYALL (ares_tac [refl])), Full_simp_tac 2, (etac rev_image_eqI 1), Force_tac 1 ]) ; (* soundness, variant, since wfp applies only to cc_cons_red *) val _ = qed_goal_spec_mp "cc_red_sound_wfp_alt" Spi_CC.thy "H : wfp cc_cons_red --> wf_cc H --> \ \ (ALL h' G'. ((h', G'), H) : cc_red^* --> thy_cons G') --> valid_cc H" (fn _ => [ Clarify_tac 1, (rtac cc_red_sound_wfp 1), TRYALL atac, (REPEAT (chop_tac 1 (etac rev_mp 1))), (etac wfp.induct 1), Clarify_tac 1, (rtac wfp.wfpI 1), Clarify_tac 1, (etac (mk_dupE allE2) 1), (etac impE 1), (rtac rtrancl_refl 1), (etac allE 1), (etac impE 1), (eatac cc_cons_red.I 1 1), Clarify_tac 1, (etac impE 1), Clarify_tac 1, (etac allE2 1), (etac mp 1), (eatac tct.rsr 1 1), (etac mp 1), (eatac pres_wf 1 1) ]) ; val _ = bind_thm ("cc_red_sound", reop tl (wfp_cc_cons_red RS cc_red_sound_wfp_alt)) ; (* combine soundness and completeness *) val _ = qed_goal_spec_mp "cc_sc" Spi_CC.thy "wf_cc H --> \ \ (ALL h' G'. ((h', G'), H) : cc_red^* --> thy_cons G') = valid_cc H" (fn _ => [ Safe_tac, (eatac cc_red_sound 1 1), (datac cc_red_complete 2 1), Full_simp_tac 1 ]) ; val _ = qed_goal "cc_c_sub" Spi_CC.thy "cc_cons_red <= cc_red" (fn _ => [ (fast_tac (ces [cc_cons_red.elims]) 1) ]) ; val _ = qed_goal "cwf_sub_cons" Spi_CC.thy "cc_cwf_red <= cc_cons_red" (fn _ => [ (fast_tac (ces [cc_cwf_red.elims]) 1) ]) ; val cwf_sub = [cwf_sub_cons, cc_c_sub] MRS subset_trans ; val _ = qed_goal "cc_c_lem" Spi_CC.thy "(ALL h' G'. ((h', G'), H) : cc_red^* --> thy_cons G') = \ \ (ALL h' G'. ((h', G'), H) : cc_cons_red^* --> thy_cons G')" (fn _ => [ Safe_tac, (etac allE2 1), etac mp 1, (etac (cc_c_sub RS rtrancl_mono RS subsetD) 1), (etac rev_mp 1), (etac rtrancl_induct 1), (ALLGOALS Clarify_tac), (etac allE2 1), etac mp 1, rtac rtrancl_refl 1, (etac (mk_dupE allE2) 1), etac mp 1, (etac tct.rsr 1), (etac cc_cons_red.I 1), (etac allE2 1), etac mp 1, rtac rtrancl_refl 1 ]) ; val _ = qed_goal_spec_mp "c_cwf_lem1" Spi_CC.thy "wf_cc H --> ((H', H) : cc_cons_red^*) = ((H', H) : cc_cwf_red^*)" (fn _ => [ Safe_tac, (etac (cwf_sub_cons RSN (2, rtrancl_mono')) 2), (etac rev_mp 1), (etac rtrancl_induct 1), (ALLGOALS Clarify_tac), etac impE 1, (etac pres_wf 1), (etac cc_cons_red.elims 1), Fast_tac 1, (etac tct.rsr 1), (eatac cc_cwf_red.I 1 1) ]) ; val _ = qed_goal_spec_mp "c_cwf_lem" Spi_CC.thy "wf_cc H --> (ALL h' G'. ((h', G'), H) : cc_cons_red^* --> thy_cons G') = \ \ (ALL h' G'. ((h', G'), H) : cc_cwf_red^* --> thy_cons G')" (fn _ => [ (rtac impI 1), (asm_simp_tac (esimps [c_cwf_lem1]) 1) ]) ; val _ = bind_thm ("cwf_lem", [cc_c_lem, c_cwf_lem] MRS trans) ; (* OBS val _ = qed_goal_spec_mp "cwf_lem" Spi_CC.thy "wf_cc H --> (ALL h' G'. ((h', G'), H) : cc_red^* --> thy_cons G') = \ \ (ALL h' G'. ((h', G'), H) : cc_cwf_red^* --> thy_cons G')" (fn _ => [ Safe_tac, (etac allE2 1), etac mp 1, (etac (cwf_sub RS rtrancl_mono RS subsetD) 1), (etac rev_mp 1), (etac rev_mp 1), (etac rtrancl_induct 1), (ALLGOALS Clarify_tac), (etac allE2 1), etac mp 1, rtac rtrancl_refl 1, (etac impE 1), etac mp 2, (eatac pres_wf 1 2), (etac (mk_dupE all_forward) 1), (etac all_forward 1), Clarify_tac 1, (etac swap 1), (etac tct.rsr 1), (etac cc_cwf_red.I 1), atac 2, (etac allE2 1), etac mp 1, rtac rtrancl_refl 1 ]) ; *) val _ = bind_thm ("cc_cons_sc", ([cc_c_lem RS sym, cc_sc] MRS trans)) ; val _ = bind_thm ("cc_cwf_sc", reop tl ([cwf_lem RS sym, cc_sc] MRS trans)) ; (* now need to show that, assuming cc_cons_red is wf, testing (ALL h' G'. ((h', G'), ?H) : cc_red^* --> thy_cons G') is finite *) val _ = qed_goal_spec_mp "R1_alt" Spi_CC.thy "{y. (y, h, G) : R1} = (%n. (h, G - {n})) ` (range Names Int G)" (fn _ => [ (safe_tac (ces [R1.elims])), Clarsimp_tac 2, (rtac (notindiffs RS R1.intros RS mem_same_Pair2) 2), Force_tac 2, (rtac image_eqI 1), Clarsimp_tac 1, (etac (Diff_insert_absorb RS sym) 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "fb_R1" Spi_CC.thy "finite G --> finite {y. (y, h, G) : R1}" (fn _ => [ (clarsimp_tac (cis [finite_imageI], esimps [R1_alt]) 1) ]) ; val _ = qed_goalw "RS1_alt" Spi_CC.thy [Let_def] "RS1 h theta <= (%(sigma, D). let rho1 = comp_subst sigma theta in \ \ (rho1, CS1 (h, rho1))) ` {(sigma, D). (sigma, D, \ \ map (apsnd (subst_con theta)) (st_dcs (fst_bt h))) : sig_rtc ndcr}" (fn _ => [ (clarify_tac (ces [RS1.elims]) 1), (res_inst_tac [("x", "(?s, ?d)")] image_eqI 1), ALLGOALS Simp_tac ]) ; val _ = qed_goalw "RS2_alt" Spi_CC.thy [Let_def] "RS2 h theta <= (%(sigma, D). let rho2 = comp_subst sigma theta in \ \ (CS2 (h, rho2), rho2)) ` {(sigma, D). (sigma, D, \ \ map (apsnd (subst_con theta)) (st_dcs (snd_bt h))) : sig_rtc ndcr}" (fn _ => [ (clarify_tac (ces [RS2.elims]) 1), (res_inst_tac [("x", "(?s, ?d)")] image_eqI 1), ALLGOALS Simp_tac ]) ; val fthm = fsfte RS fb_ndcr_rtc RS finite_imageI RSN (2, finite_subset) ; val _ = bind_thm ("finite_RS1", [RS1_alt, st_dcs_finite_alt'] MRS fthm) ; val _ = bind_thm ("finite_RS2", [RS2_alt, st_dcs_finite_alt2'] MRS fthm) ; val _ = qed_goal "R3_alt" Spi_CC.thy "{(theta, cc). (theta, cc, (h, G)) : R3} <= \ \ (%theta. (theta, (subst_bt theta h, reduce (subst_pr theta ` G)))) ` \ \ (UN (M1, M2) : G. UN (N1, N2) : G. \ \ RS1 h (the (mgu {(M1, N1)})) Un RS2 h (the (mgu {(M2, N2)})))" (fn _ => [ (safe_tac (ces [R3.elims])), (TRYALL (EVERY' [ rtac rev_image_eqI, etac UN_I, Clarsimp_tac, etac rev_bexI, Clarsimp_tac, atac ORELSE' contr_tac, rtac refl])) ]) ; val _ = qed_goal_spec_mp "fb_R3" Spi_CC.thy "finite G --> finite {(theta, cc). (theta, cc, (h, G)) : R3}" (fn _ => [ (rtac impI 1), (rtac ([R3_alt, finite_imageI] MRS finite_subset) 1), (clarsimp_tac (cesimps [finite_RS1, finite_RS2]) 1) ]) ; val _ = qed_goal_spec_mp "RC1_alt'" Spi_CC.thy "C = (flag, S, M) --> \ \ RC1 h C = (%theta1. (theta1, CS1 (h, theta1))) ` fst ` {(theta1, D). \ \ rsolved_form D & (theta1, D, C # st_dcs (fst_bt h)) : sig_rtc ndcr}" (fn _ => [ (safe_tac (ces [RC1.elims])), (rtac RC1.intros 2), Asm_simp_tac 4, atac 3, rtac refl 2, (rtac imageI 1), (res_inst_tac [("x", "(?s, ?d)")] image_eqI 1), ALLGOALS Force_tac ]) ; val _ = qed_goal_spec_mp "RC2_alt'" Spi_CC.thy "C = (flag, S, M) --> \ \ RC2 h C = (%theta2. (CS2 (h, theta2), theta2)) ` fst ` {(theta2, D). \ \ rsolved_form D & (theta2, D, C # st_dcs (snd_bt h)) : sig_rtc ndcr}" (fn _ => [ (safe_tac (ces [RC2.elims])), (rtac RC2.intros 2), Asm_simp_tac 4, atac 3, rtac refl 2, (rtac imageI 1), (res_inst_tac [("x", "(?s, ?d)")] image_eqI 1), ALLGOALS Force_tac ]) ; val [RC1_alt, RC2_alt] = [[surjective_pairing, surjective_pairing RS Pair_eqI2] MRS trans] RL [RC1_alt', RC2_alt'] ; val fthm1 = [equalityD1, finite_imageI RS finite_imageI] MRS finite_subset ; val _ = qed_goal "Collect_split_disj_eq" HOL_Gen.thy "{(th, D). P th D | Q th D} = {(th, D). P th D} Un {(th, D). Q th D}" fn_at ; val _ = qed_goal "Collect_split_conj_eq" HOL_Gen.thy "{(th, D). P th D & Q th D} = {(th, D). P th D} Int {(th, D). Q th D}" fn_at ; val _ = qed_goalw_spec_mp "RS_fte_lem" Spi_CC.thy [mk_eq Collect_split_conj_eq] "fst ` snd ` set (st_dcs (x_bth)) <= Finites --> finite S --> \ \ finite {(th, D). P D & (th, D, (f,S,M) # st_dcs (x_bth)) : sig_rtc ndcr}" (fn _ => [ Clarify_tac 1, (rtac finite_subset 1), (rtac Int_lower2 1), (rtac fb_ndcr_rtc 1), Asm_simp_tac 1 ]) ; val fthm2 = RS_fte_lem RSN (2, fthm1) ; val _ = bind_thm ("finite_RC1", [RC1_alt, st_dcs_finite_alt'] MRS fthm2) ; val _ = bind_thm ("finite_RC2", [RC2_alt, st_dcs_finite_alt2'] MRS fthm2) ; val _ = qed_goal "R2_alt" Spi_CC.thy "{(theta, cc). (theta, cc, (h, G)) : R2} <= \ \ (%theta. (theta, (subst_bt theta h, reduce (subst_pr theta ` G)))) ` \ \ (UN (Mk, Nk) : keys ` G. UN f. RC1 h (f, fst ` (oth_of h Un G), Mk) Un \ \ RC2 h (f, snd ` (oth_of h Un G), Nk))" (fn _ => [ (safe_tac (ces [R2.elims])), (TRYALL (EVERY' [ rtac imageI, (etac (imageI RS UN_I)), Clarsimp_tac, rtac exI, Fast_tac ])) ]) ; val _ = qed_goal_spec_mp "fb_R2" Spi_CC.thy "finite G --> finite {(theta, cc). (theta, cc, (h, G)) : R2}" (fn _ => [ (rtac impI 1), (rtac ([R2_alt, finite_imageI] MRS finite_subset) 1), (clarsimp_tac (cesimps [finite_RC1, finite_RC2, bool_UNIV]) 1) ]) ; val _ = qed_goalw_spec_mp "fb_ps_cc_red" Spi_CC.thy [ps_cc_red_def] "finite G --> finite {(theta, cc). (theta, cc, h, G) : ps_cc_red}" (fn _ => [ (clarsimp_tac (cesimps [Collect_split_disj_eq, fb_R2, fb_R3]) 1), (rtac finite_cartesian_product 1), Simp_tac 1, (etac fb_R1 1) ]) ; val _ = qed_goalw_spec_mp "fb_cc_red" Spi_CC.thy [cc_red_alt] "finite G --> finite {cc. (cc, h, G) : cc_red}" (fn _ => [ (rtac impI 1), (rtac finite_subset 1), (res_inst_tac [("h", "snd")] finite_imageI 2), (etac fb_ps_cc_red 2), Clarsimp_tac 1, (rtac image_eqI 1), Force_tac 2, Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "fb_cc_cwf_red" Spi_CC.thy "finite {cc. (cc, h, G) : cc_cwf_red}" (fn _ => [ (case_tac "finite G" 1), (dtac fb_cc_red 1), (rtac finite_subset 1), atac 2, Clarify_tac 1, (etac (cwf_sub RS subsetD) 1), (rtac (Finites.emptyI RSN (2, finite_subset)) 1), (clarsimp_tac (ces [cc_cwf_red.elims], esimps []) 1) ]) ; val _ = bind_thm ("fb_cc_cwf_red_rtc", tacsthm [Clarify_tac 1, rtac fb_cc_cwf_red 1] ([wf_cc_cwf_red RS wf_ssI, allI] MRS wfp_fb)) ; val _ = qed_goal_spec_mp "fb_cc_cons_red_rtc" Spi_CC.thy "wf_cc H --> finite {H'. (H', H) : cc_cons_red^*}" (fn _ => [ (rtac impI 1), (asm_simp_tac (esimps [c_cwf_lem1]) 1), rtac fb_cc_cwf_red_rtc 1 ]) ; (* that is, Theorem~\ref{thm:decidability} [Decidability of Consistency Constraints] to test validity of a well-formed consistency constraint H, by cc_cons_sc you need to calculate the set {w. (w, H) : cc_cons_red^*}, which is finite, by fb_cc_cons_red_rtc, and see if all the theory parts of those constraints are consistent *) (* Lemma~\ref{lm:bi-trace-consistency} *) val _ = qed_goal_spec_mp "bt_cons_iff_valid" Spi_CC.thy "h = Out (M, N) # h' --> validbt h --> h' : bt_cons --> \ \ H = (h', reduce (oth_of h)) --> wf_cc H & valid_cc H = (h : bt_cons)" (fn _ => [ Safe_tac, (clarsimp_tac (cesimps [reduce_fn_nc, fn_oth_insert, virt_reduce, indist.id]) 1), (rewtac (mk_eq valid_cc.simps)), (* valid_cc H ==> h : bt_cons *) (etac bt_cons.OutI 1), Clarify_tac 1, (etac allE 1), mp_tac 1, (datac (civ_lem2 RS iffD2) 2 1), (full_simp_tac (esimps [subst_oth_bt']) 1), (* h : bt_cons ==> valid_cc H *) (etac bt_cons_OutE 1), Clarify_tac 1, (etac allE2 1), mp_tac 1, (eatac (civ_lem2 RS iffD1) 1 1), (full_simp_tac (esimps [subst_oth_bt']) 1) ]) ;