File InfClass.ML


(* single objects *)

Goal "EX (b::('a::inf_class)). a ~= b";
by (cut_inst_tac [("'a", "'a")] inf_class 1);
by (Clarify_tac 1);
by (case_tac "a = f n" 1);
by (dres_inst_tac [("x", "n"), ("y", "Suc n")] inj_eq 1);
by (Auto_tac);
qed "ex_dist1";

Goal "EX (b::('a::inf_class)). b ~= a";
by (cut_inst_tac [("a", "a")] ex_dist1 1);
by (Auto_tac);
qed "ex_dist2";


(* finite sets *)

Goal "[| finite (A::(('a::inf_class) set)) ; inj (f::nat=>'a) |] \
  \ ==> EX n. ALL a:A. ALL m. a = f m --> m <= n";
by (etac finite_induct 1);
by (case_tac "EX k. x = f k" 2);
by (Fast_tac 1);
by (Clarify_tac 1);
by (case_tac "k <= n" 1);
by (res_inst_tac [("x", "Suc n")] exI 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "f m")] ballE 1);
by (Force_tac 1);
by (dres_inst_tac [("x", "m"), ("y", "k")] inj_eq 1);
by (Force_tac 1);
by (res_inst_tac [("x", "Suc k")] exI 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x", "f m")] ballE 1);
by (Force_tac 1);
by (dres_inst_tac [("x", "m"), ("y", "k")] inj_eq 1);
by (Force_tac 1);
by (Auto_tac);
qed "lemma";

Goal "finite A ==> EX (b::('a::inf_class)). b ~: A";
by (cut_inst_tac [("'a", "'a")] inf_class 1);
by (Clarify_tac 1);
by ((dtac lemma 1) THEN (atac 1));
by (Clarify_tac 1);
by (eres_inst_tac [("x", "f (Suc n)")] ballE 1);
by (Auto_tac);
qed "ex_dist_set";

Goal "finite (A::('a::inf_class) set) \
  \ ==> EX B. card B = n & finite B & A Int B = {}";
by (induct_tac "n" 1);
by (ALLGOALS Clarify_tac);
by (res_inst_tac [("x", "{}")] exI 1);
by (Asm_simp_tac 1);
by (cut_inst_tac [("'a", "'a"), ("A", "A Un B")] ex_dist_set 1);
by (Asm_simp_tac 1);
by (etac exE 1);
by (res_inst_tac [("x", "insert b B")] exI 1);
by (Auto_tac);
qed "ex_n_dist_set";


(* finite lists *)

Goalw [mk_meta_eq set_mem_eq] "EX (b::('a::inf_class)). ~(b mem xs)";
by (auto_tac ((claset() addIs [ex_dist_set]), simpset()));
qed "ex_dist_list";


(* natural numbers *)

Goal "EX (f::nat=>nat). inj f";
by (res_inst_tac [("x", "%x. x")] exI 1);
by (fast_tac (claset() addIs [datatype_injI]) 1);
qed "nat_ex_inj";