val _ = qed_goal_spec_mp "ents_red_pair" Spi_Reduce.thy "(Cs, D) : ents_red --> D : range (seqmap pair) --> Cs <= range (seqmap pair)" (fn _ => [ (strip_tac 1), (etac ents_red.elims 1), (ALLGOALS (asm_full_simp_tac (esimps [im_seqmap_pair_iff]))) ]) ; val _ = qed_goal_spec_mp "entss_red_pair" Spi_Reduce.thy "(Cs, Ds) : entss_red --> Ds <= range (seqmap pair) --> \ \ Cs <= range (seqmap pair)" (fn _ => [ (strip_tac 1), (etac entss_red.elims 1), (dtac ents_red_pair 1), ALLGOALS Fast_tac ]) ; val _ = qed_goal_spec_mp "entss_red_pair_rtc" Spi_Reduce.thy "(Cs, Ds) : entss_red^* --> Ds <= range (seqmap pair) --> \ \ Cs <= range (seqmap pair)" (fn _ => [ (strip_tac 1), (eatac converse_rtrancl_induct 1 1), (eatac entss_red_pair 1 1) ]) ; (* some of these superseded by subst_ents_red_if et seq in Spi_Subst.ML *) val _ = qed_goal_spec_mp "ents_red_if" Spi_Reduce.thy "(Ts, S) : ents_red --> (Ts <= indist) --> (S : indist)" (fn _ => [ (safe_tac (ces [ents_red.elims])), (ALLGOALS Clarsimp_tac), (rtac (insertI1 RS indist.plI) 1), (rtac (insertI1 RS indist.elI) 2), (ALLGOALS (etac indist_wk THEN' Fast_tac)) ]) ; val _ = qed_goal_spec_mp "entss_red_if" Spi_Reduce.thy "(Ts, Ss) : entss_red --> (Ts <= indist) --> (Ss <= indist)" (fn _ => [ (safe_tac (ces [entss_red.elims])), (etac ents_red_if 1), Fast_tac 1, Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "entss_red_rtc" Spi_Reduce.thy "(Ts, Ss) : entss_red^* --> (Ts <= indist) --> (Ss <= indist)" (fn _ => [ strip_tac 1, (eatac rtrancl_induct 1 1), (eatac entss_red_if 1 1) ]) ; (* TBD, currently axiom val _ = qed_goal_spec_mp "finite_ents_red" Spi_Reduce.thy "(Ts, S) : ents_red --> finite (fst S) --> finite Ts" (fn _ => [ (safe_tac (ces [ents_red.elims])), Auto_tac ]) ; *) val _ = qed_goal_spec_mp "finite_in_ents_red" Spi_Reduce.thy "(Ts, S) : ents_red --> T : Ts --> finite (fst S) --> finite (fst T)" (fn _ => [ (safe_tac (ces [ents_red.elims])), Auto_tac ]) ; val _ = qed_goal_spec_mp "finite_in_entss_red" Spi_Reduce.thy "(Ts, S) : ents_red --> (Ds, Ts) : entss_red^* --> \ \ (ALL T : Ds. finite (fst S) --> finite (fst T))" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac converse_rtrancl_induct 1), Clarify_tac 1, (eatac finite_in_ents_red 2 1), (etac entss_red.elims 1), Clarify_tac 1, (etac UnE 1), Force_tac 2, (datac finite_in_ents_red 1 1), atac 2, Force_tac 1 ]) ; val _ = qed_goal_spec_mp "fn_ents_red" Spi_Reduce.thy "(Ts, S) : ents_red --> T : Ts --> fn_oth (fst T) <= fn_oth (fst S)" (fn _ => [ (safe_tac (ces [ents_red.elims, fn_othE])), (ALLGOALS Clarsimp_tac), Safe_tac, (TRYALL (etac (insertI2 RS fn_othI) THEN' Force_tac)), (TRYALL (rtac (insertI1 RS fn_othI) THEN' Force_tac)) ]) ; val _ = qed_goal_spec_mp "fn_entss_red" Spi_Reduce.thy "(Ts, S) : ents_red --> (Ds, Ts) : entss_red^* --> \ \ (ALL T : Ds. fn_oth (fst T) <= fn_oth (fst S))" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac converse_rtrancl_induct 1), Clarify_tac 1, (eatac (fn_ents_red RS subsetD) 2 1), (etac entss_red.elims 1), Clarsimp_tac 1, (etac disjE 1), Force_tac 2, (datac fn_ents_red 1 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "ex_ec_nk" Spi_Reduce.thy "(H, G) : oth_red_nk --> (EX Ts Ds. Ds = insert (H, MN) Ts & \ \ (Ds, (G, MN)) : ents_red & (Ds <= indist) = ((G, MN) : indist))" (fn _ => [ (safe_tac (ces [oth_red_nk.elims])), (dtac ents_red.plI 1), (dtac ents_red.elI 2), (REPEAT_SOME (resolve_tac [exI,conjI])), (TRYALL (ares_tac [refl])), (ALLGOALS Clarsimp_tac), Safe_tac, (rtac (insertI1 RS indist.plI) 1), (etac pl_inv' 2), (rtac (insertI1 RS indist.elI) 2), (dtac el_inv' 4), (etac indist_ca1 4), Fast_tac 4, (ALLGOALS (etac indist_wk THEN' Fast_tac)) ]) ; val _ = qed_goal_spec_mp "ex_esc_nk" Spi_Reduce.thy "(H, G) : oth_red_nk --> (G, MN) ~: Cs --> \ \ (EX Ts Ds. Ds = insert (H, MN) Ts Un Cs & \ \ (Ds, insert (G, MN) Cs) : entss_red & \ \ (Ds <= indist) = (insert (G, MN) Cs <= indist))" (fn _ => [ (clarify_tac (cds [ex_ec_nk]) 1), (datac entss_red.I 1 1), (REPEAT_SOME (resolve_tac [exI, conjI, refl])), atac 1, Force_tac 1 ]) ; val ex_esc_nk' = notindiffs RSN (2, ex_esc_nk) ; val _ = qed_goal_spec_mp "ex_esc_nk''" Spi_Reduce.thy "(H, G) : oth_red_nk --> (G, MN) : Cs --> \ \ (EX Ds Ts. Ds = insert (H, MN) Ts Un (Cs - {(G, MN)}) & \ \ (Ds, Cs) : entss_red & (Ds <= indist) = (Cs <= indist))" (fn _ => [ Safe_tac, (dtac ex_esc_nk 1), (rtac notindiffs 1), (Clarsimp_tac 1), (datac ins2 1 1), (REPEAT_SOME (resolve_tac [exI, conjI, refl])), atac 1, Force_tac 1 ]) ; (* so there exist a set of constraints of which the lhs are all reduced *) val _ = qed_goalw_spec_mp "entss_min_red" Spi_Reduce.thy [rsmin_def] "Ss : rsmin entss_red UNIV --> (G, MN) : Ss --> G : rsmin oth_red_nk UNIV" (fn _ => [ Safe_tac, (rtac UNIV_I 1), (datac ex_esc_nk'' 1 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "entss_red_wfp" Spi_Reduce.thy "Ss : wfp entss_red --> \ \ (EX Ts. (Ts, Ss) : entss_red^* & fst ` Ts <= rsmin oth_red_nk UNIV & \ \ (Ts <= indist) = (Ss <= indist))" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (case_tac "fst ` dt <= rsmin oth_red_nk UNIV" 1), (rtac exI 1), Fast_tac 1, Clarify_tac 1, (etac swap 1), (clarsimp_tac (cesimps [rsmin_def]) 1), (datac ex_esc_nk'' 1 1), Clarify_tac 1, (etac allE 1), mp_tac 1, Clarify_tac 1, (rtac exI 1), (rtac conjI 1), (etac conjI 2), (eatac trans 1 2), (eatac tct.rsr 1 1) ]) ; val _ = qed_goal_spec_mp "entss_red_indist" Spi_Reduce.thy "Ss : wfp entss_red --> (Ss <= indist) = \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (ALL (G,MN) : Ts. (EX sp : idv_sets MN. sp <= G)))" (fn _ => [ Safe_tac, (dtac entss_red_wfp 1), Clarify_tac 1, (rtac exI 1), (etac conjI 1), Clarify_tac 1, (rtac (idv_sets RS iffD1) 1), (rtac nf_no_left' 1), (Best_tac 1), (clarsimp_tac (cesimps [rsmin_nk_equiv]) 1), etac subsetD 1, etac rev_image_eqI 1, Simp_tac 1, (dtac entss_red_rtc 1), Fast_tac 2, Clarify_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (eatac (idv_setsD RS virt_indist) 1 1) ]) ; (* entss_red is well-founded, by a proof similar to Dawson & Gore, CSL 2004 *) (* also, as finitely branching, {Ts. (Ts, Ss) : entss_red^*} is finite, by wfp_fb *) val _ = qed_goal_spec_mp "subst_entws_red_if'" Spi_Subst.thy "fg = (f,g) --> (Ts, S) : entws_red --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg S : indist)" (fn _ => [ (safe_tac (ces [entws_red.elims])), (ALLGOALS Clarsimp_tac), (rtac indist.plI 1), (etac rev_image_eqI 1), atac 2, Force_tac 1, (rtac (dest_nk indist_nk.elI) 1), (etac rev_image_eqI 1), TRYALL atac, Simp_tac 1 ]) ; val subst_entws_red_if = surjective_pairing RS subst_entws_red_if' ; val _ = qed_goal_spec_mp "subst_entwss_red_if" Spi_Subst.thy "(Ts, Ss) : entwss_red --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg ` Ss <= indist)" (fn _ => [ (safe_tac (ces [entwss_red.elims])), (dtac subst_entws_red_if 1), TRYALL Force_tac ]) ; val _ = qed_goal_spec_mp "subst_entwss_red_rtc" Spi_Subst.thy "(Ts, Ss) : entwss_red^* --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg ` Ss <= indist)" (fn _ => [ strip_tac 1, (eatac rtrancl_induct 1 1), (eatac subst_entwss_red_if 1 1) ]) ; (* do we need any of the following ? *) (* avoid using this one, implied by subst_exd_ecc_nk ?? *) val _ = qed_goal_spec_mp "subst_ex_ecc_nk" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ (EX Ds. (Ds, (G, MN)) : ents_red & \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ds <= indist) = \ \ (subst_seq fg (G Un H, MN) : indist))" (fn _ => [ (safe_tac (ces [oth_red_nk.elims])), (ALLGOALS (ftac (insertI1 RSN (2, equalityD2')) THEN' etac imageE)), (ALLGOALS (etac DiffE)), (datac subst_is_Encs 3 2), (datac subst_is_Mpairs 3 1), (safe_tac (ces [Mpairs.elims, Encs.elims])), (ALLGOALS (EVERY' [(case_tac "fg"), Clarsimp_tac, rtac exI, rtac conjI])), (* level 7 *) (etac ents_red_plI'' 1), Simp_tac 1, (rtac iffI 1), (dtac indist.plI' 1), (etac indist_wk 1), (etac image_insert_Diff_Un1 1), Simp_tac 1, (rtac pl_inv' 1), (etac indist_wk 1), (rtac image_insert_Diff_Un2 1), Simp_tac 1, (* level 18 *) (etac ents_red_elI'' 1), Simp_tac 1, Safe_tac, (datac indist_elI' 1 1), (etac indist_wk 1), (etac image_insert_Diff_Un1 1), Simp_tac 1, (rtac el_inv_ca 1), (etac indist_wk 1), (rtac image_insert_Diff_Un2 1), Simp_tac 1, Fast_tac 1, (ALLGOALS (EVERY' [etac indist_wk, (rtac (Un_upper1 RS image_mono RS transfer Main.thy xt6)), (rtac (image_diff_subset RS xt6)), (datac (sym RS insert_new_eq) 1), Force_tac ])) ]) ; val _ = qed_goal_spec_mp "subst_ex_escc_nk" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ (G, MN) ~: Cs --> \ \ (EX Ds. (Ds, insert (G, MN) Cs) : entss_red & \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ds <= indist) = \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` (insert (G, MN) Cs) <= indist))" (fn _ => [ (clarify_tac (cds [subst_ex_ecc_nk]) 1), (PRIMITIVE zero_var_indexes), (instantiate_tac [("H", "H")]), (datac entss_red.I 1 1), (REPEAT_SOME (ares_tac [exI, conjI])), (clarsimp_tac (cesimps [image_Un]) 1) ]) ; val subst_ex_escc_nk' = notindiffs RSN (3, subst_ex_escc_nk) ; val _ = qed_goal_spec_mp "subst_ex_escc_nk''" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ (G, MN) : Cs --> (EX Ds. (Ds, Cs) : entss_red & \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ds <= indist) = \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Cs <= indist))" (fn _ => [ Safe_tac, (datac subst_ex_escc_nk 1 1), (rtac notindiffs 1), (PRIMITIVE zero_var_indexes), (instantiate_tac [("H", "H")]), (Clarsimp_tac 1), (datac ins2 1 1), (REPEAT_SOME (ares_tac [exI, conjI])), Asm_simp_tac 1, (etac (sym RS thin_rl) 1), Force_tac 1 ]) ; (* now the above, with H = {} *) val _ = bind_thm ("subst_ex_ec_nk", simplify init_ss (read_instantiate [("H", "{}")] subst_ex_ecc_nk)) ; val _ = bind_thm ("subst_ex_esc_nk''", simplify init_ss (read_instantiate [("H", "{}")] subst_ex_escc_nk'')) ; (* problems in trying to prove consistency is preserved when substitution involved, but entss_red preserves pairs *) val _ = qed_goal_spec_mp "subst_entss_redc_wfp" Spi_Subst.thy "Ss : wfp entss_red --> (ALL S : Ss. S : range (seqmap pair)) --> \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (%T. subst_pr fg ` (fst T - Ne)) ` Ts <= rsmin oth_red_nk UNIV & \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ts <= indist) = \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ss <= indist))" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (case_tac "?P :: bool" 1), (REPEAT (resolve_tac [exI, conjI, impI] 1)), etac conjI 2, (rtac rtrancl_refl 1), (rtac refl 1), Clarify_tac 1, (etac swap 1), (clarsimp_tac (cesimps [rsmin_def]) 1), (dres_inst_tac [("H", "H")] subst_ex_escc_nk'' 1), (datac bspec 1 1), atac 2, (force_tac (cesimps [im_seqmap_pair_iff, subset_image_iff]) 1), Clarify_tac 1, (etac allE 1), mp_tac 1, Clarify_tac 1, (fatac (rewrite_rule [subset_def] entss_red_pair) 1 1), mp_tac 1, Clarify_tac 1, (etac allE 1), mp_tac 1, (datac tct.rsr 1 1), mp_tac 1, Clarsimp_tac 1 ]) ; val _ = bind_thm ("subst_entss_red_wfp", simplify init_ss (read_instantiate [("H", "{}")] subst_entss_redc_wfp)) ; rewrite_rule [mk_eq rsmin_nk_equiv] subst_entss_redc_wfp ; val _ = qed_goal_spec_mp "entss_red_if" Spi_Reduce.thy Goal "Ss : wfp entss_red --> (subst_seq fg ` Ss <= indist) = \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (ALL (G, MN):Ts. EX sp:idv_sets MN. subst_oth fg sp <= subst_oth fg G))" ; byall [ Safe_tac, (dtac entss_red_wfp 1), Clarify_tac 1, (rtac exI 1), (etac conjI 1), Clarify_tac 1, (rtac (idv_sets RS iffD1) 1), (rtac nf_no_left' 1), (Best_tac 1), (clarsimp_tac (cesimps [rsmin_nk_equiv]) 1), etac subsetD 1, etac rev_image_eqI 1, Simp_tac 1, (dtac entss_red_rtc 1), Fast_tac 2, Clarify_tac 1, val _ = qed_goal_spec_mp "entss_red_indist" Spi_Reduce.thy "Ss : wfp entss_red --> (Ss <= indist) = \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (ALL (G,MN) : Ts. (EX sp : idv_sets MN. sp <= G)))" (fn _ => [ Safe_tac, (dtac entss_red_wfp 1), Clarify_tac 1, (rtac exI 1), (etac conjI 1), Clarify_tac 1, (rtac (idv_sets RS iffD1) 1), (rtac nf_no_left' 1), (Best_tac 1), (clarsimp_tac (cesimps [rsmin_nk_equiv]) 1), etac subsetD 1, etac rev_image_eqI 1, Simp_tac 1, (dtac entss_red_rtc 1), Fast_tac 2, Clarify_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (eatac (idv_setsD RS virt_indist) 1 1) ]) ; (* entss_red *) (* want subst version of entss_red_indist recall subst_idv_sets subst_idv_sets_rev *) (* these carry over after substitution, because substituting may have the consequence that the first condition in ents_red.intros (ie, sth ~: G) may no longer hold, but that doesn't affect this conclusion *) (* trivially follows from subst_ents_redc_if' *) val _ = qed_goal_spec_mp "subst_ents_red_if'" Spi_Subst.thy "fg = (f,g) --> (Ts, S) : ents_red --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg S : indist)" (fn _ => [ (safe_tac (ces [ents_red.elims])), (ALLGOALS Clarsimp_tac), (rtac (insertI1 RS indist.plI) 1), (rtac (insertI1 RS indist.elI) 2), (ALLGOALS (etac indist_wk THEN' Fast_tac)) ]) ; val subst_ents_red_if = surjective_pairing RS subst_ents_red_if' ; val _ = qed_goal_spec_mp "subst_entss_red_if" Spi_Subst.thy "(Ts, Ss) : entss_red --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg ` Ss <= indist)" (fn _ => [ (safe_tac (ces [entss_red.elims])), (dtac subst_ents_red_if 1), TRYALL Force_tac ]) ; val _ = qed_goal_spec_mp "subst_entss_red_rtc" Spi_Subst.thy "(Ts, Ss) : entss_red^* --> (subst_seq fg ` Ts <= indist) --> \ \ (subst_seq fg ` Ss <= indist)" (fn _ => [ strip_tac 1, (eatac rtrancl_induct 1 1), (eatac subst_entss_red_if 1 1) ]) ; val _ = qed_goal_spec_mp "subst_ents_redc_if'" Spi_Subst.thy "fg = (f,g) --> (Ts, (G, MN)) : ents_red --> \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ts <= indist) --> \ \ (subst_seq fg (G Un H, MN) : indist)" (fn _ => [ (safe_tac (ces [ents_red.elims])), (ALLGOALS Clarsimp_tac), (rtac (insertI1 RS indist.plI) 1), (rtac (insertI1 RS indist.elI) 2), (ALLGOALS (etac indist_wk THEN' Fast_tac)) ]) ; val subst_ents_redc_if = surjective_pairing RS subst_ents_redc_if' ; val _ = qed_goal_spec_mp "subst_entss_redc_if" Spi_Subst.thy "(Ts, Ss) : entss_red --> \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ts <= indist) --> \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ss <= indist)" (fn _ => [ (safe_tac (ces [entss_red.elims])), (dtac subst_ents_redc_if 1), TRYALL Force_tac ]) ; val _ = qed_goal_spec_mp "subst_entss_redc_rtc" Spi_Subst.thy "(Ts, Ss) : entss_red^* --> \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ts <= indist) --> \ \ ((% (T, c). subst_seq fg (T Un H, c)) ` Ss <= indist)" (fn _ => [ strip_tac 1, (eatac rtrancl_induct 1 1), (eatac subst_entss_redc_if 1 1) ]) ; val _ = qed_goal_spec_mp "subst_exd_ecc_nk" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ (EX Ds. (Ds, (G, MN)) : ents_red & erprops Ds fg (G, MN) H)" (fn _ => [ (safe_tac (ces [oth_red_nk.elims])), (ALLGOALS (ftac (insertI1 RSN (2, equalityD2')) THEN' etac imageE)), (ALLGOALS (etac DiffE)), (datac subst_is_Encs 3 2), (datac subst_is_Mpairs 3 1), (safe_tac (ces [Mpairs.elims, Encs.elims])), (ALLGOALS (EVERY' [(case_tac "fg"), Clarsimp_tac, rtac exI, rtac conjI])), (* level 7 *) (etac ents_red_plI'' 1), (etac ents_red_elI'' 2), ALLGOALS Clarsimp_tac, (REPEAT_SOME (rtac conjI)), (TRYALL (EVERY' [(rtac ballI), (etac DiffE), (etac (imageI RS indist.id)) ])), (rtac indist_pc1 1), (rtac indist_pc2 2), (rtac (insertI1 RS indist.id RSN (3, indist.elI)) 4), (TRYALL (etac rev_image_eqI THEN' Force_tac)), (etac indist_wk 2), (dtac equalityD2 2), Fast_tac 2, (rtac iffI 1), (dtac indist.plI' 1), (etac indist_wk 1), (etac image_insert_Diff_Un1 1), Simp_tac 1, (rtac pl_inv' 1), (etac indist_wk 1), (rtac image_insert_Diff_Un2 1), Simp_tac 1, (* level 28 *) Safe_tac, (datac indist_elI' 1 1), (etac indist_wk 1), (etac image_insert_Diff_Un1 1), Simp_tac 1, (rtac el_inv_ca 1), (etac indist_wk 1), (rtac image_insert_Diff_Un2 1), Simp_tac 1, Fast_tac 1, (ALLGOALS (EVERY' [etac indist_wk, (rtac (Un_upper1 RS image_mono RS transfer Main.thy xt6)), (rtac (image_diff_subset RS xt6)), (datac (sym RS insert_new_eq) 1), Force_tac ])) ]) ; val _ = qed_goal_spec_mp "subst_exd_escc_nk" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ (G, MN) ~: Cs --> erprops (insert (G, MN) Cs) fg B H --> \ \ (EX Ds. (Ds, insert (G, MN) Cs) : entss_red & erprops Ds fg B H)" (fn _ => [ (clarify_tac (cds [subst_exd_ecc_nk]) 1), (rtac exI 1), (rtac conjI 1), (eatac entss_red.I 1 1), (eatac erprops_trans 1 1) ]) ; val subst_exd_escc_nk' = notindiffs RSN (3, subst_exd_escc_nk) ; val _ = qed_goal_spec_mp "subst_exd_escc_nk''" Spi_Subst.thy "(K, subst_pr fg ` (G - Ne)) : oth_red_nk --> thy_cons G --> \ \ erprops Cs fg B H --> (G, MN) : Cs --> \ \ (EX Ds. (Ds, Cs) : entss_red & erprops Ds fg B H)" (fn _ => [ Safe_tac, (datac subst_exd_escc_nk 1 1), (rtac notindiffs 1), (stac insert_Diff 1), atac 1, atac 1, (etac ex_forward 1), (clarsimp_tac (cesimps [insert_absorb]) 1) ]) ; val _ = qed_goal_spec_mp "subst_entss_redcd_wfp" Spi_Subst.thy "Ss : wfp entss_red --> Ss <= range (seqmap pair) --> \ \ erprops Ss fg B H --> \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (%T. subst_pr fg ` (fst T - Ne)) ` Ts <= rsmin oth_red_nk UNIV & \ \ erprops Ts fg B H)" (fn _ => [ (rtac impI 1), (etac wfp.induct 1), (case_tac "?P :: bool" 1), (REPEAT (resolve_tac [exI, conjI, impI] 1)), etac conjI 2, (rtac rtrancl_refl 1), atac 1, (clarsimp_tac (cesimps [rsmin_def]) 1), (dres_inst_tac [("H", "H")] subst_exd_escc_nk'' 1), TRYALL atac, (force_tac (cesimps [im_seqmap_pair_iff]) 1), Clarify_tac 1, (etac allE 1), (eatac impE 1 1), Clarify_tac 1, (etac impE 1), (fold_goals_tac [pair_def]), (eatac entss_red_pair 1 1), Clarify_tac 1, (etac allE 1), mp_tac 1, (datac tct.rsr 1 1), mp_tac 1, Clarsimp_tac 1 ]) ; val subst_entss_redcd_wfp' = rewrite_rule [mk_eq rsmin_nk_equiv] subst_entss_redcd_wfp ; val _ = qed_goal_spec_mp "entss_resp_Ne'" Spi_Subst.thy "finite G --> thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (Ts, (G, MN)) : ents_red --> (Ds, Ts) : entss_red^* --> T = (U, x) --> \ \ T : Ds --> (subst_seq fg (U Un reduce G, c) : indist) = \ \ (subst_seq fg (reduce (U Un reduce G) - Ne, c) : indist)" (fn _ => [ Clarsimp_tac 1, (rtac reduce_subs_Ne_indist_thy' 1), Asm_simp_tac 1, (datac finite_in_entss_red 2 1), Asm_simp_tac 1, Full_simp_tac 1, (rtac thy_strl_resp_mono' 1), (rtac Un_upper2 2), (etac thy_strl_resp_reduce 1), (asm_simp_tac (esimps [reduce_fn_nc, fn_oth_Un]) 1), (etac xt6 1), (datac fn_entss_red 2 1), Full_simp_tac 1 ]) ; val entss_resp_Ne = simplify (esimps []) (refl RSN (6, entss_resp_Ne')) ; val _ = qed_goal_spec_mp "entss_reduce_Ne" Spi_Subst.thy "finite G --> (G, MN) : range (seqmap pair) --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (K, subst_pr fg ` (G - Ne)) : oth_red_nk --> \ \ (EX Ts. (Ts, G, MN) : ents_red O entss_red^* & \ \ ((%(T,c). subst_seq fg (reduce (T Un reduce G) - Ne, c)) \ \ ` Ts <= indist) = (subst_seq fg (G Un reduce G, MN) : indist))" (fn _ => [ Safe_tac, (dtac subst_exd_ecc_nk 1), Force_tac 1, Clarify_tac 1, (ftac finite_ents_red 1), Simp_tac 1, (ftac wfp_entss 1), Clarsimp_tac 1, (fatac finite_in_ents_red 1 1), Simp_tac 1, Full_simp_tac 1, (dtac subst_entss_redcd_wfp 1), (etac ents_red_pair 1), Fast_tac 1, atac 1, (etac ex_forward 1), (etac conjE 1), (rtac conjI 1), (eatac rel_compI 1 1), (rtac trans 1), Clarsimp_tac 2, (chop_last (atac 2)), (simp_tac (esimps [image_subset_iff]) 1), (rtac (refl RS ball_cong) 1), Clarsimp_tac 1, (rtac (entss_resp_Ne RS sym) 1), TRYALL atac, TRYALL Simp_tac ]) ; (* in erprops, let H = reduce G ; so get fg is respectful for fst T Un H, thy_strl_resp_mono' ; so subst_seq ?fg (T Un ?H, c) = subst_seq ?fg (reduce (T Un ?H) - Ne, c) by entss_resp_Ne now reduce (T Un ?H) <= H <= T Un H, so idv_sets_reduce_le applies *) (* so we use the above with H = the original G, for each original constraint; idea is to get resulting constraints G' |- ..., where G' >= G (for respectfulness), and such that G' >= reduce G' (for using idv_sets to test |-, by idv_sets_reduce_le) ; *) (* since we get subst_pr fg ` (fst T - Ne)) is reduced, we need to consider respectful substitutions, eg, [ strl_resp_oth_red, strl_resp_oth_red_rtc, thy_strl_resp_reduce ] ; [ subst_all_Ne_indist, reduce_subs_Ne_indist_thy ] ; *) (* val _ = qed_goal_spec_mp "entss_red_if" Spi_Reduce.thy Goal "Ss : wfp entss_red --> (subst_seq fg ` Ss <= indist) = \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (ALL (G, MN):Ts. EX sp:idv_sets MN. subst_oth fg sp <= subst_oth fg G))" ; byall [ Safe_tac, (dtac entss_red_wfp 1), Clarify_tac 1, (rtac exI 1), (etac conjI 1), Clarify_tac 1, (rtac (idv_sets RS iffD1) 1), (rtac nf_no_left' 1), (Best_tac 1), (clarsimp_tac (cesimps [rsmin_nk_equiv]) 1), etac subsetD 1, etac rev_image_eqI 1, Simp_tac 1, (dtac entss_red_rtc 1), Fast_tac 2, Clarify_tac 1, val _ = qed_goal_spec_mp "entss_red_indist" Spi_Reduce.thy "Ss : wfp entss_red --> (Ss <= indist) = \ \ (EX Ts. (Ts, Ss) : entss_red^* & \ \ (ALL (G,MN) : Ts. (EX sp : idv_sets MN. sp <= G)))" (fn _ => [ Safe_tac, (dtac entss_red_wfp 1), Clarify_tac 1, (rtac exI 1), (etac conjI 1), Clarify_tac 1, (rtac (idv_sets RS iffD1) 1), (rtac nf_no_left' 1), (Best_tac 1), (clarsimp_tac (cesimps [rsmin_nk_equiv]) 1), etac subsetD 1, etac rev_image_eqI 1, Simp_tac 1, (dtac entss_red_rtc 1), Fast_tac 2, Clarify_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (eatac (idv_setsD RS virt_indist) 1 1) ]) ; *) (* this is obviously wrong, may have pair in G of which one component is Ne *) val _ = qed_goal_spec_mp "subst_entvs_min" Spi_Subst.thy "thy_cons G --> min_entvs fg G --> \ \ (H, subst_pr fg ` (G - Ne)) : oth_red_nkr --> \ \ H <= subst_pr fg ` (G - Ne)" (fn _ => [ Clarify_tac 1, (safe_tac (ces [oth_red_nkr.elims])), (TRYALL (etac equalityD2' THEN' etac insertI2)), (ALLGOALS (ftac (insertI1 RSN (2, equalityD2')) THEN' etac imageE)), (ALLGOALS (etac DiffE)), (TRYALL (datac subst_is_Encs 3)), (TRYALL (datac subst_is_Mpairs 3)), (safe_tac (ces [Mpairs.elims, Encs.elims])), (ALLGOALS (EVERY' [(case_tac "fg"), Clarsimp_tac])), (TRYALL (datac min_entvs_Mpair 1)) (TRYALL (eatac (vslem1 RS rev_notE) 2)), (TRYALL (EVERY' [ (eresolve_tac [entvs.plI, refl RS entvs.elI]), (etac contrapos_nn), Clarsimp_tac, (rtac image_eqI), (rtac (subst_pr_simps RS sym)), atac ])), ALLGOALS Clarsimp_tac, (TRYALL (EVERY' [(rtac iffI), (etac indist_wkii), (rtac indist.plI), atac o incr, (etac rev_image_eqI), Simp_tac])), Safe_tac, (etac indist_wki 1), (etac idv_wk 1), (dtac vslem2 1), Simp_tac 2, Simp_tac 1, (rtac (dest_norm indist_norm.elI) 1), atac 3, (etac idv_wk 2), (etac vslem3 2), (etac rev_image_eqI 1), Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "subst_entvss_min" Spi_Subst.thy "(G, Ts) : rsmin entvss {(G, Ts). \ \ ALL T:Ts. is_der_virt (subst_seq fg T)} --> \ \ (H, subst_pr fg ` (G - Ne)) : oth_red_nkr --> \ \ H <= subst_pr fg ` (G - Ne)" (fn _ => [ Clarify_tac 1, (dtac if_rsmin_entvss 1) (safe_tac (ces [oth_red_nkr.elims])) ]) *) (* can we better cope with Ne in the above by using subst_all_Ne_indist *) val _ = qed_goal_spec_mp "entvs_min_resp_Ne'" Spi_Subst.thy "fg = (f, g) --> finite G --> thy_cons G --> \ \ min_entvs fg G --> Ne Int G = {} --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (subst_pr fg ` G, MN) : indist --> is_der_virt (subst_pr fg ` G, MN)" (fn _ => [ Clarify_tac 1, (rtac (notI RS notnotD) 1), (datac (dest_norm idv_red_nkr_not_idv) 1 1), etac finite_imageI 1, (etac (not_def RS defD1 RS thin_rl) 1), Clarify_tac 1, (ftac nidv 1), (etac oth_red_nkr.elims 1), Safe_tac, (TRYALL (datac (insertI2 RSN (2, equalityD2')) 1 THEN' contr_tac)), (ALLGOALS (ftac (insertI1 RSN (2, equalityD2')))), (ALLGOALS (eresolve_tac [imageE])), (ALLGOALS (subgoal_tac "x ~: Ne")), (TRYALL (EVERY' [ (rtac notI), (etac (equalityD1' RS emptyE)), (eatac IntI 1) ])), (TRYALL (datac subst_is_Encs 3)), (TRYALL (datac subst_is_Mpairs 3)), (safe_tac (ces [Mpairs.elims, Encs.elims])), (TRYALL (etac Ne.elims ORELSE' etac thin_rl)), (ALLGOALS Full_simp_tac), (ALLGOALS Clarify_tac), (TRYALL (EVERY' [(datac min_entvs_Mpair 1), (etac (sub_msgs_im RSN (2, swap))), Fast_tac])), (datac min_entvs_Encs 1 1), Asm_simp_tac 1, (etac (subset_insertI RSN (2, idv_wk)) 1), (etac (sub_msgs_im RSN (2, swap)) 1), atac 1 ]) ; val entvs_min_resp_Ne = surjective_pairing RS entvs_min_resp_Ne' ; (* val _ = qed_goal_spec_mp "entvs_min_resp" Spi_Subst.thy "finite G --> thy_cons G --> min_entvs fg G --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (subst_pr fg ` G, MN) : indist --> is_der_virt (subst_pr fg ` G, MN)" (fn _ => [ Clarify_tac 1, (fatac (rewrite_rule [subst_oth_def] subst_all_Ne_indist) 2 1) (rtac (entvs_min_resp_Ne RS idv_wk) 1), (SOMEGOAL (rtac Diff_disjoint)), SOMEGOAL atac, (REPEAT_SOME (eresolve_tac [finite_Diff, Diff_subset RSN (2, cons_mono), Diff_subset RS fn_oth_mono RS subset_trans, resp_no_Ne, asm_rl])), (SOMEGOAL (rtac (Diff_subset RS image_mono))), ]) this doesn't work, can't get min_entvs fg G ==> min_entvs fg (G - Ne), again problem is that we may have pair in G of which one component is Ne *)