(* similar to Ldi_rules.ML *) (** equivalence of the set of rules for which (c)ldi is proved **) val ssdmon = (singleton_subsetI RSN (2, mk_mono' strdel_mono)) ; val srmon = (singleton_subsetI RSN (2, mk_mono' strrepI_mono)) ; val ssrmon = (UNIV_I RS imageI RS singleton_subsetI RSN (2, mk_mono' strrepI_mono)) ; (* val _ = qed_goalw_spec_mp "sda_ldi_add" Ldi_add.thy [stars_I_atoms_def] "(Y, X) : (strdel stars_I_atoms) --> ([$X |- $Z], $Y |- $Z) : derl ldi_add" (fn _ => [ Clarify_tac 1, (dtac (strdel_UN RS equalityD1') 1), Safe_tac, (rtac drl.singleI 1), (rtac ldi_add.wkI 1), (rtac seqdel.A 1), (eatac ssdmon 1 1), (ALLGOALS (datac (ssdmon RS del_repI) 1)), Safe_tac, (ALLGOALS (rtac cdthm)), (ALLGOALS (rtac drl.singleI)), (rtac ldi_add.rep_atom 1), (rtac ldi_add.wkI 2), (rtac (strrepI.same RSN (2, seqrepI.I)) 1), (eatac srmon 1 1), (etac seqdel.A 1) ]) ; val _ = qed_goal_spec_mp "sda_rtc_ldi_add" Ldi_add.thy "(Y, X) : (strdel stars_I_atoms)^* --> \ \ ([$X |- $Z], $Y |- $Z) : derl ldi_add" (fn _ => [ strip_tac 1, (etac rtrancl_induct 1), (rtac drl.asmI 1), (etac cdthm 1), (etac sda_ldi_add 1) ]) ; val _ = qed_goal "some_ldi_add" Ldi_add.thy "PC ` rulefs \ \ ({cA, ila, ils, idf} Un lil_adds Un lir_adds Un aidps) <= ldi_add" (fn _ => [ (clarsimp_tac (cesimps [rulefs_insert, rulefs_Un2]) 1), rewtac rulefs_1_def, Safe_tac, (TRYALL (eresolve_tac ldi_add.intrs)) ]) ; val srtacs = [ Clarsimp_tac 1, (dresolve_tac [seqwk_der', seqrepI_der] 1), (eatac dd1th 1 3), (rtac aidps_rlscf 1), (force_tac (cesimps [rlscf, bsrus]) 1) ] ; val dcdrth = reop rev (rewrite_rule [mk_eq drs.all, subset_def] derl_derrec_trans) ; val atacs = [(etac (reop rev drs.derI'')), Clarsimp_tac, (rtac ldi_add.aidps), (etac rulefs_mono), (force_tac (cesimps [aidps]))] ; (* NOT TRUE - ldi_add not closed under substitution but gives proof of rulefs-closure for other clauses of ldi_add val _ = qed_goal "ldi_rulefs" Ldi_add.thy "ldi_add <= PC ` rulefs ((%(x, y). Rule x y) ` ldi_add)" *) (* at this point we start using the axiom all_seq_Log *) val mra_ldi_add_sr = [mk_mono mra_ldi_add RS image_mono, image_Rule_PC] MRS xt4 ; val [ptrands, ptrora] = map (tacthm (REPEAT_FIRST (rtac conjI)) o rewrite_rule [rulefs_1_def] o full_simplify (esimps [rulefs_insert])) [trands, trora] ; val [ldands, ldora] = map (simplify (esimps [image_PC_Rule, derl_deriv_eq])) ([mra_ldi_add_sr] RLN (2, [ptrands, ptrora])) ; *) val rtacs = [ (etac (reop rev drs.derI'')), (Clarsimp_tac), (rtac imageI), (rtac rulefs.iisubI ORELSE' etac rulefs_mono) ] ; val r1tacs = [ EVERY' rtacs 1, (force_tac (cesimps [rlscf_nw]) 1) ] ; val la_alt = rewrite_rule [rulefs_1_def] (full_simplify (esimps [aidps_di, rulefs_Un2, rulefs_insert]) ldi_add.aidps) ; val la_alts = Seq.list_of (REPEAT (resolve_tac [disjI1, disjI2] 1) la_alt) ; val la_alt_l = rewrite_rule [rulefs_1_def] (full_simplify (esimps [lil_nbs, rulefs_insert]) ldi_add.lil_nbs) ; val la_alt_ls = Seq.list_of (REPEAT (resolve_tac [disjI1, disjI2] 1) la_alt_l) ; val la_alt_r = rewrite_rule [rulefs_1_def] (full_simplify (esimps [lir_nbs, rulefs_insert]) ldi_add.lir_nbs) ; val la_alt_rs = Seq.list_of (REPEAT (resolve_tac [disjI1, disjI2] 1) la_alt_r) ; val _ = qed_goalw_spec_mp "ldi_add_equiv" Ldi_add.thy [derivableR_def] "(c : derrec ldi_add {}) = (c : derivableR rlscf_nw {})" (fn _ => [ rtac iffI 1, (ALLGOALS (etac drs.inductr THEN' Fast_tac)), (etac ldi_add.elim 1), (* aidps *) (EVERY' rtacs 1), (rtac aidps_rlscf_nw 1), (* ilrules *) (EVERY' rtacs 1), (rtac ilrules_rlscf_nw 1), (EVERY r1tacs), (EVERY r1tacs), (* lil_nbs, lir_nbs *) (EVERY' rtacs 1), (force_tac (cesimps [rlscf_nw, lils]) 1), (EVERY' rtacs 1), (force_tac (cesimps [rlscf_nw, lirs]) 1), (TRYALL (EVERY' [etac dcdrth, Asm_simp_tac, (eresolve_tac (map mk_mono' [rep_from_ora, rep_from_ands])) ])), (TRYALL (rtac (mk_mono rulefs_mono RS image_mono))), (TRYALL (rtac aidps_rlscf_nw)), (TRYALL (force_tac (cesimps rule_lists))), nosg_tac 2, (chop_tac 1 (etac thin_rl 1)), (etac dcdrth 1), (clarsimp_tac (cesimps [rlscf_nw, bidis, bsrbs, ibidis, lils, lirs, rulefs_insert, rulefs_Un2]) 1), rewtac rulefs_1_def, Safe_tac, (TRYALL (EVERY' [ rtac drl.singleI', eresolve_tac (la_alts @ ldi_add.intrs)])), (ALLGOALS (eresolve_tac ([imageI] RL map mk_mono' [ands_from_rep, ora_from_rep]))), Safe_tac, (ALLGOALS Asm_simp_tac), (TRYALL (eresolve_tac ((idps_sub_a RSN (2, rulefs_mono) RS ldi_add.aidps) :: ldi_add.intrs))), (TRYALL (force_tac (cis [ldi_add.ilrules], esimps [ilrules, rulefs_insert]))) ]) ; val ldi_add_equiv' = rewrite_rule [derivableR_def] ldi_add_equiv RS set_ext ; val cldi_nw_lem = fold_rule [cldi_cldin] (ldi_add_equiv' RS cldin_equiv) ; val ldi_nw_lem = fold_rule [ldi_ldin] (ldi_add_equiv' RS ldin_equiv) ; val _ = qed_goal_spec_mp "ldi_add_cldin" Ldi_add.thy "rule : ldi_add --> cldin aidps ldi_add rule" (fn _ => [ (safe_tac (ces [ldi_add.elim])), (ALLGOALS (fn sg => if sg = 2 then all_tac else rtac cldin_ldin sg)), (SOMEGOAL (dtac ands_rep_cond)), (SOMEGOAL (dtac ora_rep_cond)), Safe_tac, (rtac lseqrepm_ldi_orF 8), (rtac lseqrepm_ldi_andT 7), Safe_tac, (ALLGOALS Asm_simp_tac), (TRYALL (eresolve_tac (la_alt_rs @ la_alt_ls @ ldi_add.intrs))), (etac ([asm_rl, inv_rules_aidps] MRS bi_lrule_ldin_lem) 1), (TRYALL (EVERY' [ (dresolve_tac [ldi_lil_nbs, ldi_lir_nbs]), (force_tac (cesimps [ldi_nw_lem])) ])), (force_tac (ces [rulefs.elim], esimps [idf, ldi_nw_lem, idf_ldi_nw] delsimps [ldi_def]) 3), (etac rulefs.elim 2), (clarsimp_tac (cesimps [ldi_nw_lem]) 2), (rtac ldi_cA 2), (clarsimp_tac (cesimps [cldi_nw_lem, ilrules]) 1), (etac rulefs.elim 1), Safe_tac, (TRYALL (resolve_tac ([ldi_ila, ldi_ils] RL [cldi_ldi]))), (TRYALL (simp_tac (esimps [iila, iils] delsimps [cldi_def]))), (TRYALL (rtac ldi_wkI_alt)), (SOMEGOAL (etac rev_subsetD)), (TRYALL (rtac aidps_rlscf_nw)), (TRYALL (resolve_tac seqdel.intrs THEN' resolve_tac ([transfer Ldi_add.thy stars.inI] RL strdel.intrs))), (auto_tac (cesimps rule_lists)) ]) ; val _ = qed_goal "ldi_add_interp" Ldi_add.thy "Ball (derrec ldi_add {}) (edin aidps ldi_add)" (fn _ => [ Clarify_tac 1, (rtac cldin_ex_interp 1), atac 2, Clarify_tac 1, (etac ldi_add_cldin 1) ]) ; val _ = qed_goalw "rlscf_nw_interp" Ldi_add.thy [derivableR_def, edi_edin] "Ball (derivableR rlscf_nw {}) (edi aidps rlscf_nw)" (fn _ => [ (simp_tac (esimps [ldi_add_equiv' RS edin_equiv RS sym, ldi_add_equiv' RS sym ]) 1), (rtac ldi_add_interp 1) ]) ;