(** Cat **) val () = qed_goalw "cat_abuts" Cat.thy [cat_def] "S ;; T = {intvl. EX s:S. EX t:T. setof intvl = setof s Un setof t & \ \ (nonempty s & nonempty t --> abuts (setof s) (setof t))}" (fn _ => [(safe_tac (claset () delrules [conjI])), (full_simp_tac (esimps [nonempty]) 2), (REPEAT (etac rev_bexI 2)), Fast_tac 2, (REPEAT (etac rev_bexI 2)), Safe_tac, (eatac abuts_less 2 2), (REPEAT (etac rev_bexI 1)), Safe_tac, (eatac abuts_lem 3 1)]) ; val () = qed_goalw "neg_cat" Cat.thy [mk_eq cat_abuts] "negint ` (S ;; T) = negint ` T ;; negint ` S" (fn _ => [(safe_tac (claset () delrules [impCE])), (REPEAT (etac (imageI RS rev_bexI) 1)), (asm_full_simp_tac (esimps [setof_neg, image_Un, Un_commute]) 1), (asm_full_simp_tac (esimps [setof_neg]) 1), (simp_tac (esimps [image_def]) 1), (rtac exI 1), rtac conjI 1, (rtac (neg_inv RS sym) 2), (REPEAT (etac (rev_bexI) 1)), (asm_simp_tac (esimps [setof_neg, image_Un, Un_commute]) 1)]) ; val () = qed_goalw "law7f" Cat.thy [mk_eq cat_abuts] "(S ;; T) ;; U <= S ;; (T ;; U)" (fn _ => [(safe_tac (claset () delrules [impCE])), (etac rev_bexI 1), (case_tac "nonempty sa" 1), (case_tac "nonempty ta" 1), (case_tac "nonempty t" 1), let val taces = [ (asm_full_simp_tac (esimps [nonempty])), (rtac exI), rtac conjI, (fn sg => (etac sym ORELSE' Fast_tac) (sg+1)), (REPEAT o etac rev_bexI), Fast_tac] ; in EVERY' taces 2 THEN EVERY' taces 2 THEN EVERY' taces 2 end, (asm_full_simp_tac (esimps [nonempty]) 1), (eres_inst_tac [("S", "setof ta")] nonemptyE 1), let val thul = rotate_prems ~1 (abuts_UnL RS iffD2) ; in datac thul 1 1 end, (rtac (ballI RS setleI) 1), (eatac (abuts_less RS order_less_imp_le) 2 1), (chop_tac 1 (ftac abuts_union 1)), etac exE 1, (rtac exI 1), (rtac conjI 1), ((REPEAT o etac rev_bexI) 1), (etac conjI 1), Fast_tac 1, (asm_simp_tac (esimps [Un_assoc]) 1), let val thur = rotate_prems ~1 (abuts_UnR RS iffD1) ; in datac thur 1 1 end, atac 2, (rtac (ballI RS setgeI) 1), (eatac (abuts_less RS order_less_imp_le) 2 1)]) ; val () = bind_thm ("abuts_Un_ub", meta_std (prove_goalw Cat.thy [isUb_def, setle_def] "C = A Un B & abuts A B --> isUb UNIV C = isUb UNIV B" (fn _ => [Safe_tac, rtac ext 1, rewrite_goals_tac [isUb_def, setle_def], Safe_tac, Fast_tac 1, Fast_tac 2, (ftac (abuts_ne RS conjunct2) 1), etac nonemptyE 1, (datac bspec 1 1), (datac abuts_less 2 1), arith_tac 1]))) ; val () = bind_thm ("abuts_Un_lub", meta_std (prove_goalw Cat.thy [isLub_def] "C = A Un B & abuts A B --> isLub UNIV C x = isLub UNIV B x" (fn _ => [Clarify_tac 1, (dtac (refl RS abuts_Un_ub) 1), (Asm_simp_tac 1)]))) ; val () = bind_thm ("abuts_Un_glb", meta_std (prove_goalw Cat.thy [isGlb_def] "C = A Un B & abuts A B --> isGlb UNIV C x = isGlb UNIV A x" (fn _ => [Clarify_tac 1, (simp_tac (esimps [image_Un]) 1), (rtac abuts_Un_lub 1), (etac (abuts_uminus RS iffD2) 2), (rtac Un_commute 1)]))) ; val () = bind_thm ("bnds_Un_ubt", meta_std (prove_goal Cat.thy "setof C = setof A Un setof B & abuts (setof A) (setof B) --> ubt C = ubt B" (fn _ => [Safe_tac, (ftac abuts_ne 1), (rtac ubc_cong 1), (rtac ext 1), Safe_tac, (rtac ((rewrite_rule [liftimp] ubc_mono) RS spec RS mp) 2), (atac 4), Fast_tac 3, (simp_tac (esimps [nonempty]) 2), Fast_tac 2, (cut_inst_tac [("z", "xb"), ("w", "x")] real_le_linear 1), (etac disjE 1), (rtac ubc_rel 2), atac 3, (subgoal_tac "x : setof C" 1), (Asm_full_simp_tac 1), etac disjE 1, (chop_tac 1 (datac abuts_less 2 1)), arith_tac 1, (subgoal_tac "xb : setof C" 2), Fast_tac 3, (etac thin_rl 2), (ALLGOALS (asm_full_simp_tac (esimps [bnd_conds]))), (rtac lbc_rel 1), atac 2, Fast_tac 1]))) ; val () = bind_thm ("bnds_Un_lbt", meta_std (prove_goal Cat.thy "setof C = setof A Un setof B & abuts (setof A) (setof B) --> lbt C = lbt A" (fn _ => [Safe_tac, (dtac (abuts_neg RS iffD2) 1), (dres_inst_tac [("C", "negint C")] (rotate_prems 1 bnds_Un_ubt) 1), (asm_simp_tac (esimps [setof_neg, image_Un]) 1), (rtac Un_commute 1), Asm_full_simp_tac 1]))) ; val () = bind_thm ("single_cat'", meta_std (prove_goalw Cat.thy [mk_eq cat_abuts] "nonempty B & nonempty C --> (A : {B} ;; {C}) = \ \ (lbt A = lbt B & ubt A = ubt C & ubt B = btopp (lbt C))" (fn _ => [Simp_tac 1, (safe_tac HOL_cs), (REPEAT ((eresolve_tac [bnds_Un_ubt, bnds_Un_lbt, abuts_bnds RS iffD1] THEN_ALL_NEW atac) 1)), (eatac (abuts_bnds RS iffD2) 2 2), (fatac (rotate_prems ~1 (abuts_bnds RS iffD2)) 2 1), (rtac set_ext 1), (asm_full_simp_tac (esimps [bnd_conds]) 1), (ftac abuts_lbc 1), (dtac abuts_ubc 1), (asm_full_simp_tac (esimps [liftimp]) 1), Fast_tac 1]))) ; val () = bind_thm ("scatD", rotate_prems ~1 (single_cat' RS iffD1)) ; val () = bind_thm ("scatI", single_cat' RS iffD2) ; val () = bind_thm ("single_cat", meta_std (prove_goal Cat.thy "nonempty B --> nonempty C --> ({A} = {B} ;; {C}) = \ \ (lbt A = lbt B & ubt A = ubt C & ubt B = btopp (lbt C))" (fn _ => [ strip_tac 1, rtac iffI 1, (eatac (single_cat' RS iffD1) 1 1), Fast_tac 1, Safe_tac, (eatac (single_cat' RS iffD2) 1 1), Fast_tac 1, (datac (single_cat' RS iffD1) 2 1), rtac bts_unique 1, ALLGOALS Asm_full_simp_tac]))) ; val () = bind_thm ("no_cat", meta_std (prove_goal Cat.thy "nonempty B & nonempty C --> ({} = {B} ;; {C}) = (ubt B ~= btopp (lbt C))" (fn _ => [ (cut_facts_tac [ex_bnds] 1), (safe_tac HOL_cs), (datac (single_cat RS iffD2) 1 1), (dres_inst_tac [("s", "{B} ;; {C}")] trans 2), (etac sym 2), Full_simp_tac 2, Fast_tac 1, (asm_simp_tac (esimps [cat_abuts, abuts_bnds]) 1)]))) ; (* val tacs1e = [ (simp_tac (esimps [nonempty, cat_abuts]) 1), Safe_tac, (rtac setof_cong 1), atac 2, (simp_tac (esimps [nonempty]) 1), Fast_tac 1] ; val () = bind_thm ("cat_emptyR", meta_std (prove_goal Cat.thy "nonempty B & ~ nonempty C --> ({B} ;; {C} = {B})" (fn _ => tacs1e))) ; val () = bind_thm ("cat_emptyL", meta_std (prove_goal Cat.thy "~ nonempty B & nonempty C --> ({B} ;; {C} = {C})" (fn _ => tacs1e))) ; *) val tacsene = [Safe_tac, ALLGOALS Asm_full_simp_tac, (rtac (setof_cong RS sym) 2), etac sym 3, rewtac (mk_eq nonempty), Fast_tac 2, (dtac equalityD2 1), (dtac subsetD 1), (rtac singletonI 1), Auto_tac] ; val () = qed_goalw_spec_mp "cat_emptyLe" Cat.thy [mk_eq nonempty, cat_def] "nonempty C --> ({B} ;; {C} = {C}) = (~ nonempty B)" (fn _ => tacsene) ; val () = qed_goalw_spec_mp "cat_emptyRe" Cat.thy [mk_eq nonempty, cat_def] "nonempty C --> ({C} ;; {B} = {C}) = (~ nonempty B)" (fn _ => tacsene) ; val [cat_emptyL, cat_emptyR] = [cat_emptyLe, cat_emptyRe] RL [iffD2] ; val enes = [[cat_emptyL, cat_emptyR] RL [set_cong], [singleton_iff]] MRL [trans] ; val eneDs as [eneDL, eneDR] = map (rotate_prems ~1) (enes RL [iffD1]) ; val eneIs = (enes RL [iffD2]) ; val () = bind_thm ("cat_empty", meta_std (prove_goalw Cat.thy [cat_def] "~ nonempty B & ~ nonempty C --> ({B} ;; {C} = {intvl. ~ nonempty intvl})" (fn _ => [ (simp_tac (esimps [nonempty]) 1)]))) ; val () = qed_goalw "cat_UN" Cat.thy [cat_def] "A ;; B = (UN a:A. UN b:B. {a} ;; {b})" (fn _ => [Auto_tac]) ; val () = qed_goal "mem_cat_UN" Cat.thy "(x : A ;; B) = (EX a:A. EX b:B. x : {a} ;; {b})" (fn _ => [rtac trans 1, rtac (cat_UN RS set_cong) 1, Simp_tac 1]) ; val () = qed_goal_spec_mp "catI" Cat.thy "x : {a} ;; {b} --> a : A --> b : B --> x : A ;; B" (fn _ => [Safe_tac, (rtac (mem_cat_UN RS iffD2) 1), Fast_tac 1]) ; val () = qed_goal "catE" Cat.thy "[| x : A ;; B ; !!a b. [| a : A ; b : B ; x : {a} ;; {b} |] ==> R |] ==> R" (fn [p1, p2] => [(cut_facts_tac [p1] 1), (dtac (mem_cat_UN RS iffD1) 1), Safe_tac, (eatac p2 2 1)]) ; fun tacs3I n = [Safe_tac, etac catE 1, rtac catI 1, atac 1, (eatac catI 2 n), Fast_tac 1] ; val () = qed_goal_spec_mp "cat3Il" Cat.thy "x : {a} ;; {b} ;; {c} --> a : A --> b : B --> c : C --> x : A ;; B ;; C" (fn _ => tacs3I 1) ; val () = qed_goal_spec_mp "cat3Ir" Cat.thy "x : {a} ;; ({b} ;; {c}) --> a : A --> b : B --> c : C --> x : A ;; (B ;; C)" (fn _ => tacs3I 2) ; fun tacs3E [p1, p2] = [(cut_facts_tac [p1] 1), etac catE 1, etac catE 1, (eatac p2 2 1), (etac catI 1), TRYALL atac, Fast_tac 1] ; val () = qed_goal "cat3El" Cat.thy "[| x : A ;; B ;; C ; !!a b c. \ \ [| a : A ; b : B ; c : C ; x : {a} ;; {b} ;; {c} |] ==> R |] ==> R" tacs3E ; val () = qed_goal "cat3Er" Cat.thy "[| x : A ;; (B ;; C) ; !!a b c. \ \ [| a : A ; b : B ; c : C ; x : {a} ;; ({b} ;; {c}) |] ==> R |] ==> R" tacs3E ; val cats3E = [cat3El, cat3Er] ; val cats3I = [cat3Il, cat3Ir] ; val () = qed_goal_spec_mp "cat_mono" Cat.thy "A <= A' --> B <= B' --> A ;; B <= A' ;; B'" (fn _ => [Safe_tac, etac catE 1, rtac catI 1, ALLGOALS Fast_tac]) ; val () = qed_goalw_spec_mp "cat_empty" Cat.thy [cat_def, mk_eq nonempty] "x : {A} ;; {B} --> nonempty x = (nonempty A | nonempty B)" (fn _ => [Auto_tac]) ; val () = qed_goalw_spec_mp "cat_empty'" Cat.thy [cat_def, mk_eq nonempty] "(~ nonempty A) & (~ nonempty B) --> x : {A} ;; {B} = (~ nonempty x)" (fn _ => [Auto_tac]) ; val () = qed_goalw_spec_mp "cat_nonempty1" Cat.thy [cat_def, mk_eq nonempty] "nonempty A --> x : {A} ;; B --> nonempty x" (fn _ => [Fast_tac 1]) ; fun tacs3' str = [ strip_tac 1, (rtac iffI 1), (etac catE 1), (fatac cat_nonempty1 1 1), (Asm_full_simp_tac 1), (REPEAT (datac scatD 2 1)), (Asm_full_simp_tac 1), (cut_facts_tac [ex_bnds] 1), Safe_tac, (subgoal_tac str 1), (rtac (single_cat RS iffD2 RS sym) 2), Fast_tac 4, (Asm_simp_tac 1), (rtac scatI 1), (ALLGOALS (Asm_simp_tac)), (full_simp_tac (esimps [nonempty, cat_def]) 1), (dtac (equalityD2 RS subsetD) 1), rtac insertI1 1, Auto_tac] ; val () = qed_goal_spec_mp "single_cat3r'" Cat.thy "nonempty A --> nonempty B --> nonempty C --> (x : {A} ;; ({B} ;; {C})) = \ \ (lbt x = lbt A & ubt x = ubt C & \ \ ubt A = btopp (lbt B) & ubt B = btopp (lbt C))" (fn _ => tacs3' "{B} ;; {C} = ?P") ; val () = qed_goal_spec_mp "single_cat3l'" Cat.thy "nonempty A --> nonempty B --> nonempty C --> (x : {A} ;; {B} ;; {C}) = \ \ (lbt x = lbt A & ubt x = ubt C & \ \ ubt A = btopp (lbt B) & ubt B = btopp (lbt C))" (fn _ => tacs3' "{A} ;; {B} = ?P") ; val single_cat3s = [single_cat3l', single_cat3r'] ; val scat3Ds = map (rotate_prems ~1) (single_cat3s RL [iffD1]) ; val scat3Is = (single_cat3s RL [iffD2]) ; val () = qed_goal "law7f" Cat.thy "(S ;; T) ;; U <= S ;; (T ;; U)" (fn _ => [Safe_tac, (eresolve_tac cats3E 1), (resolve_tac cats3I 1), (REPEAT1 (atac 2)), (case_tac "nonempty a" 1), (case_tac "nonempty b" 1), (case_tac "nonempty c" 1), (dresolve_tac scat3Ds 1), (REPEAT1 (atac 1)), (resolve_tac scat3Is 1), (REPEAT1 (atac 1)), (ALLGOALS (clarsimp_tac (cesimps [mk_eq cat_abuts, nonempty]))), (TRYALL (rtac exI THEN' ares_tac [refl])) ]) ; val () = qed_goal "law7" Cat.thy "(S ;; T) ;; U = S ;; (T ;; U)" (fn _ => [rtac equalityI 1, rtac law7f 1, (CONV_GOAL_TAC (TDSTOP_CONV ( EQ_CONV (false, false) (mk_eq (neg_neg_image RS sym)))) 1), (rtac image_mono 1), (simp_tac (esimps [neg_cat]) 1), (rtac law7f 1)]) ; val () = qed_goal_spec_mp "same_lb" Cat.thy "nonempty A --> nonempty B --> lbt A = lbt B --> \ \ (ubc (ubt B) ---> ubc (ubt A)) --> (EX C. {A} = {B} ;; {C})" (fn _ => [ strip_tac 1, (case_tac "A = B" 1), Asm_simp_tac 1, (rtac exI 1), (etac (cat_emptyR RS sym) 1), rtac empty 1, (cut_inst_tac [("U", "ubt A"), ("L", "btopp (ubt B)")] ex_bnds 1), (etac ex_match 1), (etac (single_cat RS iffD2) 1), (asm_simp_tac (esimps []) 2), (case_tac "ubc (ubt ?A) ---> ubc (ubt ?B)" 1), (datac liftimp_antisym 1 1), (dtac ubc_cong 1), (dtac bts_unique 1), (atac 1 ORELSE etac sym 1), contr_tac 1, (full_simp_tac (esimps [liftimp, nonempty]) 1), (etac exE 1), (res_inst_tac [("x", "s")] nonemptyI 1), (Clarify_tac 1), (rtac (bnd_conds RS iffD2) 1), (asm_full_simp_tac (esimps []) 1)]) ; val () = qed_goal_spec_mp "same_lb_or" Cat.thy "nonempty A --> nonempty B --> lbt A = lbt B --> \ \ (EX C. {A} = {B} ;; {C}) | (EX C. {B} = {A} ;; {C})" (fn _ => [ strip_tac 1, (cut_inst_tac [("s", "ubt A"), ("t", "ubt B")] ubc_linear 1), (etac disjE 1), (rtac disjI1 1), (rtac disjI2 2), (ALLGOALS (rtac same_lb)), (ALLGOALS Asm_simp_tac)]) ; (* examples of the equality of Wabenhorst's intended law *) fun XXtacs1 XX _ = [(safe_tac (claset () delrules [IntI])), (etac (law10a RS subsetD) 1), (etac catE 1), (etac catE 1), (rep_forw_tac neXXs 1), (subgoal_tac "lbt a = lbt aa" 1), ((case_tac "nonempty ba" THEN_ALL_NEW case_tac "nonempty b") 2), let val tacs = [ (REPEAT o (dresolve_tac (scatD :: eneDs) THEN' atac THEN' atac)), Asm_full_simp_tac] ; in (REPEAT (EVERY' tacs 2)) end, (cut_inst_tac [("s", "ubt a"), ("t", "ubt aa")] ubc_linear 1), (etac disjE 1), (subgoal_tac ("a : " ^ XX ^ "ints (no_aod Q)") 2), (subgoal_tac ("aa : " ^ XX ^ "ints (no_aod P)") 1), (rtac catI 1), (eatac IntI 1 2), atac 1, atac 1, (rtac catI 2), (eatac IntI 1 3), atac 2, atac 2, (ALLGOALS (full_simp_tac (esimps aod_set_XXs))), (subgoal_tac "setof aa <= setof a" 1), (subgoal_tac "setof a <= setof aa" 3), (REPEAT (EVERY [ (etac (mono_conds RS iffD2) 2), (Asm_simp_tac 2), Fast_tac 1])) ] ; fun dowabcorr1 XX = prove_goal Cat.thy ("(" ^ XX ^ "ints (no_aod P) Int " ^ XX ^ "ints (no_aod Q)) ;; U = \ \ (" ^ XX ^ "ints (no_aod P) ;; U) Int (" ^ XX ^ "ints (no_aod Q) ;; U)") (XXtacs1 XX) ; val _ = bind_thms ("law10rXX1s", map dowabcorr1 ["BB", "BC", "BO", "CB", "CC", "CO", "OB", "OC", "OO"]) ; fun XXtacs2 XX _ = [(safe_tac (claset () delrules [IntI])), (etac (law10b RS subsetD) 1), (etac catE 1), (etac catE 1), (rep_forw_tac neXXs 1), (subgoal_tac "ubt b = ubt ba" 1), ((case_tac "nonempty aa" THEN_ALL_NEW case_tac "nonempty a") 2), let val tacs = [ (REPEAT o (dresolve_tac (scatD :: eneDs) THEN' atac THEN' atac)), Asm_full_simp_tac] ; in (REPEAT (EVERY' tacs 2)) end, (cut_inst_tac [("s", "lbt b"), ("t", "lbt ba")] lbc_linear 1), (etac disjE 1), (subgoal_tac ("ba : " ^ XX ^ "ints (no_aod P)") 1), (subgoal_tac ("b : " ^ XX ^ "ints (no_aod Q)") 3), (rtac catI 1), (eatac IntI 1 3), atac 1, atac 1, (rtac catI 2), (eatac IntI 1 4), atac 2, atac 2, (ALLGOALS (full_simp_tac (esimps aod_set_XXs))), (subgoal_tac "setof ba <= setof b" 1), (subgoal_tac "setof b <= setof ba" 3), (REPEAT (EVERY [ (etac (mono_conds RS iffD2) 2), (Asm_simp_tac 2), Fast_tac 1])) ] ; fun dowabcorr2 XX = prove_goal Cat.thy ("U ;; (" ^ XX ^ "ints (no_aod P) Int " ^ XX ^ "ints (no_aod Q)) = \ \ (U ;; " ^ XX ^ "ints (no_aod P)) Int (U ;; " ^ XX ^ "ints (no_aod Q))") (XXtacs2 XX) ; val _ = bind_thms ("law10rXX2s", map dowabcorr2 ["BB", "BC", "BO", "CB", "CC", "CO", "OB", "OC", "OO"]) ; val ssbx = (esimps (bnd_conds :: Ball_def :: XXints_defs)) ; val () = qed_goal_spec_mp "flem" Cat.thy "x : [(-%t a w. P t & w - a = len -)] = ((ALL t: setof x. P t) & \ \ realval (ubt x) - realval (lbt x) = len & nonempty x)" (fn _ => [ (rtac iffI 1), (full_simp_tac ssbx 1), Auto_tac, (dtac dense 1), Fast_tac 1, (full_simp_tac ssbx 1), (case_tac "x" 1), (ALLGOALS Asm_full_simp_tac)]) ; val flems = XXints_rels RL [subsetD RS (flem RS iffD1)] ; val () = qed_goal_spec_mp "fidge13" Cat.thy "0 < r --> 0 < s --> \ \ BBints (%t a w. P t & w - a = r + s) = \ \ BBints (%t a w. P t & w - a = r) ;; BBints (%t a w. P t & w - a = s)" (fn _ => [Safe_tac, (dtac (flem RS iffD1) 1), (case_tac "x" 1), (subgoal_tac "x : {CO real1 (real1 + r)} ;; {CC (real1 + r) real2}" 1), (subgoal_tac "x : {CO real1 (real1 + r)} ;; {CO (real1 + r) real2}" 3), (subgoal_tac "x : {OC real1 (real1 + r)} ;; {OC (real1 + r) real2}" 5), (subgoal_tac "x : {OC real1 (real1 + r)} ;; {OO (real1 + r) real2}" 7), (REPEAT1 (EVERY [(etac catI 1), ((rtac scatI THEN_ALL_NEW Asm_full_simp_tac THEN_ALL_NEW arith_tac) 3), (REPEAT1 (MSSG (asm_full_simp_tac ssbx) 1)) ])), (* level 8 *) (etac catE 1), (REPEAT (dtac (flem RS iffD1) 1)), (dtac scatD 1), (TRYALL (rtac lt_nonempty)), (arith_tac 1), (arith_tac 1), (rtac (flem RS iffD2) 1), (asm_full_simp_tac (esimps [Ball_def, bnd_conds]) 1), (Safe_tac), Fast_tac 1, Simp_tac 1, (rtac lt_nonempty 1), Asm_full_simp_tac 1]) ; val tacsf11 = [Safe_tac, (ALLGOALS (etac catE)), (etac catE 1), (etac catI 2), (etac catI 4), Safe_tac, (dtac scatD 1), (ftac scatD 3), (REPEAT (Fast_tac 1 ORELSE (eresolve_tac neXXs 1))), (subgoal_tac "b = ba" 1), (subgoal_tac "a = aa" 1), (TRYALL (rtac bts_unique)), (ALLGOALS Asm_full_simp_tac), (full_simp_tac (esimps XXints_defs) 2), (SELECT_GOAL (safe_tac (claset () delrules [impCE])) 2), (ALLGOALS Asm_full_simp_tac), (ALLGOALS (REPINC 1 (etac impE))), (TRYALL (etac dense)), (TRYALL (rtac exI THEN' rtac conjI THEN_ALL_NEW (TRY o rtac order_refl) THEN_ALL_NEW atac)), (ALLGOALS Asm_simp_tac), (etac catI 1), Auto_tac] ; val () = qed_goal_spec_mp "fidge11ac" Cat.thy "T <= Collect nonempty --> V <= Collect nonempty --> \ \ ((S Int (BCints (%t a w. w - a = r))) ;; T) Int \ \ ((U Int (BCints (%t a w. w - a = r))) ;; V) = \ \ ((S Int U Int (BCints (%t a w. w - a = r))) ;; (T Int V))" (fn _ => tacsf11) ; val () = qed_goal_spec_mp "fidge11ao" Cat.thy "T <= Collect nonempty --> V <= Collect nonempty --> \ \ ((S Int (BOints (%t a w. w - a = r))) ;; T) Int \ \ ((U Int (BOints (%t a w. w - a = r))) ;; V) = \ \ ((S Int U Int (BOints (%t a w. w - a = r))) ;; (T Int V))" (fn _ => tacsf11) ; val () = qed_goal_spec_mp "fidge11bc" Cat.thy "S <= Collect nonempty --> T <= Collect nonempty --> \ \ (S ;; (U Int (CBints (%t a w. w - a = r)))) Int \ \ (T ;; (V Int (CBints (%t a w. w - a = r)))) = \ \ ((S Int T) ;; (U Int V Int (CBints (%t a w. w - a = r))))" (fn _ => tacsf11) ; val () = qed_goal_spec_mp "fidge11bo" Cat.thy "S <= Collect nonempty --> T <= Collect nonempty --> \ \ (S ;; (U Int (OBints (%t a w. w - a = r)))) Int \ \ (T ;; (V Int (OBints (%t a w. w - a = r)))) = \ \ ((S Int T) ;; (U Int V Int (OBints (%t a w. w - a = r))))" (fn _ => tacsf11) ; val _ = TextIO.print "Finished Cat.ML\n" ;