val ubslSucE = ubsl.mk_cases "(b, Suc n) : ubsl s" ; val ubsl0E = ubsl.mk_cases "(b, 0) : ubsl s" ; val ubslEs = [ubslSucE, ubsl0E] ; val _ = qed_goal_spec_mp "bd_wfp" bdrel.thy "bded rho <= wfp rho" (fn _ => [ (safe_tac (ces bded.elims)), (etac ubsl.induct 1), (ALLGOALS (rtac wfp.wfpI)), Auto_tac]) ; val _ = qed_goalw_spec_mp "bded_bd" bdrel.thy [bd_of_def] "x : bded rho --> (x, bd_of rho x) : ubsl rho" (fn _ => [ (safe_tac (ces bded.elims)), (etac LeastI 1)]) ; val _ = qed_goal_spec_mp "ubsl_mono'" bdrel.thy "(a, m) : ubsl rho --> sig <= rho --> (ALL n. m <= n --> (a, n) : ubsl sig)" (fn _ => [ (rtac impI 1), (etac ubsl.induct 1), Safe_tac, (case_tac "n" 2), (case_tac "na" 1), (safe_tac (cis ubsl.intrs)), Auto_tac]) ; val _ = qed_goal_spec_mp "bded_mono" bdrel.thy "sig <= rho --> bded rho <= bded sig" (fn _ => [ (clarsimp_tac (cesimps [bded.unfold]) 1), (datac ubsl_mono' 1 1), Auto_tac]) ; val _ = qed_goalw_spec_mp "fb_mono" bdrel.thy [fb_def] "sig <= rho --> fb rho --> fb sig" (fn _ => [ (Clarify_tac 1), (rtac finite_subset 1), (etac spec 2), Auto_tac]) ; val _ = qed_goal_spec_mp "fb_wfp_bd" bdrel.thy "fb rho --> wfp rho <= bded rho" (fn _ => [ (Safe_tac), (etac wfp.induct 1), (full_simp_tac (esimps [bded.unfold, fb_def]) 1), (eres_inst_tac [("x", "dt")] allE 1), (dtac finite_list 1), (Clarify_tac 1), (res_inst_tac [("x", "Suc (maxl (map (bd_of rho) l))")] exI 1), (rtac ubsl.SucI 1), (etac all_match 1), (Clarify_tac 1), (dtac (bded.I RS bded_bd) 1), (etac ubsl_mono' 1), (rtac maxlG 2), Auto_tac]) ; val _ = qed_goal_spec_mp "ubsl_nrel_comp" bdrel.thy "ALL a. ((a, n) : ubsl r) = (ALL b. (b, a) ~: nrel_comp r (Suc n))" (fn _ => [ (induct_tac "n" 1), (ALLGOALS (rtac (iffI RS allI))), (TRYALL (force_tac (cis ubsl.intrs addSEs ubslEs, HOL_ss addsimps [nrel_comp_0, nrel_comp_Suc']) )) ]) ; val _ = qed_goal_spec_mp "O_UN" HOL_Ths.thy "{a. (a, x) : s O r} = (UN y: {y. (y, x) : s}. {a. (a, y) : r})" fn_at ; val _ = qed_goalw_spec_mp "trancl_UN_rtrancl" HOL_Ths.thy [mk_eq (O_rtc RS sym)] "{a. (a, x) : r^+} = (UN y: {y. (y, x) : r}. {a. (a, y) : r^*})" (fn _ => [ (rtac O_UN 1)]) ; val _ = qed_goalw_spec_mp "fb_rtrancl" bdrel.thy [fb_def] "wf r --> fb r --> fb (r^*)" (fn _ => [ Safe_tac, (eres_inst_tac [("a", "b")] wf_induct 1), (eres_inst_tac [("x", "x")] allE 1), (* don't combine the following *) (simp_tac (simpset_of Relation_thy addsimps [reflcl_trancl RS sym, Collect_disj_eq]) 1), (simp_tac (esimps [trancl_UN_rtrancl]) 1), (rtac finite_UN_I 1), Auto_tac]) ; val _ = qed_goalw_spec_mp "fb_O" bdrel.thy [fb_def] "fb s --> fb r --> fb (s O r)" (fn _ => [ Safe_tac, (simp_tac (esimps [O_UN]) 1), (rtac finite_UN_I 1), Auto_tac ]) ;