structure oep = ext_ppt_one_ext_ppt ; (* for brevity *) val ext_ppt_UnfE = oep.mk_cases "(Unf c, dt) : ext_ppt rls" ; val ext_ppt_DerE = oep.mk_cases "(Der c ps, dt) : ext_ppt rls" ; structure oepi = epi_one_epi ; (* for brevity *) val epi_UnfE = oepi.mk_cases "((Unf c, dt), inf) : epi rls" ; val epi_DerE = oepi.mk_cases "((Der c ps, dt), inf) : epi rls" ; val oeinduct' = rotate_prems ~1 (oep.induct RS conjunct2 RS mp) ; val oeinduct = tacsthm [ etac oep.Unf 2, etac oep.Der 2, etac thin_rl 2 ] oeinduct' ; val epinduct = rotate_prems ~1 (oep.induct RS conjunct1 RS mp) ; val _ = qed_goal "ext_ppt_Der" dtext.thy "((Der c ps, Der c qs) : ext_ppt rls) = ((ps, qs) : one_ext_ppt rls)" (fn _ => [ (safe_tac (cis [oep.Der] addSEs [ext_ppt_DerE])) ]) ; val _ = qed_goal "one_ext_ppt_onerel" dtext.thy "one_ext_ppt rls = onerel (ext_ppt rls)" (fn _ => [ Safe_tac, (etac oeinduct 1), (etac onerel.onerelI1 1), (etac onerel.onerelI2 1), (etac onerel.induct 1), (etac oep.oneI1 1), (etac oep.oneI2 1) ]) ; val _ = qed_goal "Der_ext_ppt_onerel" dtext.thy "(Der c ps, Der d qs) : ext_ppt rls = \ \ (c = d & (ps, qs) : onerel (ext_ppt rls))" (fn _ => [ (simp_tac (esimps [one_ext_ppt_onerel RS sym]) 1), (rtac iffI 1), Clarify_tac 2, (etac oep.Der 2), (eresolve_tac oep.elims 1), ALLGOALS Force_tac ]) ; val oep_size = prove_goal dtext.thy "((dt, dte) : (ext_ppt rls) --> size dt < size dte) & \ \ ((ps, qs) : (one_ext_ppt rls) --> \ \ dertree_list_size ps < dertree_list_size qs)" (fn _ => [ (rtac oep.induct 1), (ALLGOALS Clarsimp_tac) ]) ; val _ = bind_thm ("ext_ppt_size", oep_size RS conjunct1 RS mp) ; val _ = bind_thm ("one_ext_ppt_size", oep_size RS conjunct2 RS mp) ; val _ = qed_goal_spec_mp "ext_ppt_tc_size" dtext.thy "(dt, dte) : (ext_ppt rls)^+ --> size dt < size dte" (fn _ => [ (rtac impI 1), (etac trancl_induct 1), (etac less_trans 2), ALLGOALS (etac ext_ppt_size) ]) ; val _ = qed_goal_spec_mp "ext_ppt_acyclic" dtext.thy "(dt, dte) : (ext_ppt rls)^+ --> dt ~= dte" (fn _ => [ Clarify_tac 1, (dtac ext_ppt_tc_size 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "one_ext_ppt_tc_size" dtext.thy "(dt, dte) : (one_ext_ppt rls)^+ --> \ \ dertree_list_size dt < dertree_list_size dte" (fn _ => [ (rtac impI 1), (etac trancl_induct 1), (etac less_trans 2), ALLGOALS (etac one_ext_ppt_size) ]) ; val _ = qed_goal_spec_mp "one_ext_ppt_acyclic" dtext.thy "(dt, dte) : (one_ext_ppt rls)^+ --> dt ~= dte" (fn _ => [ Clarify_tac 1, (dtac one_ext_ppt_tc_size 1), Force_tac 1 ]) ; val _ = qed_goal_spec_mp "oep_Der" dtext.thy "(dt, dta) : ext_ppt rls --> (EX c ps. dta = Der c ps)" (fn _ => [ (rtac impI 1), (etac oep.elim 1), TRYALL Fast_tac ]) ; (* (one_)epi *) val epi_ep' = prove_goal dtext.thy "(((dt, dte), inf) : epi rls --> (dt, dte) : ext_ppt rls & \ \ (ALL psa ps c psb. inf = Epi psa (ps, c) psb --> (ps, c) : rls & \ \ premsDT dt = psa @ c # psb & premsDT dte = psa @ ps @ psb)) & \ \ (((dts, dtes), inf) : one_epi rls --> (dts, dtes) : one_ext_ppt rls & \ \ (ALL psa ps c psb. inf = Epi psa (ps, c) psb --> (ps, c) : rls & \ \ premsDTs dts = psa @ c # psb & premsDTs dtes = psa @ ps @ psb))" (fn _ => [ (rtac oepi.induct 1), (REPEAT_SOME (resolve_tac [conjI, impI])), ALLGOALS (clarsimp_tac (cesimps [premsDTs_Unf])), (TRYALL (resolve_tac oep.intrs THEN_ALL_NEW atac)) ]) ; val _ = ListPair.app bind_thm (["epi_ep", "epi_rl", "epi_pr", "epi_pre", "oepi_oep", "oepi_rl", "oepi_pr", "oepi_pre"], map (tacthm (TRYALL (rtac refl))) (msc epi_ep')) ; val ep_epi' = prove_goal dtext.thy "((dt, dte) : ext_ppt rls --> (EX inf. ((dt, dte), inf) : epi rls)) & \ \ ((dts, dtes) : one_ext_ppt rls --> \ \ (EX inf. ((dts, dtes), inf) : one_epi rls))" (fn _ => [ (rtac oep.induct 1), Safe_tac, (TRYALL (case_tac "inf" o incr)), Safe_tac, (ALLGOALS (rtac exI THEN' resolve_tac oepi.intrs)), TRYALL atac ]) ; val _ = ListPair.app bind_thm (["ep_epi", "oep_oepi"], map (tacthm (TRYALL (rtac refl))) (msc ep_epi')) ; val epi_e_unique' = prove_goal dtext.thy "(((dt, dte), inf) : epi rls --> \ \ (ALL dte'. ((dt, dte'), inf) : epi rls --> dte' = dte)) & \ \ (((dts, dtes), inf) : one_epi rls --> \ \ (ALL dtes'. ((dts, dtes'), inf) : one_epi rls --> dtes' = dtes))" (fn _ => [ (rtac oepi.induct 1), Safe_tac, (etac epi_UnfE 1), Force_tac 1, (etac epi_DerE 1), Force_tac 1, (ALLGOALS (chop_last o eresolve_tac (tl oepi.elims))), Fast_tac 1, Fast_tac 3, ALLGOALS Clarify_tac, (dtac oepi_pr 1), (dtac epi_pr 2), (ALLGOALS (dres_inst_tac [("f", "size")] arg_cong)), (ALLGOALS (etac thin_rl THEN' etac thin_rl)), ALLGOALS Clarsimp_tac ]) ; val _ = ListPair.app bind_thm (["epi_e_unique", "one_epi_e_unique"], msc epi_e_unique') ; val epi_i_unique' = prove_goal dtext.thy "(((dt, dte), inf) : epi rls --> \ \ (ALL inf'. ((dt, dte), inf') : epi rls --> inf' = inf)) & \ \ (((dts, dtes), inf) : one_epi rls --> \ \ (ALL inf'. ((dts, dtes), inf') : one_epi rls --> inf' = inf))" (fn _ => [ (rtac oepi.induct 1), Safe_tac, (etac epi_UnfE 1), Clarsimp_tac 1, (rtac ([asm_rl, premsDTs_Unf, premsDTs_Unf] MRS box_equals) 1), Force_tac 1, (etac epi_DerE 1), Force_tac 1, (ALLGOALS (chop_last o eresolve_tac (tl oepi.elims))), Fast_tac 1, Fast_tac 3, ALLGOALS Clarify_tac, (TRYALL (eresolve_tac ([epi_ep RS ext_ppt_size, oepi_oep RS one_ext_ppt_size] RL [order_less_irrefl RS notE]))) ]) ; val _ = ListPair.app bind_thm (["epi_i_unique", "one_epi_i_unique"], msc epi_i_unique') ; val _ = qed_goal_spec_mp "frg_s" dtext.thy "frg rls dt --> frgs rls dt" (fn _ => [ (case_tac "dt" 1), ALLGOALS Clarsimp_tac, (rtac exI 1), rtac conjI 1, atac 2, Force_tac 1 ]) ; val _ = qed_goal "concl_dtc" dtext.thy "conclDT ppst :# dt_contents ppst" (fn _ => [ (case_tac "ppst" 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal "dtcss_sum" dtext.thy "dt_contentss dts = foldr (op + o dt_contents) dts {#}" (indAu "dts") ; val oep_concl = prove_goal dtext.thy "((dt, dte) : ext_ppt rls --> conclDT dt = conclDT dte) & \ \ ((dts, dtes) : one_ext_ppt rls --> map conclDT dts = map conclDT dtes)" (fn _ => [ (rtac oep.induct 1), ALLGOALS Clarsimp_tac ]) ; val _ = ListPair.map bind_thm (["ext_ppt_concl" , "one_ext_ppt_concls"], msc oep_concl) ; val oep_dtc = prove_goal dtext.thy "((dt, dte) : ext_ppt rls --> dt_contents dt <= dt_contents dte) & \ \ ((dts, dtes) : one_ext_ppt rls --> dt_contentss dts <= dt_contentss dtes)" (fn _ => [ (rtac oep.induct 1), ALLGOALS (clarsimp_tac (cesimps [mins_def])) ]) ; val _ = ListPair.map bind_thm (["ext_ppt_dtc" , "one_ext_ppt_dtc"], msc oep_dtc) ; val oep_frg = prove_goal dtext.thy "((pta, ptb) : ext_ppt rls --> \ \ allDT (frg rls) pta --> allDT (frg rls) ptb) & \ \ ((ptas, ptbs) : one_ext_ppt rls --> \ \ allDTs (frg rls) ptas --> allDTs (frg rls) ptbs)" (fn _ => [ (rtac oep.induct 1), ALLGOALS Clarsimp_tac , (dtac one_ext_ppt_concls 2), Force_tac 2, (clarsimp_tac (cesimps [allDTs, matches_Unf]) 1) ]) ; val _ = ListPair.map bind_thm (["ext_ppt_frg" , "one_ext_ppt_frg"], msc oep_frg) ; val _ = qed_goal_spec_mp "one_le_dtcss" dtext.thy "dta : set dts --> dt_contents dta <= dt_contentss dts" (fn _ => [ (induct_tac "dts" 1), ALLGOALS Clarsimp_tac, (etac (reop rev xt6) 1), Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "dtb_eq" dtext.thy "ALL bra brb. (dt_of_branch bra m = dt_of_branch brb m) = \ \ (ALL j. j <= m --> bra j = brb j)" (fn _ => [ (induct_tac "m" 1), ALLGOALS Clarsimp_tac, Safe_tac, (case_tac "j" 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "dtl_dtb_app" dtext.thy "ALL f. dt_of_list f fs = dt_of_branch (nth (f # fs @ xs)) (length fs)" (fn _ => [ (induct_tac "fs" 1), ALLGOALS Clarsimp_tac, (cong_tac 1), rtac ext 1, Force_tac 1 ]) ; val _ = bind_thm ("dtl_dtb", simplify (esimps []) (read_instantiate [("xs", "[]")] dtl_dtb_app)) ; val _ = qed_goal_spec_mp "dtb_dtl" dtext.thy "ALL br. dt_of_branch br n = dt_of_list (br 0) (map br [1..n])" (fn _ => [ (induct_tac "n" 1), ALLGOALS Clarsimp_tac, Safe_tac, ALLGOALS Clarsimp_tac, cong_tac 2, arith_tac 2, (simp_tac (HOL_ss addsimps [dtl_m RS sym]) 1), cong_tac 1, (rtac nth_equalityI 1), ALLGOALS Clarsimp_tac, (res_inst_tac [("s", "br (Suc i)")] trans 1), (case_tac "i" 1), (ALLGOALS (asm_simp_tac (esimps [nth_append]))) , Safe_tac, (TRYALL cong1_tac), (stac nth_upt 1), arith_tac 1, Simp_tac 1, arith_tac 1, (stac nth_upt 1), arith_tac 1, Simp_tac 1, (subgoal_tac "i = n | Suc i = n" 1) , arith_tac 2, Force_tac 1 ]) ; val _ = qed_goal "dtc_one" dtext.thy "c :# dt_contentss dts = (EX dt:set dts. c :# dt_contents dt)" (indAu "dts") ; val do1 = [Not_eq_iff, dtc_one] MRS iffD2 ; val do2 = rewrite_rule [mk_eq not_gr0] do1 ; val _ = bind_thm ("not_dtc_all", simplify (HOL_ss addsimps (not_gr0 :: bex_simps)) do2) ; val _ = qed_goal_spec_mp "height_dtb" dtext.thy "ALL br. heightDT (dt_of_branch br m) = m" (indAu "m") ; val _ = qed_goal_spec_mp "height_dtl" dtext.thy "ALL x. heightDT (dt_of_list x xs) = length xs" (indAu "xs") ; val _ = qed_goal_spec_mp "dtc_subt" dtext.thy "c :# dt_contents dt --> (EX dtn. (dtn, dt) : subt & c = conclDT dtn & \ \ count (dt_contents dtn) c = 1)" (fn _ => [ (res_inst_tac [("dertree", "dt")] dertree_induct 1), (ALLGOALS (clarsimp_tac (cesimps [dtc_one]))), Safe_tac, (res_inst_tac [("x", "Unf c")] exI 3), Force_tac 3, (datac bspec 1 2), mp_tac 2, (etac ex_forward 2), Safe_tac, (rtac sub1t_subt 2), (eatac sub1t.sub1tI 1 2), (* c is conclusion of dt *) (case_tac "EX dtl: set list. c :# dt_contents dtl" 1), (res_inst_tac [("x", "Der c list")] exI 2), (clarsimp_tac (cesimps [count_mins]) 2), (etac rev_mp 2), (induct_tac "list" 2), ALLGOALS Clarsimp_tac, (datac bspec 1 1), mp_tac 1, (etac ex_forward 1), Safe_tac, (rtac sub1t_subt 1), (eatac sub1t.sub1tI 1 1) ]) ; val _ = qed_goal "dtc_dtl" dtext.thy "ALL f. dt_contents (dt_of_list f fs) = mins f (ms_of_list fs)" (fn _ => [ (induct_tac "fs" 1), ALLGOALS (clarsimp_tac (cesimps [mins_empty])) ]) ; val _ = qed_goal_spec_mp "prems_dt_of_br" dtext.thy "ALL br. premsDT (dt_of_branch br n) = [br n]" (indAu "n") ; val _ = qed_goal_spec_mp "concl_dt_of_br" dtext.thy "conclDT (dt_of_branch br n) = br 0" (indAu "n") ; val _ = qed_goal_spec_mp "nextUp_dt_of_br" dtext.thy "nextUp (dt_of_branch br (Suc m)) = [dt_of_branch (br o Suc) m]" (fn _ => [ (induct_tac "m" 1), (ALLGOALS (clarsimp_tac (cesimps [o_def]))) ]) ; Addsimps [concl_dt_of_br, prems_dt_of_br, nextUp_dt_of_br] ; val _ = qed_goal_spec_mp "prems_dt_of_list" dtext.thy "ALL f. premsDT (dt_of_list f fs) = [last (f # fs)]" (indAu "fs") ; val _ = qed_goal_spec_mp "concl_dt_of_list" dtext.thy "conclDT (dt_of_list f fs) = f" (indAu "fs") ; val _ = qed_goal_spec_mp "nextUp_dt_of_list" dtext.thy "ALL fa. nextUp (dt_of_list f (fa # fs)) = [dt_of_list fa fs]" (indAu "fs") ; Addsimps [concl_dt_of_list, prems_dt_of_list, nextUp_dt_of_list] ; val _ = qed_goal_spec_mp "ssubDT_dtc" dtext.thy "(cs, dta) : ssubDT dt --> ms_of_list cs + dt_contents dt <= dt_contents dta" (fn _ => [ (rtac impI 1), (etac ssubDT.induct 1), ALLGOALS (clarsimp_tac (cesimps [mins_assoc])), (simp_tac (esimps [mins_def]) 1), (etac (reop rev xt6) 1), (etac one_le_dtcss 1) ]) ; val _ = qed_goal_spec_mp "branch_contents" dtext.thy "ALL br. set_of (dt_contents (dt_of_branch br n)) = br ` {i. i <= n}" (fn _ => [ (induct_tac "n" 1), (ALLGOALS (clarsimp_tac (cesimps [set_of_mins]))), Safe_tac, (REPEAT (rtac imageI 1 THEN Force_tac 1)), (case_tac "xa" 1), Fast_tac 1, (etac notE 1), (rtac image_eqI 1), Fast_tac 1, Force_tac 1 ]) ; val _ = qed_goal_spec_mp "in_branch_contents" dtext.thy "i <= n --> br i :# dt_contents (dt_of_branch br n)" (fn _ => [ (force_tac (cesimps [mem_set_of_iff RS sym, branch_contents]) 1) ]) ; val _ = qed_goal_spec_mp "branch_mono" dtext.thy "ALL m br. m <= n --> allDT (frgs rls) (dt_of_branch br n) --> \ \ allDT (frgs rls) (dt_of_branch br m)" (fn _ => [ (induct_tac "n" 1), ALLGOALS (simp_tac (esimps [allDTs])), Clarify_tac 1, (case_tac "m" 1), Safe_tac, Simp_tac 2, (etac allE2 2), REPEAT (mp_tac 2), (Clarsimp_tac 2), Fast_tac 2, Simp_tac 1 ]) ; (* ssubDT, then making single branch tree, preserves the allDT frgs property *) val _ = qed_goal_spec_mp "ssubDT_frgs" dtext.thy "(cs, dts) : ssubDT dt --> \ \ allDT (frgs rls) dts --> (ALL xs. xs = cs @ [conclDT dt] --> \ \ allDT (frgs rls) (dt_of_list (hd xs) (tl xs)))" (fn _ => [ (rtac impI 1), (etac ssubDT.induct 1), ALLGOALS Clarsimp_tac, (etac impE 1), (force_tac (cesimps [allDTs]) 1), (simp_tac (esimps [allDT_Next, allNextDTUp]) 1), (case_tac "cs @ [conclDT dt]" 1), Force_tac 1, Clarsimp_tac 1, (rtac exI 1), (rtac conjI 1), atac 2, (etac subsetD 1), (etac rev_image_eqI 1),(etac ssubDT.elim 1), TRYALL Force_tac ]) ;