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