src/CCL/Trancl.ML

Installation of new simplfier. Previously appeared to set up the old
simplifier to rewrite with the partial ordering [=, something not possible
with the new simplifier. But such rewriting appears not to have actually
been used, and there were few complications. In terms.ML setloop was used
to avoid infinite rewriting with the letrec rule. Congruence rules were
deleted, and an occasional SIMP_TAC had to become asm_simp_tac.

(*  Title: 	CCL/trancl
    ID:         $Id$

For trancl.thy.

Modified version of
    Title: 	HOL/trancl.ML
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

*)

open Trancl;

(** Natural deduction for trans(r) **)

val prems = goalw Trancl.thy [trans_def]
    "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
val transI = result();

val major::prems = goalw Trancl.thy [trans_def]
    "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
by (cut_facts_tac [major] 1);
by (fast_tac (FOL_cs addIs prems) 1);
val transD = result();

(** Identity relation **)

goalw Trancl.thy [id_def] "<a,a> : id";  
by (rtac CollectI 1);
by (rtac exI 1);
by (rtac refl 1);
val idI = result();

val major::prems = goalw Trancl.thy [id_def]
    "[| p: id;  !!x.[| p = <x,x> |] ==> P  \
\    |] ==>  P";  
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (eresolve_tac prems 1);
val idE = result();

(** Composition of two relations **)

val prems = goalw Trancl.thy [comp_def]
    "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
by (fast_tac (set_cs addIs prems) 1);
val compI = result();

(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
val prems = goalw Trancl.thy [comp_def]
    "[| xz : r O s;  \
\       !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
\    |] ==> P";
by (cut_facts_tac prems 1);
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
val compE = result();

val prems = goal Trancl.thy
    "[| <a,c> : r O s;  \
\       !!y. [| <a,y>:s;  <y,c>:r |] ==> P \
\    |] ==> P";
by (rtac compE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1));
val compEpair = result();

val comp_cs = set_cs addIs [compI,idI] 
		       addEs [compE,idE] 
		       addSEs [pair_inject];

val prems = goal Trancl.thy
    "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
by (cut_facts_tac prems 1);
by (fast_tac comp_cs 1);
val comp_mono = result();

(** The relation rtrancl **)

goal Trancl.thy "mono(%s. id Un (r O s))";
by (rtac monoI 1);
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
val rtrancl_fun_mono = result();

val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);

(*Reflexivity of rtrancl*)
goal Trancl.thy "<a,a> : r^*";
br (rtrancl_unfold RS ssubst) 1;
by (fast_tac comp_cs 1);
val rtrancl_refl = result();

(*Closure under composition with r*)
val prems = goal Trancl.thy
    "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
br (rtrancl_unfold RS ssubst) 1;
by (fast_tac (comp_cs addIs prems) 1);
val rtrancl_into_rtrancl = result();

(*rtrancl of r contains r*)
val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
by (rtac prem 1);
val r_into_rtrancl = result();


(** standard induction rule **)

val major::prems = goal Trancl.thy 
  "[| <a,b> : r^*; \
\     !!x. P(<x,x>); \
\     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
\  ==>  P(<a,b>)";
by (rtac (major RS (rtrancl_def RS def_induct)) 1);
by (rtac rtrancl_fun_mono 1);
by (fast_tac (comp_cs addIs prems) 1);
val rtrancl_full_induct = result();

(*nice induction rule*)
val major::prems = goal Trancl.thy
    "[| <a,b> : r^*;    \
\       P(a); \
\	!!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]  \
\     ==> P(b)";
(*by induction on this formula*)
by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1);
(*now solve first subgoal: this formula is sufficient*)
by (fast_tac FOL_cs 1);
(*now do the induction*)
by (resolve_tac [major RS rtrancl_full_induct] 1);
by (fast_tac (comp_cs addIs prems) 1);
by (fast_tac (comp_cs addIs prems) 1);
val rtrancl_induct = result();

(*transitivity of transitive closure!! -- by induction.*)
goal Trancl.thy "trans(r^*)";
by (rtac transI 1);
by (res_inst_tac [("b","z")] rtrancl_induct 1);
by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
val trans_rtrancl = result();

(*elimination of rtrancl -- by induction on a special formula*)
val major::prems = goal Trancl.thy
    "[| <a,b> : r^*;  (a = b) ==> P; \
\	!!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
\    ==> P";
by (subgoal_tac "a = b  | (EX y. <a,y> : r^* & <y,b> : r)" 1);
by (rtac (major RS rtrancl_induct) 2);
by (fast_tac (set_cs addIs prems) 2);
by (fast_tac (set_cs addIs prems) 2);
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
val rtranclE = result();


(**** The relation trancl ****)

(** Conversions between trancl and rtrancl **)

val [major] = goalw Trancl.thy [trancl_def]
    "[| <a,b> : r^+ |] ==> <a,b> : r^*";
by (resolve_tac [major RS compEpair] 1);
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
val trancl_into_rtrancl = result();

(*r^+ contains r*)
val [prem] = goalw Trancl.thy [trancl_def]
   "[| <a,b> : r |] ==> <a,b> : r^+";
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
val r_into_trancl = result();

(*intro rule by definition: from rtrancl and r*)
val prems = goalw Trancl.thy [trancl_def]
    "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
by (REPEAT (resolve_tac ([compI]@prems) 1));
val rtrancl_into_trancl1 = result();

(*intro rule from r and rtrancl*)
val prems = goal Trancl.thy
    "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+";
by (resolve_tac (prems RL [rtranclE]) 1);
by (etac subst 1);
by (resolve_tac (prems RL [r_into_trancl]) 1);
by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1);
by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
val rtrancl_into_trancl2 = result();

(*elimination of r^+ -- NOT an induction rule*)
val major::prems = goal Trancl.thy
    "[| <a,b> : r^+;  \
\       <a,b> : r ==> P; \
\	!!y.[| <a,y> : r^+;  <y,b> : r |] ==> P  \
\    |] ==> P";
by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+  &  <y,b> : r)" 1);
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
by (etac rtranclE 1);
by (fast_tac comp_cs 1);
by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1);
val tranclE = result();

(*Transitivity of r^+.
  Proved by unfolding since it uses transitivity of rtrancl. *)
goalw Trancl.thy [trancl_def] "trans(r^+)";
by (rtac transI 1);
by (REPEAT (etac compEpair 1));
by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
by (REPEAT (assume_tac 1));
val trans_trancl = result();

val prems = goal Trancl.thy
    "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
val trancl_into_trancl2 = result();