fun ufe _ = update_thy "Fextra" ; val disjIs = [disjI1, disjI2] ; val refl_disjIs = [refl] RL disjIs ; val refl_conjIs = [refl RS conjI, refl RSN (2, conjI)] ; val refl_cds = refl_conjIs RL disjIs ; val Comma_inject = hd pstructr.inject ; val refl_Commas = refl_conjIs RL [Comma_inject RS iffD2] ; val _ = qed_goalw_spec_mp "lemma_s14b" Fextra.thy [same_substr_def, spec_substr_def] "((Gt Wn Wp, Gt Wn' Wp) = (W, W')) --> \ \ ((Lt X Y, Lt X' Y'), (Wn, Wn')) : same_substr {Comma} {Comma} --> \ \ (ALL WZ' Z V V'. (WZ' = Comma W' Z | WZ' = Comma Z W') --> \ \ (EX str str' U UZ' UZt UZt'. ($V |- $W, $X |- $Y,, $str) : red & \ \ ($V' |- $WZ', $X' |- $Y',, $str') : red & \ \ ((Gt V UZt, Gt V' UZt'), (str, str')) : same_substr {} {Gt} & \ \ ((U, UZ'), (UZt, UZt')) : same_substr {Comma} {Comma} & \ \ (UZ' = Comma U Z | UZ' = Comma Z U) & \ \ (Wp, UZt) : spec_substr {Comma} {Comma} & \ \ (Wp, UZt') : spec_substr {Comma} {Comma}))" (fn _ => [ (Clarify_tac 1), (dtac ed1_9_10 1), (dtac lemma_s4' 1), Clarify_tac 1, (* first rules applied are rule 4 and rule 9/10 respectively *) (dtac (ed1.s4 RS rede.stt) 1), (datac rede.stt' 1 1), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (REPEAT (ares_tac [rtrancl_refl] 1)), (* NB TRYALL fails *) Simp_tac 1, Simp_tac 1, (Fast_tac 1) ]) ; val th1 = (same_substr_mksym o same_nh_substr_mksym) lemma_sG_neg ; val th2 = read_instantiate [("R", "revpair ` ?R")] th1 ; val lemma_sG_neg_sym = full_simplify (esimps [revpair_has_excl_R RS sym, revpair_Gt_has_R RS sym]) th2 ; val _ = qed_goal_spec_mp "lemma_s14_neg" Fextra.thy "((Gt Wn Wp, Gt Wn' Wp), (W, W')) : \ \ same_nh_substr {Comma} {Comma, Gt} (Gt_has_R (has_excl_R R)) --> \ \ ((Lt X Y, Lt X' Y'), (Wn, Wn')) : same_substr {Comma} {Comma} --> \ \ (ALL WZ' Z V V'. (WZ' = Comma W' Z | WZ' = Comma Z W') --> \ \ (EX str str' VT VT' U UZ' UZt UZt'. ($V |- $W, $X |- $Y,, $str) : red & \ \ ($V' |- $WZ', $X' |- $Y',, $str') : red & \ \ ((Gt VT UZt, Gt VT' UZt'), (str, str')) : same_substr {} {Gt} & \ \ ((V, V'), (VT, VT')) : same_substr {Comma} {Comma} & \ \ ((V, V') ~: has_excl_R R --> (VT, VT') ~: has_excl_R R) & \ \ (V ~: unpairs (has_excl_R R) --> VT ~: unpairs (has_excl_R R)) & \ \ (V' ~: unpairs (has_excl_R R) --> VT' ~: unpairs (has_excl_R R)) & \ \ ((U, UZ'), (UZt, UZt')) : same_substr {Comma} {Comma} & \ \ (UZ' = Comma U Z | UZ' = Comma Z U) & \ \ (Wp, UZt) : spec_substr {Comma} {Comma} & \ \ (Wp, UZt') : spec_substr {Comma} {Comma}))" (fn _ => [ (Clarify_tac 1), (datac lemma_sG_neg_sym 1 1), Clarify_tac 1, (chop_last (etac disjE 1)), ALLGOALS Clarify_tac, (* second case of lemma_sG *) (datac ([refl, asm_rl, disj_commute'] MRS lemma_s14b) 1 2), Clarify_tac 2, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 2), (eatac rede.rtt' 1 2), (eatac rede.rtt' 1 2), atac 2, (REPEAT (atac 2)), nosg_tac 2, (* first case of lemma_sG *) (etac oaE 1), (dtac ed1_9_10 1), (dtac ed1_9_10 1), (datac tct.rst 1 1), (datac tct.rst 1 1), (dtac lemma_s4 1), Clarify_tac 1, (datac rede.ttt' 1 1), (datac rede.ttt' 1 1), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), atac 3, (TRYALL eq_assume_tac), (etac disj_commute' 2), rewtac spec_substr_def, rewtac same_substr_def, (etac tct.rsr 1), TRYALL Fast_tac ]) ; val _ = bind_thm ("lemma_s14_ne", mk_ne lemma_s14_neg) ; val _ = bind_thm ("lemma_s14", mk_std lemma_s14_neg) ; val _ = qed_goal_spec_mp "lemma_Yex" Fextra.thy "YU = Comma U Y | YU = Comma Y U --> \ \ ((YU, U'), Z, Z') : same_ipsubstr {Comma} {Comma} --> \ \ (EX X XY R R'. ($V |- $Z, $V |- $R) : ed1 & \ \ ($V' |- $Z', $V' |- $R') : Id & \ \ (XY = Comma X Y | XY = Comma Y X) & \ \ (R = Comma U XY & R' = Comma U' X | \ \ R = Comma XY U & R' = Comma X U'))" (fn _ => [ (safe_tac (ces same_ipsubstr.elims)), (REPEAT_FIRST (resolve_tac [exI, conjI, IdI])), (TRYALL (EVERY' [resolve_tac refl_cds, match_tac refl_Commas, rtac refl])), (REPEAT (resolve_tac ed1.intrs 1 THEN Fast_tac 1)) ]) ; val _ = qed_goal_spec_mp "lemma_sE_neg" Fextra.thy "((Gt XT YUt, Gt XT' YUt'), (W, W')) : \ \ same_nh_substr {Comma} {Comma, Gt} (Gt_has_R (has_excl_R R)) --> \ \ ((YU, U'), (YUt, YUt')) : \ \ same_nh_substr {Comma} {Comma,Gt} (Gt_has_R (has_excl_R R)) --> \ \ (YU = Comma U Y | YU = Comma Y U) --> \ \ ((Gt Ua Up, Gt Ua' Up'), (U, U')) : \ \ same_nh_substr {Comma} {Comma,Gt} (Gt_has_R (has_excl_R R)) --> \ \ ((V, V) ~: has_excl_R R) --> \ \ (EX Vt Vt' Q Q' YS S. \ \ ($V |- $W, $Ua |- $Vt >> ($Up,, $Q)) : ed1^+ & \ \ ((XT, XT'), (Vt, Vt')) : same_substr {Comma} {Comma} & \ \ ((XT, XT') ~: has_excl_R R --> (Vt, Vt') ~: has_excl_R R) & \ \ (($V |- $W', $Ua' |- $Vt' >> ($Up',, $Q')) : ed1^+ & \ \ (YS = Comma Y S | YS = Comma S Y) & \ \ ((YS, S), (Q, Q')) : same_substr {Comma} {Comma} | \ \ ($V |- $W', $Ua' |- $Vt' >> $Up') : ed1^+ & Q = Y) & \ \ (XT ~: unpairs (has_excl_R R) --> Vt ~: unpairs (has_excl_R R)) & \ \ (XT' ~: unpairs (has_excl_R R) --> Vt' ~: unpairs (has_excl_R R)))" (fn _ => [ Clarify_tac 1, (dtac lemma_s6p_neg 1), (REPEAT (eresolve_tac [exE, conjE, make_elim sed1_3_11_12] 1)), (datac tct.rst 1 1), (datac tct.rst 1 1), (dtac ss_nhR_ip_eq 1), (etac (mk_mono' Un_mono) 1), (rtac same_ipsubstr_mono 1), ALLGOALS Clarify_tac, (chop_last (dtac lemma_s6p_neg 1)), Clarify_tac 1, (datac tct.trt 1 1), (datac tct.trt 1 1), (* cases of ((YU, U'), ZAa, ZA'a) : (same_ipsubstr {Comma} {Comma})^= *) (chop_last (etac UnE 1)), (* first case, non-reflexive case *) (datac lemma_Yex 1 1), Clarify_tac 1, (datac tct.tst 1 1), (datac lemma_s5p_neg 1 1), Clarify_tac 1, (datac tct.trt 1 1), (datac tct.trt 1 1), (chop_last (etac oaE 1)), (dtac ed1_9_10 1), (dtac ed1_9_10 1), (datac tct.tst 1 1), (datac tct.tst 1 1), (* level 26 *) (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (rtac disjI1 4), (REPEAT_ALL_NEW (resolve_tac [conjI]) 4), (TRYALL (etac mem_tc_asm_rl)), TRYALL eq_assume_tac, (dtac same_substr_eq1 1), Clarify_tac 1, (etac sms.rrr' 1), (etac sms.srr' 1), try_same_ipsubstr_tac 1, (clarify_tac (cds [Comma_has_excl_R_D]) 1), etac disj_commute' 1, eq_assume_tac 1, (* level 39 *) (clarify_tac (cds [Comma_up_has_excl_R_D, not_unpairsD]) 1) , (clarify_tac (cds [Comma_up_has_excl_R_D, not_unpairsD]) 1) , (* second case, reflexive case *) Clarify_tac 1, (datac lemma_sG_neg 1 1), Clarify_tac 1, (datac tct.trt 1 1), (datac tct.trt 1 1), (chop_last (etac disjE 1)), (* sg 2 is special case of sg 1 where Yt, Yt' are just Y and nothing *) Clarify_tac 2, (datac (ed1_9_10' RS tct.tst') 1 2), (dtac (ed1.s4 RS tct.tst') 2), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 2), atac 2, (rtac disjI2 4), (REPEAT_ALL_NEW (resolve_tac [exI, conjI, refl]) 4), atac 4, (clarify_tac (cds [Comma_has_excl_R_D]) 3), (etac sms.rrr' 2), (etac sms.srr' 2), (dtac same_substr_eq1 2), Fast_tac 2, (* level 60 *) (clarify_tac (cds [Comma_up_has_excl_R_D, not_unpairsD]) 2) , (clarify_tac (cds [Comma_up_has_excl_R_D, not_unpairsD]) 2) , (* regular case of Yt, Yt' *) Clarify_tac 1, (etac oaE 1), (dtac ed1_9_10 1), (dtac ed1_9_10 1), (datac tct.tst 1 1), (datac tct.tst 1 1), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (rtac disjI1 4), (REPEAT_ALL_NEW (resolve_tac [conjI]) 4), (TRYALL (etac mem_tc_asm_rl)), TRYALL eq_assume_tac, (etac sms.rrr' 1), (etac sms.srr' 1), (dtac same_substr_eq1 1), Fast_tac 1, atac 2, (clarify_tac (cds [Comma_has_excl_R_D]) 1), (ALLGOALS (clarify_tac (cds [Comma_up_has_excl_R_D, not_unpairsD]))) ]) ; val _ = bind_thm ("lemma_sE_ne", mk_ne lemma_sE_neg) ; val _ = bind_thm ("lemma_sE", mk_std lemma_sE_neg) ; val _ = qed_goalw_spec_mp "seq_exclns_ne" Fextra.thy [mk_eq seq_exclns_def] "seq_exclns ($V |- $W) ~= [] --> seq_LtGtOK ($V |- $W) --> \ \ (V, V) : has_excl | \ \ (EX Ws. (Ws, W) : spec_substr {Comma} {Comma, Gt} & \ \ (Ws, Ws) : Gt_has_excl)" (fn _ => [ Clarsimp_tac 1, Safe_tac, (* exclusion in antecedent *) (REPEAT (etac rev_mp 1)), (induct_tac "V" 1), Force_tac 2, (* sg 2 - structure is Gt - impossible *) Fast_tac 3, Fast_tac 3, Fast_tac 3, (clarsimp_tac (cesimps [has_excl_def, same_substr_def]) 2), (REPEAT (etac thin_rl 2)), Fast_tac 2, (* sg 1 - structure is Comma - use induction *) (clarsimp_tac (cesimps [str_exclns_Comma]) 1), (chop_last (etac impCE 1)), (TRYALL (rtac Comma_has_exclI THEN' Asm_full_simp_tac)), (* exclusion in succedent *) rewrite_goals_tac [str_exclns_def, mk_eq (set_empty RS sym), mk_eq set_filter], (Clarsimp_tac 1), (datac Lt_substr_Gt 1 1), Fast_tac 1 ]) ; val [lem_15_prop_def] = map (rewrite_rule [lfp_const]) lem_15_prop.defs ; val elitacs = [ REPEAT1 o (etac disjE THEN' Fast_tac), etac swap THEN' (REPEAT1 o etac ex_forward), REPEAT_ALL_NEW (eresolve_tac [disj_forward, conj_forward, asm_rl, tct.rsr] ORELSE' try_spec_ipsubstr_tac) ] ; val _ = qed_goalw_spec_mp "excl_loc_lem_sx1_neg" Fextra.thy [same_substr_def, same_psubstr_def, same_nh_substr_def] "pfs R --> ((A, A'), (W, W')) : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B), (W, W)) : same_nh_substr {Comma} {Comma, Gt} R --> \ \ (EX B'. ((A, A'), (B, B')) : same_psubstr {Comma} {Comma, Gt} & \ \ ((B, B'), (W, W')) : same_nh_substr {Comma} {Comma, Gt} R) | \ \ ((B, B), (A, A)) : same_nh_substr {Comma} {Comma, Gt} R & \ \ ((A, A'), (W, W')) : same_nh_substr {Comma} {Comma, Gt} R | \ \ (EX P P' Q. (((Comma P Q, Comma P' Q), (W, W')) : \ \ same_nh_substr {Comma} {Comma, Gt} R | \ \ ((Comma Q P, Comma Q P'), (W, W')) : \ \ same_nh_substr {Comma} {Comma, Gt} R) & \ \ ((A, A'), (P, P')) : same_substr {Comma} {Comma, Gt} & \ \ ((B, B), (Q, Q)) : same_nh_substr {Comma} {Comma, Gt} R)" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac pairs_rtrancl_induct 1), (* case W = A *) (rtac impI 1), (etac higher_not_rel.elim 1), Force_tac 1, (datac higher_not_rel.ext 2 1), Force_tac 1, (* inductive case, A is proper substr of W *) (rtac impI 1), (etac higher_not_rel.elim 1), (clarify_tac csp 1), Asm_full_simp_tac 1, (* case B = W *) (rtac disjI1 1), rtac exI 1, rtac conjI 1, rtac higher_not_rel.same 2, (eatac tct.rst 1 1), (* case B is proper substr of W *) (split_all_tac 1), (clarify_tac csp 1), (case_tac "a = ac" 1), (* immediate substrs of W are ac and a *) (chop_last (ftac (hnr_rtrancl RS subsetD RS same_ipsubstr_rtc_eq1) 1)), hyp_subst_tac 1, mp_tac 1, (REPEAT_FIRST (ematch_tac [disj_forward, ex_forward, conj_forward, asm_rl])), (TRYALL (EVERY' [(eatac higher_not_rel.ext 1), etac contrapos_nn, (eatac pfsD 1) ] )), nosg_tac 2, (* level 25 *) (* case y ~= ya, W must be y, ya or vv *) (rtac disjI2 1), (rtac disjI2 1), (thin_tac "?P --> ?Q" 1), ((etac same_ipsubstr.elim THEN_ALL_NEW Clarify_tac) 1), (ALLGOALS (etac same_ipsubstr.elim)), ALLGOALS Clarify_tac, (REPEAT_FIRST (ares_tac [exI, conjI])), (TRYALL (resolve_tac ([higher_not_rel.same] RL disjIs))) ]) ; val _ = bind_thm ("excl_loc_lem_sx1", mk_std excl_loc_lem_sx1_neg) ; val _ = qed_goalw_spec_mp "excl_loc_lem_si1" Fextra.thy [same_substr_def] "((A, A'), (W, W')) : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B'), (W, W')) : same_substr {Comma} {Comma, Gt} --> \ \ ((A, A'), (B, B')) : same_substr {Comma} {Comma, Gt} | \ \ ((B, B'), (A, A')) : same_substr {Comma} {Comma, Gt} | W = W'" (fn _ => [ (rtac impI 1), (etac pairs_rtrancl_induct 1), (* case W = A *) (rtac impI 1), (etac rtranclE 1), Force_tac 1, (datac tct.rsr 1 1), Force_tac 1, (* inductive case, A is proper substr of W *) (rtac impI 1), (chop_last (etac rtranclE 1)), Asm_full_simp_tac 1, (* case B = W *) (datac tct.rsr 1 1), Force_tac 1, (* case B is proper substr of W *) (split_all_tac 1), (case_tac "(a, b) = (ab, bb)" 1), (* immediate substrs of W are ab and a *) Clarsimp_tac 1, (dtac same_ipsubstr_eq1 1), contr_tac 1, (* case y ~= ya, W must be y, ya or vv *) Clarify_tac 1, (ALLGOALS (etac same_ipsubstr.elim)), (ALLGOALS Clarify_tac), (ALLGOALS (etac same_ipsubstr.elim)), (ALLGOALS Clarsimp_tac) ]) ; (* shouldn't need this - use excl_loc_lem_si1 and then excl_loc_lem1 *) val _ = qed_goalw_spec_mp "excl_loc_lem_s1" Fextra.thy [same_substr_def] "((A, A'), (W, W')) : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B'), (W, W')) : same_substr {Comma} {Comma, Gt} --> \ \ ((A, A'), (B, B')) : same_substr {Comma} {Comma, Gt} | \ \ ((B, B'), (A, A')) : same_substr {Comma} {Comma, Gt} | \ \ (EX P P' Q Q'. (((Comma P Q, Comma P' Q'), (W, W')) : \ \ same_substr {Comma} {Comma, Gt} | \ \ ((Comma Q P, Comma Q' P'), (W, W')) : \ \ same_substr {Comma} {Comma, Gt}) & \ \ ((A, A'), (P, P')) : same_substr {Comma} {Comma, Gt} & \ \ ((B, B'), (Q, Q')) : same_substr {Comma} {Comma, Gt})" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), (* case W = A *) (rtac impI 1), (etac rtranclE 1), Force_tac 1, (datac tct.rsr 1 1), Force_tac 1, (* inductive case, A is proper substr of W *) (rtac impI 1), (chop_last (etac rtranclE 1)), hyp_subst_tac 1, (* case B = W *) (datac tct.rsr 1 1), Force_tac 1, (* case B is proper substr of W *) (case_tac "y = ya" 1), (* immediate substrs of W are y and ya *) Clarify_tac 1, ((etac disjE THEN_ALL_NEW ((chop_last o datac tct.rsr 1) THEN' Fast_tac)) 1), (* case y ~= ya, W must be y, ya or vv *) ((etac same_ipsubstr.elim THEN_ALL_NEW Clarify_tac) 1), (ALLGOALS (etac same_ipsubstr.elim THEN_ALL_NEW Fast_tac)) ]) ; val _ = qed_goalw_spec_mp "excl_loc_lem_sd1" Fextra.thy [same_substr_def] "((A, A), (W, W)) : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B), (W, W)) : same_substr {Comma} {Comma, Gt} --> \ \ ((A, A), (B, B)) : same_substr {Comma} {Comma, Gt} | \ \ ((B, B), (A, A)) : same_substr {Comma} {Comma, Gt} | \ \ (EX P P Q Q. (((Comma P Q, Comma P Q), (W, W)) : \ \ same_substr {Comma} {Comma, Gt} | \ \ ((Comma Q P, Comma Q P), (W, W)) : \ \ same_substr {Comma} {Comma, Gt}) & \ \ ((A, A), (P, P)) : same_substr {Comma} {Comma, Gt} & \ \ ((B, B), (Q, Q)) : same_substr {Comma} {Comma, Gt})" (fn _ => [ (rtac impI 1), (etac rtrancl_induct 1), (* case W = A *) (rtac impI 1), (etac rtranclE 1), Force_tac 1, (datac tct.rsr 1 1), Force_tac 1, (* inductive case, A is proper substr of W *) (rtac impI 1), (chop_last (etac rtranclE 1)), hyp_subst_tac 1, (* case B = W *) (datac tct.rsr 1 1), Force_tac 1, (* case B is proper substr of W *) (case_tac "y = ya" 1), (* immediate substrs of W are y and ya *) Clarify_tac 1, ((etac disjE THEN_ALL_NEW ((chop_last o datac tct.rsr 1) THEN' Fast_tac)) 1), (* case y ~= ya, W must be y, ya or vv *) ((etac same_ipsubstr.elim THEN_ALL_NEW Clarify_tac) 1), (ALLGOALS (etac same_ipsubstr.elim THEN_ALL_NEW Fast_tac)) ]) ; (* excl_loc_lem1 : version involving spec_substr *) val excl_loc_lem1 = full_simplify (esimps []) excl_loc_lem_sd1 ; val excl_loc_lem_x1 = full_simplify (esimps []) excl_loc_lem_sx1 ; val excl_loc_lem_x1_neg = full_simplify (esimps []) excl_loc_lem_sx1_neg ; (* uses the spec_substr version of excl_loc_lem1 (* try not to use this one, just excl_loc_lem1 instead *) val _ = qed_goal_spec_mp "excl_loc_lem2" Fextra.thy "(Gt XT YUt, W) : spec_substr {Comma} {Comma, Gt} --> \ \ (Gt Wn Wp, W) : spec_substr {Comma} {Comma, Gt} --> \ \ Gt XT YUt = Gt Wn Wp | \ \ (Gt Wn Wp, YUt) : spec_substr {Comma} {Comma, Gt} | \ \ (Gt XT YUt, Wp) : spec_substr {Comma} {Comma, Gt} | \ \ (EX P Q. ((Comma P Q, W) : spec_substr {Comma} {Comma, Gt} | \ \ (Comma Q P, W) : spec_substr {Comma} {Comma, Gt}) & \ \ (Gt XT YUt, P) : spec_substr {Comma} {Comma, Gt} & \ \ (Gt Wn Wp, Q) : spec_substr {Comma} {Comma, Gt})" (fn _ => [ (REPEAT (rtac impI 1)), (datac excl_loc_lem1 1 1), (etac thin_rl 1), (REPEAT_FIRST (etac disjE)), Asm_simp_tac 3, rewtac spec_substr_def, (ALLGOALS (EVERY' [etac rtranclE, Asm_simp_tac, etac spec_ipsubstr.elim THEN_ALL_NEW Clarify_tac])) ]) ; *) val excl_loc_lem1' = (tacthm (etac disjE 3 THEN Safe_tac) (excl_loc_lem1 RS revcut_rl)) ; val excl_loc_lem_x1' = (zero_var_indexes o same_substr_mksym) (tacthm (etac disjE 4 THEN Safe_tac) (excl_loc_lem_x1 RS revcut_rl)) ; val excl_loc_lem_x1_neg' = (zero_var_indexes o same_substr_mksym o same_psubstr_mksym) (tacthm (etac disjE 4 THEN Safe_tac) (excl_loc_lem_x1_neg RS revcut_rl)) ; (* the following lemmas may not be needed, they were part of exploring how to prove what was needed for lemma_15_rec_suc *) val _ = qed_goal_spec_mp "Comma_same" Fextra.thy "((Comma Q' P', Comma Q P), W, W') : same_substr {Comma} {Comma, Gt} --> \ \ ((P', P), W, W') : same_substr {Comma} {Comma, Gt} --> P' = P | Q' = Q" (fn _ => [ (Clarify_tac 1), (datac excl_loc_lem_si1 1 1), Safe_tac, (dtac (same_spec_substr RS spec_substr_size) 1 THEN Force_tac 1), (etac thin_rl 1), (SELECT_GOAL (rewtac same_substr_def) 1), (etac rtranclE 1), Fast_tac 1, (etac same_ipsubstr.elim 1), Safe_tac, (etac same_substr_eq2 1) ]) ; val _ = qed_goal_spec_mp "Comma_has_substr" Fextra.thy "((Comma Q' P', Comma Q P), W, W') : same_substr {Comma} {Comma, Gt} --> \ \ ((A, A'), W, W') : same_substr {Comma} {Comma, Gt} --> \ \ ((A, A'), P', P) : same_substr {Comma} {Comma, Gt} --> P' = P | Q' = Q" (fn _ => [ (Clarify_tac 1), (datac excl_loc_lem_si1 1 1), Safe_tac, (etac thin_rl 1), (rewtac same_substr_def), (datac tct.rrr' 1 1), (dtac (same_spec_ipsubstr_rtc RS spec_ipsubstr_rtc_size) 1 THEN Force_tac 1), (chop_last (etac rtranclE 1)), Clarify_tac 1, (REPEAT (dtac (same_spec_ipsubstr_rtc RS spec_ipsubstr_rtc_size) 1)), Force_tac 1, (fast_tac (ces same_ipsubstr.elims) 1), (dtac same_ipsubstr_rtc_eq2 1), Clarify_tac 1, (etac same_ipsubstr_rtc_eq1 1) ]) ; val _ = qed_goal_spec_mp "same_substr_twice" Fextra.thy "((Comma Q P, Comma Q' P'), W, W') : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B'), W, W') : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B'), P, P') : same_substr {Comma} {Comma, Gt} --> \ \ ((B, B'), Q, Q') : same_substr {Comma} {Comma, Gt} --> B = B'" (fn _ => [ Clarify_tac 1, (datac Comma_has_substr 2 1), Safe_tac, (TRYALL (etac same_substr_eq2)) ]); (* case exclusion in antecedent *) val _ = qed_goal_spec_mp "lemma_15_rec_ant" Fextra.thy "(W, W') : lem_15_prop X X' Y --> (V, V) : has_excl --> (EX Vd Wd Wd'. \ \ ($V |- $W, $Vd |- $Wd) : red & ($V |- $W', $Vd |- $Wd') : red & \ \ (Wd, Wd') : lem_15_prop X X' Y)" (fn _ => [ (Clarify_tac 1), (etac has_excl.elim 1), Clarify_tac 1, (ftac same_substr_eq2 1), (dtac lemma_s4 1), Clarify_tac 1, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), atac 1, atac 1, (clarsimp_tac (cesimps [lem_15_prop_def]) 1), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), atac 3, atac 2, atac 2, atac 2, (SELECT_GOAL (rewtac same_substr_def) 1), (etac tct.rrr 1), (rtac tct.rsr 1), try_same_ipsubstr_tac 2, simrtctac 1, TRYALL atac ]) ; (* now to prove lemma 15 - try the recurrent part *) (* case exclusion in succedent *) (* because excl_loc_lem_x1_neg' got pairs reversed for same_substr but not for same_nh_substr *) val ellx1 = (Gt_has_excl_pfs RS excl_loc_lem_x1_neg') ; val ellx1_sym = tacthm (TRYALL (dtac (Gt_has_excl_sym RS same_nh_substr_sym))) ellx1 ; val remove_nhs = [spec_nh_substr_le RS subsetD, same_nh_substr_le RS subsetD] ; val l15Htacs = [ (REPEAT o dresolve_tac remove_nhs), (dtac lemma_sH THEN' Fast_tac), atac, (etac unpairsD), (REPEAT o eresolve_tac [exE, conjE]), (REPEAT_ALL_NEW (UNIQUE o ares_tac [exI, conjI])), (SELECT_GOAL (rewtac same_substr_def)), (etac tct.rrr THEN' eresolve_tac [asm_rl]) ] ; val thin_nh = same_nh_substr_le RS subsetD RSN (2, thin_same RS thin_rl) ; val sBxtacs = [ (datac lemma_sB_ne 1), Fast_tac, (etac (spec_same_nh_substr RS iffD2)), (etac Gt_has_excl.I), Clarify_tac o incr, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) o incr), atac o incr, atac o incr, (ematch_tac [forgetD]), atac, (chop_last o dtac same_substr_mono'), (eatac sms.rrr 1 o incr o incr), Fast_tac, Fast_tac, atac, (eatac sms.rrr 1), (fn _ => TRYALL eq_assume_tac), nosg_tac ] ; val _ = qed_goal_spec_mp "lemma_15_rec_suc" Fextra.thy "(W, W') : lem_15_prop X X' Y --> (Ws', Ws') : Gt_has_excl --> \ \ (Ws', W') : spec_substr {Comma} {Comma, Gt} --> \ \ forget ((V, V) ~: has_excl) --> \ \ (EX Vd Wd Wd'. \ \ ($V |- $W, $Vd |- $Wd) : red & ($V |- $W', $Vd |- $Wd') : red & \ \ (Wd, Wd') : lem_15_prop X X' Y)" (fn _ => [ Clarify_tac 1, (* get Ws as highest Gt_has_excl *) (rewtac spec_substr_def), (dtac ex_gfr 1), (etac unpairs.I 1), (clarsimp_tac (cesimps [gfr_def]) 1), (fold_goals_tac [spec_substr_def, spec_nh_substr_def]), (clarsimp_tac (cesimps [lem_15_prop_def]) 1), (etac thin_rl 1), (eatac (mk_dupE ellx1_sym) 1 1), (* level 9 *) (EVERY' l15Htacs 4), (EVERY' l15Htacs 3), (* note, for the remaining two subgoals we know that t = Gt XT' YUt' is not possible since XT and XT' does not have an exclusion *) ((REPEAT o dresolve_tac remove_nhs) 1), (SELECT_GOAL (rewrite_goals_tac [same_substr_def, same_psubstr_def]) 1), (etac (tacthm Safe_tac (converse_tranclD RS exE)) 1), (* case (B', t) ~= (Gt XT YUt, Gt XT' YUt') *) ((etac same_ipsubstr.elim THEN_ALL_NEW Clarify_tac) 1), (TRYALL (etac unpairs_Gt_has_exclE THEN' Clarify_tac)), nosg_tac 3, (etac has_excl.elim 1), fold_goals_tac [same_substr_def], Clarify_tac 1, (ftac same_substr_eq2 1), (datac lemma_sA 1 1), Clarify_tac 1, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), atac 1, atac 1, (TRYALL (UNIQUE o atac)), nosg_tac 3, (SELECT_GOAL (rewtac same_substr_def) 1), (rtac tct.rsr 1), try_same_ipsubstr_tac 2, (eatac tct.rrr 1 1), (* level 32 *) (* now the remaining cases, where the exclusion to be deleted appears below YUt and YUt' *) (etac (spec_nh_substr_Gt RS disjE) 1), (fast_tac (cis [unpairs.I]) 1), (eatac (mk_dupE ellx1_sym) 1 1), (* level 35 *) (EVERY' sBxtacs 4), (EVERY' sBxtacs 3), (ftac Gt_same_psubstr2 1), Clarify_tac 1, (datac lemma_sC_ne 1 1), TRYALL eq_assume_tac, Clarify_tac 2, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 2), atac 2, atac 2, (ematch_tac [forgetD] 1), atac 1, atac 2, TRYALL eq_assume_tac, (eatac sms.rrr 1 2), (dtac Gt_Gt_same_psubstr 1), (etac UnE 1), (etac sms.rsr 1 THEN etac same_ipsubstr_mono' 1), Fast_tac 1, Fast_tac 1, Fast_tac 1, (* level 56 *) (REPEAT (eatac thin_nh 1 1)), (* remove redundant premises *) (datac lemma_sE_ne 2 1), (etac (spec_same_nh_substr RS iffD2) 1), (etac forgetD 1), Clarify_tac 1, (((chop_last o etac disjE) THEN_ALL_NEW Clarify_tac) 1), (* now try using lemma_15_rec_ant *) (ftac (thin_rl RS lemma_15_rec_ant) 2), (clarsimp_tac (cesimps [lem_15_prop_def]) 4), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 4), (eatac rede.ttt' 1 4), (eatac rede.ttt' 1 4), (TRYALL (UNIQUE o atac)), (TRYALL (UNIQUE o atac)), (TRYALL (UNIQUE o atac)), nosg_tac 3, (simp_tac (esimps [lem_15_prop_def]) 2), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 2), (rtac sms.refl 2), (rtac sms.refl 2), Fast_tac 2, (eatac sms.rrr 1 2), TRYALL atac, nosg_tac 2, (ftac (thin_rl RS lemma_15_rec_ant) 1), (clarsimp_tac (cesimps [lem_15_prop_def]) 3), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 3), (eatac rede.ttt' 1 3), (eatac rede.ttt' 1 3), (TRYALL (UNIQUE o atac)), (TRYALL (UNIQUE o atac)), (TRYALL (UNIQUE o atac)), nosg_tac 2, (simp_tac (esimps [lem_15_prop_def]) 1), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (rtac sms.refl 1), (rtac sms.rsr 1), try_same_ipsubstr_tac 2, ((etac same_substr_mono' THEN_ALL_NEW Fast_tac) 1), (etac disj_commute' 1), TRYALL eq_assume_tac, (eatac sms.rrr 1 1) ]) ; val _ = qed_goal_spec_mp "lemma_15_rec" Fextra.thy "(W, W') : lem_15_prop X X' Y --> seq_LtGtOK ($V |- $W') --> \ \ seq_exclns ($V |- $W') ~= [] --> \ \ (EX Wd Wd' Vd. \ \ ($V |- $W, $Vd |- $Wd) : red & ($V |- $W', $Vd |- $Wd') : red & \ \ (Wd, Wd') : lem_15_prop X X' Y)" (fn _ => [ (Clarify_tac 1), (datac seq_exclns_ne 1 1), (case_tac "(V, V) : has_excl" 1), (datac lemma_15_rec_ant 1 1), (ALLGOALS (clarsimp_tac HOL_css)), (REPEAT_ALL_NEW (ares_tac [exI, conjI, r_into_rtrancl]) 1), (datac lemma_15_rec_suc 2 1), (etac forgetI 1), Clarify_tac 1, (REPEAT_ALL_NEW (ares_tac [exI, conjI, r_into_rtrancl]) 1) ]) ; val _ = qed_goal_spec_mp "lemma_15" Fextra.thy "(ALL W W' V. seq = ($V |- $W') --> \ \ (W, W') : lem_15_prop X X' Y --> seq_LtGtOK ($V |- $W') --> \ \ (EX Wd Wd' Vd. \ \ ($V |- $W, $Vd |- $Wd) : red^* & ($V |- $W', $Vd |- $Wd') : red^* & \ \ (Wd, Wd') : lem_15_prop X X' Y & seq_exclns ($Vd |- $Wd') = []))" (fn _ => [ (res_inst_tac [("a", "seq")] (wf_red RS wf_induct) 1) , Clarify_tac 1, (case_tac "seq_exclns ($V |- $W') = []" 1), (REPEAT_ALL_NEW (ares_tac [exI, conjI, rtrancl_refl]) 1), (datac lemma_15_rec 2 1), Clarify_tac 1, (etac allE 1), (etac impE 1), (force_tac (cesimps [C_def]) 1) , (REPEAT (etac allE 1)), (etac impE 1), (rtac refl 1), mp_tac 1, (etac impE 1), (eatac (red_pres_LtGtOK RS iffD1) 1 1), Clarify_tac 1, (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (eatac tct.srr 1 1), (eatac tct.srr 1 1), TRYALL atac ]);