File Procs.ML


(* free names *)

Goal "fnaa (%x y. ffP y x) = fnaa ffP";
by (auto_tac (claset(), simpset() addsimps [fna_def, fnaa_def]));
qed "fnaa_sym";

Goal "a ~: fna (%x. .t.fP x) ==> a ~: fna fP";
by (auto_tac (claset(), simpset() addsimps [fna_def]));
qed "not_fna1";

Goal "a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fnna fa";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna2a";

Goal "a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fnna fb";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna2b";

Goal "a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna2c";

Goal "a ~: fna (%x. fa x[y].ffP y x) ==> a ~: fnna fa";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnaa_def, fnna_def]));
qed "not_fna3a";

Goal "a ~: fna (%x. fa x[y].ffP y x) ==> a ~: fnaa ffP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnaa_def, fnna_def]));
qed "not_fna3b";

Goal "a ~: fna (%x. .#y. ffP y x) ==> a ~: fnaa ffP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnaa_def]));
qed "not_fna4";

Goal "a ~: fna (%x. fP x .+ fQ x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna5a";

Goal "a ~: fna (%x. fP x .+ fQ x) ==> a ~: fna fQ";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna5b";

Goal "a ~: fna (%x. fP x .| fQ x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna6a";

Goal "a ~: fna (%x. fP x .| fQ x) ==> a ~: fna fQ";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna6b";

Goal "a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fnna fa";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna7a";

Goal "a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fnna fb";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna7b";

Goal "a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna7c";

Goal "a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fnna fa";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna8a";

Goal "a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fnna fb";
by (auto_tac (claset(),
              simpset() addsimps [fna_def, fnna_def]));
qed "not_fna8b";

Goal "a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna8c";

Goal "a ~: fna (%x. .!fP x) ==> a ~: fna fP";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "not_fna9";

Goal "fna (%x. .t.fP x) <= A ==> fna fP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "fna_subset1";

Goal "fna (%x. fa x<fb x>.fP x) <= A ==> \
  \ fnna fa <= A & fnna fb <= A & fna fP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fnna_def, fna_def]));
qed "fna_subset2";

Goal "fna (%x. fa x[y].ffP y x) <= A ==> \
  \ fnna fa <= A & fnaa ffP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fnna_def, fna_def, fnaa_def]));
qed "fna_subset3";

Goal "fna (%x. .#y. ffP y x) <= A ==> fnaa ffP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fnaa_def, fna_def]));
qed "fna_subset4";

Goal "fna (%x. fP x .+ fQ x) <= A ==> fna fP <= A & fna fQ <= A";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "fna_subset5";

Goal "fna (%x. fP x .| fQ x) <= A ==> fna fP <= A & fna fQ <= A";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "fna_subset6";

Goal "fna (%x. .[fa x.=fb x]fP x) <= A ==> \
  \ fnna fa <= A & fnna fb <= A & fna fP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fnna_def, fna_def]));
qed "fna_subset7";

Goal "fna (%x. .[fa x.~=fb x]fP x) <= A ==> \
  \ fnna fa <= A & fnna fb <= A & fna fP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fnna_def, fna_def]));
qed "fna_subset8";

Goal "fna (%x. .!fP x) <= A ==> fna fP <= A";
by (auto_tac (claset(),
              simpset() addsimps [fna_def]));
qed "fna_subset9";

Goal "fna fP = Inter {A. EX a. A = fn (fP a)}";
by (auto_tac (claset(), simpset() addsimps [fna_def]));
qed "fna_Inter";

Goal "fnaa ffP = Inter {A. EX a b. A = fn (ffP a b)}";
by (auto_tac (claset(), simpset() addsimps [fna_def, fnaa_def]));
qed "fnaa_Inter";

Goal "EX A:AA. finite A ==> finite (Inter AA)";
by (auto_tac (claset() addIs [Inter_finite_elem], simpset()));
qed "lemma";

Goal "finite (fn P)";
by (induct_tac "P" 1);
by (cut_inst_tac [("fP", "fun")] fna_Inter 5);
by (cut_inst_tac [("fP", "fun")] fna_Inter 4);
by (auto_tac (claset(), simpset() addsimps [fna_def,fna_Inter]));
by (ALLGOALS (rtac lemma));
by (ALLGOALS Force_tac);
qed "finite_fn";

Goalw [mk_meta_eq fna_Inter] "finite (fna fP)";
by (res_inst_tac [("A", "fn (fP a)")] Inter_finite_elem 1);
by (auto_tac (claset() addIs [finite_fn], simpset()));
qed "finite_fna";

Goalw [mk_meta_eq fnaa_Inter] "finite (fnaa ffP)";
by (res_inst_tac [("A", "fn (ffP a a)")] Inter_finite_elem 1);
by (auto_tac (claset() addIs [finite_fn], simpset()));
qed "finite_fnaa";

Goal "a ~: fn (fP b) ==> a ~: fna fP";
by (auto_tac (claset(), simpset() addsimps [fna_def]));
qed "not_fn_fna";


(* fresh names -- monotonicity *)

Goal "fresh a (fP b) ==> fresha a fP";
by (auto_tac (claset(), simpset() addsimps
              [fna_def, fresh_def, fresha_def]));
qed "fresh_mono";

Goal "fresha a (ffP b) ==> freshaa a ffP";
by (auto_tac (claset(), simpset() addsimps
              [fna_def, fnaa_def, fresha_def, freshaa_def]));
qed "fresha_mono";


(* depth of binders *)

Goal "doba (%x. .t.fP x) c <= n ==> doba fP c <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq1";

Goal "doba (%x. fa x<fb x>.fP x) c <= n ==> doba fP c <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq2";

Goal "doba (%x. fa x[y].ffP y x) c <= n ==> Suc (doba (ffP c) c) <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq3";

Goal "doba (%x. .#y. ffP y x) c <= n ==> Suc (doba (ffP c) c) <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq4";

Goal "doba (%x. fP x .+ fQ x) c <= n ==> doba fP c <= n & doba fQ c <= n";
by (auto_tac (claset() addDs [max_le1],
              simpset() addsimps [doba_def]));
qed "doba_leq5";

Goal "doba (%x. fP x .| fQ x) c <= n ==> doba fP c <= n & doba fQ c <= n";
by (auto_tac (claset() addDs [max_le1],
              simpset() addsimps [doba_def]));
qed "doba_leq6";

Goal "doba (%x. .[fa x.=fb x]fP x) c <= n ==> doba fP c <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq7";

Goal "doba (%x. .[fa x.~=fb x]fP x) c <= n ==> doba fP c <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq8";

Goal "doba (%x. .!fP x) c <= n ==> doba fP c <= n";
by (auto_tac (claset(), simpset() addsimps [doba_def]));
qed "doba_leq9";

Goalw [fna_def] "fn (In a fP) = {a} Un fna fP";
by (Auto_tac);
qed "fn3'";

Goalw [fna_def] "fn (Res fP) = fna fP";
by (Auto_tac);
qed "fn4'";

Delsimps [fn3,fn4];
Addsimps [fn3',fn4'];