src/HOL/Lambda/ParRed.ML

alist_rec and assoc are now defined using primrec and thus no longer
refer to the recursion combinator list_rec, which should be considered
internal.

(*  Title:      HOL/Lambda/ParRed.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1995 TU Muenchen

Properties of => and cd, in particular the diamond property of => and
confluence of beta.
*)

Addsimps par_beta.intrs;

val par_beta_cases = 
    map par_beta.mk_cases
       ["Var n => t", 
	"Abs s => Abs t",
	"(Abs s) $ t => u", 
	"s $ t => u", 
	"Abs s => t"];

AddSIs par_beta.intrs;
AddSEs par_beta_cases;

(*** beta <= par_beta <= beta^* ***)

Goal "(Var n => t) = (t = Var n)";
by (Blast_tac 1);
qed "par_beta_varL";
Addsimps [par_beta_varL];

Goal "t => t";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed"par_beta_refl";
Addsimps [par_beta_refl];
(* AddSIs [par_beta_refl]; causes search to blow up *)

Goal "beta <= par_beta";
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac beta.induct 1);
by (ALLGOALS(blast_tac (claset() addSIs [par_beta_refl])));
qed "beta_subset_par_beta";

Goal "par_beta <= beta^*";
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac par_beta.induct 1);
by (Blast_tac 1);
(* rtrancl_refl complicates the proof by increasing the branching factor*)
by (ALLGOALS (blast_tac (claset() delrules [rtrancl_refl]
				 addIs [rtrancl_into_rtrancl])));
qed "par_beta_subset_beta";

(*** => ***)

Goal "!t' n. t => t' --> lift t n => lift t' n";
by (induct_tac "t" 1);
by (ALLGOALS(fast_tac (claset() addss (simpset()))));
qed_spec_mp "par_beta_lift";
Addsimps [par_beta_lift];

Goal
  "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
by (induct_tac "t" 1);
  by (asm_simp_tac (addsplit(simpset())) 1);
 by (strip_tac 1);
 by (eresolve_tac par_beta_cases 1);
  by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [subst_subst RS sym]) 1);
 by (fast_tac (claset() addSIs [par_beta_lift] addss (simpset())) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed_spec_mp "par_beta_subst";

(*** Confluence (directly) ***)

Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
by (rtac (impI RS allI RS allI) 1);
by (etac par_beta.induct 1);
by (ALLGOALS(blast_tac (claset() addSIs [par_beta_subst])));
qed "diamond_par_beta";


(*** cd ***)

Goal "!t. s => t --> t => cd s";
by (res_inst_tac[("u","s")] cd.induct 1);
by (Auto_tac);
by (fast_tac (claset() addSIs [par_beta_subst]) 1);
qed_spec_mp "par_beta_cd";

(*** Confluence (via cd) ***)

Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
by (blast_tac (claset() addIs [par_beta_cd]) 1);
qed "diamond_par_beta2";

Goal "confluent(beta)";
by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
			     par_beta_subset_beta, beta_subset_par_beta]) 1);
qed"beta_confluent";