val _ = goal GSub.thy "True" ; (* for following read *) val [tm_pFind, tm_fFind, tm_sFind, tm_nFind] = map read ["pFind", "fFind", "sFind", "nFind"] ; val [ctm_pFind, ctm_fFind, ctm_sFind, ctm_nFind] = map (cterm_of GSub.thy) [tm_pFind, tm_fFind, tm_sFind, tm_nFind] ; val [distinct_appendD1, distinct_appendD2, distinct_append_disj] = msc (distinct_append RS iffD1) ; val () = qed_goal "strIsFml" GSub.thy "strIsFml pat = (EX fml. pat = Structform fml)" (fn _ => [ (case_tac "pat" 1), ALLGOALS Asm_simp_tac]) ; val () = bind_thm ("strIsFmlE", (strIsFml RS iffD1) RS exE) ; val () = qed_goal_spec_mp "strIsFmlSub" GSub.thy "strIsFml pat --> strIsFml (strSubst sub pat)" (fn _ => [simp_tac (esimps [strIsFml]) 1, Safe_tac, Simp_tac 1]) ; val () = qed_goal_spec_mp "strIsCtnsFml" GSub.thy "strIsFml pat --> strCtnsFml pat" (fn _ => [ (case_tac "pat" 1), ALLGOALS Asm_simp_tac]) ; val () = qed_goal "strCtnsNE" GSub.thy "strCtnsFml p = (strFmls p ~= [])" (indAu "p") ; val () = qed_goal_spec_mp "strSubNoFml" GSub.thy "(~ strCtnsFml p --> strSubst (fs, ss) p = strSubst (fs', ss) p)" (indAu "p") ; val seqSubNoFml = prove_goal GSub.thy "~ seqCtnsFml pat --> seqSubst (fs, ss) pat = seqSubst (fs', ss) pat" (fn _ => [ (case_tac "pat" 1), (hyp_subst_tac 1), Simp_tac 1, (fast_tac (claset () addSEs [strSubNoFml]) 1) ]) RS mp ; val tacs'' = [ (induct_tac "str strs" 1), (ALLGOALS Asm_full_simp_tac), (rtac allI 1), (eres_inst_tac [("x", "tl ton")] allE 1), (case_tac "hd ton" 1)] ; val () = qed_goalw "strSVs_eq" GSub.thy [strSVs''_def] "set (strSVs str) = set (strSVs'' str)" (fn _ => [(induct_tac "str" 1), ALLGOALS (asm_full_simp_tac (esimps [ Un_commute, Un_assoc, Un_left_commute]))]) ; val () = qed_goalw "strSVs_eqlen" GSub.thy [strSVs''_def] "length (strSVs str) = length (strSVs'' str)" (fn _ => [(induct_tac "str" 1), ALLGOALS Asm_full_simp_tac ]) ; val () = qed_goal "strSVs_eqdist" GSub.thy "distinct (strSVs str) = distinct (strSVs'' str)" (fn _ => [ (simp_tac (esimps [distinct_card_iff, strSVs''_def, strSVs_eqlen, strSVs_eq]) 1) ]) ; val () = qed_goal_spec_mp "SV_single" GSub.thy "{sv} = set (strSVs' b pstr) --> distinct (strSVs pstr) --> \ \ strSVs' b pstr = [sv]" (fn _ => [ (clarsimp_tac (cesimps [strSVs_eqdist, strSVs''_def]) 1), (case_tac "strSVs' b pstr" 1), Force_tac 1, (case_tac "list" 1), Force_tac 1, (case_tac "b" 1), Force_tac 1, Force_tac 1 ]) ; val tacseq'' = [ (case_tac "seq" 1), hyp_subst_tac 1, (simp_tac (esimps [seqSVs''_def, strSVs''_def, strSVs_eq, strSVs_eqlen, Un_commute, Un_assoc, Un_left_commute]) 1)] ; val () = qed_goal "seqSVs_eq" GSub.thy "set (seqSVs seq) = set (seqSVs'' seq)" (fn _ => tacseq'') ; val () = qed_goal "seqSVs_eqlen" GSub.thy "length (seqSVs seq) = length (seqSVs'' seq)" (fn _ => tacseq'') ; val () = qed_goal "seqSVs_eqdist" GSub.thy "distinct (seqSVs seq) = distinct (seqSVs'' seq)" (fn _ => [ (case_tac "seq" 1), hyp_subst_tac 1, (simp_tac (esimps [seqSVs''_def, strSVs''_def, strSVs_eq, strSVs_eqdist, Int_Un_distrib, Int_Un_distrib2]) 1), (rtac iffI 1), (ALLGOALS Asm_simp_tac), (safe_tac HOL_cs), (TRYALL (etac (Int_commute RS trans)))]) ; val () = qed_goal "strSVs_1" GSub.thy "set (strSVs' pn str) <= set (strSVs str)" (fn _ => [ (simp_tac (esimps [strSVs''_def, strSVs_eq]) 1), (case_tac "pn" 1), Auto_tac]) ; val () = qed_goal "seqSVs_1" GSub.thy "set (seqSVs' pn seq) <= set (seqSVs seq)" (fn _ => [ (simp_tac (esimps [seqSVs''_def, seqSVs_eq]) 1), (case_tac "pn" 1), Auto_tac]) ; val () = qed_goal "subSV" GSub.thy "(ALL s : set (strSVs str). sub1 s = sub2 s) = \ \ (strSubst (pf, sub1) str = strSubst (pf, sub2) str)" (indAu "str") ; val () = qed_goal "strSubSVFml" GSub.thy "((ALL s : set (strSVs str). sub1 s = sub2 s) & \ \ (ALL fml : set (strFmls str). fmlSubst fs1 fml = fmlSubst fs2 fml)) = \ \ (strSubst (fs1, sub1) str = strSubst (fs2, sub2) str)" (indAu "str") ; val [subSV1, strSubSVFml1] = [subSV, strSubSVFml] RL [iffD1] ; val () = qed_goal "seqSubSVFml" GSub.thy "((ALL s : set (seqSVs seq). sub1 s = sub2 s) & \ \ (ALL fml : set (seqFmls seq). fmlSubst fs1 fml = fmlSubst fs2 fml)) = \ \ (seqSubst (fs1, sub1) seq = seqSubst (fs2, sub2) seq)" (fn _ => [(case_tac "seq" 1), (asm_simp_tac (esimps [ball_Un, strSubSVFml RS sym]) 1), Safe_tac]) ; val () = ListPair.app bind_thm (["seqSubFml", "seqSubSV", "seqSubSsame", "seqSubFsame"], let val fwd = conjI RS (seqSubSVFml RS iffD1) ; fun f i = tacthm (rtac ballI i THEN rtac refl i) fwd ; val [r1, r2] = [seqSubSVFml RS iffD2] RL [conjunct1, conjunct2] ; in [f 1, f 2, r2 RS f 1, r1 RS f 2] end) ; val () = qed_goal_spec_mp "strSVs'_sub" GSub.thy "(ALL b. set (strSVs' b (strSubst (pf, sub) str)) = \ \ ((UN sv : set (strSVs' True str). set (strSVs' b (sub sv))) Un \ \ (UN sv : set (strSVs' False str). set (strSVs' (~b) (sub sv)))))" (fn _ => [ (induct_tac "str" 1), (auto_tac (cesimps [UN_Un])) ]) ; val () = bind_thm ("seqSVs'_sub", prove_goal GSub.thy "set (seqSVs' b (seqSubst (pf, sub) seq)) = \ \ ((UN sv : set (seqSVs' True seq). set (strSVs' b (sub sv))) Un \ \ (UN sv : set (seqSVs' False seq). set (strSVs' (~b) (sub sv))))" (fn _ => [(case_tac "seq" 1), (asm_simp_tac (esimps [strSVs'_sub, UN_Un]) 1), Safe_tac])) ; val _ = qed_goal_spec_mp "PP_sub_lem" GSub.thy "PP list : fmlFVPPs formula --> \ \ PP (fst fs list) : fmlFVPPs (fmlSubst fs formula)" (indAu "formula") ; val _ = qed_goal_spec_mp "FV_sub_lem" GSub.thy "FV list : fmlFVPPs formula --> x : fmlFVPPs (snd fs list) --> \ \ x : fmlFVPPs (fmlSubst fs formula)" (indAu "formula") ; val _ = qed_goalw_spec_mp "FVPPs_sub_PP_lem" GSub.thy [strFVPPs_def] "PP list : strFVPPs str --> \ \ PP (fst fs list) : strFVPPs (strSubst (fs, ss) str)" (fn _ => [ (induct_tac "str" 1), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (etac bexI THEN' eresolve_tac [UnI1, UnI2])), ALLGOALS Clarsimp_tac, (etac PP_sub_lem 1) ]); val _ = qed_goalw_spec_mp "FVPPs_sub_FV_lem" GSub.thy [strFVPPs_def] "FV list : strFVPPs str --> x : fmlFVPPs (snd fs list) --> \ \ x : strFVPPs (strSubst (fs, ss) str)" (fn _ => [ (induct_tac "str" 1), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (etac bexI THEN' eresolve_tac [UnI1, UnI2])), ALLGOALS Clarsimp_tac, (eatac FV_sub_lem 1 1) ]); val _ = qed_goal_spec_mp "FVPPs_sub_mono_lem" GSub.thy "fmlFVPPs intp <= strFVPPs str --> \ \ fmlFVPPs (fmlSubst fs intp) <= strFVPPs (strSubst (fs, ss) str)" (fn _ => [ (induct_tac "intp" 1), ALLGOALS Clarsimp_tac, (etac FVPPs_sub_PP_lem 2), (eatac FVPPs_sub_FV_lem 1 1) ]) ; val _ = qed_goalw "strFVPPs_Structform" GSub.thy [strFVPPs_def] "strFVPPs (Structform fml) = fmlFVPPs fml" fn_at ; Addsimps [strFVPPs_Structform] ; val () = qed_goal "findf_match" GSub.thy "findf f ((sv, rep) # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goalw "nFind_match" GSub.thy [nFind_def] "nFind ((sv, rep) # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goalw "sFind_match" GSub.thy [sFind_def] "sFind ((sv, rep) # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goalw "fFind_match" GSub.thy [fFind_def] "fFind ((fv, rep) # ffs) fv = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goalw "pFind_match" GSub.thy [pFind_def] "pFind ((str, rep) # pfs) str = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goal_spec_mp "findf_next" GSub.thy "sv ~= sv' --> findf f sfs sv = rep --> findf f ((sv', rep') # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val [sFind_eqI, fFind_eqI] = [sFind_def, fFind_def] RL [def_imp_eq RS fun_cong RS fun_cong RS trans] ; val () = qed_goalw_spec_mp "sFind_next" GSub.thy [sFind_def] "sv ~= sv' --> sFind sfs sv = rep --> sFind ((sv', rep') # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val () = qed_goalw_spec_mp "fFind_next" GSub.thy [fFind_def] "sv ~= sv' --> fFind sfs sv = rep --> fFind ((sv', rep') # sfs) sv = rep" (fn _ => [Simp_tac 1]) ; val _ = bind_thm ("rulefs_find", read_instantiate_sg GSub.thy [("fs1", "((?ps, fFind ?fs), sFind ?ss)")] (singletonI RS rulefs.iisubI RS mem_same)) ; val _ = bind_thm ("nrulefs_find", read_instantiate_sg GSub.thy [("fs1", "((?ps, fFind ?fs), nFind ?ss)")] (singletonI RS nrulefs.iisubI RS mem_same)) ; val _ = qed_goalw "rulefs_cutr" GSub.thy [GDC.cut] "([$X |- A, A |- $Y], $X |- $Y) : rulefs {cutr}" (fn _ => [ (rtac rulefs_find 1), (auto_tac (cis [findf_match], esimps [sFind_def, fFind_def])) ]) ; val _ = qed_goal_spec_mp "str_no_fml_sub_same" GSub.thy "~ strCtnsFml str --> \ \ strSubst (fs, sub) str = strSubst (fs', sub) str" (indAu "str") ; (* UNUSED ?? *) val _ = qed_goal_spec_mp "str_no_fml_sub" GSub.thy "~ strCtnsFml str --> \ \ strSubst (fs, sub) str = strSubst ((%x. x, FV), sub) str" (indAu "str") ; val _ = qed_goal_spec_mp "seq_no_fml_sub_same" GSub.thy "~ seqCtnsFml seq --> \ \ seqSubst (fs, sub) seq = seqSubst (fs', sub) seq" (fn _ => [ (case_tac "seq" 1), (force_tac (ces [str_no_fml_sub_same], esimps []) 1) ]); (* UNUSED ?? *) val _ = qed_goal_spec_mp "seq_no_fml_sub" GSub.thy "~ seqCtnsFml seq --> \ \ seqSubst (fs, sub) seq = seqSubst ((%x. x, FV), sub) seq" (fn _ => [ (case_tac "seq" 1), (force_tac (ces [str_no_fml_sub], esimps []) 1) ]); val _ = qed_goal_spec_mp "seq_no_fml_sub'" GSub.thy "~ seqCtnsFml seq --> \ \ seqSubst (fs, snd sub) seq = seqSubst sub seq" (fn _ => [ (case_tac "sub" 1), Clarsimp_tac 1, (etac seq_no_fml_sub_same 1) ]) ; val da1 = prove_goal GSub.thy "distinct (list1 @ list2) --> (ALL s. s : set list1 --> ~ s : set list2)" (fn _ => [ Auto_tac ]) RS mp ; val da2 = prove_goal GSub.thy "distinct (list1 @ list2) --> (ALL s. s : set list2 --> ~ s : set list1)" (fn _ => [ Auto_tac ]) RS mp ; val [da1m, da2m] = map (fold_rule [mk_eq set_mem_eq]) [da1, da2] ; val () = qed_goal_spec_mp "defSubs_append1" GSub.thy "defSubs (strla @ strlb) suby suba = \ \ defSubs strlb suby (defSubs strla suby suba)" (fn _ => [ (rtac ext 1), rewtac defSubs_def, Auto_tac ]) ; val () = qed_goal_spec_mp "defSubs_append2" GSub.thy "defSubs (strla @ strlb) suby suba = \ \ defSubs strla suby (defSubs strlb suby suba)" (fn _ => [ (rtac ext 1), rewtac defSubs_def, Auto_tac ]) ; val () = qed_goal_spec_mp "defSubs_gen_same_str" GSub.thy "(ALL x : set (strSVs str) Int set strl. suba x = suby x) --> \ \ strSubst (fs, defSubs strl suby suba) str = strSubst (fs, suba) str" (fn _ => [ (clarsimp_tac (cesimps [strSubSVFml RS sym, defSubs_def]) 1)]) ; val () = qed_goal_spec_mp "defSubs_gen_same" GSub.thy "(ALL x : set (seqSVs seq) Int set strl. suba x = suby x) --> \ \ seqSubst (fs, defSubs strl suby suba) seq = seqSubst (fs, suba) seq" (fn _ => [ (clarsimp_tac (cesimps [seqSubSVFml RS sym, defSubs_def]) 1)]) ; val () = qed_goal_spec_mp "defSubs_gen_same2" GSub.thy "(ALL x : set (seqSVs seq) - set strl. suba x = suby x) --> \ \ seqSubst (fs, defSubs strl suby suba) seq = seqSubst (fs, suby) seq" (fn _ => [ (clarsimp_tac (cesimps [seqSubSVFml RS sym, defSubs_def]) 1)]) ; val () = qed_goal_spec_mp "defSubs_same" GSub.thy "set (seqSVs seq) <= set strl --> \ \ seqSubst (fs, defSubs strl suby suba) seq = seqSubst (fs, suby) seq" (fn _ => [ (force_tac (cesimps [seqSubSVFml RS sym, defSubs_def]) 1)]) ; val () = qed_goal_spec_mp "sameDefSub" GSub.thy "seqSubst (fs1, suby1) concl = seqSubst (fs2, suby2) concl --> \ \ seqSubst (fs', defSubs (seqSVs concl) suby1 suba) seq = \ \ seqSubst (fs', defSubs (seqSVs concl) suby2 suba) seq" (fn _ => [ (auto_tac (cesimps [seqSubSVFml RS sym, defSubs_def]))]) ; val () = qed_goal_spec_mp "sameDefSub'" GSub.thy "seqSubst (fs1, suba1) seq = seqSubst (fs2, suba2) seq --> \ \ seqSubst (fs1, defSubs svs suby suba1) seq = \ \ seqSubst (fs2, defSubs svs suby suba2) seq" (fn _ => [ (auto_tac (cesimps [seqSubSVFml RS sym, defSubs_def]))]) ; (* properties of rules *) val bcprops = store_thm ("bcprops", prove_goalw GSub.thy [bprops_def, cprops_def, C3_def, C5_def] "bprops rule --> cprops (conclRule rule)" (fn _ => [Fast_tac 1]) RS mp) ; (* comSub' : given two structures pat1 and pat2 with no structure variables in common, if they can be substituted for to give structures str1 and str2 (where the two substitutions substitute for formula variables the same way) there is a single substitution which takes pat1 to str1 and pat2 to str2 *) val () = qed_goal "comSub'" GSub.thy "[| distinct (strSVs pat1 @ strSVs pat2) ; \ \ strSubst (fs, sub1) pat1 = new1 ; strSubst (fs, sub2) pat2 = new2 |] ==> \ \ EX suby. strSubst (fs, suby) pat1 = new1 & strSubst (fs, suby) pat2 = new2" (fn it => [(cut_facts_tac it 1), (res_inst_tac [("x", "%s. if s : set (strSVs pat1) then sub1 s else sub2 s")] exI 1), (rtac conjI 1), (REPEAT (EVERY [(rtac trans 1), atac 2, (rtac subSV1 1), Force_tac 1]))]) ; (* better, get this as a consequence of comSub', using strSubNoFml *) val () = qed_goal "comSub" GSub.thy "[| distinct (strSVs pat1 @ strSVs pat2) ; \ \ ~ strCtnsFml pat1 ; ~ strCtnsFml pat2 ; \ \ strSubst sub1 pat1 = new1 ; strSubst sub2 pat2 = new2 |] ==> \ \ EX suby. strSubst suby pat1 = new1 & strSubst suby pat2 = new2" (fn it => [(cut_facts_tac it 1), (case_tac "sub1" 1), (case_tac "sub2" 1), (hyp_subst_tac 1), Simp_tac 1, (rtac exI 1), (rtac exI 1), (res_inst_tac [("x", "(%s. if s : set (strSVs pat1) then b s else ba s)")] exI 1), (full_simp_tac (esimps [strCtnsNE]) 1), (rtac conjI 1), (ALLGOALS (rtac strSubSVFml1)), Auto_tac]) ; (* ; val prems = it ; *) val list1 = prove_goal List_thy "[a] = map f list ==> EX a'. list = [a']" (fn prems => [ (cut_facts_tac prems 1), (case_tac "list" 1), (ALLGOALS Asm_full_simp_tac)]) ; fun fl prems = [ (cut_facts_tac prems 1), (case_tac "list" 1), (ALLGOALS Asm_full_simp_tac), etac conjE 1, (case_tac "lista" 1), (ALLGOALS Asm_full_simp_tac)] ; val list2 = prove_goal List_thy "[a, b] = map f list ==> EX a' b'. list = [a', b']" fl ; val list2' = prove_goal List_thy "[a, b] = map f list ==> EX b' a'. list = [a', b']" fl ; val _ = qed_goalw_spec_mp "lrc_fs" GSub.thy [cut] "premsRule inst = map conclDT dtl --> inst : rulefs {cutr} --> \ \ (EX a' b'. dtl = [a', b'])" (fn _ => [ (clarsimp_tac (ces rulefs.elims, esimps []) 1) ]) ; val lrc_fs' = (reop rev) lrc_fs ; val rmic_fs = read_instantiate_sg (sign_of GSub.thy) [("f", "%rule. inst : rulefs {rule}")] arg_cong ; fun tacpr rs = EVERY [ dresolve_tac rs 1, (SELECT_GOAL (rewtac rulefs_mdef) 1), etac exE 1, (hyp_subst_tac 1), (safe_asm_full_simp_tac (HOL_ss addsimps ([premsSub, premsRule_Pair, premsRule_Rule] @ thms "map.simps")) 1), (eresolve_tac [list1, list2, list2'] 1 ORELSE atac 1)] ; val ctmr_fs = read_cterm (sign_of GSub.thy) ("[| (premsRule (inst :: structr rule)) = map conclDT dtl ; \ \ inst : rulefs {?rule} |] ==> ?P", propT) ; val rcut_fs = [cut] RL [meta_eq_to_obj_eq RS rmic_fs RS iffD1] ; (* alternative to the above val [lrc, _] = map standard (Seq.list_of (tacpr rcut (trivial ctmr))) ; *)