(** unit contraction rules **) fun dvi_uc_tacs dths = [ (rtac ex_conjI), sdvitac, (eresolve_tac [der_asm, dd1th] THEN_ALL_NEW resolve_tac dths THEN_ALL_NEW resolve_tac singleton_sub_bdiaidps_thms) ] ; fun init_dvi_uc_tacs dths = [ (clarsimp_tac (cesimps rule_defs)), (SELECT_GOAL (EVERY [ (* split up say F delible from (X,Y),Z |- W into cases: F (with stars) is X,Y or Z, or F is delible from X,Y,Z or W *) (REPEAT_SOME (eresolve_tac [seqdel.elim, strdel_CommaR, strdel_StarR, strdel_BlobR] THEN_ALL_NEW Clarsimp_tac)), (* when deletion to substituted variable in rule *) TRYALL (EVERY' (dvi_uc_tacs dths)) ])) ] ; fun xstacs th = [ (rtac ex_conjI 1), (etac dd1th 2), ((rtac th THEN_ALL_NEW resolve_tac singleton_sub_bdiaidps_thms) 2), sdvitac 1 ] ; val uc_ibdista_tacs = [ (EVERY' (init_dvi_uc_tacs [dbidista]) 1), (EVERY (xstacs (dbidista RS duAl))), (EVERY (xstacs (dbidista RS duAr))), (EVERY (xstacs (tn [dcommA RS duAl, dassoc, dbidista RS duAr]))), (EVERY (xstacs (tn [dassoc, dbidista RS duAr]))), (EVERY (xstacs (tn [diassoc, dbidista RS duAl]))), (EVERY (xstacs (tn [dcommA RS duAr, diassoc, dbidista RS duAl]))) ] ; val uc_ibdists_tacs = [ (EVERY' (init_dvi_uc_tacs [dbidists]) 1), (EVERY (xstacs (dbidists RS duSl))), (EVERY (xstacs (dbidists RS duSr))), (EVERY (xstacs (tn [dcommS RS duSl, dassocS, dbidists RS duSr]))), (EVERY (xstacs (tn [dassocS, dbidists RS duSr]))), (EVERY (xstacs (tn [diassocS, dbidists RS duSl]))), (EVERY (xstacs (tn [dcommS RS duSr, diassocS, dbidists RS duSl]))) ] ; val uc_assoc_tacs = [ (EVERY' (init_dvi_uc_tacs [dassoc]) 1), (EVERY (xstacs (tn [dca1, dassoc]))), (EVERY (xstacs (tn [dica2, dassoc]))), (EVERY (xstacs (tn [dassoc, dassoc]))), (EVERY (xstacs (tn [dassoc, dica2, dassoc]))) ] ; val uc_ica1_tacs = [ (EVERY' (init_dvi_uc_tacs [dica1]) 1), (EVERY (xstacs (tn [dics2, dica1]))), (EVERY (xstacs (tn [dcs1, dica1]))), (EVERY (xstacs (tn [dassocS, dica1]))), (EVERY (xstacs (tn [dassocS, dcs1, dica1]))) ] ; val uc_ica2_tacs = [ (EVERY' (init_dvi_uc_tacs [dica2]) 1), (EVERY (xstacs (tn [dca1, dica2]))), (EVERY (xstacs (tn [dica2, dica2]))) ] ; val uc_ics1_tacs = [ (EVERY' (init_dvi_uc_tacs [dics1]) 1), (EVERY (xstacs (tn [dca1, dics1]))), (EVERY (xstacs (tn [dica2, dics1]))), (EVERY (xstacs (tn [diassoc, dca1, dics1]))), (EVERY (xstacs (tn [diassoc, dics1]))) ] ; val uc_ics2_tacs = [ (EVERY' (init_dvi_uc_tacs [dics2]) 1), (EVERY (xstacs (tn [dics2, dics2]))), (EVERY (xstacs (tn [dcs1, dics2]))) ] ; val uc_iblob_tacs = [ (EVERY' (init_dvi_uc_tacs [dblobS]) 1), (EVERY (xstacs (tn [dca1, dblobS]))), (EVERY (xstacs (tn [dica2, dblobS]))) ] ; val uc_ca1_tacs = [ (EVERY' (init_dvi_uc_tacs [dca1]) 1), (EVERY (xstacs (tn [dca1, dca1]))), (EVERY (xstacs (tn [dica2, dca1]))) ] ; val uc_ca2_tacs = [ (EVERY' (init_dvi_uc_tacs [dca2]) 1), (EVERY (xstacs (tn [dics2, dca2]))), (EVERY (xstacs (tn [dcs1, dca2]))), (EVERY (xstacs (tn [dassocS, dca2]))), (EVERY (xstacs (tn [dassocS, dcs1, dca2]))) ] ; val uc_cs1_tacs = [ (EVERY' (init_dvi_uc_tacs [dcs1]) 1), (EVERY (xstacs (tn [dics2, dcs1]))), (EVERY (xstacs (tn [dcs1, dcs1]))) ] ; val uc_cs2_tacs = [ (EVERY' (init_dvi_uc_tacs [dcs2]) 1), (EVERY (xstacs (tn [dca1, dcs2]))), (EVERY (xstacs (tn [dica2, dcs2]))), (EVERY (xstacs (tn [diassoc, dca1, dcs2]))), (EVERY (xstacs (tn [diassoc, dcs2]))) ] ; val uc_rstars_tacs = [ (EVERY' (init_dvi_uc_tacs [drstars]) 1), (EVERY (xstacs (tn [dics2, disxyy]))), (EVERY (xstacs (tn [dcs1, disxyy]))), (EVERY (xstacs (tn [dca1, disxxy]))), (EVERY (xstacs (tn [dica2, disxxy]))) ] ; val uc_rssA_tacs = [ (EVERY' (init_dvi_uc_tacs [drssA]) 1), (EVERY (xstacs (tn [dca1, drssA]))), (EVERY (xstacs (tn [dica2, drssA]))), (EVERY (xstacs (tn [dstarA, dics2, disxyy]))), (EVERY (xstacs (tn [dstarA, dcs1, disxyy]))) ] ; val uc_blob_tacs = [ (EVERY' (init_dvi_uc_tacs [dblobA]) 1), (EVERY (xstacs (tn [dics2, dblobA]))), (EVERY (xstacs (tn [dcs1, dblobA]))) ] ; val uc_del_tacs = [ EVERY (init_del_gen_tacs' bdiaidps_list), EVERY uc_ibdista_tacs, EVERY uc_ibdists_tacs, EVERY uc_assoc_tacs, EVERY uc_ica1_tacs, EVERY uc_ica2_tacs, EVERY uc_ics1_tacs, EVERY uc_ics2_tacs, (EVERY' (init_dvi_uc_tacs [dastars]) 1), (EVERY' (init_dvi_uc_tacs [dassA]) 1), EVERY uc_iblob_tacs, EVERY uc_ca1_tacs, EVERY uc_ca2_tacs, EVERY uc_cs1_tacs, EVERY uc_cs2_tacs, EVERY uc_rstars_tacs, EVERY uc_rssA_tacs, EVERY uc_blob_tacs ] ; (* easier this way around, rather than getting ex_box_uc direct *) val _ = qed_goalw_spec_mp "ex_box_uc'" Uc.thy [derivableR_def] "atom = I --> (C, Cd) : seqdel (stars atom) --> \ \ Cd' : derivableR bdiaidps {Cd} --> \ \ (EX C'. (C', Cd') : seqdel (stars atom) & C' : derivableR bdiaidps {C})" (fn _ => [ EVERY uc_del_tacs ] ) ; val _ = bind_thm ("ex_box_uc", fold_rule [mk_eq inv_der_bdaidps] ex_box_uc') ; val ds = [dca1, dica2, dcs1, dics2] ; val ldi_iltacs = [ (clarsimp_tac (cesimps [edi_def]) 1), (dtac (reop rev ex_box_uc) 1), rtac refl 2, Clarify_tac 2, (etac allE 2), mp_tac 2, (sdvitac 1), (case_tac "C'" 1), (case_tac "seq'" 1), (etac ex_forward 1), (clarsimp_tac (cesimps [interp_def]) 1), (etac seqdel.elim 1), (ALLGOALS (clarsimp_tac (cesimps [derivableR_def]))), (ALLGOALS (EVERY' [rtac conjI, datac delI_der 1, (force_tac (cesimps [ila, ils])), (etac dd1th THEN' etac subsetD THEN' Fast_tac), (dtac vars_strdel_stars), Asm_simp_tac ])) ] ; val _ = qed_goalw_spec_mp "ldi_ils" Uc.thy [ils] "idps <= rules --> {ila, ils} <= rules --> \ \ ldi bdaidps rules (PC (ruleSubst (fs, ss) ils))" (fn _ => ldi_iltacs) ; val _ = qed_goalw_spec_mp "ldi_ila" Uc.thy [ila] "idps <= rules --> {ila, ils} <= rules --> \ \ ldi bdaidps rules (PC (ruleSubst (fs, ss) ila))" (fn _ => ldi_iltacs) ;