impconv.ml

   1 (* ========================================================================= *)
   2 (* Implicational conversions, implicational rewriting and target rewriting.  *)
   3 (*                                                                           *)
   4 (*   (c) Copyright, Vincent Aravantinos, 2012-2013                           *)
   5 (*                  Analysis and Design of Dependable Systems                *)
   6 (*                  fortiss GmbH, Munich, Germany                            *)
   7 (*                                                                           *)
   8 (*       Formerly:  Hardware Verification Group,                             *)
   9 (*                  Concordia University                                     *)
  10 (*                                                                           *)
  11 (*           Contact: <vincent.aravantinos@fortiss.org>                      *)
  12 (* ========================================================================= *)
  13
  14 let IMP_REWRITE_TAC,TARGET_REWRITE_TAC,HINT_EXISTS_TAC,
  15     SEQ_IMP_REWRITE_TAC,CASE_REWRITE_TAC =
  16
  17 let I = fun x -> x in
  18
  19 (* Same as [UNDISCH] but also returns the undischarged term *)
  20 let UNDISCH_TERM th =
  21   let p = (fst o dest_imp o concl) th in
  22   p,UNDISCH th in
  23
  24 (* Same as [UNDISCH_ALL] but also returns the undischarged terms *)
  25 let rec UNDISCH_TERMS th =
  26   try
  27     let t,th' = UNDISCH_TERM th in
  28     let ts,th'' = UNDISCH_TERMS th' in
  29     t::ts,th''
  30   with Failure _ -> [],th in
  31
  32 (* Comblies the function [f] to the conclusion of an implicational theorem. *)
  33 let MAP_CONCLUSION f th =
  34   let p,th = UNDISCH_TERM th in
  35   DISCH p (f th) in
  36
  37 let strip_conj = binops `(/\)` in
  38
  39 (* For a list [f1;...;fk], returns the first [fi x] that succeeds. *)
  40 let rec tryfind_fun fs x =
  41   match fs with
  42   |[] -> failwith "tryfind_fun"
  43   |f::fs' -> try f x with Failure _ -> tryfind_fun fs' x in
  44
  45 (* Same as [mapfilter] but also provides the rank of the iteration as an
  46  * argument to [f]. *)
  47 let mapfilteri f =
  48   let rec self i = function
  49     |[] -> []
  50     |h::t ->
  51         let rest = self (i+1) t in
  52         try f i h :: rest with Failure _ -> rest
  53   in
  54   self 0 in
  55
  56 let list_of_option = function None -> [] | Some x -> [x] in
  57
  58 let try_list f x = try f x with Failure _ -> [] in
  59
  60 (* A few constants. *)
  61 let A_ = `A:bool` and B_ = `B:bool` and C_ = `C:bool` and D_ = `D:bool` in
  62 let T_ = `T:bool` in
  63
  64 (* For a term t, builds `t ==> t` *)
  65 let IMP_REFL =
  66   let lem = TAUT `A ==> A` in
  67   fun t -> INST [t,A_] lem in
  68
  69 (* Conversion version of [variant]:
  70  * Given variables [v1;...;vk] to avoid and a term [t],
  71  * returns [|- t = t'] where [t'] is the same as [t] without any use of the
  72  * variables [v1;...;vk].
  73  *)
  74 let VARIANT_CONV av t =
  75   let vs = variables t in
  76   let mapping = filter (fun (x,y) -> x <> y) (zip vs (variants av vs)) in
  77   DEPTH_CONV (fun u -> ALPHA_CONV (assoc (bndvar u) mapping) u) t in
  78
  79 (* Rule version of [VARIANT_CONV] *)
  80 let VARIANT_RULE = CONV_RULE o VARIANT_CONV in
  81
  82 (* Discharges the first hypothesis of a theorem. *)
  83 let DISCH_HD th = DISCH (hd (hyp th)) th in
  84
  85 (* Rule version of [REWR_CONV] *)
  86 let REWR_RULE = CONV_RULE o REWR_CONV in
  87
  88 (* Given a list [A1;...;Ak] and a theorem [th],
  89  * returns [|- A1 /\ ... /\ Ak ==> th].
  90  *)
  91 let DISCH_IMP_IMP =
  92   let f = function
  93     |[] -> I
  94     |t::ts -> rev_itlist (fun t -> REWR_RULE IMP_IMP o DISCH t) ts o DISCH t
  95   in
  96   f o rev in
  97
  98 (* Given a term [A /\ B] and a theorem [th], returns [|- A ==> B ==> th]. *)
  99 let rec DISCH_CONJ t th =
 100   try
 101     let t1,t2 = dest_conj t in
 102     REWR_RULE IMP_IMP (DISCH_CONJ t1 (DISCH_CONJ t2 th))
 103   with Failure _ -> DISCH t th in
 104
 105 (* Specializes all the universally quantified variables of a theorem,
 106  * and returns both the theorem and the list of variables.
 107  *)
 108 let rec SPEC_VARS th =
 109   try
 110     let v,th' = SPEC_VAR th in
 111     let vs,th'' = SPEC_VARS th' in
 112     v::vs,th''
 113   with Failure _ -> [],th in
 114
 115 (* Comblies the function [f] to the body of a universally quantified theorem. *)
 116 let MAP_FORALL_BODY f th =
 117   let vs,th = SPEC_VARS th in
 118   GENL vs (f th) in
 119
 120 (* Given a theorem of the form [!xyz. P ==> !uvw. C] and a function [f],
 121  * return [!xyz. P ==> !uvw. f C].
 122  *)
 123 let GEN_MAP_CONCLUSION = MAP_FORALL_BODY o MAP_CONCLUSION o MAP_FORALL_BODY in
 124
 125 (* Turn a theorem of the form [x ==> y /\ z] into [(x==>y) /\ (x==>z)].
 126  * Also deals with universal quantifications if necessary
 127  * (e.g., [x ==> !v. y /\ z] will be turned into
 128  * [(x ==> !v. y) /\ (x ==> !v. z)])
 129  *
 130  * possible improvement: apply the rewrite more locally
 131  *)
 132 let IMPLY_AND =
 133   let IMPLY_AND_RDISTRIB = TAUT `(x ==> y /\ z) <=> (x==>y) /\(x==>z)` in
 134   PURE_REWRITE_RULE [GSYM AND_FORALL_THM;IMP_IMP;
 135     RIGHT_IMP_FORALL_THM;IMPLY_AND_RDISTRIB;GSYM CONJ_ASSOC] in
 136
 137 (* Returns the two operands of a binary combination.
 138  * Contrary to [dest_binary], does not check what is the operator.
 139  *)
 140 let dest_binary_blind = function
 141   |Comb(Comb(_,l),r) -> l,r
 142   |_ -> failwith "dest_binary_blind" in
 143
 144 let spec_all = repeat (snd o dest_forall) in
 145
 146 let thm_lt (th1:thm) th2 = th1 < th2 in
 147
 148 (* GMATCH_MP (U1 |- !x1...xn. H1 /\ ... /\ Hk ==> C) (U2 |- P)
 149  * = (U1 u U2 |- !y1...ym. G1' /\ ... /\ Gl' ==> C')
 150  * where:
 151  * - P matches some Hi
 152  * - C' is the result of applying the matching substitution to C
 153  * - Gj' is the result of applying the matching substitution to Hj
 154  * - G1',...,Gl' is the list corresponding to H1,...,Hk but without Hi
 155  * - y1...ym are the variables among x1,...,xn that are not instantiated
 156  *
 157  * possible improvement: make a specific conversion,
 158  * define a MATCH_MP that also returns the instantiated variables *)
 159 let GMATCH_MP =
 160   let swap = CONV_RULE (REWR_CONV (TAUT `(p==>q==>r) <=> (q==>p==>r)`)) in
 161   fun th1 ->
 162     let vs,th1' = SPEC_VARS th1 in
 163     let hs,th1'' = UNDISCH_TERMS (PURE_REWRITE_RULE [IMP_CONJ] th1') in
 164     fun th2 ->
 165       let f h hs =
 166         let th1''' = DISCH h th1'' in
 167         let th1'''' =
 168           try swap (DISCH_IMP_IMP hs th1''') with Failure _ -> th1'''
 169         in
 170         MATCH_MP (GENL vs th1'''') th2
 171       in
 172       let rec loop acc = function
 173         |[] -> []
 174         |h::hs ->
 175             (try [f h (acc @ hs)] with Failure _ -> []) @ loop (h::acc) hs
 176       in
 177       loop [] hs in
 178
 179 let GMATCH_MPS ths1 ths2 =
 180   let insert (y:thm) = function
 181     |[] -> [y]
 182     |x::_ as xs when equals_thm x y -> xs
 183     |x::xs when thm_lt x y -> x :: insert y xs
 184     |_::_ as xs -> y::xs
 185   in
 186   let inserts ys = itlist insert ys in
 187   match ths1 with
 188   |[] -> []
 189   |th1::ths1' ->
 190     let rec self acc th1 ths1 = function
 191       |[] -> (match ths1 with [] -> acc | th::ths1' -> self acc th ths1' ths2)
 192       |th2::ths2' -> self (inserts (GMATCH_MP th1 th2) acc) th1 ths1 ths2'
 193     in
 194     self [] th1 ths1' ths2 in
 195
 196 let MP_CLOSURE ths1 ths2 =
 197   let ths1 = filter (is_imp o spec_all o concl) ths1 in
 198   let rec self ths2 = function
 199     |[] -> []
 200     |_::_ as ths1 ->
 201       let ths1'' = GMATCH_MPS ths1 ths2 in
 202       self ths2 ths1'' @ ths1''
 203   in
 204   self ths2 ths1 in
 205
 206 (* Set of terms. Implemented as ordered lists. *)
 207 let module Tset =
 208   struct
 209     type t = term list
 210     let cmp (x:term) y = Pervasives.compare x y
 211     let lt (x:term) y = Pervasives.compare x y < 0
 212     let lift f = List.sort cmp o f
 213     let of_list = lift I
 214     let insert ts t =
 215       let rec self = function
 216         |[] -> [t]
 217         |x::xs when lt x t -> x::self xs
 218         |x::_ as xs when x = t -> xs
 219         |xs -> t::xs
 220       in
 221       if t = T_ then ts else self ts
 222     let remove ts t =
 223       let rec self = function
 224         |[] -> []
 225         |x::xs when lt x t -> x::self xs
 226         |x::xs when x = t -> xs
 227         |_::_ as xs -> xs
 228       in
 229       self ts
 230     let strip_conj =
 231       let rec self acc t =
 232         try
 233           let t1,t2 = dest_conj t in
 234           self (self acc t1) t2
 235         with Failure _ -> insert acc t
 236       in
 237       self []
 238     let rec union l1 l2 =
 239       match l1 with
 240       |[] -> l2
 241       |h1::t1 ->
 242           match l2 with
 243           |[] -> l1
 244           |h2::t2 when lt h1 h2 -> h1::union t1 l2
 245           |h2::t2 when h1 = h2 -> h1::union t1 t2
 246           |h2::t2 -> h2::union l1 t2
 247     let rec mem x = function
 248       |x'::xs when x' = x -> true
 249       |x'::xs when lt x' x -> mem x xs
 250       |_ -> false
 251     let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1
 252     let empty = []
 253     let flat_revmap f =
 254       let rec self acc = function
 255         |[] -> acc
 256         |x::xs -> self (union (f x) acc) xs
 257       in
 258       self []
 259     let flat_map f = flat_revmap f o rev
 260     let rec frees acc = function
 261       |Var _ as t -> insert acc t
 262       |Const _ -> acc
 263       |Abs(v,b) -> remove (frees acc b) v
 264       |Comb(u,v) -> frees (frees acc u) v
 265     let freesl ts = itlist (C frees) ts empty
 266     let frees = frees empty
 267   end in
 268
 269 let module Type_annoted_term =
 270   struct
 271     type t =
 272       |Var_ of string * hol_type
 273       |Const_ of string * hol_type * term
 274       |Comb_ of t * t * hol_type
 275       |Abs_ of t * t * hol_type
 276
 277     let type_of = function
 278       |Var_(_,ty) -> ty
 279       |Const_(_,ty,_) -> ty
 280       |Comb_(_,_,ty) -> ty
 281       |Abs_(_,_,ty) -> ty
 282
 283     let rec of_term = function
 284       |Var(s,ty) -> Var_(s,ty)
 285       |Const(s,ty) as t -> Const_(s,ty,t)
 286       |Comb(u,v) ->
 287           let u' = of_term u and v' = of_term v in
 288           Comb_(u',v',snd (dest_fun_ty (type_of u')))
 289       |Abs(x,b) ->
 290           let x' = of_term x and b' = of_term b in
 291           Abs_(x',b',mk_fun_ty (type_of x') (type_of b'))
 292
 293     let rec equal t1 t2 =
 294       match t1,t2 with
 295       |Var_(s1,ty1),Var_(s2,ty2)
 296       |Const_(s1,ty1,_),Const_(s2,ty2,_) -> s1 = s2 & ty1 = ty2
 297       |Comb_(u1,v1,_),Comb_(u2,v2,_) -> equal u1 u2 & equal v1 v2
 298       |Abs_(v1,b1,_),Abs_(v2,b2,_) -> equal v1 v2 & equal b1 b2
 299       |_ -> false
 300
 301     let rec to_term = function
 302       |Var_(s,ty) -> mk_var(s,ty)
 303       |Const_(_,_,t) -> t
 304       |Comb_(u,v,_) -> mk_comb(to_term u,to_term v)
 305       |Abs_(v,b,_) -> mk_abs(to_term v,to_term b)
 306
 307     let dummy = Var_("",aty)
 308
 309     let rec find_term p t =
 310       if p t then t else
 311         match t with
 312         |Abs_(_,b,_) -> find_term p b
 313         |Comb_(u,v,_) -> try find_term p u with Failure _ -> find_term p v
 314         |_ -> failwith "Annot.find_term"
 315   end in
 316
 317 let module Annot = Type_annoted_term in
 318
 319 (* ------------------------------------------------------------------------- *)
 320 (* First-order matching of terms.                                            *)
 321 (*                                                                           *)
 322 (* Same note as in [drule.ml]:                                               *)
 323 (* in the event of spillover patterns, this may return false results;        *)
 324 (* but there's usually an implicit check outside that the match worked       *)
 325 (* anyway. A test could be put in (see if any "env" variables are left in    *)
 326 (* the term after abstracting out the pattern instances) but it'd be slower. *)
 327 (* ------------------------------------------------------------------------- *)
 328
 329 let fo_term_match lcs p t =
 330   let fail () = failwith "fo_term_match" in
 331   let rec self bnds (tenv,tyenv as env) p t =
 332     match p,t with
 333     |Comb(p1,p2),Annot.Comb_(t1,t2,_) -> self bnds (self bnds env p1 t1) p2 t2
 334     |Abs(v,p),Annot.Abs_(v',t,_) ->
 335         let tyenv' = type_match (type_of v) (Annot.type_of v') tyenv in
 336         self ((v',v)::bnds) (tenv,tyenv') p t
 337     |Const(n,ty),Annot.Const_(n',ty',_) ->
 338         if n <> n' then fail ()
 339         else
 340           let tyenv' = type_match ty ty' tyenv in
 341           tenv,tyenv'
 342     |Var(n,ty) as v,t ->
 343         (* Is [v] bound? *)
 344         (try if Annot.equal t (rev_assoc v bnds) then env else fail ()
 345         (* No *)
 346         with Failure _ ->
 347           if mem v lcs
 348           then
 349             match t with
 350             |Annot.Var_(n',ty') when n' = n & ty' = ty -> env
 351             |_ -> fail ()
 352           else
 353             let tyenv' = type_match ty (Annot.type_of t) tyenv in
 354             let t' = try Some (rev_assoc v tenv) with Failure _ -> None in
 355             match t' with
 356             |Some t' -> if t = t' then tenv,tyenv' else fail ()
 357             |None -> (t,v)::tenv,tyenv')
 358     |_ -> fail ()
 359   in
 360   let tenv,tyenv = self [] ([],[]) p (Annot.of_term t) in
 361   let inst = inst tyenv in
 362   List.rev_map (fun t,v -> Annot.to_term t,inst v) tenv,tyenv in
 363
 364 let GEN_PART_MATCH_ALL =
 365   let rec match_bvs t1 t2 acc =
 366     try let v1,b1 = dest_abs t1
 367         and v2,b2 = dest_abs t2 in
 368         let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in
 369         let newacc = if n1 = n2 then acc else insert (n1,n2) acc in
 370         match_bvs b1 b2 newacc
 371     with Failure _ -> try
 372         let l1,r1 = dest_comb t1
 373         and l2,r2 = dest_comb t2 in
 374         match_bvs l1 l2 (match_bvs r1 r2 acc)
 375     with Failure _ -> acc
 376   in
 377   fun partfn th ->
 378     let sth = SPEC_ALL th in
 379     let bod = concl sth in
 380     let pbod = partfn bod in
 381     let lcs = intersect (frees (concl th)) (freesl(hyp th)) in
 382     let fvs = subtract (subtract (frees bod) (frees pbod)) lcs in
 383     fun tm ->
 384       let bvms = match_bvs tm pbod [] in
 385       let abod = deep_alpha bvms bod in
 386       let ath = EQ_MP (ALPHA bod abod) sth in
 387       let insts,tyinsts = fo_term_match lcs (partfn abod) tm in
 388       let eth = INSTANTIATE_ALL ([],insts,tyinsts) (GENL fvs ath) in
 389       let fth = itlist (fun v th -> snd(SPEC_VAR th)) fvs eth in
 390       let tm' = partfn (concl fth) in
 391       if Pervasives.compare tm' tm = 0 then fth else
 392       try SUBS[ALPHA tm' tm] fth
 393       with Failure _ -> failwith "PART_MATCH: Sanity check failure" in
 394
 395 let exists_subterm p t =
 396   try ignore (find_term p t);true with Failure _ -> false in
 397
 398 let module Fo_nets =
 399   struct
 400     type term_label =
 401       |Vnet of int
 402       |Lcnet of string * int
 403       |Cnet of string * int
 404       |Lnet of int
 405
 406     type 'a t = Netnode of (term_label * 'a t) list * 'a list
 407
 408     let empty_net = Netnode([],[])
 409
 410     let enter =
 411       let label_to_store lcs t =
 412         let op,args = strip_comb t in
 413         let nargs = length args in
 414         match op with
 415         |Const(n,_) -> Cnet(n,nargs),args
 416         |Abs(v,b) ->
 417           let b' = if mem v lcs then vsubst [genvar(type_of v),v] b else b in
 418           Lnet nargs,b'::args
 419         |Var(n,_) when mem op lcs -> Lcnet(n,nargs),args
 420         |Var(_,_) -> Vnet nargs,args
 421         |_ -> assert false
 422       in
 423       let rec net_update lcs elem (Netnode(edges,tips)) = function
 424         |[] -> Netnode(edges,elem::tips)
 425         |t::rts ->
 426             let label,nts = label_to_store lcs t in
 427             let child,others =
 428               try (snd F_F I) (remove (fun (x,y) -> x = label) edges)
 429               with Failure _ -> empty_net,edges in
 430             let new_child = net_update lcs elem child (nts@rts) in
 431             Netnode ((label,new_child)::others,tips)
 432       in
 433       fun lcs (t,elem) net -> net_update lcs elem net [t]
 434
 435     let lookup =
 436       let label_for_lookup t =
 437         let op,args = strip_comb t in
 438         let nargs = length args in
 439         match op with
 440         |Const(n,_) -> Cnet(n,nargs),args
 441         |Abs(_,b) -> Lnet nargs,b::args
 442         |Var(n,_) -> Lcnet(n,nargs),args
 443         |Comb _ -> assert false
 444       in
 445       let rec follow (Netnode(edges,tips)) = function
 446         |[] -> tips
 447         |t::rts ->
 448             let label,nts = label_for_lookup t in
 449             let collection =
 450               try follow (assoc label edges) (nts@rts) with Failure _ -> []
 451             in
 452             let rec support = function
 453               |[] -> [0,rts]
 454               |t::ts ->
 455                   let ((k,nts')::res') as res = support ts in
 456                   (k+1,(t::nts'))::res
 457             in
 458             let follows =
 459               let f (k,nts) =
 460                 try follow (assoc (Vnet k) edges) nts with Failure _ -> []
 461               in
 462               map f (support nts)
 463             in
 464             collection @ flat follows
 465       in
 466       fun t net -> follow net [t]
 467
 468     let rec filter p (Netnode(edges,tips)) =
 469       Netnode(
 470         List.map (fun l,n -> l,filter p n) edges,
 471         List.filter p tips)
 472   end in
 473
 474 let module Variance =
 475   struct
 476     type t = Co | Contra
 477     let neg = function Co -> Contra | Contra -> Co
 478   end in
 479
 480 (*****************************************************************************)
 481 (* IMPLICATIONAL RULES                                                       *)
 482 (* i.e., rules to build propositions based on implications rather than       *)
 483 (* equivalence.                                                              *)
 484 (*****************************************************************************)
 485
 486 let module Impconv =
 487   struct
 488
 489 let MKIMP_common lem th1 th2 =
 490   let a,b = dest_imp (concl th1) and c,d = dest_imp (concl th2) in
 491   MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 492
 493 (* Similar to [MK_CONJ] but theorems should be implicational instead of
 494  * equational, i.e., conjoin both sides of two implicational theorems.
 495  *
 496  * More precisely: given two theorems [A ==> B] and [C ==> D],
 497  * returns [A /\ C ==> B /\ D].
 498  *)
 499 let MKIMP_CONJ = MKIMP_common MONO_AND
 500
 501 (* Similar to [MK_DISJ] but theorems should be implicational instead of
 502  * equational, i.e., disjoin both sides of two implicational theorems.
 503  *
 504  * More precisely: given two theorems [A ==> B] and [C ==> D],
 505  * returns [A \/ C ==> B \/ D].
 506  *)
 507 let MKIMP_DISJ = MKIMP_common MONO_OR
 508
 509 let MKIMP_IFF =
 510   let lem =
 511     TAUT `((A ==> B) ==> (C ==> D)) /\ ((B ==> A) ==> (D ==> C)) ==> (A <=> B)
 512       ==> (C <=> D)`
 513   in
 514   fun th1 th2 ->
 515     let ab,cd = dest_imp (concl th1) in
 516     let a,b = dest_imp ab and c,d = dest_imp cd in
 517     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 518
 519 (* th1 = (A ==> B) ==> C1
 520  * th2 = (B ==> A) ==> C2
 521  * output = (A <=> B) ==> (C1 /\ C2)
 522  *)
 523 let MKIMP_CONTRA_IFF =
 524   let lem =
 525     TAUT `((A ==> B) ==> C) /\ ((B ==> A) ==> D) ==> (A <=> B) ==> C /\ D`
 526   in
 527   fun th1 th2 ->
 528     let ab,c = dest_imp (concl th1) and _,d = dest_imp (concl th2) in
 529     let a,b = dest_imp ab in
 530     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 531
 532 let MKIMPL_CONTRA_IFF =
 533   let lem = TAUT `((A ==> B) ==> C) ==> (A <=> B) ==> C /\ (B ==> A)` in
 534   fun th ->
 535     let ab,c = dest_imp (concl th) in
 536     let a,b = dest_imp ab in
 537     MP (INST [a,A_;b,B_;c,C_] lem) th
 538
 539 let MKIMPR_CONTRA_IFF =
 540   let lem =
 541     TAUT `((B ==> A) ==> D) ==> (A <=> B) ==> (A ==> B) /\ D`
 542   in
 543   fun th ->
 544     let ba,d = dest_imp (concl th) in
 545     let b,a = dest_imp ba in
 546     MP (INST [a,A_;b,B_;d,D_] lem) th
 547
 548 let MKIMP_CO_IFF =
 549   let lem =
 550     TAUT `(C ==> A ==> B) /\ (D ==> B ==> A) ==> C /\ D ==> (A <=> B)`
 551   in
 552   fun th1 th2 ->
 553     let c,ab = dest_imp (concl th1) and d,_ = dest_imp (concl th2) in
 554     let a,b = dest_imp ab in
 555     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 556
 557 let MKIMPL_CO_IFF =
 558   let lem =
 559     TAUT `(C ==> A ==> B) ==> C /\ (B ==> A) ==> (A <=> B)`
 560   in
 561   fun th ->
 562     let c,ab = dest_imp (concl th) in
 563     let a,b = dest_imp ab in
 564     MP (INST [a,A_;b,B_;c,C_] lem) th
 565
 566 let MKIMPR_CO_IFF =
 567   let lem = TAUT `(D ==> B ==> A) ==> (A ==> B) /\ D ==> (A <=> B)` in
 568   fun th ->
 569     let d,ba = dest_imp (concl th) in
 570     let b,a = dest_imp ba in
 571     MP (INST [a,A_;b,B_;d,D_] lem) th
 572
 573 (* Given two theorems [A ==> B] and [C ==> D],
 574  * returns [(B ==> C) ==> (A ==> D)].
 575  *)
 576 let MKIMP_IMP th1 th2 =
 577   let b,a = dest_imp (concl th1) and c,d = dest_imp (concl th2) in
 578   MP (INST [a,A_;b,B_;c,C_;d,D_] MONO_IMP) (CONJ th1 th2)
 579
 580 let MKIMPL_common lem =
 581   let lem' = REWRITE_RULE[] (INST [C_,D_] lem) in
 582   fun th t ->
 583     let a,b = dest_imp (concl th) in
 584     MP (INST [a,A_;b,B_;t,C_] lem') th
 585
 586 (* Given a theorem [A ==> B] and a term [C],
 587  * returns [A /\ C ==> B /\ C].
 588  *)
 589 let MKIMPL_CONJ = MKIMPL_common MONO_AND
 590
 591 (* Given a theorem [A ==> B] and a term [C],
 592  * returns [A \/ C ==> B \/ C].
 593  *)
 594 let MKIMPL_DISJ = MKIMPL_common MONO_OR
 595
 596 (* Given a theorem [A ==> B] and a term [C],
 597  * returns [(B ==> C) ==> (A ==> C)].
 598  *)
 599 let MKIMPL_IMP =
 600   let MONO_IMP' = REWRITE_RULE[] (INST [C_,D_] MONO_IMP) in
 601   fun th t ->
 602     let b,a = dest_imp (concl th) in
 603     MP (INST [a,A_;b,B_;t,C_] MONO_IMP') th
 604
 605 let MKIMPR_common lem =
 606   let lem' = REWRITE_RULE[] (INST [A_,B_] lem) in
 607   fun t th ->
 608     let c,d = dest_imp (concl th) in
 609     MP (INST [c,C_;d,D_;t,A_] lem') th
 610
 611 (* Given a term [A] and a theorem [B ==> C],
 612  * returns [A /\ B ==> A /\ C].
 613  *)
 614 let MKIMPR_CONJ = MKIMPR_common MONO_AND
 615
 616 (* Given a term [A] and a theorem [B ==> C],
 617  * returns [A \/ B ==> A \/ C].
 618  *)
 619 let MKIMPR_DISJ = MKIMPR_common MONO_OR
 620
 621 (* Given a term [A] and a theorem [B ==> C],
 622  * returns [(A ==> B) ==> (A ==> C)].
 623  *)
 624 let MKIMPR_IMP = MKIMPR_common MONO_IMP
 625
 626 (* Given a theorem [A ==> B], returns [~B ==> ~A]. *)
 627 let MKIMP_NOT th =
 628   let b,a = dest_imp (concl th) in
 629   MP (INST [a,A_;b,B_] MONO_NOT) th
 630
 631 let MKIMP_QUANT lem x th =
 632   let x_ty = type_of x and p,q = dest_imp (concl th) in
 633   let p' = mk_abs(x,p) and q' = mk_abs(x,q) in
 634   let P = mk_var("P",mk_fun_ty x_ty bool_ty) in
 635   let Q = mk_var("Q",mk_fun_ty x_ty bool_ty) in
 636   let lem = INST [p',P;q',Q] (INST_TYPE [x_ty,aty] lem) in
 637   let c = ONCE_DEPTH_CONV (ALPHA_CONV x) THENC ONCE_DEPTH_CONV BETA_CONV in
 638   MP (CONV_RULE c lem) (GEN x th)
 639
 640 (* Given a variable [x] and a theorem [A ==> B],
 641  * returns [(!x. A) ==> (!x. B)]. *)
 642 let MKIMP_FORALL = MKIMP_QUANT MONO_FORALL
 643
 644 (* Given a variable [x] and a theorem [A ==> B],
 645  * returns [(?x. A) ==> (?x. B)]. *)
 646 let MKIMP_EXISTS = MKIMP_QUANT MONO_EXISTS
 647
 648 (* Given two theorems [A ==> B] and [B ==> C ==> D],
 649  * returns [(B ==> C) ==> (A ==> D)],
 650  * i.e., similar to [MKIMP_IMP] but allows to remove the context [B]
 651  * since it is a consequence of [A].
 652  *)
 653 let MKIMP_IMP_CONTRA_CTXT =
 654   let lem = TAUT `(B==>A) /\ (A==>B==>C==>D) ==> (A==>C) ==> (B==>D)` in
 655   fun th1 th2 ->
 656     let a,bcd = dest_imp (concl th2) in
 657     let b,cd = dest_imp bcd in
 658     let c,d = dest_imp cd in
 659     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 660
 661 let MKIMP_IMP_CO_CTXT =
 662   let lem = TAUT `(A==>B) /\ (A==>B==>D==>C) ==> (B==>D) ==> (A==>C)` in
 663   fun th1 th2 ->
 664     let a,bdc = dest_imp (concl th2) in
 665     let b,dc = dest_imp bdc in
 666     let d,c = dest_imp dc in
 667     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 668
 669 (* Given a theorem [B ==> C ==> D], returns [(B ==> C) ==> (B ==> D)],
 670  * i.e., similar to [MKIMP_IMP] but allows to remove the context [B]
 671  * since it is a consequence of [A].
 672  *)
 673 let MKIMPR_IMP_CTXT =
 674   let lem = TAUT `(A==>C==>D) ==> (A==>C) ==> (A==>D)` in
 675   fun th ->
 676     let a,cd = dest_imp (concl th) in
 677     let c,d = dest_imp cd in
 678     MP (INST [c,C_;d,D_;a,A_] lem) th
 679
 680 (* Given two theorems [A ==> B] and [A ==> B ==> C ==> D],
 681  * returns [(A /\ C) ==> (B /\ D)],
 682  * i.e., similar to [MKIMP_CONJ] but allows to remove the contexts [A] and [B].
 683  *)
 684 let MKIMP_CONJ_CONTRA_CTXT =
 685   let lem = TAUT `(C==>A==>B) /\ (A==>B==>C==>D) ==> (A/\C==>B/\D)` in
 686   fun th1 th2 ->
 687     let a,bcd = dest_imp (concl th2) in
 688     let b,cd = dest_imp bcd in
 689     let c,d = dest_imp cd in
 690     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 691
 692 let MKIMPL_CONJ_CONTRA_CTXT =
 693   let lem = TAUT `(C==>A==>B) ==> (A/\C==>B/\C)` in
 694   fun th ->
 695     let c,ab = dest_imp (concl th) in
 696     let a,b = dest_imp ab in
 697     MP (INST [a,A_;b,B_;c,C_] lem) th
 698
 699 let MKIMPR_CONJ_CONTRA_CTXT =
 700   let lem = TAUT `(A==>C==>D) ==> (A/\C==>A/\D)` in
 701   fun th ->
 702     let a,cd = dest_imp (concl th) in
 703     let c,d = dest_imp cd in
 704     MP (INST [a,A_;c,C_;d,D_] lem) th
 705
 706 let MKIMP_CONJ_CO_CTXT =
 707   let lem = TAUT `(B==>A) /\ (B==>D==>C) ==> (B/\D==>A/\C)` in
 708   fun th1 th2 ->
 709     let b,a = dest_imp (concl th1) in
 710     let d,c = dest_imp (snd (dest_imp (concl th2))) in
 711     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
 712
 713 let MKIMPL_CONJ_CO_CTXT =
 714   let lem = TAUT `(B==>A) ==> (B/\C==>A/\C)` in
 715   fun th ->
 716     let b,a = dest_imp (concl th) in
 717     fun c -> MP (INST [a,A_;b,B_;c,C_] lem) th
 718
 719 let MKIMPL_CONJ_CO2_CTXT =
 720   let lem = TAUT `(C==>B==>A) ==> (B/\C==>A/\C)` in
 721   fun th ->
 722     let c,ba = dest_imp (concl th) in
 723     let b,a = dest_imp ba in
 724     MP (INST [a,A_;b,B_;c,C_] lem) th
 725
 726 let MKIMPR_CONJ_CO_CTXT = MKIMPR_CONJ_CONTRA_CTXT
 727
 728
 729 (*****************************************************************************)
 730 (* IMPLICATIONAL CONVERSIONS                                                 *)
 731 (*****************************************************************************)
 732
 733 open Variance
 734
 735 (* An implicational conversion maps a term t to a theorem of the form:
 736  * t' ==> t if covariant
 737  * t ==> t' if contravariant
 738  *)
 739 type imp_conv = Variance.t -> term -> thm
 740
 741 (* Trivial embedding of conversions into implicational conversions. *)
 742 let imp_conv_of_conv:conv->imp_conv =
 743   fun c v t ->
 744     let th1,th2 = EQ_IMP_RULE (c t) in
 745     match v with Co -> th2 | Contra -> th1
 746
 747 (* Retrieves the outcome of an implicational conversion, i.e., t'. *)
 748 let imp_conv_outcome th v =
 749   let t1,t2 = dest_binary_blind (concl th) in
 750   match v with Co -> t1 | Contra -> t2
 751
 752 (* [ALL_IMPCONV _ t] returns `t==>t` *)
 753 let ALL_IMPCONV:imp_conv = fun _ -> IMP_REFL
 754
 755 (* The implicational conversion which always fails. *)
 756 let NO_IMPCONV:imp_conv = fun _ _ -> failwith "NO_IMPCONV"
 757
 758 let bind_impconv (c:imp_conv) v th =
 759   let t1,t2 = dest_imp (concl th) in
 760   match v with
 761   |Co -> IMP_TRANS (c v t1) th
 762   |Contra -> IMP_TRANS th (c v t2)
 763
 764 let THEN_IMPCONV (c1:imp_conv) c2 v t = bind_impconv c2 v (c1 v t)
 765
 766
 767 (*****************************************************************************)
 768 (* SOME USEFUL IMPLICATIONAL CONVERSIONS                                     *)
 769 (*****************************************************************************)
 770
 771 (* Given a theorem [p ==> c], returns the implicational conversion which:
 772   * - in the covariant case, matches the input term [t] against [c] and returns
 773   *   [s(p) ==> t], where [s] is the matching substitution
 774   * - in the contravariant case, matches the input term [t] against [p] and returns
 775   *   [t ==> s(c)], where [s] is the matching substitution
 776   *)
 777 let MATCH_MP_IMPCONV:thm->imp_conv =
 778   fun th -> function
 779     |Co -> GEN_PART_MATCH rand th
 780     |Contra -> GEN_PART_MATCH lhand th
 781
 782
 783 (*****************************************************************************)
 784 (* INTERFACE                                                                 *)
 785 (*****************************************************************************)
 786
 787 (* From an implicational conversion builds a rule, i.e., a function which
 788  * takes a theorem and returns a new theorem.
 789  *)
 790 let IMPCONV_RULE:imp_conv->thm->thm =
 791   fun c th ->
 792     let t = concl th in
 793     MATCH_MP (c Contra t) th
 794
 795 (* From an implicational conversion builds a tactic. *)
 796 let IMPCONV_TAC:imp_conv->tactic =
 797   fun cnv (_,c as g) ->
 798     (MATCH_MP_TAC (cnv Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
 799
 800
 801 (*****************************************************************************)
 802 (* CONTEXT HANDLING                                                          *)
 803 (*****************************************************************************)
 804
 805 (* [term list] = terms to add to the context *)
 806 type 'a with_context =
 807   With_context of 'a * (Tset.t -> 'a with_context) * (term -> 'a with_context)
 808
 809 let apply (With_context(c,_,_)) = c
 810
 811 (* Maybe avoid the augment if the input list is empty? *)
 812 let augment (With_context(_,a,_)) = a
 813 let diminish (With_context(_,_,d)) = d
 814 let apply_with_context c ctx v t =
 815   DISCH_CONJ ctx (apply (augment c (Tset.strip_conj ctx)) v t)
 816
 817 let imp_conv_of_ctx_imp_conv = (apply:imp_conv with_context -> imp_conv)
 818
 819 (* Consider two implicational conversions ic1, ic2.
 820  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C],
 821  * then [CONJ_IMPCONV ic1 ic2 Co (A /\ C)] returns [B /\ D ==> A /\ C].
 822  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns
 823  * [C ==> D], then [CONJ_IMPCONV ic1 ic2 Contra (A /\ B)]
 824  * returns [A /\ B ==> C /\ D].
 825  *
 826  * Additionally takes the context into account, i.e., if [ic2 Co C] returns
 827  * [A |- D ==> C],
 828  * then [CONJ_IMPCONV ic1 ic2 Co (A /\ B)] returns [|- C /\ D ==> A /\ B]
 829  * (i.e., [A] does not appear in the hypotheses).
 830  *)
 831 let rec CONJ_CTXIMPCONV (c:imp_conv with_context) =
 832   With_context(
 833     ((fun v t ->
 834       let t1,t2 = dest_conj t in
 835       match v with
 836       |Co ->
 837           (try
 838             let th1 = apply c Co t1 in
 839             try
 840               let t1' = imp_conv_outcome th1 Co in
 841               MKIMP_CONJ_CO_CTXT th1 (apply_with_context c t1' Co t2)
 842               with Failure _ -> MKIMPL_CONJ_CO_CTXT th1 t2
 843           with Failure _ -> MKIMPR_CONJ_CO_CTXT (apply_with_context c t1 Co t2))
 844       |Contra ->
 845           try
 846             (* note: we remove t1 in case it appears in t2, since otherwise,
 847              * t1 removes t2 and t2 removes t1
 848              *)
 849             let t2s = Tset.remove (Tset.strip_conj t2) t1 in
 850             let th1 = apply (augment c t2s) Contra t1 in
 851               try
 852                 let t1' = imp_conv_outcome th1 Contra in
 853                 let t1s = Tset.strip_conj t1 and t1s' = Tset.strip_conj t1' in
 854                 let t1s'' = Tset.union t1s t1s' in
 855                 let th2 = apply (augment c t1s'') Contra t2 in
 856                 let th2' = DISCH_CONJ t1 (DISCH_CONJ t1' th2) in
 857                 MKIMP_CONJ_CONTRA_CTXT (DISCH_CONJ t2 th1) th2'
 858               with Failure _ -> MKIMPL_CONJ_CONTRA_CTXT (DISCH_CONJ t2 th1)
 859             with Failure _ ->
 860               MKIMPR_CONJ_CONTRA_CTXT (apply_with_context c t1 Contra t2))
 861       :imp_conv),
 862     CONJ_CTXIMPCONV o augment c,
 863     CONJ_CTXIMPCONV o diminish c)
 864
 865 (* Consider two implicational conversions ic1, ic2.
 866  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C],
 867  * then [DISJ_IMPCONV ic1 ic2 Co (A \/ C)] returns [B \/ D ==> A \/ C].
 868  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns
 869  * [C ==> D], then [DISJ_IMPCONV ic1 ic2 Contra (A \/ B)]
 870  * returns [A \/ B ==> C \/ D].
 871  *)
 872 let rec DISJ_CTXIMPCONV (c:imp_conv with_context) =
 873   With_context(
 874     ((fun v t ->
 875       let t1,t2 = dest_disj t in
 876       try
 877         let th1 = apply c v t1 in
 878         try MKIMP_DISJ th1 (apply c v t2) with Failure _ -> MKIMPL_DISJ th1 t2
 879       with Failure _ -> MKIMPR_DISJ t1 (apply c v t2)):imp_conv),
 880     DISJ_CTXIMPCONV o augment c,
 881     DISJ_CTXIMPCONV o diminish c)
 882
 883 (* Consider two implicational conversions ic1, ic2.
 884  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Co C] returns [D ==> C],
 885  * then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns [(B ==> D) ==> (A ==> C)].
 886  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Contra C] returns
 887  * [C ==> D], then [IMP_IMPCONV ic1 ic2 Contra (A ==> C)]
 888  * returns [(A ==> C) ==> (B ==> D)].
 889  *
 890  * Additionally takes the context into account, i.e., if [ic2 Co C] returns
 891  * [B |- D ==> C], then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns
 892  * [|- (B ==> D) ==> (A ==> C)] (i.e., [B] does not appear in the hypotheses).
 893  *)
 894 let rec IMP_CTXIMPCONV (c:imp_conv with_context)  =
 895   With_context(
 896     ((fun v t ->
 897       let t1,t2 = dest_imp t in
 898       try
 899         let v' = Variance.neg v in
 900         let th1 = apply c v' t1 in
 901         let t1' = imp_conv_outcome th1 v' in
 902         let t1s = Tset.union (Tset.strip_conj t1) (Tset.strip_conj t1') in
 903         let c' = augment c t1s in
 904         let mk =
 905           match v with Co -> MKIMP_IMP_CO_CTXT | Contra -> MKIMP_IMP_CONTRA_CTXT
 906         in
 907         try mk th1 (DISCH_CONJ t1 (DISCH_CONJ t1' (apply c' v t2)))
 908         with Failure _ -> MKIMPL_IMP th1 t2
 909       with Failure _ -> MKIMPR_IMP_CTXT (apply_with_context c t1 v t2)
 910       ):imp_conv),
 911     IMP_CTXIMPCONV o augment c,
 912     IMP_CTXIMPCONV o diminish c)
 913
 914 let rec IFF_CTXIMPCONV (c:imp_conv with_context) =
 915   With_context(
 916     ((fun v t ->
 917       let t1,t2 = dest_iff t in
 918       let lr,l,r =
 919         match v with
 920         |Co -> MKIMP_CO_IFF,MKIMPL_CO_IFF,MKIMPR_CO_IFF
 921         |Contra -> MKIMP_CONTRA_IFF,MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
 922       in
 923       (try
 924         let th1 = apply c v (mk_imp (t1,t2)) in
 925         try
 926           let th2 = apply c v (mk_imp (t2,t1)) in
 927           (try MKIMP_IFF th1 th2 with Failure _ -> lr th1 th2)
 928         with Failure _ -> l th1
 929       with Failure _ -> r (apply c v (mk_imp (t2,t1))))):imp_conv),
 930     IFF_CTXIMPCONV o augment c,
 931     IFF_CTXIMPCONV o diminish c)
 932
 933 (* Consider an implicational conversion ic.
 934  * Suppose [ic Contra A] returns [A ==> B]
 935  * then [NOT_IMPCONV ic Co ~A] returns [~B ==> ~A].
 936  * Suppose [ic Co A] returns [B ==> A]
 937  * then [NOT_IMPCONV ic Contra ~A] returns [~A ==> ~B].
 938  *)
 939 let rec NOT_CTXIMPCONV (c:imp_conv with_context) =
 940   With_context(
 941     ((fun v t -> MKIMP_NOT (apply c (Variance.neg v) (dest_neg t))):imp_conv),
 942     NOT_CTXIMPCONV o augment c,
 943     NOT_CTXIMPCONV o diminish c)
 944
 945 let rec QUANT_CTXIMPCONV mkimp sel (c:imp_conv with_context) =
 946   With_context(
 947     ((fun v t ->
 948       let x,b = sel t in
 949       let c' = diminish c x in
 950       mkimp x (apply c' v b)):imp_conv),
 951     QUANT_CTXIMPCONV mkimp sel o augment c,
 952     QUANT_CTXIMPCONV mkimp sel o diminish c)
 953
 954 (* Consider an implicational conversion ic.
 955  * Suppose [ic Co A] returns [B ==> A]
 956  * then [FORALL_IMPCONV ic Co (!x.A)] returns [(!x.B) ==> (!x.A)].
 957  * Suppose [ic Contra A] returns [A ==> B]
 958  * then [FORALL_IMPCONV ic Contra (!x.A)] returns [(!x.A) ==> (!x.B)].
 959  *)
 960 let FORALL_CTXIMPCONV = QUANT_CTXIMPCONV MKIMP_FORALL dest_forall
 961
 962 (* Consider an implicational conversion ic.
 963  * Suppose [ic Co A] returns [B ==> A]
 964  * then [EXISTS_IMPCONV ic Co (?x.A)] returns [(?x.B) ==> (?x.A)].
 965  * Suppose [ic Contra A] returns [A ==> B]
 966  * then [EXISTS_IMPCONV ic Contra (?x.A)] returns [(?x.A) ==> (?x.B)].
 967  *)
 968 let EXISTS_CTXIMPCONV = QUANT_CTXIMPCONV MKIMP_EXISTS dest_exists
 969
 970 (* Applies an implicational conversion on the subformula(s) of the input term*)
 971 let rec SUB_CTXIMPCONV =
 972   let iff_ty = `:bool->bool->bool` in
 973   fun c ->
 974     With_context(
 975     ((fun v t ->
 976       let n,ty = dest_const (fst (strip_comb t)) in
 977       apply
 978         ((match n with
 979         |"==>" -> IMP_CTXIMPCONV
 980         |"/\\" -> CONJ_CTXIMPCONV
 981         |"\\/" -> DISJ_CTXIMPCONV
 982         |"=" when ty = iff_ty -> IFF_CTXIMPCONV
 983         |"!" -> FORALL_CTXIMPCONV
 984         |"?" -> EXISTS_CTXIMPCONV
 985         |"~" -> NOT_CTXIMPCONV
 986         |_ -> failwith "SUB_CTXIMPCONV") c)
 987         v t):imp_conv),
 988     SUB_CTXIMPCONV o augment c,
 989     SUB_CTXIMPCONV o diminish c)
 990
 991 (* Takes a theorem which results of an implicational conversion and applies
 992  * another implicational conversion on the outcome.
 993  *)
 994 let bind_ctximpconv (c:imp_conv with_context) v th =
 995   let t1,t2 = dest_imp (concl th) in
 996   match v with
 997   |Co -> IMP_TRANS (apply c v t1) th
 998   |Contra -> IMP_TRANS th (apply c v t2)
 999
1000 let rec BIND_CTXIMPCONV (c:imp_conv with_context) =
1001   With_context(
1002     ((fun v th -> bind_ctximpconv c v th),
1003     BIND_CTXIMPCONV o augment c,
1004     BIND_CTXIMPCONV o diminish c))
1005
1006 (* Sequential combinator. *)
1007 let rec THEN_CTXIMPCONV (c1:imp_conv with_context) (c2:imp_conv with_context) =
1008   With_context(
1009     ((fun v t -> bind_ctximpconv c2 v (apply c1 v t)):imp_conv),
1010     (fun x -> THEN_CTXIMPCONV (augment c1 x) (augment c2 x)),
1011     (fun x -> THEN_CTXIMPCONV (diminish c1 x) (diminish c2 x)))
1012
1013 (* Try combinator *)
1014 let rec TRY_CTXIMPCONV (c:imp_conv with_context) =
1015     With_context(
1016       ((fun v t ->
1017         try apply c v t
1018         with Failure _ | Unchanged -> ALL_IMPCONV v t):imp_conv),
1019       TRY_CTXIMPCONV o augment c,
1020       TRY_CTXIMPCONV o diminish c)
1021
1022
1023 (* Applies the first of two implicational conversions that succeeds. *)
1024 let rec ORELSE_CTXIMPCONV
1025   (c1:imp_conv with_context) (c2:imp_conv with_context) =
1026   With_context(
1027     ((fun v t -> try apply c1 v t with Failure _ -> apply c2 v t):imp_conv),
1028     (fun x -> ORELSE_CTXIMPCONV (augment c1 x) (augment c2 x)),
1029     (fun x -> ORELSE_CTXIMPCONV (diminish c1 x) (diminish c2 x)))
1030
1031 (* Makes an implicational conversion fail if applying it leaves a term
1032  * unchanged.
1033  *)
1034 let rec CHANGED_CTXIMPCONV (c:imp_conv with_context) =
1035   With_context(
1036     ((fun v t ->
1037       let th = apply c v t in
1038       let l,r = dest_imp (concl th) in
1039       if aconv l r then failwith "CHANGED_CTXIMPCONV" else th):imp_conv),
1040     CHANGED_CTXIMPCONV o augment c,
1041     CHANGED_CTXIMPCONV o diminish c)
1042
1043 let rec UNCHANGED_OF_FAIL_CTXIMPCONV (c:imp_conv with_context) =
1044   With_context(
1045     ((fun v t -> try apply c v t with Failure _ -> raise Unchanged
1046       ):imp_conv),
1047     UNCHANGED_OF_FAIL_CTXIMPCONV o augment c,
1048     UNCHANGED_OF_FAIL_CTXIMPCONV o diminish c)
1049
1050 let rec REPEAT_UNCHANGED_CTXIMPCONV =
1051   let rec map_all f xs x =
1052     match xs with
1053     |[] -> []
1054     |y::ys -> f y x :: map_all f ys x
1055   in
1056   fun (cs:imp_conv with_context list) ->
1057     With_context(
1058       ((fun v t ->
1059         let rec loop changed acc = function
1060           |[] when changed -> loop false acc cs
1061           |[] -> acc
1062           |c::cs' ->
1063               try
1064                 let acc' = bind_ctximpconv c v acc in
1065                 loop true acc' cs'
1066               with Unchanged -> loop changed acc cs'
1067         in
1068         loop false (IMP_REFL t) cs):imp_conv),
1069       REPEAT_UNCHANGED_CTXIMPCONV o map_all augment cs,
1070       REPEAT_UNCHANGED_CTXIMPCONV o map_all diminish cs)
1071
1072
1073 type atomic = Atomic | Non_atomic
1074
1075 let DEPTH_CTXIMPCONV =
1076   let bind c na v th =
1077     let t1,t2 = dest_imp (concl th) in
1078     match v with
1079     |Co -> IMP_TRANS (apply c na v t1) th
1080     |Contra -> IMP_TRANS th (apply c na v t2)
1081   in
1082   let rec self (c:(atomic->imp_conv) with_context) =
1083     With_context(
1084       (fun v t ->
1085         try
1086           let th1 = apply (SUB_CTXIMPCONV (self c)) v t in
1087           (try bind c Non_atomic v th1 with Failure _ -> th1)
1088         with
1089         | Failure "SUB_CTXIMPCONV" ->
1090           let th1 = apply c Atomic v t in
1091           (try bind_ctximpconv (self c) v th1 with Failure _ -> th1)
1092         | Failure _ -> apply c Non_atomic v t),
1093       self o augment c,
1094       self o diminish c)
1095   in
1096   UNCHANGED_OF_FAIL_CTXIMPCONV o self
1097
1098 let TOP_DEPTH_CTXIMPCONV =
1099   let rec self (c:imp_conv with_context) =
1100     With_context(
1101       (fun v t ->
1102         try
1103           let th = apply c v t in
1104           try bind_ctximpconv (self c) v th with Failure _ -> th
1105         with Failure _ -> apply (SUB_CTXIMPCONV (self c)) v t),
1106       self o augment c,
1107       self o diminish c)
1108   in
1109   UNCHANGED_OF_FAIL_CTXIMPCONV o self
1110
1111 let ONCE_DEPTH_CTXIMPCONV =
1112   let rec self (c:(atomic->imp_conv) with_context) =
1113     With_context(
1114       (fun v t ->
1115         try apply (SUB_CTXIMPCONV (self c)) v t
1116         with
1117         | Failure "SUB_CTXIMPCONV" -> apply c Atomic v t
1118         | Failure _ -> apply c Non_atomic v t),
1119       self o augment c,
1120       self o diminish c)
1121   in
1122   UNCHANGED_OF_FAIL_CTXIMPCONV o self
1123
1124
1125 let CTXIMPCONV_RULE (c:imp_conv with_context) th =
1126   MATCH_MP (apply c Contra (concl th)) th
1127
1128 let CTXIMPCONV_TAC (cnv:imp_conv with_context) : tactic =
1129   fun (asms,c as g) ->
1130     let cnv' = augment cnv (map (concl o snd) asms) in
1131     (MATCH_MP_TAC (apply cnv' Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
1132
1133 (*****************************************************************************)
1134 (* REWRITE IMPLICATIONAL CONVERSION                                          *)
1135 (*****************************************************************************)
1136
1137 (* Given a theorem [H1,...,Hn |- P ==> l = r],
1138  * returns the variables that occur in [P] and [r] but not in the rest.
1139  * Basically represents the variables that are introduced by the implicational
1140  * rewrite (similar status as variables occurring in the r.h.s. of a rewrite
1141  * but not in the l.h.s.).
1142  *)
1143 let indep_vars th =
1144   let hs,c = dest_thm (SPEC_ALL th) in
1145   let p,c = dest_imp c in
1146   let all_vars = union (frees p) (frees (rhs c)) in
1147   let dep_vars = union (frees (lhs c)) (freesl hs) in
1148   subtract all_vars dep_vars
1149
1150 (* Given a list of variables to avoid [v1,...,vk], a theorem of the form
1151  * [hs |- !x1...xn. p ==> !y1...ym. l = r], and a term [t], matches [t] with
1152  * [l], yielding the substitution [s], and returns the theorem
1153  * [s(hs) |- !z1...zp. s(p) ==> s(l) = s(r)] where [z1], ..., [zp] are the
1154  * variables among [x1], ..., [xn], [y1], ..., [ym] that are not instantiated
1155  * by [s], and renamed so as to avoid [v1], ..., [vk].
1156  *)
1157 let GEN_IMPREWR_CONV avs =
1158   let sel = lhs o snd o strip_forall o snd o dest_imp in
1159   let pmatch = GEN_PART_MATCH_ALL sel in
1160   fun th ->
1161     let pmatch' = pmatch th in
1162     fun t ->
1163       let th' = pmatch' t in
1164       VARIANT_RULE avs (GENL (indep_vars th') th')
1165
1166 (* A conversion which returns not only a theorem but also a list of terms
1167  * which is a sublist of the theorem hypotheses, and a list of terms which
1168  * are the variables newly introduced by the conversion.
1169  *
1170  * See [IMPREWR_CONV] for an example.
1171  *)
1172 type annot_conv = term -> thm * term option * term list
1173
1174 (* Takes a list of variables to avoid [av], a theorem [th] of the form
1175  * [h1,..,hk |- !x1...xn. p ==> !y1...ym. l = r], and a term [t]
1176  * and returns a conversion with hypotheses defined as follows:
1177  * for a term [t], if [t] matches [l] with substitution [s], then return
1178  * the theorem [h1,...,hk,s(p) |- t = s(r)] and the the list containing only
1179  * [s(p)].
1180  *
1181  * The purpose of the conversion with hypothesis is to be able to distinguish
1182  * which hypothesis comes from the input theorem and which is added by the
1183  * conversion itself.
1184  *)
1185 let IMPREWR_CONV:Tset.t->thm->annot_conv =
1186   fun avs th ->
1187     let f t = SPEC_VARS (GEN_IMPREWR_CONV avs th t) in
1188     fun t ->
1189       let vs,uh = f t in
1190       let u = fst (dest_imp (concl uh)) in
1191       UNDISCH uh,Some u,Tset.of_list vs
1192
1193 let REWR_ANNOTCONV avs th t =
1194   let th' = PART_MATCH lhs th t in
1195   let _,t' = dest_binary_blind (concl th') in
1196   let new_vars = Tset.frees t' in
1197   let old_vars = Tset.union (Tset.frees t) (Tset.freesl (hyp th')) in
1198   th',None,Tset.subtract new_vars old_vars
1199
1200 let ORDER_ANNOTCONV cnv t =
1201   let th,_,_ as res = cnv t in
1202   let l,r = dest_binary_blind (concl th) in
1203   if term_order l r then res else failwith "ORDER_ANNOTCONV"
1204
1205 (* Takes a theorem, a net of conversions with hypotheses (which also take
1206  * variables to avoid), and adds to the net the conversion corresponding to
1207  * the theorem.
1208  *
1209  * Special cases:
1210  * - usual term rewriting is handled with [REWR_CONV] instead of introducing
1211  *   a fake premise. Might be useful though to introduce a fake premise since
1212  *   the conversion would benefit from a better handling of variables occurring
1213  *   in the r.h.s. but not in the l.h.s.
1214  * - a theorem of the form [p ==> c] where [c] is not equational is turned into
1215  *   [p ==> c = T]
1216  * - a theorem of the form [p ==> ~c] is turned into [p ==> c = F]
1217  *)
1218 let pat_cnv_of_thm th : (term * (term list->annot_conv)) =
1219   let th = SPEC_ALL th in
1220   let lconsts = freesl (hyp th) and c = concl th in
1221   match c with
1222   |Comb(Comb(Const("=",_),l),r) as t ->
1223       let matches = C (can o term_match lconsts) in
1224       if free_in l r or (matches l r & matches r l)
1225       then t,C REWR_ANNOTCONV (MAP_FORALL_BODY EQT_INTRO th)
1226       else l,C REWR_ANNOTCONV th
1227   |Comb(Comb(Const("==>",_),p),c) as t ->
1228       let matches = C (can o fo_term_match lconsts) in
1229       let imprewr_concl f = C IMPREWR_CONV (GEN_MAP_CONCLUSION f th) in
1230       (match c with
1231       |Comb(Comb(Const("=",_),l),r) ->
1232           if free_in l r or (matches l r & matches r l) or is_var l
1233           then
1234             if matches p c
1235             then t, C REWR_ANNOTCONV (EQT_INTRO th)
1236             else c, imprewr_concl EQT_INTRO
1237           else l, C IMPREWR_CONV th
1238       |Comb(Const("~",_),l) -> l, imprewr_concl EQF_INTRO
1239       |l -> l, imprewr_concl EQT_INTRO)
1240   |Comb(Const("~",_),l) -> l, C REWR_ANNOTCONV (EQF_INTRO th)
1241   |Const("T",bool_ty) -> failwith "pat_cnv_of_thm"
1242   |l -> l, C REWR_ANNOTCONV (EQT_INTRO th)
1243
1244 let impconv_net_of_thm th =
1245   try
1246     let p,c = pat_cnv_of_thm th in
1247     let vs = Tset.freesl (hyp th) in
1248     Fo_nets.enter vs (p,(c,vs,th))
1249   with Failure _ -> I
1250
1251 let patterns_of_thm = fst o pat_cnv_of_thm
1252
1253 (* Apply a conversion net to the term at the top level, taking
1254  * avoided variables as parameter too.
1255  *)
1256 let REWRITES_IMPCONV
1257   (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t =
1258   tryfind (fun c,_,_ -> c avs t) (Fo_nets.lookup t net)
1259
1260 let extra_basic_rewrites =
1261   itlist (mk_rewrites false) [NOT_FORALL_THM;NOT_IMP] []
1262
1263 let IMPREWR_CTXCONV :thm list -> (atomic->annot_conv) with_context =
1264   let rec top_depth c avs t =
1265     let rec (++) c1 c2 avs t =
1266       match c1 avs t with
1267       |_,Some _,_ as c1t -> c1t
1268       |th1,None,vs1 as c1t ->
1269         (try
1270           let th2,ho2,vs2 = c2 (Tset.union vs1 avs) (rand (concl th1)) in
1271           TRANS th1 th2, ho2, Tset.union vs1 vs2
1272         with Failure _ -> c1t)
1273     and (+) c1 c2 avs t = try (c1 ++ c2) avs t with Failure _ -> c2 avs t
1274     and COMB_QCONV c avs l r =
1275       try
1276         match c avs l with
1277         |th,(Some _ as ho),vs -> AP_THM th r,ho,vs
1278         |th1,None,vs1 ->
1279           (try
1280             let th2,ho2,vs2 = c (Tset.union vs1 avs) r in
1281             MK_COMB (th1,th2), ho2, Tset.union vs1 vs2
1282           with Failure _ -> AP_THM th1 r,None,vs1)
1283       with Failure _ ->
1284         let th2,ho2,vs2 = c avs r in
1285         AP_TERM l th2,ho2,vs2
1286     in
1287     let SUB_QCONV c avs t =
1288       match t with
1289       |Comb(l,r) -> COMB_QCONV c avs l r
1290       |Abs(v,_) ->
1291           let ho = ref None and vs = ref [] in
1292           let c' t =
1293             let th,ho',vs' = c (Tset.insert avs v) t in
1294             ho := ho'; vs := vs'; th
1295           in
1296           let res = ABS_CONV c' t in
1297           res,!ho,!vs
1298       |_ -> failwith "SUB_QCONV"
1299     in
1300     let rec (!) c avs t = (c ++ !c) avs t in
1301     (!c + (SUB_QCONV (top_depth c) ++ top_depth c)) avs t
1302   in
1303   let bigger_net() =
1304     itlist (net_of_thm false) extra_basic_rewrites (basic_net()) in
1305   let basic_cnv t = REWRITES_CONV (bigger_net ()) t,None,[] in
1306   let rec self net ths =
1307     let avs = Tset.flat_revmap (Tset.freesl o hyp) ths in
1308     let cnv avs t =
1309       try REWRITES_IMPCONV net avs t with Failure _ -> basic_cnv t
1310     in
1311     With_context(
1312       (fun a t ->
1313         let f = match a with Atomic -> top_depth | Non_atomic -> I in
1314         f cnv (Tset.union (Tset.frees t) avs) t),
1315       (fun ts ->
1316         let ths' = map ASSUME ts in
1317         (*let ths'' = ths' @ GMATCH_MPS ths ths' in*)
1318         let ths'' = MP_CLOSURE ths' ths' @ ths' @ MP_CLOSURE ths ths' in
1319         self (itlist impconv_net_of_thm ths'' net) (ths'' @ ths)),
1320       (fun v ->
1321         let ths = ref [] in
1322         let f (_,vs,th) =
1323           if not (Tset.mem v vs) then (ths := th :: !ths; true) else false
1324         in
1325         let net' = Fo_nets.filter f net in
1326         self net' !ths))
1327   in
1328   fun ths -> self (itlist impconv_net_of_thm ths Fo_nets.empty_net) ths
1329
1330
1331 (*****************************************************************************)
1332 (* SOME USEFUL IMPLICATIONAL CONVERSIONS                                     *)
1333 (*****************************************************************************)
1334
1335 (* Takes a conversion with hypotheses (with context) and makes an
1336  * implicational conversion out of it.
1337  * Basically turns a rewrite with hypotheses into an implicational rewrite
1338  * withouth hypotheses.
1339  * Adds existential quantifications for variables introduced by the rewrite.
1340  *)
1341 let rec REWR_IMPCONV_OF_CONV =
1342   let IMP_SYM = REWR_RULE (TAUT `A==>B==>C <=> B==>A==>C`) in
1343   let IMP_EXIST = GSYM LEFT_IMP_EXISTS_THM in
1344   let TRY_GEN v th = try GEN v th with Failure _ -> th in
1345   fun (c:(atomic -> annot_conv) with_context) ->
1346     With_context(
1347       ((fun a v t ->
1348         let th,ho,new_vars = apply c a t in
1349         let th1,th2 = EQ_IMP_RULE th in
1350         let res =
1351           match v with
1352           |Co ->
1353               let p,th2' = UNDISCH_TERM th2 in
1354               let rec exists_intro = function
1355                 |[] -> DISCH_IMP_IMP (p::list_of_option ho) th2'
1356                 |v::vs ->
1357                     let th = exists_intro vs in
1358                     try REWR_RULE IMP_EXIST (GEN v th) with Failure _ -> th
1359               in
1360               exists_intro new_vars
1361           |Contra ->
1362               let th1' =
1363                 match ho with None -> th1 | Some h -> IMP_SYM (DISCH h th1)
1364               in
1365               match new_vars with
1366               |[] -> th1'
1367               |_::_ -> MAP_CONCLUSION (itlist TRY_GEN new_vars) th1'
1368         in
1369         let t1,t2 = dest_imp (concl res) in
1370         if t1 = t2 then raise Unchanged else res):atomic->imp_conv),
1371       REWR_IMPCONV_OF_CONV o augment c,
1372       REWR_IMPCONV_OF_CONV o diminish c)
1373
1374 (* Applies the implicational rewrite, with context simplifications. *)
1375 let REWRITE_CTXIMPCONV =
1376   DEPTH_CTXIMPCONV o REWR_IMPCONV_OF_CONV o IMPREWR_CTXCONV
1377
1378
1379 (*****************************************************************************)
1380 (* INTERFACE                                                                 *)
1381 (*****************************************************************************)
1382
1383 (* Preprocessor. For now takes a theorem of the form [p ==> c1 /\ ... /\ ck]
1384  * and returns the list of theorems [p ==> c1], ..., [p ==> ck].
1385  *)
1386 let preprocess = CONJUNCTS o IMPLY_AND
1387
1388 (* Tactic for implicational rewrite. *)
1389 let IMP_REWRITE_TAC ths =
1390   CTXIMPCONV_TAC (REWRITE_CTXIMPCONV (flat (map preprocess ths)))
1391
1392 let SEQ_IMP_REWRITE_TAC ths =
1393   let cnv =
1394     match ths with
1395     |[] -> REWRITE_CTXIMPCONV [TRUTH]
1396     |[th] -> REWRITE_CTXIMPCONV (preprocess th)
1397     |_::_ ->
1398         let fcnv = REWRITE_CTXIMPCONV o preprocess in
1399         REPEAT_UNCHANGED_CTXIMPCONV (map fcnv ths)
1400   in
1401   CTXIMPCONV_TAC cnv
1402
1403 (* Tactic for implicational rewrite with assumptions. *)
1404 let ASM_IMP_REWRITE_TAC = ASM IMP_REWRITE_TAC
1405
1406 (* Cases-like conversion for implicational theorems, i.e., for a theorem of
1407  * the form:
1408  * [h1,..,hk |- !x1...xn. p ==> !y1...ym. l = r], and a term [t],
1409  * return [(p ==> t') /\ (~p ==> t)], where [t'] is the result of rewriting
1410  * [t] by [l=r].
1411  *)
1412 let rec CASE_REWR_IMPCONV_OF_CONV =
1413   let MP_TAUT th = MATCH_MP (TAUT th) in
1414   let MP_LEM1 = MP_TAUT `(~P ==> Q = R) ==> (Q <=> (~P ==> R) /\ (P ==> Q))` in
1415   let MP_LEM2 = MP_TAUT `(P ==> Q = R) ==> (Q <=> (P ==> R) /\ (~P ==> Q))` in
1416   fun (c:(atomic -> annot_conv) with_context) ->
1417     With_context(
1418       (fun a v t ->
1419         match apply c a t with
1420         |_,None,_ -> failwith "CASE_REWR_IMPCONV_OF_CONV"
1421         |th,Some h,_ ->
1422             let th' = DISCH h th in
1423             let th'' = try MP_LEM1 th' with Failure _ -> MP_LEM2 th' in
1424             imp_conv_of_conv (REWR_CONV th'') v t),
1425       CASE_REWR_IMPCONV_OF_CONV o augment c,
1426       CASE_REWR_IMPCONV_OF_CONV o diminish c)
1427
1428 let CASE_REWRITE_CTXIMPCONV =
1429   ONCE_DEPTH_CTXIMPCONV o CASE_REWR_IMPCONV_OF_CONV o IMPREWR_CTXCONV
1430
1431 (* Tactic version of it. *)
1432 let CASE_REWRITE_TAC = CTXIMPCONV_TAC o CASE_REWRITE_CTXIMPCONV o preprocess
1433
1434 (*****************************************************************************)
1435 (* IMPLICATIONAL CONVERSIONS WITH MULTIPLE RESULTS                           *)
1436 (*****************************************************************************)
1437
1438 (* Multiple implicational conversion. *)
1439 type imp_mconv = Variance.t -> term -> thm list
1440
1441 let mapply_with_context c ctx v t =
1442   map (DISCH_CONJ ctx) (apply (augment c (Tset.strip_conj ctx)) v t)
1443
1444 (* Consider two multiple implicational conversions ic1, ic2.
1445  * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A],
1446  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
1447  * then [CONJ_IMPMCONV ic1 ic2 Co (A /\ C)] returns
1448  * [B1 /\ C ==> A /\ C; ...; Bk /\ C ==> A /\ C; A /\ D1 ==> A /\ C; ...; Dn
1449  * ==> A /\ C].
1450  *
1451  * And similarly for the contravariant case.
1452  *)
1453 let rec CONJ_CTXIMPMCONV (c:imp_mconv with_context)
1454   : imp_mconv with_context =
1455   With_context(
1456     (fun v t ->
1457       let t1,t2 = dest_conj t in
1458       let left,right =
1459         match v with
1460         |Co -> MKIMPL_CONJ_CO2_CTXT,MKIMPR_CONJ_CO_CTXT
1461         |Contra -> MKIMPL_CONJ_CONTRA_CTXT,MKIMPR_CONJ_CONTRA_CTXT
1462       in
1463       let th1s = map left (mapply_with_context c t2 v t1) in
1464       let th2s = map right (mapply_with_context c t1 v t2) in
1465       th1s @ th2s),
1466     CONJ_CTXIMPMCONV o augment c,
1467     CONJ_CTXIMPMCONV o diminish c)
1468
1469 (* Consider two multiple implicational conversions ic1, ic2.
1470  * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A],
1471  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
1472  * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns
1473  * [B1 \/ C ==> A \/ C; ...; Bk \/ C ==> A \/ C; A \/ D1 ==> A \/ C; ...; Dn
1474  * ==> A \/ C].
1475  *
1476  * And similarly for the contravariant case.
1477  *)
1478 let rec DISJ_CTXIMPMCONV (c:imp_mconv with_context)
1479   : imp_mconv with_context =
1480   With_context(
1481     (fun v t ->
1482       let t1,t2 = dest_disj t in
1483       let th1s = map (C MKIMPL_DISJ t2) (apply c v t1) in
1484       let th2s = map (MKIMPR_DISJ t1) (apply c v t2) in
1485       th1s @ th2s),
1486     DISJ_CTXIMPMCONV o augment c,
1487     DISJ_CTXIMPMCONV o diminish c)
1488
1489 (* Consider two multiple implicational conversions ic1, ic2.
1490  * Suppose [ic1 Contra A] returns a list [A ==> B1; ...; A ==> Bk],
1491  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
1492  * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns
1493  * [(B1 ==> C) ==> (A ==> C); ...; (Bk ==> C) ==> (A ==> C); (A ==> D1) ==> (A
1494  * ==> C); ...; (A ==> Dn) ==> (A ==> C)].
1495  *
1496  * And similarly for the contravariant case.
1497  *)
1498 let rec IMP_CTXIMPMCONV (c:imp_mconv with_context)
1499   : imp_mconv with_context =
1500   With_context(
1501     (fun v t ->
1502       let t1,t2 = dest_imp t in
1503       let th1s = map (C MKIMPL_IMP t2) (apply c (Variance.neg v) t1) in
1504       let th2s = map MKIMPR_IMP_CTXT (mapply_with_context c t1 v t2) in
1505       th1s @ th2s),
1506     CONJ_CTXIMPMCONV o augment c,
1507     CONJ_CTXIMPMCONV o diminish c)
1508
1509 let rec IFF_CTXIMPCONV (c:imp_mconv with_context) =
1510   With_context(
1511     ((fun v t ->
1512       let t1,t2 = dest_iff t in
1513       let left,right =
1514         match v with
1515         |Co -> MKIMPL_CO_IFF,MKIMPR_CO_IFF
1516         |Contra -> MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
1517       in
1518       let th1s = map left (apply c v (mk_imp(t1,t2))) in
1519       let th2s = map right (apply c v (mk_imp(t2,t1))) in
1520       th1s @ th2s):imp_mconv),
1521     IFF_CTXIMPCONV o augment c,
1522     IFF_CTXIMPCONV o diminish c)
1523
1524 (* Consider one multiple implicational conversion ic.
1525  * Suppose [ic Contra A] returns a list [A ==> B1; ...; A ==> Bk],
1526  * then [NOT_IMPMCONV ic Co ~A] returns [~B1 ==> ~A; ...; ~Bk ==> ~A].
1527  *
1528  * And similarly for the contravariant case.
1529  *)
1530 let rec NOT_CTXIMPMCONV (c:imp_mconv with_context) : imp_mconv with_context =
1531   With_context(
1532     (fun v t ->
1533       map MKIMP_NOT (try_list (apply c (Variance.neg v)) (dest_neg t))),
1534     NOT_CTXIMPMCONV o augment c,
1535     NOT_CTXIMPMCONV o diminish c)
1536
1537 let rec QUANT_CTXIMPMCONV mkimp sel (c:imp_mconv with_context)
1538   : imp_mconv with_context =
1539   With_context(
1540     (fun v t ->
1541       let x,b = sel t in
1542       let c' = diminish c x in
1543       map (mkimp x) (try_list (apply c' v) b)),
1544     QUANT_CTXIMPMCONV mkimp sel o augment c,
1545     QUANT_CTXIMPMCONV mkimp sel o diminish c)
1546
1547 (* Consider one multiple implicational conversion ic.
1548  * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A],
1549  * then [FORALL_IMPMCONV ic Co (!x.A)] returns [(!x.B1) ==> (!x.A); ...;
1550  * (!x.Bk) ==> (!x.A)].
1551  *
1552  * And similarly for the contravariant case.
1553  *)
1554 let FORALL_CTXIMPMCONV = QUANT_CTXIMPMCONV MKIMP_FORALL dest_forall
1555
1556 (* Consider one multiple implicational conversion ic.
1557  * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A],
1558  * then [EXISTS_IMPMCONV ic Co (?x.A)] returns [(?x.B1) ==> (?x.A); ...;
1559  * (?x.Bk) ==> (?x.A)].
1560  *
1561  * And similarly for the contravariant case.
1562  *)
1563 let EXISTS_CTXIMPMCONV = QUANT_CTXIMPMCONV MKIMP_EXISTS dest_exists
1564
1565 (* Applies a multiple implicational conversion on the subformula(s) of the
1566  * input term
1567  *)
1568 let rec SUB_CTXIMPMCONV =
1569   let iff_ty = `:bool->bool->bool` in
1570   fun c ->
1571   With_context(
1572     ((fun v t ->
1573       let n,ty = dest_const (fst (strip_comb t)) in
1574       apply
1575         ((match n with
1576         |"==>" -> IMP_CTXIMPMCONV
1577         |"/\\" -> CONJ_CTXIMPMCONV
1578         |"\\/" -> DISJ_CTXIMPMCONV
1579         |"!" -> FORALL_CTXIMPMCONV
1580         |"?" -> EXISTS_CTXIMPMCONV
1581         |"~" -> NOT_CTXIMPMCONV
1582         |"=" when ty = iff_ty -> IFF_CTXIMPCONV
1583         |_ -> failwith "SUB_CTXIMPMCONV") c) v t):imp_mconv),
1584     SUB_CTXIMPMCONV o augment c,
1585     SUB_CTXIMPMCONV o diminish c)
1586
1587
1588 (* Applies a multiple implicational conversion once to the first suitable sub-term(s)
1589  * encountered in bottom-up order.
1590  *)
1591 let rec DEPTH_CTXIMPMCONV (c : (atomic->imp_mconv) with_context) =
1592   With_context(
1593     (fun v t ->
1594       try
1595         let ths = apply (SUB_CTXIMPMCONV (DEPTH_CTXIMPMCONV c)) v t in
1596         apply c Non_atomic v t @ ths
1597       with Failure "SUB_CTXIMPMCONV" ->
1598         (apply c Atomic v t)),
1599       DEPTH_CTXIMPMCONV o augment c,
1600       DEPTH_CTXIMPMCONV o diminish c)
1601
1602
1603 (*****************************************************************************)
1604 (* REWRITE IMPLICATIONAL CONVERSIONS                                         *)
1605 (*****************************************************************************)
1606
1607 (* Multiple implicational conversion with hypotheses. *)
1608 type annot_mconv = term -> (thm * term option * term list) list
1609
1610 (* Takes a theorem, a net of conversions with hypotheses (which also take
1611  * variables to avoid), and adds to the net the conversion corresponding to
1612  * the theorem.
1613  *
1614  * Special cases:
1615  * - usual term rewriting is handled with [REWR_CONV] instead of introducing
1616  *   a fake premise. Might be useful though to introduce a fake premise since
1617  *   the conversion would benefit from a better handling of variables occurring
1618  *   in the r.h.s. but not in the l.h.s.
1619  * - a theorem of the form [p ==> c] where [c] is not equational is turned into
1620  *   [p ==> c = T]
1621  * - a theorem of the form [p ==> ~c] is turned into [p ==> c = F]
1622  *)
1623 let target_pat_cnv_of_thm th : (term * (term list->annot_conv)) =
1624   let th = SPEC_ALL th in
1625   match concl th with
1626   |Comb(Comb(Const("=",_),l),_) -> l,C REWR_ANNOTCONV th
1627   |Comb(Comb(Const("==>",_),_),c) ->
1628       let pat,th' =
1629         match c with
1630         |Comb(Comb(Const("=",_),l),_) -> l, th
1631         |Comb(Const("~",_),l) -> l, GEN_MAP_CONCLUSION EQF_INTRO th
1632         |l -> c, GEN_MAP_CONCLUSION EQT_INTRO th
1633       in
1634       pat, C IMPREWR_CONV th'
1635   |Comb(Const("~",_),l) -> l, C REWR_ANNOTCONV (EQF_INTRO th)
1636   |Const("T",bool_ty) -> failwith "target_pat_cnv_of_thm"
1637   |l -> l, C REWR_ANNOTCONV (EQT_INTRO th)
1638
1639 let target_impconv_net_of_thm th =
1640   try
1641     let p,c = target_pat_cnv_of_thm th in
1642     let vs = Tset.freesl (hyp th) in
1643     Fo_nets.enter vs (p,(c,vs,th))
1644   with Failure _ -> I
1645
1646 let target_patterns_of_thm = fst o target_pat_cnv_of_thm
1647
1648 (* Multiple conversion which returns all the possible rewrites (on one subterm
1649  * only) by one theorem.
1650  *)
1651
1652 let DEEP_IMP_REWR_MCONV:thm list->(atomic->annot_mconv) with_context =
1653   let map_fst f (x,y,z) = f x,y,z in
1654   let COMB_MCONV c l r =
1655     map (map_fst (C AP_THM r)) (c l) @ map (map_fst (AP_TERM l)) (c r)
1656   and ABS_MCONV c v b =
1657     let ths = c b in
1658     try map (map_fst (ABS v)) ths
1659     with Failure _ ->
1660       let gv = genvar(type_of v) in
1661       let f (gth,ho,vs) =
1662         let gtm = concl gth in
1663         let l,r = dest_eq gtm in
1664         let v' = variant (frees gtm) v in
1665         let l' = alpha v' l and r' = alpha v' r in
1666         EQ_MP (ALPHA gtm (mk_eq(l',r'))) gth,ho,vs
1667       in
1668       let b' = vsubst[gv,v] b in
1669       map f (map (map_fst (ABS gv)) (c b'))
1670   in
1671   let SUB_MCONV c = function
1672     |Comb(l,r) -> COMB_MCONV c l r
1673     |Abs(v,b) -> ABS_MCONV c v b
1674     |Const _ | Var _ -> []
1675   in
1676   let rec top_depth c t = SUB_MCONV (top_depth c) t @ c t in
1677   let REWRITES_IMPCONV (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t =
1678     mapfilter (fun c,_,_ -> c avs t) (Fo_nets.lookup t net)
1679   in
1680   let rec self net ths =
1681     let avs = Tset.flat_revmap (Tset.freesl o hyp) ths in
1682     With_context(
1683       (fun a t ->
1684         let avs' = Tset.union (Tset.frees t) avs in
1685         let cnv t = REWRITES_IMPCONV net avs' t in
1686         let f =
1687           match a with
1688           |Atomic -> top_depth
1689           |Non_atomic -> (fun cnv avs -> cnv avs)
1690         in
1691         f cnv t),
1692       (fun _ -> self net ths),
1693       (fun v ->
1694         let ths = ref [] in
1695         let f (_,vs,th) =
1696           if not (Tset.mem v vs) then (ths := th :: !ths; true) else false
1697         in
1698         let net' = Fo_nets.filter f net in
1699         self net' !ths))
1700   in
1701   fun ths ->
1702     self (itlist target_impconv_net_of_thm ths Fo_nets.empty_net) ths
1703
1704 (* Takes a multiple conversion with hypotheses (which also takes a context as
1705  * parameter) and makes a multiple implicational conversion out of it.
1706  *
1707  * Basically extends [GENERAL_REWRITE_IMPCONV] to the multiple conversion
1708  * case.
1709  *)
1710 let rec REWR_IMPMCONV_OF_MCONV =
1711   let IMP_SYM = REWR_RULE (TAUT `A==>B==>C <=> B==>A==>C`) in
1712   let IMP_EXIST = GSYM LEFT_IMP_EXISTS_THM in
1713   let TRY_GEN v th = try GEN v th with Failure _ -> th in
1714   fun (c:(atomic -> annot_mconv) with_context) ->
1715     With_context(
1716       ((fun a v t ->
1717         let f (th,ho,new_vars) =
1718           let th1,th2 = EQ_IMP_RULE th in
1719           match v with
1720           |Co ->
1721               let p,th2' = UNDISCH_TERM th2 in
1722               let rec exists_intro = function
1723                 |[] -> DISCH_IMP_IMP (p::list_of_option ho) th2'
1724                 |v::vs ->
1725                     let th = exists_intro vs in
1726                     try REWR_RULE IMP_EXIST (GEN v th) with Failure _ -> th
1727               in
1728               exists_intro new_vars
1729           |Contra ->
1730               let th1' =
1731                 match ho with None -> th1 | Some h -> IMP_SYM (DISCH h th1)
1732               in
1733               match new_vars with
1734               |[] -> th1'
1735               |_::_ -> MAP_CONCLUSION (itlist TRY_GEN new_vars) th1'
1736         in
1737         map f (apply c a t)):atomic->imp_mconv),
1738       REWR_IMPMCONV_OF_MCONV o augment c,
1739       REWR_IMPMCONV_OF_MCONV o diminish c)
1740
1741
1742 (*****************************************************************************)
1743 (* TARGET REWRITING                                                          *)
1744 (*****************************************************************************)
1745
1746 let EXISTS_CTXIMPCONV:imp_conv with_context =
1747   let EXISTSs i p =
1748     let codom,dom = unzip i in
1749     let f i ps = vsubst [i] (snd (dest_exists (hd ps))) :: ps in
1750     let h::ps = rev_itlist f i [list_mk_exists(dom,p)] in
1751     rev_itlist EXISTS (zip ps (rev codom)) (ASSUME h)
1752   in
1753   let LEFT_FORALL_IMP = REWR_RULE LEFT_FORALL_IMP_THM in
1754   let rec self ts =
1755     With_context
1756     ((fun v t ->
1757       match v,t with
1758       |Co,Comb(Const("?",_),_) ->
1759           let vs,b = strip_exists t in
1760           let bs = strip_conj b in
1761           let hmatch (n,b) =
1762             match partition (C mem vs) (variables b) with
1763             |[],_ -> failwith "EXISTS_CTXIMPCONV"
1764             |_::_ as lvs,lcs ->
1765                 fun h ->
1766                   match term_match lcs b h with
1767                   |_,i,j when filter (uncurry (<>)) j = [] ->
1768                       (if i = [] then zip lvs lvs else i),n
1769                   |_ -> failwith "EXISTS_CTXIMPCONV"
1770           in
1771           let s,n = tryfind_fun (mapfilteri (curry (tryfind o hmatch)) bs) ts in
1772           let th = EXISTSs (map (fun v -> rev_assocd v s v,v) vs) b in
1773           let th' = DISCH_HD th in
1774           let h = fst (dest_imp (concl th')) in
1775           (match strip_conj h with
1776           |[] -> assert false
1777           |[h] -> DISCH T_ th
1778           |_::_ as hs ->
1779             let hs1,h'::hs2 = chop_list n hs in
1780             let hs_th = CONJ_ACI_RULE (mk_eq(h,list_mk_conj (h'::(hs1@hs2)))) in
1781             let th1 = CONV_RULE (LAND_CONV (REWR_CONV hs_th)) th' in
1782             let th2 = UNDISCH (CONV_RULE (REWR_CONV IMP_CONJ) th1) in
1783             let vs' = subtract vs (map snd s) in
1784             let f v th = try LEFT_FORALL_IMP (GEN v th) with Failure _ -> th in
1785             itlist f vs' th2)
1786       |_ -> failwith "EXISTS_CTXIMPCONV"),
1787       (fun ts' -> self (Tset.union ts' ts)),
1788       (fun _ -> self ts))
1789   in
1790   self []
1791
1792 (* Takes a theorem which results of an implicational conversion and applies a
1793  * multiple implicational conversion on the outcome.
1794  *)
1795 let bind_impmconv (c:imp_mconv) v th =
1796   let t1,t2 = dest_imp (concl th) in
1797   match v with
1798   |Co -> map (C IMP_TRANS th) (c v t1)
1799   |Contra -> map (IMP_TRANS th) (c v t2)
1800
1801
1802 (* Target rewrite implicational conversion:
1803  * [TARGET_REWRITE_IMPCONV sths ts] is an implicational conversion which
1804  * applies all the possible implicational rewrites on the input term until
1805  * one of the resulting terms matches one of the terms in [ts].
1806  *
1807  * Note that we allow several target terms and not just one. See
1808  * TARGET_REWRITE_TAC for a justification.
1809  *)
1810 let TARGET_REWRITE_IMPCONV : thm list -> term list -> imp_conv =
1811   let PRE = apply (TRY_CTXIMPCONV (REWRITE_CTXIMPCONV [])) in
1812   let POST = TRY_CTXIMPCONV (TOP_DEPTH_CTXIMPCONV EXISTS_CTXIMPCONV) in
1813   fun sths ->
1814     let one_step_sths v uh =
1815       let pre v th = try bind_impconv PRE v th with Unchanged -> th in
1816       let post v = bind_ctximpconv POST v in
1817       let f =
1818         DEPTH_CTXIMPMCONV o REWR_IMPMCONV_OF_MCONV o DEEP_IMP_REWR_MCONV
1819       in
1820       map (post v) (bind_impmconv (apply (f sths)) v (pre v uh))
1821     in
1822     let flat l = uniq (itlist (merge thm_lt) l []) in
1823     fun ts v t ->
1824       let rec self ths =
1825         let pool = flat (map (mergesort thm_lt o one_step_sths v) ths) in
1826         let sel th = imp_conv_outcome th v in
1827         let is_one_sol g = (can o find_term o can o fo_term_match []) g o sel in
1828         let is_sol th = tryfind is_one_sol ts th in
1829         try bind_ctximpconv POST v (find is_sol pool)
1830         with _ ->
1831           match pool with
1832           |[] -> failwith "TARGET_REWRITE_IMPCONV: no path found"
1833           |_::_ -> self (map (bind_ctximpconv POST v) pool)
1834       in
1835       self [IMP_REFL t]
1836
1837 (* Tactic version of it.
1838  *
1839  * Since the target theorem is preprocessed, it can yield several theorems.
1840  * Therefore, there is not just one possible target pattern but several.
1841  *)
1842 let TARGET_REWRITE_TAC sths th =
1843   let sths' = flat (map preprocess sths) in
1844   let ths = preprocess th and (+) = THEN_IMPCONV in
1845   IMPCONV_TAC
1846   (TARGET_REWRITE_IMPCONV sths' (map patterns_of_thm ths)
1847     + imp_conv_of_ctx_imp_conv (REWRITE_CTXIMPCONV ths))
1848
1849 let HINT_EXISTS_TAC = CTXIMPCONV_TAC (TOP_DEPTH_CTXIMPCONV EXISTS_CTXIMPCONV)
1850
1851 end in
1852
1853 Impconv.IMP_REWRITE_TAC,
1854 Impconv.TARGET_REWRITE_TAC,
1855 Impconv.HINT_EXISTS_TAC,
1856 Impconv.SEQ_IMP_REWRITE_TAC,
1857 Impconv.CASE_REWRITE_TAC;;