File WellFormed.ML


(* well-formed names *)

Goal "wfnaa ffa ==> wfna (ffa a)";
by (fast_tac (claset() addEs WFNAA.elims
                       addIs WFNA.intrs) 1);
qed "wfnaa_wfna1";

Goal "wfnaa ffa ==> wfna (%x. ffa x a)";
by (fast_tac (claset() addEs WFNAA.elims
                       addIs WFNA.intrs) 1);
qed "wfnaa_wfna2";

Goal "[| wfna fa ; fnna fa <= A ; a : A |] ==> fa a : A";
by (etac WFNA.elim 1);
by (auto_tac (claset(), simpset() addsimps [fnna_def]));
qed "fnna_subset";

Goal "[| fa a = fb a ; wfna fa ; wfna fb ; \
  \ a ~: fnna fa ; a ~: fnna fb |] \
  \ ==> fa b = fb b";
by (auto_tac (claset() addSEs WFNA.elims,
              simpset() addsimps [fnna_def]));
qed "fresh_names_eq";

Goal "[| fa a ~= fb a ; wfna fa ; wfna fb ; \
  \ a ~: fnna fa ; a ~: fnna fb ; b ~: fnna fa ; b ~: fnna fb |] \
  \ ==> fa b ~= fb b";
by (auto_tac (claset() addSEs WFNA.elims,
              simpset() addsimps [fnna_def]));
qed "fresh_names_ineq";


(* substitutions of names *)

Goalw [nsubst_def, fnna_def] "wfna fa ==> \
  \ a ~: fnna fa --> nsubst a b (fa a) = fa b";
by (etac WFNA.induct 1);
by (case_tac "aa=a" 2);
by (Auto_tac);
qed "lemma";

Goal "[| wfna fa ; a ~: fnna fa |] ==> nsubst a b (fa a) = fa b";
by (fast_tac (claset() addDs [lemma]) 1);
qed "wfna_nsubst";


(* well-formed processes *)

Goal "wfpa fP ==> wfp fP a";
by (etac WFPA.induct 1);
by (auto_tac (claset() addIs WFP.intrs, simpset()));
qed "wfpa_wfp_mono";

Goal "[| .0 = fP a ; wfpa fP |] ==> fP = (%x. .0)";
by (auto_tac (claset() addEs WFPA.elims, simpset()));
qed "wfpa_cases0";

Goal "[| .t.P = fP a ; wfpa fP |] ==> EX fP'. \
  \ wfpa fP' & fP = (%x. .t.fP' x)";
by (auto_tac (claset() addEs WFPA.elims, simpset()));
qed "wfpa_cases1";

Goal "[| b<c>.P = fP a ; wfpa fP |] ==> EX fb fc fP'. \
  \ wfna fb & wfna fc & wfpa fP' & \
  \ fP = (%x. fb x<fc x>.fP' x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases2";

Goal "[| b[y].fP' y = fP a ; wfpa fP |] ==> EX fb ffP. \
  \ wfna fb & (ALL b. wfpa ffP b) & (ALL b. wfpa (%x. ffP x b)) & \
  \ fP = (%x. fb x[y]. ffP y x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases3";

Goal "[| .#y. fP' y = fP a ; wfpa fP |] ==> EX ffP. \
  \ (ALL b. wfpa ffP b) & (ALL b. wfpa (%x. ffP x b)) & \
  \ fP = (%x. .#y. ffP y x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases4";

Goal "[| P .+ Q = fP a ; wfpa fP |] ==> EX fP' fQ. \
  \ wfpa fP' & wfpa fQ & fP = (%x. fP' x .+ fQ x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases5";

Goal "[| P .| Q = fP a ; wfpa fP |] ==> EX fP' fQ. \
  \ wfpa fP' & wfpa fQ & fP = (%x. fP' x .| fQ x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases6";

Goal "[| .[b.=c]P = fP a ; wfpa fP |] ==> EX fb fc fP'. \
  \ wfna fb & wfna fc & wfpa fP' & \
  \ fP = (%x. .[fb x.=fc x]fP' x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases7";

Goal "[| .[b.~=c]P = fP a ; wfpa fP |] ==> EX fb fc fP'. \
  \ wfna fb & wfna fc & wfpa fP' & \
  \ fP = (%x. .[fb x.~=fc x]fP' x)";
by (eresolve_tac WFPA.elims 1);
by (Auto_tac);
qed "wfpa_cases8";

Goal "[| .!P = fP a ; wfpa fP |] ==> EX fP'. \
  \ wfpa fP' & fP = (%x. .!fP' x)";
by (auto_tac (claset() addEs WFPA.elims, simpset()));
qed "wfpa_cases9";


(* free and fresh names of well-formed processes *)

Goal "wfpa fP ==> a : fn (fP c) & a ~= c --> a : fn (fP b)";
by (etac WFPA.induct 1);
by (auto_tac (claset() addSEs WFNA.elims,
              simpset() addsimps [fna_def]));
qed "lemma";

Goal "[| wfpa fP ; a : fn (fP c) ; a ~= c |] ==> a : fn (fP b)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "fn_fn";

Goal "wfpa fP ==> a ~: fn (fP b) & a ~= c --> a ~: fn (fP c)";
by (etac WFPA.induct 1);
by (auto_tac (claset() addSEs WFNA.elims,
              simpset() addsimps [fna_def]));
qed "lemma";

Goal "[| wfpa fP ; a ~: fn (fP b) ; a ~= c |] ==> a ~: fn (fP c)";
by (fast_tac (claset() addDs [lemma]) 1);
qed "not_fn_fn";

Goal "[| wfpa fP ; fresh a (fP b) ; a ~= c |] ==> fresh a (fP c)";
by (auto_tac (claset() addDs [not_fn_fn],
              simpset() addsimps [fresh_def]));
qed "fresh_fresh";

Goal "[| wfpa fP ; a : fn (fP c) ; a ~= c |] ==> a : fna fP";
by (auto_tac (claset() addDs [fn_fn],
              simpset() addsimps [fna_def]));
qed "fn_fna";

Goal "[| wfpa fP ; a ~: fna fP ; a ~= c |] ==> a ~: fn (fP c)";
by (auto_tac (claset() addDs [not_fn_fn],
              simpset() addsimps [fna_def]));
qed "not_fna_fn";

Goal "[| wfpa fP ; fresha a fP ; a ~= c |] ==> fresh a (fP c)";
by (auto_tac (claset() addDs [not_fna_fn],
              simpset() addsimps [fresh_def, fresha_def]));
qed "fresha_fresh";

Goalw [fnaa_def, fna_def]
"[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ a : fna (ffP c) ; a ~= c |] ==> a : fnaa ffP";
by (fast_tac (claset() addIs [fn_fn]) 1);
qed "fna_fnaa";

Goalw [fnaa_def, fna_def]
"[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ a ~: fnaa ffP ; a ~= c |] ==> a ~: fna (ffP c)";
by (Clarify_tac 1);
by (dres_inst_tac [("fP", "%x. ffP x ba")]
                  (rotate_prems 1 not_fn_fn) 1);
by (REPEAT (fast_tac (claset() addDs [not_fn_fna]) 1));
qed "not_fnaa_fna";

Goal "[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ freshaa a ffP ; a ~= c |] ==> fresha a (ffP c)";
by (auto_tac (claset() addDs [not_fnaa_fna],
              simpset() addsimps [freshaa_def, fresha_def]));
qed "freshaa_fresha";

Goal "[| A <= B ; x ~: B |] ==> x ~: A";
by (Auto_tac);
qed "rev_contra_subsetD";

Goal "[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
  \ fnaa ffP <= A |] ==> fna (ffP a) <= insert a A";
by (Clarify_tac 1);
by (dtac rev_contra_subsetD 1);
by (atac 1);
by (case_tac "x = a" 1);
by (atac 1);
by (fast_tac (claset() addSDs [not_fnaa_fna]) 1);
qed "fnaa_fna_subset";

Goalw [fna_def] "[| wfpa fP ; wfpa fQ |] \
  \ ==> fna (%x. fP x .| fQ x) = fna fP Un fna fQ";
by (auto_tac (claset() addDs [rotate_prems 1 not_fn_fn] addIs [fn_fn],
              simpset()));
qed "fna6";


(* depth of binders *)

Goal "[| ALL b a ba c d. dob (ffP b a) ba = dob (ffP b c) d ; \
  \ ALL b a ba c d. dob (ffP a b) ba = dob (ffP c b) d |] \
  \ ==> dob (ffP b a) b = dob (ffP d c) d";
by (eres_inst_tac [("x", "b")] allE 1);
by (eres_inst_tac [("x", "c")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (eres_inst_tac [("x", "b")] allE 1);
by (eres_inst_tac [("x", "b")] allE 1);
by (eres_inst_tac [("x", "d")] allE 1);
by (eres_inst_tac [("x", "c")] allE 1);
by (eres_inst_tac [("x", "d")] allE 1);
by (Auto_tac);
qed "lemma1";

Goal "[| ALL a b c d. dob (fP a) b = dob (fP c) d ; \
  \ ALL a b c d. dob (fQ a) b = dob (fQ c) d |] \
  \ ==> max (dob (fP a) b) (dob (fQ a) b) = \
  \ max (dob (fP c) d) (dob (fQ c) d)";
by (eres_inst_tac [("x", "a")] allE 1);
by (eres_inst_tac [("x", "a")] allE 1);
by (eres_inst_tac [("x", "b")] allE 1);
by (eres_inst_tac [("x", "b")] allE 1);
by (eres_inst_tac [("x", "c")] allE 1);
by (eres_inst_tac [("x", "c")] allE 1);
by (Auto_tac);
qed "lemma2";

Goal "wfpa fP ==> ALL a b c d. dob (fP a) b = dob (fP c) d";
by (etac WFPA.induct 1);
by (auto_tac (claset() addSEs [all_conjE] addIs [lemma1, lemma2],
              simpset() addsimps [doba_def]));
qed "lemma";

Goal "wfpa fP ==> dob (fP a) b = dob (fP c) d";
by (fast_tac (claset() addSDs [lemma]) 1);
qed "dob_vara";

Goal "wfpa fP ==> doba fP a = doba fP b";
by (fast_tac (claset() addSDs [dob_vara] addSss
              (simpset() addsimps [doba_def])) 1);
qed "doba_vara";

Goal "wfp P ==> dob P a = dob P b";
by (etac WFP.induct 1);
by (auto_tac (claset() addIs [dob_vara], simpset()));
qed "dob_var";

Goal "[| ALL b. wfpa ffP b ; ALL b. wfpa (%x. ffP x b) |] \
  \ ==> doba (ffP a) b = doba (ffP c) b";
by (fast_tac (claset() addSDs [dob_vara] addSss
              (simpset() addsimps [doba_def])) 1);
qed "lemma";

Goal "[| ALL b. wfpa ffP b ; ALL b. wfpa (%x. ffP x b) |] \
  \ ==> doba (ffP a) b = doba (ffP c) d";
by (forw_inst_tac [("a", "a"), ("b", "b"), ("c", "c")] lemma 1);
by (atac 1);
by (fast_tac (claset() addSDs [dob_vara] addSss
              (simpset() addsimps [doba_def])) 1);
qed "doba_varaa";