structure Spi_SI = struct val thy = the_context () end ; val _ = use_legacy_bindings Spi_SI.thy ; (* note that the converse doesn't hold, since, eg, a reduction may split a pair, with the first component in Ne, which gets disregarded, and then derivation may not be possible without some respectfulness assumption *) val unif_ch1_def = rewrite_rule [unif_ch1a_def] unif_ch1_pdef ; (* summary of main results towards decidability : unif_ch does the following for a given bi-trace: one bitrace -> several respectfulness constraints (bt_resp_constrs) unif_ch1 does the following for one given constraint: one constraint -> several sets of right constraints (orkvss_iff); unif_ch1a does the following for one set of right constraints: one right constraint G |-R M -> G >= G' for one of several possible G', idv_sets; for a set of right constraints, combine the sets using sat_unifs thence one of a set of unifiers must be satisfied (idv_match); and unif_ch1 takes the union of these and unif_ch combines the resulting unifiers using UN_choices *) (* lemmas to illustrate what unif_ch1a, unif_ch1 does, ie, return sets of pairs, which, if they are equal, gives that sequents derivable: need to translate these into results about what happens when a substitution is made which makes these pairs become equal, ie want to extend unif_ch1a_eq_idv to something like this "unif : unif_ch1a f S --> (ALL (m,n): unif. subst_pr g m = subst_pr g n) --> \ \ (ALL (Gamma, MN) : S. \ \ is_der_virt (subst_seq (comp_psub g f) (Gamma - Ne, M,N))) " ; *) val _ = qed_goalw_spec_mp "unif_ch1a_iff" Spi_SI.thy [unif_ch1a_def] "(EX unif' : unif_ch1a f Cs. unif' <= unif) = \ \ (ALL (G, MN) : Cs. (EX sp : idv_sets (subst_pr f MN). \ \ (EX U. U <= unif & fst ` U = sp & snd ` U <= subst_pr f ` (G - Ne))))" (fn _ => [ (simp_tac (esimps [sat_unifs_iff]) 1), (rtac iffI 1), (ALLGOALS (EVERY' [ (etac ball_match), Clarsimp_tac, etac rev_bexI, rtac exI, etac conjI, Asm_simp_tac ])) ]) ; val unif_ch1a_iff' = read_instantiate [("unif", "Collect (split op =)")] unif_ch1a_iff ; val _ = qed_goal_spec_mp "unif_ch1a_eqs" Spi_SI.thy "(EX unif : unif_ch1a f Cs. (ALL (m,n): unif. m = n)) = \ \ (ALL (G, MN) : Cs. (EX sp : idv_sets (subst_pr f MN). \ \ sp <= subst_pr f ` (G - Ne)))" (fn _ => [ (rtac box_equals 1), (rtac unif_ch1a_iff' 1), (simp_tac (esimps [subset_def, Bex_def]) 1), Safe_tac, (ALLGOALS (EVERY' [datac bspec 1, Clarsimp_tac, etac rev_bexI])), (etac xt6 1), Force_tac 1, (res_inst_tac [("x", "pair ` sp")] exI 1), Force_tac 1 ]) ; val _ = qed_goalw_spec_mp "unif_ch1a_eq_idv" Spi_SI.thy [unif_ch1a_def] "(EX unif : unif_ch1a f S. (ALL (m,n): unif. m = n)) = \ \ (ALL (Gamma, MN) : S. is_der_virt (subst_seq f (Gamma - Ne, MN)))" (fn _ => [ (rtac trans 1), (rtac sat_unifs_lem 1), (rtac (refl RS ball_cong) 1), Clarify_tac 1, rewtac o_def, (rtac trans 1), (rtac (idv_match RS sym) 1), Simp_tac 1 ]) ; val _ = qed_goalw_spec_mp "unif_ch1_eq_idv" Spi_SI.thy [unif_ch1_pdef] "(EX unif : unif_ch1 f G M. (ALL (m,n): unif. m = n)) = \ \ (EX (H, Vs):{x. (x, ?G, {}) : orkvss^*}. \ \ ALL (Gamma, MN) : (insert (H, M, M) Vs). \ \ is_der_virt (subst_seq f (Gamma - Ne, MN)))" (fn _ => [ Safe_tac, rtac rev_bexI 1, Fast_tac 1, Simp_tac 1, Safe_tac, (datac (bexI RS (unif_ch1a_eq_idv RS iffD1) RS bspec) 1 1), (rtac insertI1 1), Full_simp_tac 1, (datac (bexI RS (unif_ch1a_eq_idv RS iffD1) RS bspec) 1 1), (etac insertI2 1), Full_simp_tac 1, (etac (unif_ch1a_eq_idv RS iffD2 RS bexE) 1), Fast_tac 1 ]) ; (* to help explain unif_ch1, see also ex_orkvss_unif_sub *) val _ = qed_goal_spec_mp "unif_ch1_Name_eq_der" Spi_SI.thy "finite G --> \ \ (EX unif : unif_ch1 (Name, Name) G M. (ALL (m,n): unif. m = n)) = \ \ ((G, M, M) : indist)" (fn _ => [ (rtac impI 1), (rtac (unif_ch1_eq_idv RS trans) 1), (rtac iffI 1), (dtac ex_orkvss_idv 2), Force_tac 2, (force_tac (cesimps [idv_Ne]) 2), Clarify_tac 1, (dtac orkvss_if_rtc 1), Full_simp_tac 2, (clarsimp_tac (cesimps [idv_Ne]) 1), (etac virt_indist 1) ]) ; val _ = qed_goal_spec_mp "Diff_insert_absorb_eq" HOL_Gen.thy "x ~: A --> B = insert x A --> B - {x} = A" fn_at ; val _ = qed_goal_spec_mp "indist_nsv_wk" Spi_SI.thy "(oth, MN) : indist_nsv fg --> \ \ (ALL othl. oth <= othl --> (othl, MN) : indist_nsv fg)" (fn _ => [ (rtac impI 1), (etac indist_nsv.induct 1), Safe_tac, (rtac indist_nsv.virt 1), (etac idv_wk 1), (Fast_tac 1), (rtac indist_nsv.plI 1), (eatac subsetD 1 1), (etac allE 1), (etac mp 1), Fast_tac 1, (rtac indist_nsv.elI 1), (eatac subsetD 1 1), (etac idv_wk 1), Fast_tac 1, (etac allE 1), (etac mp 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "indist_nsv_norm_Ne" Spi_SI.thy "(oth, MN) : indist_nsv fg --> (subst_pr fg ` (oth - Ne), MN) : indist_norm" (fn _ => [ (case_tac "fg" 1), (rtac impI 1), (etac indist_nsv.induct 1), Safe_tac, (rtac indist_norm.virt 1), (etac idv_wk 1), Fast_tac 1, (rtac indist_norm.elI 2), (rtac indist_norm.plI 1), (TRYALL (etac (DiffI RS rev_image_eqI) THEN' fast_tac (ces [Ne.elims]) THEN' Force_tac)), (ALLGOALS Clarsimp_tac), (etac indist_norm_wk 1), Force_tac 1, rewtac indist_norm, (etac indist_ca1 1), Force_tac 1, (etac (virt_indist RS indist_wk) 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "indist_nsv_norm" Spi_SI.thy "(oth, MN) : indist_nsv fg --> (subst_pr fg ` oth, MN) : indist_norm" (fn _ => [ (rtac impI 1), (dtac indist_nsv_norm_Ne 1), (etac indist_norm_wk 1), Fast_tac 1 ]) ; val _ = qed_goal_spec_mp "idvsNe_orkvs_if'" Spi_SI.thy "fg = (f, g) --> ((T, Ts), S) : orkvs --> (Ball Ts (idvsNe fg)) --> \ \ ((T, MN) : indist_nsv fg) --> ((S, MN) : indist_nsv fg)" (fn _ => [ (safe_tac (ces [orkvs.elims])), (ALLGOALS Clarsimp_tac), (rtac (insertI1 RS indist_nsv.plI) 1), (rtac (insertI1 RS indist_nsv.elI) 2), (TRYALL (etac indist_nsv_wk THEN' Fast_tac)), Asm_simp_tac 1]) ; val idvsNe_orkvs_if = surjective_pairing RS idvsNe_orkvs_if' ; val _ = qed_goal_spec_mp "idvsNe_orkvss_rtc_if" Spi_SI.thy "((T, Ts), (S, Ss)) : orkvss^* --> (Ball Ts (idvsNe fg)) --> \ \ ((T, MN) : indist_nsv fg) --> ((S, MN) : indist_nsv fg)" (fn _ => [ rtac impI 1, (etac rtrancl_induct_pair 1), Simp_tac 1, Clarsimp_tac 1, (etac orkvss.elims 1), Clarify_tac 1, (dtac idvsNe_orkvs_if 1), atac 2, (dtac orkvss_rtc_sub 1), Fast_tac 1, atac 1 ]) ; val is_simps = [idv_ss_def, pair_minus_Ne', subst_pr_im_pair', pair_def] ; val _ = qed_goal_spec_mp "smder_sub_altD" Spi_SI.thy "(S, M) : smder_sub f --> seqmap pair (S, M) : indist_nsv (f,f)" (fn _ => [ (rtac impI 1), (etac smder_sub.induct 1), Simp_tac 1, (rtac indist_nsv.virt 1), (full_simp_tac (esimps is_simps) 1), (ALLGOALS Clarsimp_tac), (rtac indist_nsv.elI 2), (rtac indist_nsv.plI 1), (TRYALL (etac imageI)), TRYALL atac, (TRYALL (rtac notI THEN' Fast_tac)), (full_simp_tac (esimps is_simps) 1) ]) ; val _ = qed_goal_spec_mp "smder_sub_altI" Spi_SI.thy "(G, MN) : indist_nsv (f,f) --> \ \ (ALL ss. (G, MN) = seqmap pair ss --> ss : smder_sub f)" (fn _ => [ (rtac impI 1), (etac indist_nsv.induct 1), Clarify_tac 1, (rtac smder_sub.virt 1), (asm_full_simp_tac (esimps is_simps) 1), ALLGOALS Clarsimp_tac, (etac smder_sub.elI 2), (etac smder_sub.plI 1), (TRYALL (rtac notI THEN' Force_tac)), (TRYALL (etac allE THEN' etac mp THEN' Simp_tac)), (full_simp_tac (esimps is_simps) 1) ]) ; val _ = bind_thm ("smder_sub_alt", (tacsthm [etac smder_sub_altD 1, rtac smder_sub_altI 1, Clarsimp_tac 2, (rtac conjI 2), rtac refl 2, rtac refl 2, Full_simp_tac 1 ] iffI)) ; val _ = qed_goal_spec_mp "smder_sub_der" Spi_SI.thy "(S, M) : smder_sub f --> (subst_msg f ` S, M) : derrec smpsc {}" (fn _ => [ (clarsimp_tac (cds [indist_nsv_norm], esimps [smder_sub_alt, indist_norm, indist_smpsc_eq, subst_pr_im_pair]) 1) ]) ; val _ = qed_goal_spec_mp "smder_sub_der_Ne" Spi_SI.thy "(S, M) : smder_sub f --> \ \ (subst_msg f ` (S - range Name), M) : derrec smpsc {}" (fn _ => [ (clarsimp_tac (cds [indist_nsv_norm_Ne], esimps [smder_sub_alt, indist_norm, indist_smpsc_eq, pair_minus_Ne, subst_pr_im_pair]) 1) ]) ; val _ = qed_goal_spec_mp "min_orkvs_indist_nsv" Spi_SI.thy "(oth, MN) : indist_nsv fg --> min_orkvs_Ne fg oth --> \ \ is_der_virt (subst_pr fg ` (oth - Ne), MN)" (fn _ => [ (rtac impI 1), (etac indist_nsv.elims 1), Fast_tac 1, (ALLGOALS (EVERY' [(clarsimp_tac (cesimps [min_orkvs_Ne_def])), (etac allE2), (etac impE) ])), (etac orkvs_plI'' 1), Fast_tac 1, (etac orkvs_elI'' 1), Clarify_tac 1, (etac notE 1), (etac idv_wk 1), Fast_tac 1 ]) ; (* try completely different approach, ie induction on size *) val indist_nsv_excl_plI' = [notindiffs RS indist_nsv_excl.plI, insert_Diff] MRS mem_same_Pair1 ; val indist_nsv_excl_elI' = [notindiffs RS indist_nsv_excl.elI, insert_Diff] MRS mem_same_Pair1 ; val _ = qed_goal_spec_mp "indist_nsv_excl_wk" Spi_SI.thy "(oth, MN) : indist_nsv_excl fg --> \ \ (ALL othl. oth <= othl --> (othl, MN) : indist_nsv_excl fg)" (fn _ => [ (rtac impI 1), (etac indist_nsv_excl.induct 1), Safe_tac, (rtac indist_nsv_excl.virt 1), (etac idv_wk 1), Fast_tac 1, (rtac indist_nsv_excl_plI' 1), (etac (insertI1 RS rev_subsetD) 2), (etac allE 1), etac mp 1, Fast_tac 1, (rtac indist_nsv_excl_elI' 1), (etac (insertI1 RS rev_subsetD) 3), (etac idv_wk 1), Fast_tac 1, (etac allE 1), etac mp 1, Fast_tac 1 ]) ; val pair_tacs = [ (datac rev_subsetD 1), Asm_full_simp_tac, (etac (Diff_subset RS subset_trans))] ; val fn_oth_le_tacs = [ (etac xt6), (dtac fn_oth_mem), (clarsimp_tac (cesimps [fn_oth_def])), (datac bspec 1), Force_tac ] ; val _ = qed_goal_spec_mp "indist_ne_nsv_excl'" Spi_SI.thy "fg = (f, g) --> \ \ (ALL H MN G. setsum (msg_size o fst) G < n --> finite G --> \ \ (H, MN) : indist_norm_excl --> \ \ (H = subst_pr fg ` G --> (G <= range pair) --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (G, MN) : indist_nsv_excl fg))" (fn _ => [ (rtac impI 1), hyp_subst_tac 1, (induct_tac "n" 1), Simp_tac 1, Clarify_tac 1, (dtac (less_Suc_eq_le RS iffD1) 1), (case_tac "G - Ne = G" 1), (SELECT_GOAL (REPEAT_FIRST (eresolve_tac [allE, impE])) 2), (SOMEGOAL (eatac resp_no_Ne 1)), (SOMEGOAL (etac (Diff_subset RS subset_trans))), (SOMEGOAL (etac (Diff_subset RS fn_oth_mono RS subset_trans))), (SOMEGOAL (rtac refl)), (SOMEGOAL (etac finite_Diff)), (SOMEGOAL (eatac ((dest_so o mk_ne o mk_norm) subst_all_Ne_indist) 2)), (etac xt8 2), (etac ss_ms_lt 2), Fast_tac 2, (etac (Diff_subset RSN (2, indist_nsv_excl_wk)) 2), (* level ?? *) (* case "G - Ne = G" *) (etac indist_norm_excl.elims 1), ALLGOALS Clarify_tac, (rtac indist_nsv_excl.virt 1), Asm_simp_tac 1, (* plI rule *) (ftac eq_insertD 1), Clarify_tac 1, (fatac (thy_cons_in_pair RS subst_is_Mpairs) 2 1), (datac equalityD2' 1 1), Fast_tac 1, (clarify_tac (ces [Mpairs.elims]) 1), (rtac indist_nsv_excl_plI' 1), atac 2, (SELECT_GOAL (REPEAT_FIRST (eresolve_tac [allE, impE])) 1), (rtac refl 4), (etac xt8 1), atac 7, Simp_tac 1, (eatac plI_rem_in_fms_s 1 1), Simp_tac 1, (EVERY' pair_tacs 2), (eatac (oth_red_plI'' RS strl_resp_oth_red) 1 2), (EVERY' fn_oth_le_tacs 2), (datac Diff_insert_absorb_eq 1 1), hyp_subst_tac 1, Clarsimp_tac 1, (etac indist_norm_excl_wk 1), (clarify_tac (HOL_cs addSIs [insert_mono, image_diff_subset RS xt6]) 1), Simp_tac 1, (* elI rule *) (ftac eq_insertD 1), Clarify_tac 1, (fatac (thy_cons_in_pair RS subst_is_Encs) 2 1), (datac equalityD2' 1 1), Fast_tac 1, (clarify_tac (ces [Encs.elims]) 1), (rtac indist_nsv_excl_elI' 1), atac 3, (stac Diff_Diff_commute 1), Clarsimp_tac 1, (etac idv_wk 1), (datac Diff_insert_absorb_eq 1 1), (clarsimp_tac (cis [image_diff_subset RS xt6], esimps []) 1), (SELECT_GOAL (REPEAT_FIRST (eresolve_tac [allE, impE])) 1), (rtac refl 4), atac 7, (etac xt8 1), Simp_tac 1, (eatac elI_rem_in_fms_s 1 1), Simp_tac 1, (EVERY' pair_tacs 2), (eatac (UNIV_I RS oth_red_k_elI'' RS strl_resp_oth_red_k) 1 2), (EVERY' fn_oth_le_tacs 2), (datac Diff_insert_absorb_eq 1 1), hyp_subst_tac 1, Clarsimp_tac 1, (etac indist_norm_excl_wk 1), (clarify_tac (HOL_cs addSIs [insert_mono, image_diff_subset RS xt6]) 1), Simp_tac 1 ]) ; val indist_ne_nsv_excl = [surjective_pairing, lessI] MRS indist_ne_nsv_excl' ; val _ = qed_goal_spec_mp "indist_nsv_excl_le" Spi_SI.thy "(G, MN) : indist_nsv_excl fg --> (G, MN) : indist_nsv fg" (fn _ => [ rtac impI 1, (etac indist_nsv_excl.induct 1), (etac indist_nsv.virt 1), (rtac (insertI1 RS indist_nsv.plI) 1), (etac indist_nsv_wk 1), Fast_tac 1, (rtac (insertI1 RS indist_nsv.elI) 1), (etac idv_wk 1), Fast_tac 1, (etac indist_nsv_wk 1), Fast_tac 1 ]) ; val indist_ne_nsv' = indist_ne_nsv_excl RS indist_nsv_excl_le ; val _ = bind_thm ("indist_ne_nsv", rewrite_rule [indist_norm_excl] indist_ne_nsv') ; val _ = bind_thm ("indist_nsv_resp", rewrite_rule [indist_norm] indist_ne_nsv) ; (* should be possible to get a result of the form (EX H Vs. ALL MN. ...) but would require a different proof, possibly involving confluence of orkvss can proof similar to indist_resp_ex_orkvss_red give this better result ? NO - because H would have to involve all reductions such that the clause ALL (K, X) : Vs. ... is satisfied, but that may involve splitting pairs such that first components is in Ne, which is disregarded, but may be required for some MN *) val _ = qed_goal_spec_mp "indist_nsv_ex_orkvss" Spi_SI.thy "(G, MN) : indist_nsv_excl fg --> (EX H Vs. ((H, Vs), (G, {})) : orkvss^* & \ \ is_der_virt (subst_pr fg ` (H - Ne), MN) & \ \ (ALL (K, X) : Vs. is_der_virt (subst_seq fg (K - Ne, X))))" (fn _ => [ (rtac impI 1), (etac indist_nsv_excl.induct 1), Fast_tac 1, Safe_tac, (ALLGOALS (EVERY' [ rtac exI, rtac exI, rtac conjI, rtac tct.rsr])), (TRYALL (rtac orkvss.I THEN' eresolve_tac orkvs.intros)), Force_tac 1, Force_tac 1, (dtac orkvss_rtc_exp 1), Force_tac 1, (force_tac (ces [idv_wk], esimps []) 1) ]) ; val _ = qed_goal_spec_mp "nsv_idv_red" Spi_SI.thy "(G, MN) : indist_nsv_excl fg --> \ \ ~ is_der_virt (subst_pr fg ` (G - Ne), MN) --> \ \ (EX H Vs. ((H, Vs), G) : orkvs & \ \ (ALL (K, X) : Vs. is_der_virt (subst_seq fg (K - Ne, X))))" (fn _ => [ Clarify_tac 1, (etac indist_nsv_excl.elims 1), Safe_tac, (REPEAT_FIRST (resolve_tac [exI, conjI])), (etac orkvs.plI 1), Simp_tac 1, (etac orkvs.elI 1), Simp_tac 1, (etac idv_wk 1), Fast_tac 1 ]) ; (* doesn't hold - what if orkvs splits pairs, and one component is Ne val _ = qed_goal_spec_mp "orkvs_idv_nsv1" Spi_SI.thy "((G, MN) : indist_nsv_excl fg) --> ((H, Vs), G) : orkvs --> \ \ ((H, MN) : indist_nsv_excl fg)" (fn _ => [ (rtac impI 1), (etac indist_nsv_excl.induct 1), (rtac impI 1), (rtac indist_nsv_excl.virt 1), (etac orkvs.elims 1), Safe_tac, (TRYALL (EVERY' [etac idv_ca1, Fast_tac, case_tac "fg", (asm_simp_tac (esimps [image_insert])) ])) (TRYALL (etac idv_ca1 THEN' Fast_tac THEN' Simp_tac)) (* need pl_inv, el_inv for idv *) ]) val _ = qed_goal_spec_mp "orkvs_idv_nsv1" Spi_SI.thy "((H, Vs), G) : orkvs --> \ \ ((G, MN) : indist_nsv_excl fg) --> ((H, MN) : indist_nsv_excl fg)" val _ = qed_goal_spec_mp "orkvs_idv_nsv_nc" Spi_SI.thy "((H, Vs), G) : orkvs --> \ \ (ALL (K, X):Vs. is_der_virt (subst_seq fg (K - Ne, X))) --> \ \ ((G, MN) : indist_nsv_excl fg) = ((H, MN) : indist_nsv_excl fg)" alternative - use indist_ne_nsv_excl strl_resp_orkvs fn_orkvs_eq finite_ine val _ = qed_goal_spec_mp "indist_nsv_ex_orkvss_ext'" Spi_SI.thy "(G, Us) : wfp orkvss --> (EX H Vs. ((H, Vs), (G, Us)) : orkvss^* & \ \ ((ALL (K, X) : Us. is_der_virt (subst_seq fg (K - Ne, X))) --> \ \ (ALL (K, X) : Vs. is_der_virt (subst_seq fg (K - Ne, X)))) & \ \ (ALL MN. (G, MN) : indist_nsv_excl fg --> \ \ is_der_virt (subst_pr fg ` (H - Ne), MN)))" (fn _ => [ (rtac impI 1), (etac wfp_induct_pair 1), (case_tac "(ALL MN. (a, MN) : indist_nsv_excl fg --> \ \ is_der_virt (subst_pr fg ` (a - Ne), MN))" 1), (REPEAT (resolve_tac [exI, conjI] 1)), (rtac rtrancl_refl 1), rtac conjI 1, Simp_tac 1, atac 1, Clarsimp_tac 1, (datac nsv_idv_red 1 1), Clarify_tac 1, (etac allE2 1), (etac impE 1), (etac orkvss.I 1), (etac conjE 1), (REPEAT_FIRST (eresolve_tac [ex_forward, conj_forward, all_forward])), (etac tct.rsr 1), (etac orkvss.I 1), (rtac impI 1), (etac mp 1), Force_tac 1, (rtac impI 1), (etac mp 1), (* depends on orkvs_idv_nsv1 above which doesn't seem to be true ; what if G is {(, )}, and H is {(x,x), (A,B)}, then (x,x) in H gets disregarded ; equally the main result isn't true - depending on the choice of MN, may want to reduce G to H or not *) ]) ; *) val _ = qed_goal_spec_mp "indist_resp_ex_orkvss_red'" Spi_SI.thy "(G, Us) : wfp orkvss --> finite G --> G <= range pair --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (EX H Vs. ((H, Vs), (G, Us)) : orkvss^* & \ \ ((ALL (K, X) : Us. is_der_virt (subst_seq fg (K - Ne, X))) --> \ \ (ALL (K, X) : Vs. is_der_virt (subst_seq fg (K - Ne, X)))) & \ \ min_orkvs_Ne fg H & \ \ (ALL MN. ((subst_pr fg ` G, MN) : indist) = \ \ is_der_virt (subst_pr fg ` (H - Ne), MN)))" (fn _ => [ (rtac impI 1), (etac wfp_induct_pair 1), (case_tac "min_orkvs_Ne fg a" 1), (etac thin_rl 1), (REPEAT (resolve_tac [impI, exI, conjI] 1)), (rtac rtrancl_refl 1), rtac conjI 1, Simp_tac 1, rtac conjI 1, atac 1, Clarify_tac 1, (rtac iffI 1), (etac (virt_indist RS indist_wk) 2), Fast_tac 2, (datac (rewrite_rule [subst_oth_def] subst_all_Ne_indist) 2 1), (datac (thy_cons_in_pair RS min_orkvs_orar RS iffD1) 1 1), (etac nf_no_left' 1), (simp_tac (esimps [rsmin_or_alt RS sym, rsmin_or_altr RS sym]) 1), (dtac (min_orkvs_Ne_def RS def_imp_eq RS (Not_eq_iff RS iffD2) RS iffD1) 1), Clarsimp_tac 1, (etac allE2 1), (etac impE 1), (etac orkvss.I 1), (etac conjE 1), (etac impE 1), (eatac (orkvs_finite_iff RS iffD1) 1 1), (etac impE 1), (eatac (rewrite_rule [pair_def] orkvs_pair) 1 1), (etac impE 1), (eatac strl_resp_orkvs 1 1), (etac impE 1), (ftac fn_orkvs_eq 1), Clarsimp_tac 1, (REPEAT_FIRST (eresolve_tac [ex_forward, conj_forward, all_forward])), (etac tct.rsr 1), (etac orkvss.I 1), (rtac impI 1), (etac mp 1), Force_tac 1, atac 1, (rtac trans 1), atac 2, (rtac iffI 1), (eatac subst_orkvs_indist 1 1), (etac subst_orkvs_if 1), atac 2, Clarify_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (etac (virt_indist RS indist_wk) 1), Fast_tac 1 ]) ; val indist_resp_ex_orkvss_red = reop tl (wfp_orkvss RS indist_resp_ex_orkvss_red') ; (* can we do the above simpler using min_orkvs_indist_nsv ?? possibly, but it is good to see what we can do without using indist_nsv *) (* subst_orkvss_idv_nc gives converse to resp_ex_orkvss *) (* resp_ex_orkvss follows from indist_resp_ex_orkvss *) val _ = qed_goal_spec_mp "resp_ex_orkvss" Spi_SI.thy "finite G --> subst_seq fg (G, MN) : indist --> G <= range pair --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (EX H Vs. ((H,Vs), G,{}) : orkvss^* & \ \ (ALL (K,X) : insert (H,MN) Vs. is_der_virt (subst_seq fg (K - Ne, X))))" (fn _ => [ Safe_tac, (dtac (indist_ne_nsv_excl RS indist_nsv_ex_orkvss) 1), (TRYALL (ares_tac [refl])), (full_simp_tac (esimps [indist_norm_excl, indist_norm]) 1), (REPEAT (eresolve_tac [ex_forward, conj_forward, asm_rl] 1)), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "resp_ex_orkvss_red" Spi_SI.thy "finite G --> G <= range pair --> \ \ thy_strl_resp fg ns G --> fn_oth G <= Union (set ns) --> \ \ (EX H Vs. ((H, Vs), (G, {})) : orkvss^* & \ \ reduce (subst_pr fg ` (H - Ne)) = (subst_pr fg ` (H - Ne)))" (fn _ => [ Safe_tac, (fatac indist_resp_ex_orkvss_red 3 1), (etac ex_forward 1), (etac ex_forward 1), Clarify_tac 1, (rtac conjI 1), atac 1, (fatac orkvss_rtc_pair 1 1), (datac (thy_cons_in_pair RS min_orkvs_orar RS iffD1) 1 1), (rtac (orar_min_reduce RS iffD1) 1), atac 2, (datac orkvss_finite_rtc 1 1), rtac finite_imageI 1, etac finite_Diff 1 ]) ; val _ = qed_goalw_spec_mp "resp_ex_orkvss_idv_sets'" Spi_SI.thy [ork_idv_prop_def] "finite G --> G <= range pair --> \ \ thy_strl_resp fg ns G --> fn_oth (insert (M,M) G) <= Union (set ns) --> \ \ (subst_seq fg (G, (M,M)) : indist) = ork_idv_prop fg G M" (fn _ => [ strip_tac 1, (rtac iffI 1), (datac resp_ex_orkvss 3 1), (clarsimp_tac (cesimps [fn_oth_insert]) 1), (REPEAT1 (etac ex_forward 1)), Clarify_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (etac disjE 1), Clarify_tac 1, (etac idv_sets_sub_idv 1), (datac orkvss_rtc_kc_pair 1 1), Fast_tac 1, Clarsimp_tac 1, (etac idv_sets_sub_idv 1), (* level 15 *) Clarify_tac 1, (ftac subst_orkvss_i_if_rtc 1), Full_simp_tac 2, Clarsimp_tac 1, Safe_tac, (etac idv_sets_sub_indist 1), (etac subset_trans 3), Fast_tac 3, (eatac strl_resp_orkvss_rtc 1 1), (dtac fn_orkvss_rtc 1), (asm_full_simp_tac (esimps [fn_oth_insert]) 1), (etac subset_trans 1), Asm_simp_tac 1, Clarsimp_tac 1, (datac bspec 1 1), Clarsimp_tac 1, (etac idv_sets_sub_indist 1), (etac subset_trans 3), Fast_tac 3, (eatac strl_resp_kc_orkvss_rtc 1 1), Fast_tac 1, (dtac fn_orkvss_kc_rtc 1), Fast_tac 1, (etac subset_trans 1), (etac xt6 1), (simp_tac (esimps [fn_oth_insert, Un_upper2]) 1) ]) ; val resp_ex_orkvss_idv_sets = rewrite_rule [ork_idv_prop_def] resp_ex_orkvss_idv_sets' ; val _ = qed_goalw_spec_mp "resp_ork_idvs_comp'" Spi_SI.thy [ork_idv_cprop_def] "g = (ga, gb) --> fg = (comp_psub g (f, f)) --> \ \ finite G --> G <= range pair --> \ \ thy_strl_resp fg ns G --> fn_oth (insert (M,M) G) <= Union (set ns) --> \ \ (subst_seq fg (G, (M,M)) : indist) = ork_idv_cprop g (f,f) G M" (fn _ => [ (rtac impI 1), (etac thin_rl 1), Clarify_tac 1, rtac iffI 1, (datac resp_ex_orkvss 3 1), (clarsimp_tac (cesimps [fn_oth_insert]) 1), (REPEAT1 (eresolve_tac [ex_forward] 1)), (etac conjE 1), (rtac conjI 1), atac 1, (etac ball_match 1), (clarsimp_tac (cesimps [comp_pr]) 1), (dtac (reop rev (idv_sets_sub_idv')) 1), (full_simp_tac (esimps [image_compose]) 2), (etac disjE 1), Force_tac 1, (datac orkvss_rtc_kc_pair 1 1), Fast_tac 1, Force_tac 1, Clarify_tac 1, (rtac (resp_ex_orkvss_idv_sets RS iffD2) 1), TRYALL atac, (rtac exI 1), (rtac exI 1), (rtac conjI 1), (atac 1), (etac ball_match 1), Clarify_tac 1, (subgoal_tac "aa = b" 1), (etac insertE 2), Fast_tac 2, (datac orkvss_rtc_kc_pair 1 2), Fast_tac 2, (force_tac (cesimps [im_pair_iff]) 2), Clarify_tac 1, rewtac o_def, (rewtac (mk_eq snd_conv)), (dtac subst_idv_sets_rev 1), (etac bex_match 1), (simp_tac (esimps [comp_pr, image_compose]) 1), (rtac subset_trans 1), (eatac image_mono 1 1) ]) ; val resp_ork_idvs_comp = [surjective_pairing, refl] MRS resp_ork_idvs_comp' ; val _ = bind_thm ("sat_unifs_orkvss", fold_rule [mk_eq sat_unifs_ex_f_equiv] resp_ex_orkvss_idv_sets) ; val _ = bind_thm ("ork_idv_prop_unif", fold_rule [mk_eq sat_unifs_ex_f_equiv] ork_idv_prop_def) ; val _ = bind_thm ("ork_idv_cprop_unif", fold_rule [mk_eq sat_unifs_ex_f_equiv] ork_idv_cprop_def) ; val _ = qed_goalw "ork_idv_prop_unif_u" Spi_SI.thy [meta_eq_def, ork_idv_prop_unif] "ork_idv_prop fg G M == (EX unif : UNION {x. (x, G, {}) : orkvss^*} \ \ (% (H, Vs). sat_unifs (idv_sets o snd) (%(K, X). K - Ne) \ \ (insert (H, M, M) Vs)). Ball unif ?P)" (fn _ => [ Safe_tac, (REPEAT ((REPEAT_SOME (ares_tac [bexI, exI, conjI, refl])) THEN ALLGOALS Simp_tac)) ]) ; val _ = qed_goalw "ork_idv_cprop_unif_u" Spi_SI.thy [meta_eq_def, ork_idv_cprop_unif] "ork_idv_cprop g f G M == (EX unif : UNION {x. (x, G, {}) : orkvss^*} \ \ (% (H, Vs). sat_unifs (idv_sets o subst_pr f o snd) \ \ (%(K, X). subst_pr f ` (K - Ne)) \ \ (insert (H, M, M) Vs)). Ball unif ?P)" (fn _ => [ Safe_tac, (REPEAT ((REPEAT_SOME (ares_tac [bexI, exI, conjI, refl])) THEN ALLGOALS Clarsimp_tac)), (ALLGOALS (EVERY' [(etac (equalityD1 RSN (2, rev_subsetD))), cong_tac, rtac ext, Clarsimp_tac])) ]) ; val _ = bind_thm ("resp_orkvss_unif", rewrite_rule [ork_idv_prop_unif_u] resp_ex_orkvss_idv_sets') ; val _ = bind_thm ("resp_ork_comp_unif", rewrite_rule [ork_idv_cprop_unif_u, symmetric unif_ch1_def] resp_ork_idvs_comp) ; val resp_ork_comp_unif' = [refl, refl] MRS rewrite_rule [ork_idv_cprop_unif_u, symmetric unif_ch1_def] resp_ork_idvs_comp' ; val _ = qed_goalw "ork_idv_prop_def'" Spi_SI.thy [meta_eq_def, ork_idv_prop_def, Let_def] "ork_idv_prop fg G M == \ \ (let AA = {insert (H, M, M) Vs | H Vs. ((H, Vs), G, {}) : orkvss^*} \ \ in EX A : AA. ALL KX : A. ?P KX)" (fn _ => [ Safe_tac, (REPEAT ((REPEAT_SOME (ares_tac [bexI, exI, conjI, refl])) THEN ALLGOALS Simp_tac)) ]) ; val _ = qed_goalw "ork_idv_prop_bl" Spi_SI.thy [meta_eq_def, ork_idv_prop_def', Let_def] "ork_idv_prop fg G M == \ \ (let AA = {insert (H, M, M) Vs | H Vs. ((H, Vs), G, {}) : orkvss^*} \ \ in ALL B : block AA. EX KX : B. ?P KX)" (fn _ => [ (rtac trans 1), (rtac block 2), (rtac refl 1) ]) ; val resp_ex_orkvss_idv_sets_bl = rewrite_rule [ork_idv_prop_bl, Let_def] resp_ex_orkvss_idv_sets' ; val eeui = prove_goal HOL_Gen.thy "(EX KX:B. EX sp:f KX. Q sp) = (EX sp : Union (f ` B). Q sp)" fn_at ; (* can't use eeui on resp_ex_orkvss_idv_sets_bl because KX is involved in Q *) (* if a null unifier is found then the constraint is satisfied, without assuming respectfulness *) val _ = qed_goal_spec_mp "ex_orkvss_ns" Spi_SI.thy "((H,Vs), G,{}) : orkvss^* --> \ \ (ALL KX : insert (H,(M,M)) Vs. (EX sp : (idv_sets o snd) KX. \ \ sp <= fst KX)) --> (G, (M,M)) : indist" (fn _ => [ strip_tac 1, (dtac (read_instantiate [("fg", "(Name, Name)")] subst_orkvss_if_rtc) 1), (Force_tac 2), (clarsimp_tac (cesimps [idv_sets RS sym]) 1), (etac virt_indist 1) ]) ; val _ = qed_goalw_spec_mp "ex_orkvss_unif_sub" Spi_SI.thy [unif_ch1_def] "unif : unif_ch1 (f,f) G M --> unif <= range pair --> \ \ subst_seq (f,f) (G, (M,M)) : indist" (fn _ => [ Clarify_tac 1, (dtac subst_orkvss_if_rtc 1), Full_simp_tac 2, Simp_tac 1, Safe_tac, (ALLGOALS (dtac sat_unifs_charD)), (rtac insertI1 1), (rtac virt_indist 1), (etac insertI2 2), (ALLGOALS (EVERY' [(Clarsimp_tac), (etac idv_setsD), (datac subset_trans 1), (asm_full_simp_tac (esimps [im_pair_12_eq])), (etac subset_trans), (rtac (Diff_subset RS image_mono)) ])) ]); (* [resp_ork_comp_unif, ex_orkvss_unif_sub] ; now use results resp_ork_comp_unif (and resp_ork_idvs_comp) and comparable inverse result which is ex_orkvss_unif_sub now do similar to Spi_Mgrs.ML, but can't use gmgrs1 directly (except that present results are for just one constraint) ; but it might be easier to do one constraint at a time anyway [kaF.simps, kaG.simps] ; but do we want to adapt these results to all constraints simultaneously bt_resp_constrs ; ext_constrs_ug ; *) (* considering indist_resp_ex_orkvss_red, want to find the substitutions for each (H, Vs), got using idv_all_su ; thus, for each (H, Vs) from indist_resp_ex_orkvss_red, use idv_all_su red_unifs Vs gives pairs to be unified, and red_unifs_inv shows that these are sufficient to satisfy all the Vs, to get most general substitutions, then use ex_umgrs_resp and umgrs_resp_id to get most general respectful substitutions, (this done in red_mgrs, in Spi_Mgrs) ; ensure these do not allow further reductions (if not, irrelevant, as indist_resp_ex_orkvss_red includes min_orkvs_Ne property), get other side of respectful substitution, (BIG problem here, theorems second_sub, and subst_exists, subst_unique, assume bitrace consistency, which is what we are examining, NOW FIXED, with second_sub_tl, and subst_exists_tl, subst_unique_tl) ensure this permits the same reductions in orkvss (if not, not consistent, by ss_red_cons) then pick M and M', unify, refine substitution to respectful one, get other side of respectful substitution, ensure it unifies N and N' (if not, inconsistent) ; need to ensure further refinement on side 1 doesn't remove property that N and N' are unified (match_rc1_subst part of this) then we're done !! *) val _ = qed_goalw "slice_unif_UNch'" Spi_SI.thy [slice_unif_alt] "UN_choices Vs H = slice_unif ` UN_choices Vs (image (image pair_unif) o H)" (fn _ => [ (simp_tac (esimps [UN_choices_im, image_compose RS sym]) 1), (rtac (image_id_eq RS sym) 1), rtac ext 1, Simp_tac 1, (rtac inj_vimage_image_eq 1), (clarsimp_tac (cesimps [inj_on_def]) 1) ]) ; val _ = bind_thm ("slice_unif_UNch", rewrite_rule [o_def, pair_unif_alt] slice_unif_UNch') ; val _ = qed_goalw_spec_mp "red_unifs_ss_slice" Spi_SI.thy [red_unifs_def, red_unifs_ss_def] "red_unifs_ss Vs = slice_unif ` red_unifs (seqmap pair ` Vs)" (fn _ => [ (simp_tac (esimps [su_idv_pair RS sym]) 1), (simp_tac (esimps [sat_unifs_UNch, match_sets_im]) 1), (rtac slice_unif_UNch 1) ]) ; val _ = qed_goalw_spec_mp "red_unifs_inv" Spi_SI.thy [red_unifs_def] "finite G --> G <= range pair --> thy_strl_resp fg ns G --> \ \ fn_oth G <= Union (set ns) --> ((H, Vs), G, {}) : orkvss^* --> \ \ unif : red_unifs Vs --> \ \ (ALL (a, b) : unif. subst_pr fg a = subst_pr fg b) --> \ \ subst_seq fg ` Vs <= indist" (fn _ => [ Clarsimp_tac 1, (fatac ([sat_unifs_ex_f_equiv', bexI] MRS iffD1) 1 1), (datac bspec 1 1), Clarify_tac 1, (rtac idv_sets_sub_indist 1), Full_simp_tac 1, (etac subset_trans 3), (rtac (Diff_subset RS image_mono) 3), (eatac strl_resp_kc_orkvss_rtc 1 1), Fast_tac 1, (etac xt6 1), (etac fn_orkvss_kc_rtc 1), Fast_tac 1 ]) ;