Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199401281420.AA17597@relay.cs.ruu.nl>
Subject: is this formula perhaps decidable?
To: info-hol@cs.uidaho.edu (hol mailing list)
Date: Fri, 28 Jan 1994 15:20:15 +0100 (MET)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 26875

Hi!

I'm trying to prove that if a relation U contains no cycle, then U is
a dag. Unfortunately I'm stuck and I thought that perhaps someone who
has more experience with graph theory may tell me whether my
proposition makes sense.

Here is the formula I'm trying to prove:

    "(!x:*A. ~TC U x x) ==> (!x. InDAG U x)"

TC U is the least transitive closure of U. InDAG U x means x is in the
dag induced by relation U.

In case, you need details all required definitions are given below.

Anyway, unfolding all definitions I come to the following second order
formula. Now I know FAUST only works for fisrt order formulas, but it
sometimes also works for second order. Unfortunately my HOL88 runs out
of stack when I tried it, perhaps someone can try it with new FAUST on
HOL90?

Here is the formula:

"(!x:*A.
   ~(!X.
      (!x y. U x y ==> X x y) /\ (!x y z. X x y /\ X y z ==> X x z) ==>
      X x x)) ==>
 (!x P.
   (!y.
     (!x.
       (!X.
         (!x y. U x y ==> X x y) /\ (!x y z. X x y /\ X y z ==> X x z) ==>
         X x y) ==>
       P x) ==>
     P y) ==>
   P x)";;


Kindly thank you for the help.

Wishnu Prasetya

---------------------------------------------------------------------------

Definitions:

let TRANS_DEF = new_definition (`TRANS_DEF`,
    "TRANS U = !(x:*) y z. U x y /\ U y z ==> U x z") ;;

let TC_DEF = new_definition
  (`TC_DEF`,
   "TC (U:*->*->bool) x y = !X. U SUBREL X /\ TRANS X ==> X x y") ;;

let MonoRel = ":*A->*A->bool" ;;

let TC_INDUCTIVE = new_definition
  (`TC_INDUCTIVE`,
   "TC_INDUCTIVE (U:^MonoRel) P = !y. (!x. (TC U) x y ==> P x) ==> P y") ;;

let InDAG = new_definition
  (`InDAG`,
   "InDAG (U:^MonoRel) x = !P. TC_INDUCTIVE U P ==> P x") ;;


     U SUBREL V   : U is a sub-relation of V
     REFL U       : U is a reflexive relation
     TRANS U      : U is a transitive relation
     Ri_TR U V    : V is the right transitive extension of U
     LDISJ W U    : U is a left disjunctive relation, wrt W
     DISJ W U     : U is a left and right over W disjunctive relation
     U ANDREL V   : the intersection of U and V


-------------------------------------------------------------------------------------%

let SUBREL_DEF = new_infix_definition (`SUBREL_DEF`,
    "SUBREL U V = !(x:*) (y:**). U x y ==> V x y") ;;

let REFL_DEF = new_definition (`REFL_DEF`,
    "REFL U = !(x:*). U x x") ;;


let LDISJ_DEF = new_definition (`LDISJ_DEF`,
    "LDISJ U =  !W (y:*B).
                  (?x:^Pred. W x) /\ (!x::W. U x y)
                  ==> U (??x::W. x) y") ;;

let DISJ_DEF = new_definition (`DISJ_DEF`,
   "DISJ W U =  !(f:*index->(*A->bool)) (g:*index->(*B->bool)).
                 (?i. W i) /\ (!i::W. U (f i) (g i))
                ==> U (??i::W. f i) (??i::W. g i)") ;;

let Ri_TR_DEF  = new_definition (`Ri_TR_DEF`,
    "Ri_TR U V = !(x:*A) y (z:*C). U x y /\ V y z ==> V x z") ;; 

let ANDREL_DEF = new_infix_definition (`ANDREL_DEF`,
    "ANDREL U V (x:*A) (y:*B) = U x y /\ V x y") ;;

%--------------------------------------------------------------------------------
   Some properties:
        - ANDREL produces a lower bound
        - SUBREL is transitive
--------------------------------------------------------------------------------%
        
let ANDREL_LB = prove_thm (`ANDREL_LB`,
    "!(U:^RelT) V. (U ANDREL V) SUBREL V",
     REWRITE_TAC [SUBREL_DEF; ANDREL_DEF]
     THEN TAUT_TAC) ;;

let SUBREL_TRANS = prove_thm (`SUBREL_TRANS`,
    "TRANS (SUBREL:^RelT->^RelT->bool)",
    REWRITE_TAC [TRANS_DEF; SUBREL_DEF]  
    THEN REPEAT STRIP_TAC  
    THEN REPEAT RES_TAC) ;;

%------------------------------------------------------------------------------
  Below are some simple disjuctivity properties.

    GEN_LDISJ    : a more generalized formulation of left disjuctivity
    GEN_RDISJ    : right disjuctivity
    SIMPLE_DISJ  : simple disjunctivity
    CANCEL       : calcelation law 

------------------------------------------------------------------------------%
 
let APP_TRANS_TAC U =
    MATCH_MP_TAC (REWRITE_RULE [TRANS_DEF] (ASSUME "TRANS ^U")) ;;

let APP_LDISJ_TAC U = 
    MATCH_MP_TAC (REWRITE_RULE [LDISJ_DEF] (ASSUME "LDISJ ^U")) ;;

let lemma1 = prove
  ("(??i:*index::W. f i) = (??x:^Pred::(\p. ?i. W i /\ (p = f i)). x)",
   REWRITE_TAC [RES_qOR]
   THEN CONV_TAC (FUN_EQ_CONV)
   THEN BETA_TAC THEN GEN_TAC
   THEN EQ_TAC THEN REPEAT STRIP_TAC
   THENL [EXISTS_TAC "(f:*index->^Pred) i"
          THEN ASM_REWRITE_TAC[]
          THEN EXISTS_TAC "i:*index"
          THEN ASM_REWRITE_TAC[] ;
          EXISTS_TAC "i':*index"
          THEN EVERY_ASSUM (\thm. REWRITE_TAC [SYM thm] ? ALL_TAC)
          THEN ASM_REWRITE_TAC []]) ;;

let lemma2 = 
    let lemma = ((SPEC "\p:^Pred. ?i:*index. W i /\ (p = f i)")
                o (REWRITE_RULE [LDISJ_DEF])
                o ASSUME) "LDISJ (U:^RelT)" in
    BETA_RULE(RESTRICT_SHIFT lemma) ;;


let LDISJ_GEN = prove_thm (`LDISJ_GEN`,
    "!(U:^RelT) W f q.
     (LDISJ U) /\
     (?i:*index.W i) /\ (!i::W. U (f i) q)
     ==>
     U (??i::W. f i) q",
    RESTRICT_DEF_TAC
    THEN REPEAT STRIP_TAC
    THEN REWRITE_TAC[lemma1]
    THEN MATCH_MP_TAC lemma2 THEN CONJ_TAC
    THENL [ EXISTS_TAC "(f:*index -> ^Pred) i"
            THEN EXISTS_TAC "i:*index"
            THEN ASM_REWRITE_TAC[] ;
            REPEAT STRIP_TAC THEN RES_TAC
            THEN ASM_REWRITE_TAC[] ]) ;;


let lemma = TAC_PROOF
  ((["(W:*index->bool) i"],"p = (??i:*index::W. p:^Pred)"),
    REWRITE_TAC [RES_qOR]
    THEN CONV_TAC FUN_EQ_CONV
    THEN BETA_TAC THEN GEN_TAC
    THEN EQ_TAC THEN REPEAT STRIP_TAC
    THEN EXISTS_TAC "i:*index"
    THEN ASM_REWRITE_TAC[]) ;;

let GEN_RDISJ = prove_thm (`GEN_RDISJ`,
    "!(U:^RelT) W f p.
     DISJ W U /\
     (?i:*index.W i) /\ (!i::W. U p (f i))
     ==>
     U p (??i::W. f i)",
     REWRITE_TAC [DISJ_DEF]
     THEN RESTRICT_DEF_TAC
     THEN REPEAT STRIP_TAC
     THEN XRULE_ASSUM_TAC (SPEC "\i:*index. p:^Pred")
     THEN XRULE_ASSUM_TAC BETA_RULE
     THEN SUBST1_TAC lemma
     THEN RES_TAC) ;;


let GEN_LDISJ = prove_thm (`GEN_LDISJ`,
    "!(U:^RelT) W f q.
     DISJ W U /\
     (?i:*index.W i) /\ (!i::W. U (f i) q)
     ==>
     U (??i::W. f i) q",
     REWRITE_TAC [DISJ_DEF]
     THEN RESTRICT_DEF_TAC
     THEN REPEAT STRIP_TAC
     THEN XRULE_ASSUM_TAC (SPECL ["f:*index->^Pred";
                                  "\i:*index. q:^Pred"])
     THEN XRULE_ASSUM_TAC BETA_RULE
     THEN SUBST1_TAC (SPEC "q:^Pred" (GEN_ALL lemma))
     THEN RES_TAC) ;;


let MYRULE = 
    RESTRICT_SHIFT  o (REWRITE_RULE [RES_qOR]) o
    (ISPECL ["\i. i => (p:^Pred) | r"; 
             "\i. i => (q:^Pred) | s"]) ;;
            
let lemma2 = prove (
    "(p:^Pred) OR q = (\s. ?i. (i => p | q) s)",
    REWRITE_TAC [pOR_DEF]
    THEN CONV_TAC FUN_EQ_CONV
    THEN BETA_TAC THEN GEN_TAC THEN EQ_TAC
    THEN STRIP_TAC
    THENL [ EXISTS_TAC "T" THEN ASM_REWRITE_TAC[] ;
            EXISTS_TAC "F" THEN ASM_REWRITE_TAC[] ;
            ASM_CASES_TAC "i:bool"
            THEN UNDISCH_TAC "(i => (p:^Pred) | q)x"
            THEN ASM_REWRITE_TAC[]
            THEN TAUT_TAC ]) ;;

let SIMPLE_DISJ = prove_thm (`SIMPLE_DISJ`,
    "!(U:^RelT) p q r s.
        DISJ (TT:bool->bool) U /\
        U p q /\ U r s
        ==>
        U (p OR r) (q OR s)",
     REWRITE_TAC [DISJ_DEF; TT_DEF]
     THEN REPEAT STRIP_TAC
     THEN XRULE_ASSUM_TAC MYRULE
     THEN REWRITE_TAC [lemma2]
     THEN FIRST_ASSUM MATCH_MP_TAC 
     THEN GEN_TAC
     THEN ASM_CASES_TAC "x:bool"
     THEN ASM_REWRITE_TAC[]) ;;
    
let CANCEL = prove_thm (`CANCEL`,
    "!(U:^RelT) p q r s.    
         TRANS U  /\ DISJ (TT:bool->bool) U /\
         U q q /\ U p (q OR r) /\ U r s
         ==>
         U p (q OR s)",
     REPEAT STRIP_TAC
     THEN APP_TRANS_TAC "U:^RelT"
     THEN EXISTS_TAC "(q:^Pred) OR r" 
     THEN ASM_REWRITE_TAC[]
     THEN MATCH_MP_TAC SIMPLE_DISJ
     THEN ASM_REWRITE_TAC[]) ;;

%---------------------------------------------------------------------------------
    The principle of reachability by bounded decrement:

    Given a transitive, left disjunctive, and IMP-containing relation -->:AxA,
          a well-founded relation <<:DxD
          a metric function M:A->D

    the principle says (informally!):

             !m. (p /\ M=m) --> ((p /\ M<m) \/ q)
           ---------------------------------------
                          p --> q

----------------------------------------------------------------------------------%

let MRel = ":*M->*M->bool" ;;
let Metric = ":*A->*M" ;;

let MK_ABS_CONV x trm = SYM (BETA_CONV "(\^x. ^trm) ^x") ;;

let lemma = prove
    ("((??x:*M::(\x. LESS x (y:*M)). p AND (\s:*A. M s = x)) OR q) =
      ((p AND (\s. LESS (M s) y)) OR q)",
     REWRITE_TAC (map snd (definitions `predicate`))
     THEN CONV_TAC FUN_EQ_CONV
     THEN GEN_TAC THEN BETA_TAC 
     THEN EQ_TAC THEN REPEAT STRIP_TAC
     THEN ASM_REWRITE_TAC[]
     THEN DISJ1_TAC
     THEN EXISTS_TAC "(M:^Metric) x" 
     THEN ASM_REWRITE_TAC[]) ;;

let lemma1 = prove
    ("~(?i:*. W i) ==> ((??i::W. (P i):^Pred) = FF)",
     (CONV_TAC o DEPTH_CONV) NOT_EXISTS_CONV
     THEN REWRITE_TAC [RES_qOR; FF_DEF]
     THEN STRIP_TAC
     THEN CONV_TAC FUN_EQ_CONV
     THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC 
     THEN REPEAT STRIP_TAC
     THEN ASM_REWRITE_TAC[]
     THEN RES_TAC) ;;


let BOUNDED_REACH_lemma  = prove
  ("!(LESS:^MRel) (M:^Metric) (U:^RelT) p q.
        ADMIT_WF_INDUCTION LESS /\        
        TRANS U /\ LDISJ U /\ DISJ (TT:bool->bool) U /\ 
        U q q /\
        (!m. U (p AND (\s. M s = m)) ((p AND (\s. LESS (M s) m)) OR q))
        ==>
        (!m. U (p AND (\s. M s = m)) q)",
    REWRITE_TAC [ADMIT_WF_INDUCTION]    
    THEN REPEAT GEN_TAC THEN STRIP_TAC
    THEN ((CONV_TAC o RAND_CONV o ABS_CONV) (MK_ABS_CONV "m:*M"))
    THEN FIRST_ASSUM MATCH_MP_TAC
    THEN BETA_TAC THEN REPEAT STRIP_TAC
    THEN APP_TRANS_TAC "U:^RelT"
    THEN EXISTS_TAC 
         "(??x:*M::(\x. LESS x (y:*M)). (p AND (\s:*A. M s = x))) OR q"
    THEN CONJ_TAC
         %---- Split the two transitive cases ---%
    THENL 
    [ %-- (1) --%
      ASM_REWRITE_TAC [lemma] ;
      %-- (2) --%
      ASM_CASES_TAC "?x. (\x. (LESS:^MRel) x y)x"
      THENL
      [ %-- 2.1 y is not bottom --%
        ((CONV_TAC o RAND_CONV o REWRITE_CONV) (SYM(SPEC_ALL pOR_REFL)))
        THEN MATCH_MP_TAC SIMPLE_DISJ
        THEN ASM_REWRITE_TAC[] 
        THEN (CONV_TAC o ONCE_DEPTH_CONV o RAND_CONV o ABS_CONV)
             (MK_ABS_CONV "x:*M")
        THEN MATCH_MP_TAC LDISJ_GEN
        THEN ASM_REWRITE_TAC[]
        THEN RESTRICT_DEF_TAC
        THEN ASM_REWRITE_TAC[] ;
        %-- 2.2 y is bottom --%
        (CONV_TAC o ONCE_DEPTH_CONV o RAND_CONV o ABS_CONV)
             (MK_ABS_CONV "x:*M")
        THEN IMP_RES_TAC lemma1
        THEN ASM_REWRITE_TAC[]
        THEN ASM_REWRITE_TAC [pOR_UNIT]]
    ])  ;;


let lemma2 = prove
   ("p = (??m:*M::TT. p AND (\s:*A. M s = m))",
     REWRITE_TAC [RES_qOR; pAND_DEF; TT_DEF]
     THEN CONV_TAC FUN_EQ_CONV
     THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC 
     THEN REPEAT STRIP_TAC
     THEN ASM_REWRITE_TAC[]
     THEN EXISTS_TAC "(M:^Metric) x"
     THEN REFL_TAC) ;;

let BOUNDED_REACH = prove_thm 
  (`BOUNDED_REACH`,
   "!(LESS:^MRel) (M:^Metric) (U:^RelT) p q.
        ADMIT_WF_INDUCTION LESS /\        
        TRANS U /\ LDISJ U /\ DISJ (TT:bool->bool) U /\ 
        U q q /\
        (!m. U (p AND (\s. M s = m)) ((p AND (\s. LESS (M s) m)) OR q))
        ==>
        U p q",
   REPEAT STRIP_TAC
   THEN SUBST1_TAC lemma2
   THEN ((CONV_TAC o ONCE_DEPTH_CONV o RAND_CONV o ABS_CONV)
         (MK_ABS_CONV "m:*M"))
   THEN MATCH_MP_TAC LDISJ_GEN
   THEN ASM_REWRITE_TAC[] THEN CONJ_TAC
   THENL
   [ %-- (1) --%
     EXISTS_TAC "i:*M" THEN REWRITE_TAC [TT_DEF] ;
     %-- (2) --%
     RESTRICT_DEF_TAC THEN REWRITE_TAC [TT_DEF]
     THEN IMP_RES_TAC BOUNDED_REACH_lemma]) ;;

%---------------------------------------------------------------------------------
    A special case of the reachability by bounded decrement principle is the
    following: 

             !m. (~p /\ M=m) --> M<m
           ----------------------------
                    true --> p

----------------------------------------------------------------------------------%

let BOUNDED_ALWAYS_REACH = prove_thm (
   `BOUNDED_ALWAYS_REACH`,
   "!(LESS:^MRel) (M:^Metric) U p.
        ADMIT_WF_INDUCTION LESS /\
        TRANS U /\ LDISJ U /\ DISJ (TT:bool->bool) U /\ 
        U p p /\
        (!m. U ((NOT p) AND (\s. M s = m)) ((\s. LESS (M s) m) OR p))
        ==> 
        U TT p",
    REPEAT STRIP_TAC
    THEN SUBST1_TAC (SYM(ISPEC "p:^Pred" pOR_REFL))
    THEN SUBST1_TAC (prove("TT=((p:^Pred) OR (NOT p))", pred_CYAN_TAC))
    THEN MATCH_MP_TAC SIMPLE_DISJ
    THEN ASM_REWRITE_TAC[] 
    THEN MATCH_MP_TAC BOUNDED_REACH
    THEN EXISTS_TAC "LESS:^MRel"
    THEN EXISTS_TAC "M:^Metric" 
    THEN ASM_REWRITE_TAC []
    THEN ASM_REWRITE_TAC 
         [ prove("(((NOT p) AND q) OR (p:^Pred)) = (q OR p)",
                  pred_CYAN_TAC)]) ;;

%---------------------------------------------------------------------------------

   PART II : least transitive and disjunctive closures.

   Some basic definitions:

      TC U     : the least transitive closure of U
      RTC U    : the least reflexive and transitive closure of U
      TDC U    : the least transitive and left disjuctive closure of U
      Ri_TDC U : the least right transitive and left disjuctive closure of U


   As will be shown latter, TDC = Ri_TDC. Ri_TDC provides a slightly 
   stronger induction hypothesis, which may be useful in some cases.

----------------------------------------------------------------------------------%


let RTC_DEF = new_definition
  (`RTC_DEF`,
   "RTC (U:*->*->bool) x y = !X. U SUBREL X /\ REFL X /\ TRANS X ==> X x y") ;;


let TDC_DEF = new_definition (`TDC_DEF`,
    "TDC U (x:^Pred) y = !X. (SUBREL U X) /\ (TRANS X) /\ (LDISJ X) ==> X x y") ;;

let Ri_TDC_DEF = new_definition (`Ri_TDC_DEF`,
    "Ri_TDC U (x:^Pred) y = !X. (SUBREL U X) /\ (Ri_TR U X) /\ (LDISJ X) ==> X x y") ;;

%------------------------------------------------------------------------------------
       TC U, RTC U, and TDC U all include U and transitive
       RTC U is reflexive and TDC U is left disjunctive
------------------------------------------------------------------------------------%

let TC_LIFT = prove_thm (`TC_LIFT`,
    "!(U:*->*->bool). SUBREL U (TC U)",
    REWRITE_TAC [SUBREL_DEF; TC_DEF]
    THEN REPEAT STRIP_TAC THEN RES_TAC) ;;

let RTC_LIFT = prove_thm (`RTC_LIFT`,
    "!(U:*->*->bool). SUBREL U (RTC U)",
    REWRITE_TAC [SUBREL_DEF; RTC_DEF]
    THEN REPEAT STRIP_TAC THEN RES_TAC) ;;

let TDC_LIFT = prove_thm (`TDC_LIFT`,
    "!(U:^RelT). SUBREL U (TDC U)",
    REWRITE_TAC [SUBREL_DEF; TDC_DEF]
    THEN REPEAT STRIP_TAC THEN RES_TAC) ;;

let TC_TRANS = prove_thm (`TC_TRANS`,
    "!(U:*->*->bool). TRANS (TC U)",
    REWRITE_TAC [TRANS_DEF; TC_DEF]
    THEN REPEAT STRIP_TAC THEN REPEAT RES_TAC) ;;

let RTC_TRANS = prove_thm (`RTC_TRANS`,
    "!(U:*->*->bool). TRANS (RTC U)",
    REWRITE_TAC [TRANS_DEF; RTC_DEF]
    THEN REPEAT STRIP_TAC THEN REPEAT RES_TAC) ;;

let TDC_TRANS = prove_thm (`TDC_TRANS`,
    "!(U:^RelT). TRANS (TDC U)",
    REWRITE_TAC [TRANS_DEF; TDC_DEF]
    THEN REPEAT STRIP_TAC THEN REPEAT RES_TAC) ;;

let TDC_Ri_TRANS = prove_thm (`TDC_Ri_TRANS`,
    "!(U:^RelT). Ri_TR U (TDC U)",
    REWRITE_TAC [Ri_TR_DEF]
    THEN REPEAT STRIP_TAC 
    THEN IMP_RES_TAC (REWRITE_RULE [SUBREL_DEF] TDC_LIFT)
    THEN IMP_RES_TAC (REWRITE_RULE [TRANS_DEF] TDC_TRANS)) ;;

let RTC_REFL = prove_thm (`RTC_REFL`,
    "!(U:*->*->bool). REFL (RTC U)",
    REWRITE_TAC [REFL_DEF; RTC_DEF]
    THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]) ;;

let TDC_LDISJ = prove_thm (`TDC_LDISJ`,
    "!(U:^RelT). LDISJ (TDC U)",
    REWRITE_TAC [LDISJ_DEF; TDC_DEF]
    THEN RESTRICT_DEF_TAC
    THEN REPEAT STRIP_TAC 
    THEN SUBGOAL_THEN "!x. W x ==> (X:^RelT) x y"
         (\thm. ASSUME_TAC thm) 
    THENL [ REPEAT STRIP_TAC THEN RES_TAC ; RES_TAC]) ;;

%--------------------------------------------------------------------------------
                           RTC includes TC
--------------------------------------------------------------------------------%

let TC_IMP_RTC = prove_thm (`TC_IMP_RTC`,
   "!(U:*->*->bool). (TC U) SUBREL (RTC U)",
    REWRITE_TAC [TC_DEF; SUBREL_DEF]
    THEN REPEAT STRIP_TAC
    THEN FIRST_ASSUM MATCH_MP_TAC
    THEN REWRITE_TAC [REWRITE_RULE [SUBREL_DEF] RTC_LIFT; RTC_TRANS]) ;;
 
%--------------------------------------------------------------------------------
   an induction princile for TDC:
      
   To prove that a relation X includes TDC U it suffices to show that
      
       (1) X includes U
       (2) TRANS X
       (3) DISJ X
      
--------------------------------------------------------------------------------%

let TDC_INDUCT1 = prove_thm (`TDC_INDUCT1`,
    "!(U:^RelT) X. SUBREL U X /\ TRANS X /\ LDISJ X ==> (TDC U) SUBREL X",
    REWRITE_TAC [SUBREL_DEF; TDC_DEF]
    THEN REPEAT STRIP_TAC
    THEN RES_TAC) ;;

let MK_2ABS_CONV p q (trm:term) =
    SYM (((ONCE_DEPTH_CONV BETA_CONV) 
          THENC BETA_CONV) "(\^p ^q. ^trm) ^p ^q") ;;

let TDC_INDUCT2 = prove_thm (`TDC_INDUCT2`,
    "!(U:^RelT) X.  
        U SUBREL ((TDC U) ANDREL X) /\ 
        TRANS ((TDC U) ANDREL X)    /\ 
        LDISJ ((TDC U) ANDREL X) 
        ==> (TDC U) SUBREL X",
    REWRITE_TAC [SUBREL_DEF; TRANS_DEF; LDISJ_DEF; ANDREL_DEF]
    THEN REPEAT GEN_TAC THEN STRIP_TAC
    THEN REPEAT GEN_TAC
    THEN MATCH_MP_TAC (REWRITE_RULE [TRANS_DEF; SUBREL_DEF] SUBREL_TRANS)
    THEN EXISTS_TAC "(TDC (U:^RelT)) ANDREL X"
    THEN REWRITE_TAC [ANDREL_DEF]
    THEN CONJ_TAC
    THENL [ ALL_TAC ; TAUT_TAC]
    THEN REPEAT GEN_TAC 
    THEN CONV_TAC (RAND_CONV (MK_2ABS_CONV "x:^Pred" "y:^Pred"))
    THEN MATCH_MP_TAC (REWRITE_RULE [SUBREL_DEF] TDC_INDUCT1)
    THEN REWRITE_TAC [TRANS_DEF; LDISJ_DEF]
    THEN BETA_TAC THEN REPEAT STRIP_TAC
    THEN RES_TAC) ;;


%------------------------------------------------------------------------------
   Some monotonicity properties of TDC:                 

     (1) if V includes U, then TDC V includes U 
     (2) TDC is monotonic wrt SUBREL  

------------------------------------------------------------------------------%

let TDC_SUBREL = prove_thm (`TDC_SUBREL`,
   "!(U:^RelT) V. (U SUBREL V) ==> (U SUBREL (TDC V))",
    REWRITE_TAC [SUBREL_DEF]
    THEN REPEAT STRIP_TAC
    THEN MATCH_MP_TAC (REWRITE_RULE [SUBREL_DEF] TDC_LIFT)
    THEN RES_TAC) ;;
    
let TDC_MONO = prove_thm (`TDC_MONO`,
    "!(U:^RelT) V. (U SUBREL V) ==> (TDC U) SUBREL (TDC V)",
    REPEAT STRIP_TAC 
    THEN MATCH_MP_TAC TDC_INDUCT1
    THEN REWRITE_TAC [TDC_TRANS; TDC_LDISJ]
    THEN MATCH_MP_TAC TDC_SUBREL
    THEN ASM_REWRITE_TAC[]) ;;

%-------------------------------------------------------------------------------
   Ri_TDC U is a closure of U, right transitive, and disjunctive
-------------------------------------------------------------------------------%

let Ri_TDC_LIFT = prove_thm (`Ri_TDC_LIFT`,
    "!(U:^RelT). SUBREL U (Ri_TDC U)",
    REWRITE_TAC [SUBREL_DEF; Ri_TDC_DEF]
    THEN REPEAT STRIP_TAC THEN RES_TAC) ;;

let Ri_TDC_Ri_TRANS = prove_thm (`Ri_TDC_Ri_TRANS`,
    "!(U:^RelT). Ri_TR U (Ri_TDC U)",
    REWRITE_TAC [Ri_TR_DEF; Ri_TDC_DEF]
    THEN REPEAT STRIP_TAC THEN REPEAT RES_TAC) ;;

let Ri_TDC_LDISJ = prove_thm (`Ri_TDC_LDISJ`,
    "!(U:^RelT). LDISJ (Ri_TDC U)",
    REWRITE_TAC [LDISJ_DEF; Ri_TDC_DEF]
    THEN RESTRICT_DEF_TAC
    THEN REPEAT STRIP_TAC 
    THEN SUBGOAL_THEN "!x. W x ==> (X:^RelT) x y"
         (\thm. ASSUME_TAC thm) 
    THENL [ REPEAT STRIP_TAC THEN RES_TAC ; RES_TAC]) ;;

%--------------------------------------------------------------------------------
                  an induction principle for Ri_TDC
--------------------------------------------------------------------------------%
 
let Ri_TDC_INDUCT1 = prove_thm (`Ri_TDC_INDUCT1`,
    "!(U:^RelT) X. (SUBREL U X) /\ (Ri_TR U X) /\ (LDISJ X) 
       ==> (SUBREL (Ri_TDC U) X)",
    REWRITE_TAC [SUBREL_DEF; Ri_TDC_DEF]
    THEN REPEAT STRIP_TAC
    THEN RES_TAC) ;;

%--------------------------------------------------------------------------------
                 another induction principle for Ri_TDC
--------------------------------------------------------------------------------%

let Ri_TDC_INDUCT2 = prove_thm (`Ri_TDC_INDUCT2`,
    "!(U:^RelT) X. 
       (U SUBREL X)  /\ 
       (!x y z. U x y /\ X y z /\ Ri_TDC U y z ==> X x z)  /\
       (!W y. (?x. W x) /\ (!x::W. X x y /\ Ri_TDC U x y) ==> X (??x::W.x) y)
       ==>
       ((Ri_TDC U) SUBREL X)",
    REPEAT STRIP_TAC
    THEN MATCH_MP_TAC (REWRITE_RULE [TRANS_DEF] SUBREL_TRANS)
    THEN EXISTS_TAC "(Ri_TDC U) ANDREL (X:^RelT)"
    THEN REWRITE_TAC[ANDREL_LB]  
    THEN MATCH_MP_TAC Ri_TDC_INDUCT1 
    THEN UNDISCH_ALL_TAC
    THEN REWRITE_TAC [SUBREL_DEF; ANDREL_DEF; Ri_TR_DEF; LDISJ_DEF]
    THEN RESTRICT_DEF_TAC
    THEN REPEAT STRIP_TAC
    THENL [ IMP_RES_TAC (REWRITE_RULE [SUBREL_DEF] Ri_TDC_LIFT) ;
            RES_TAC ;
            IMP_RES_TAC (REWRITE_RULE [Ri_TR_DEF] Ri_TDC_Ri_TRANS) ;
            RES_TAC ;
            MATCH_MP_TAC (REWRITE_RULE [LDISJ_DEF] Ri_TDC_LDISJ)
            THEN CONJ_TAC
            THENL [ EXISTS_TAC "x:^Pred" THEN ASM_REWRITE_TAC[] ; ALL_TAC]
            THEN RESTRICT_DEF_TAC
            THEN REPEAT STRIP_TAC THEN RES_TAC ;
            FIRST_ASSUM MATCH_MP_TAC
            THEN CONJ_TAC
            THENL [ EXISTS_TAC "x:^Pred" THEN ASM_REWRITE_TAC[] ; ALL_TAC]
            THEN REPEAT STRIP_TAC THEN RES_TAC ]) ;;

%-------------------------------------------------------------------------------
   Ri_TDC U is also transitive (so, not only right-transitive wrt U)
-------------------------------------------------------------------------------%

let lemma = prove 
           ("((X (x:*) (y:*)) /\ X y z ==> X x z) =
             (X x y ==> ((\x y. X y z ==> X x z) x y))",
            BETA_TAC THEN TAUT_TAC) ;;

let Ri_TDC_TRANS = prove_thm (`Ri_TDC_TRANS`,
    "!(U:^RelT). TRANS (Ri_TDC U)",
    REWRITE_TAC [TRANS_DEF; lemma]
    THEN REPEAT GEN_TAC
    THEN MATCH_MP_TAC (REWRITE_RULE [SUBREL_DEF] Ri_TDC_INDUCT1)
    THEN BETA_TAC THEN REPEAT CONJ_TAC
    THENL [ REPEAT STRIP_TAC
            THEN IMP_RES_TAC (REWRITE_RULE [Ri_TR_DEF] Ri_TDC_Ri_TRANS) ;
            REWRITE_TAC [Ri_TR_DEF]
            THEN BETA_TAC THEN REPEAT STRIP_TAC
            THEN RES_TAC
            THEN IMP_RES_TAC (REWRITE_RULE [Ri_TR_DEF] Ri_TDC_Ri_TRANS) ;
            REWRITE_TAC [LDISJ_DEF]
            THEN BETA_TAC THEN RESTRICT_DEF_TAC
            THEN REPEAT STRIP_TAC
            THEN SUBGOAL_THEN "!x::W. Ri_TDC (U:^RelT) x z"
                 (\thm. ASSUME_TAC thm)
            THENL [ RESTRICT_DEF_TAC 
                    THEN REPEAT STRIP_TAC THEN RES_TAC ;
                    IMP_RES_TAC (REWRITE_RULE [LDISJ_DEF] Ri_TDC_LDISJ)]
          ]) ;;

%--------------------------------------------------------------------------------
                    TDC is equal to Ri_TDC
--------------------------------------------------------------------------------%
 
let Ri_TDC_IMP_TDC = prove
  ("(Ri_TDC (U:^RelT)) SUBREL (TDC U)",
   MATCH_MP_TAC Ri_TDC_INDUCT1
   THEN REWRITE_TAC [TDC_LIFT; TDC_Ri_TRANS; TDC_LDISJ]) ;;

let TDC_IMP_Ri_TDC = prove
  ("(TDC (U:^RelT)) SUBREL (Ri_TDC U)",
   MATCH_MP_TAC TDC_INDUCT1
   THEN REWRITE_TAC [Ri_TDC_LIFT; Ri_TDC_TRANS; Ri_TDC_LDISJ]) ;;

let TDC_EQU_Ri_TDC = prove_thm (`TDC_EQU_Ri_TDC`,
   "(TDC:^RelT -> ^RelT) = Ri_TDC",
    REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC)
    THEN EQ_TAC
    THEN REWRITE_TAC (map (\thm. REWRITE_RULE [SUBREL_DEF] thm)
                          [Ri_TDC_IMP_TDC ; TDC_IMP_Ri_TDC])) ;; 
    
%--------------------------------------------------------------------------------------
                the double induction principle for Ri_TDC
--------------------------------------------------------------------------------------%

let XX = "\(r:^Pred) (s:^Pred) (p:^Pred) (q:^Pred). ri_TDC (U:^RelT) p q /\ X p q r s" ;;
let Type_of_X  = ":^Pred->^Pred->^Pred->^Pred->bool" ;;

let DOUBLE_INDUCT_ante =
    "(!p q r s. (X:^Type_of_X) p q r s = X r s p q) /\
     (!p q r s. U p q ==> X p q r s) /\
     (!W q r s. 
         (?p. W p) /\ (!p :: W. Ri_TDC U p q /\ X p q r s) 
         ==> X (?? p :: W. p) q r s) /\   
     (!p q r u v w.  
         U p q /\ U u v /\ Ri_TDC U q r /\  Ri_TDC U v w /\
         X p r v w /\ X u w q r /\ X q r v w 
         ==> X p r u w)" ;;

let DISJ_TAC x =
    FIRST_ASSUM (\thm. MATCH_MP_TAC (SPEC "W:^Pred->bool" thm)) 
    THEN CONJ_TAC
    THENL [ EXISTS_TAC x THEN ASM_REWRITE_TAC[] ; ALL_TAC ] 
    THEN RESTRICT_DEF_TAC THEN REPEAT STRIP_TAC
    THEN XRULE_ASSUM_TAC RESTRICT_SHIFT THEN OLD_RES_TAC ;;

let DOUBLE_INDUCT_thm = prove(
      "^DOUBLE_INDUCT_ante
     ==>
     (Ri_TDC (U:^RelT)) SUBREL 
         ((\p q. (Ri_TDC U) SUBREL (\r s. X p q r s)))",
    REPEAT STRIP_TAC
    THEN MATCH_MP_TAC Ri_TDC_INDUCT2
    THEN REWRITE_TAC [Ri_TR_DEF; LDISJ_DEF; ANDREL_DEF] 
    THEN BETA_TAC
    THEN REPEAT CONJ_TAC THEN REPEAT STRIP_TAC
    THENL 
    [ %-- (1) Lift Case ---------------%
      REWRITE_TAC [SUBREL_DEF; ANDREL_DEF]
      THEN BETA_TAC THEN REPEAT STRIP_TAC 
      THEN XRULE_ASSUM_TAC (SPECL ["x:^Pred"; "y:^Pred"; "x':^Pred"; "y':^Pred"])
      THEN OLD_RES_TAC ;
      %--- (2) transitivity case ------%
      MATCH_MP_TAC Ri_TDC_INDUCT2
      THEN UNDISCH_ALL_TAC
      THEN REWRITE_TAC [SUBREL_DEF; ANDREL_DEF; DISJ_DEF; Ri_TR_DEF] THEN BETA_TAC 
      THEN REPEAT STRIP_TAC
      THENL 
      [ %-- (2.1) Lift Case ---------------%
        XRULE_ASSUM_TAC (SPECL ["x':^Pred"; "y':^Pred"; "x:^Pred"; "z:^Pred"])
        THEN OLD_RES_TAC ;
        %--- (2.2) transitivity case ------%
        IMP_RES_TAC (REWRITE_RULE [Ri_TR_DEF] Ri_TDC_Ri_TRANS)
        THEN REPEAT OLD_RES_TAC ;
        %--- (2.3) disjunctive case ------%
        EVERY_ASSUM (\thm. ONCE_REWRITE_TAC [thm])
        THEN DISJ_TAC "x':^Pred" ] ;
      %-- (3) Disjunctivity case --------%
      REWRITE_TAC [SUBREL_DEF]
      THEN REPEAT STRIP_TAC THEN BETA_TAC
      THEN DISJ_TAC "x:^Pred"
      THEN XRULE_ASSUM_TAC (BETA_RULE o (REWRITE_RULE [SUBREL_DEF]))
      THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] ]) ;;

let Ri_TDC_DOUBLE_INDUCT = prove_thm (`Ri_TDC_DOUBLE_INDUCT`,
    "!(U:^RelT) X. 
     ^DOUBLE_INDUCT_ante
     ==>
     (!p q r s. Ri_TDC U p q /\ Ri_TDC U r s ==> X p q r s)",
     REPEAT STRIP_TAC
     THEN IMP_RES_TAC (BETA_RULE (REWRITE_RULE [SUBREL_DEF] DOUBLE_INDUCT_thm))) ;;

close_theory () ;;
%------------------------------------------------------------------------------------
  
   Written by Wishnu Prasetya
   Dept. of Computer Science,
   Utrecht University
   Email : wishnu@cs.ruu.nl

------------------------------------------------------------------------------------%