1 module DerivedRules where
    2 
    3 import Type_defs
    4 
    5 import Kernel
    6 
    7 import Core_datatype
    8 
    9 import Build_Tm
   10 
   11 import Edlib
   12 
   13 import Parse
   14 
   15 import Sub_Core1
   16 
   17 import Sub_Core2
   18 
   19 import Sub_Core3
   20 
   21 import Sub_Core4
   22 
   23 import Vtslib
   24 
   25 conj_thm_trm 
   26         = Binder Forall (Symbol_dec (Constant Bool' [] []) [])
   27           ( Binder Forall (Symbol_dec (Constant Bool' [] []) [])
   28           ( Binder Imp (Symbol_dec (Sym 1 0 [] []) [])
   29           ( Binder Imp (Symbol_dec (Sym 1 0 [] []) [])
   30           ( Binary' And (Sym 3 0 [] []) (Sym 2 0 [] []) [] []) [] [])
   31             [] []) [] []) [] []
   32 
   33 disj_thm_trm 
   34         = Binder Forall (Symbol_dec (Constant Bool' [] []) [])
   35           ( Binder Forall (Symbol_dec (Constant Bool' [] []) [])
   36           ( Binder Forall (Symbol_dec (Constant Bool' [] []) [])
   37           ( Binder Imp (Symbol_dec 
   38             (Binary' Or (Sym 2 0 [] []) (Sym 1 0 [] []) [] []) [])
   39             ( Binder Imp (Symbol_dec (Binder Imp (Symbol_dec (Sym 3 0 [] []) [])
   40             ( Sym 2 0 [] []) [] []) [])
   41             ( Binder Imp (Symbol_dec (Binder Imp (Symbol_dec (Sym 3 0 [] []) [])
   42             (Sym 3 0 [] []) [] []) []) (Sym 3 0 [] []) [] [])
   43             [] []) [] []) [] []) [] []) [] []
   44 
   45 
   46 conj_thm = taut (trm_to_Trm empty conj_thm_trm)
   47 
   48 
   49 
   50 disj_thm = taut (trm_to_Trm empty disj_thm_trm)
   51 
   52 
   53 find_trms :: (Int -> ITrm -> Bool) -> (Int -> ITrm -> ITrm) -> ITrm 
   54                                    -> (ITrm, [[Int]])
   55 
   56 find_trms p f tm 
   57         = (tm', map (\ (_,iL) -> iL) iLL) 
   58           where
   59           find n iL tm | p n tm    = [(n,iL)] 
   60                        | otherwise = find' n iL tm
   61         
   62           find' n iL (App tm1 tm2 _ _) 
   63                 = find n (iL <: 0) tm1 ++ 
   64                   find n (iL <: 1) tm2
   65 
   66           find' n iL (Pair tm1 tm2 tm3 _ _) 
   67                 = find n (iL <: 0) tm1 ++ 
   68                   find n (iL <: 1) tm2 ++
   69                   find n (iL <: 2) tm3
   70 
   71           find' n iL (Binder q dc tm _ _) 
   72                 = find_dec n (iL <: 0) dc ++
   73                   find (n+1) (iL <: 1) tm
   74 
   75           find' n iL (Unary _ tm _ _) 
   76                 = find n (iL <: 0) tm
   77 
   78           find' n iL (Binary' _ tm1 tm2 _ _) 
   79                 = find n (iL <: 0) tm1 ++
   80                   find n (iL <: 1) tm2
   81 
   82           find' n iL (Cond dc tm1 tm2 _ _) 
   83                 = find_dec n (iL <: 0) dc ++
   84                   find (n+1) (iL <: 1) tm1 ++
   85                   find (n+1) (iL <: 2) tm2 
   86 
   87           find' n iL (Recurse tmL tm _ _) 
   88                 = concat (map' (\ i tm -> find n (iL <: i) tm) tmL)
   89         
   90           find' _ _ _ = []
   91 
   92 
   93           find_dec n iL (Symbol_dec tm _) 
   94                 = find n (iL <: 0) tm
   95 
   96           find_dec n iL (Axiom_dec tm _) 
   97                 = find n (iL <: 0) tm
   98 
   99           find_dec n _ _ = []
  100 
  101 
  102 
  103           lift_fn tm (n,iL) 
  104                 = replace_trm tm (f n subtm) iL 
  105                   where
  106                   (subtm,_) = select_trm tm iL
  107 
  108           iLL = find 0 [] tm
  109 
  110           tm' = foldl lift_fn  tm iLL
  111 
  112 
  113 {-
  114 (******************************************************************************)
  115 (*                                                                            *)
  116 (*                 --------- conj                                             *)
  117 (*                                                                            *)
  118 (******************************************************************************)
  119 -}
  120 
  121 conj th1 th2 
  122         = th6 
  123           where
  124           sg = sgn_of_Thm th1
  125           th3 = specialise (weaken sg conj_thm) (typ_of_Thm th1)
  126           th4 = specialise th3 (typ_of_Thm th2)
  127           th5 = modus_ponens th4 th1
  128           th6 = modus_ponens th5 th2
  129 
  130 
  131 
  132 disj th1 th2 th3 
  133         = th8 
  134           where
  135           sg = sgn_of_Thm th1
  136           th3 = specialise (weaken sg disj_thm) (typ_of_Thm th1)
  137           th4 = specialise th3 (typ_of_Thm th2)
  138           th5 = specialise th4 (typ_of_Thm th3)
  139           th6 = modus_ponens th5 th1
  140           th7 = modus_ponens th6 th2
  141           th8 = modus_ponens th7 th3
  142 
  143 
  144 
  145 find_betas :: ITrm -> (ITrm, [[Int]])
  146 
  147 find_betas 
  148         = find_trms is_beta_red do_beta_red 
  149           where
  150           is_beta_red _ (App (Binder Lambda _ _ _ _) _ _ _) = True
  151           is_beta_red _ _ = False
  152           do_beta_red _ (App (Binder Lambda dc tm1 _ _) tm2 _ _) 
  153                 = subst_trm dc tm1 tm2
  154 
  155 rep_beta = foldl beta_rw
  156