impconv.ml.patch

18,19c18,22
< let IMP_REWRITE_TAC,TARGET_REWRITE_TAC,HINT_EXISTS_TAC,
<     SEQ_IMP_REWRITE_TAC,CASE_REWRITE_TAC =
---
> (* OA: Reorganized this file b/c first-class modules.
> 
>        Lots of the syntax was incompatible with out parser, and there was
>        an 'open' somewhere in there.
>  *)
21c24
< let I = fun x -> x in
---
> module Impconv = struct
26c29
<   p,UNDISCH th in
---
>   p,UNDISCH th ;;
34c37
<   with Failure _ -> [],th in
---
>   with Failure _ -> [],th ;;
39c42
<   DISCH p (f th) in
---
>   DISCH p (f th) ;;
41c44
< let strip_conj = binops `(/\)` in
---
> let strip_conj = binops `(/\)` ;;
47c50
<   |f::fs' -> try f x with Failure _ -> tryfind_fun fs' x in
---
>   |f::fs' -> try f x with Failure _ -> tryfind_fun fs' x ;;
58c61
<   self 0 in
---
>   self 0 ;;
60c63
< let list_of_option = function None -> [] | Some x -> [x] in
---
> let list_of_option = function None -> [] | Some x -> [x] ;;
62c65
< let try_list f x = try f x with Failure _ -> [] in
---
> let try_list f x = try f x with Failure _ -> [] ;;
65,66c68,69
< let A_ = `A:bool` and B_ = `B:bool` and C_ = `C:bool` and D_ = `D:bool` in
< let T_ = `T:bool` in
---
> let A_Tm = `A:bool` and B_Tm = `B:bool` and C_Tm = `C:bool` and D_Tm = `D:bool`
> and T_Tm = `T:bool` ;;
71c74
<   fun t -> INST [t,A_] lem in
---
>   fun t -> INST [t,A_Tm] lem ;;
81c84
<   DEPTH_CONV (fun u -> ALPHA_CONV (assoc (bndvar u) mapping) u) t in
---
>   DEPTH_CONV (fun u -> ALPHA_CONV (assoc (bndvar u) mapping) u) t ;;
84c87
< let VARIANT_RULE = CONV_RULE o VARIANT_CONV in
---
> let VARIANT_RULE = CONV_RULE o VARIANT_CONV ;;
87c90
< let DISCH_HD th = DISCH (hd (hyp th)) th in
---
> let DISCH_HD th = DISCH (hd (hyp th)) th ;;
90c93
< let REWR_RULE = CONV_RULE o REWR_CONV in
---
> let REWR_RULE = CONV_RULE o REWR_CONV ;;
100c103
<   f o rev in
---
>   f o rev ;;
107c110
<   with Failure _ -> DISCH t th in
---
>   with Failure _ -> DISCH t th ;;
117c120
<   with Failure _ -> [],th in
---
>   with Failure _ -> [],th ;;
122c125
<   GENL vs (f th) in
---
>   GENL vs (f th) ;;
127c130
< let GEN_MAP_CONCLUSION = MAP_FORALL_BODY o MAP_CONCLUSION o MAP_FORALL_BODY in
---
> let GEN_MAP_CONCLUSION = MAP_FORALL_BODY o MAP_CONCLUSION o MAP_FORALL_BODY ;;
139c142
<     RIGHT_IMP_FORALL_THM;IMPLY_AND_RDISTRIB;GSYM CONJ_ASSOC] in
---
>     RIGHT_IMP_FORALL_THM;IMPLY_AND_RDISTRIB;GSYM CONJ_ASSOC] ;;
146c149
<   |_ -> failwith "dest_binary_blind" in
---
>   |_ -> failwith "dest_binary_blind" ;;
148c151
< let spec_all = repeat (snd o dest_forall) in
---
> let spec_all = repeat (snd o dest_forall) ;;
150c153
< let thm_lt (th1:thm) th2 = th1 < th2 in
---
> let thm_lt (th1:thm) th2 = Thm.(<) th1 th2 ;;
181c184
<       loop [] hs in
---
>       loop [] hs ;;
198c201
<     self [] th1 ths1' ths2 in
---
>     self [] th1 ths1' ths2 ;;
208c211
<   self ths2 ths1 in
---
>   self ths2 ths1 ;;
211,319c214,308
< let module Tset =
<   struct
<     type t = term list
<     let cmp (x:term) y = Pervasives.compare x y
<     let lt (x:term) y = Pervasives.compare x y < 0
<     let lift f = List.sort cmp o f
<     let of_list = lift I
<     let insert ts t =
<       let rec self = function
<         |[] -> [t]
<         |x::xs when lt x t -> x::self xs
<         |x::_ as xs when x = t -> xs
<         |xs -> t::xs
<       in
<       if t = T_ then ts else self ts
<     let remove ts t =
<       let rec self = function
<         |[] -> []
<         |x::xs when lt x t -> x::self xs
<         |x::xs when x = t -> xs
<         |_::_ as xs -> xs
<       in
<       self ts
<     let strip_conj =
<       let rec self acc t =
<         try
<           let t1,t2 = dest_conj t in
<           self (self acc t1) t2
<         with Failure _ -> insert acc t
<       in
<       self []
<     let rec union l1 l2 =
<       match l1 with
<       |[] -> l2
<       |h1::t1 ->
<           match l2 with
<           |[] -> l1
<           |h2::t2 when lt h1 h2 -> h1::union t1 l2
<           |h2::t2 when h1 = h2 -> h1::union t1 t2
<           |h2::t2 -> h2::union l1 t2
<     let rec mem x = function
<       |x'::xs when x' = x -> true
<       |x'::xs when lt x' x -> mem x xs
<       |_ -> false
<     let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1
<     let empty = []
<     let flat_revmap f =
<       let rec self acc = function
<         |[] -> acc
<         |x::xs -> self (union (f x) acc) xs
<       in
<       self []
<     let flat_map f = flat_revmap f o rev
<     let rec frees acc = function
<       |Var _ as t -> insert acc t
<       |Const _ -> acc
<       |Abs(v,b) -> remove (frees acc b) v
<       |Comb(u,v) -> frees (frees acc u) v
<     let freesl ts = itlist (C frees) ts empty
<     let frees = frees empty
<   end in
< 
< let module Type_annoted_term =
<   struct
<     type t =
<       |Var_ of string * hol_type
<       |Const_ of string * hol_type * term
<       |Comb_ of t * t * hol_type
<       |Abs_ of t * t * hol_type
< 
<     let type_of = function
<       |Var_(_,ty) -> ty
<       |Const_(_,ty,_) -> ty
<       |Comb_(_,_,ty) -> ty
<       |Abs_(_,_,ty) -> ty
< 
<     let rec of_term = function
<       |Var(s,ty) -> Var_(s,ty)
<       |Const(s,ty) as t -> Const_(s,ty,t)
<       |Comb(u,v) ->
<           let u' = of_term u and v' = of_term v in
<           Comb_(u',v',snd (dest_fun_ty (type_of u')))
<       |Abs(x,b) ->
<           let x' = of_term x and b' = of_term b in
<           Abs_(x',b',mk_fun_ty (type_of x') (type_of b'))
< 
<     let rec equal t1 t2 =
<       match t1,t2 with
<       |Var_(s1,ty1),Var_(s2,ty2)
<       |Const_(s1,ty1,_),Const_(s2,ty2,_) -> s1 = s2 && ty1 = ty2
<       |Comb_(u1,v1,_),Comb_(u2,v2,_) -> equal u1 u2 && equal v1 v2
<       |Abs_(v1,b1,_),Abs_(v2,b2,_) -> equal v1 v2 && equal b1 b2
<       |_ -> false
< 
<     let rec to_term = function
<       |Var_(s,ty) -> mk_var(s,ty)
<       |Const_(_,_,t) -> t
<       |Comb_(u,v,_) -> mk_comb(to_term u,to_term v)
<       |Abs_(v,b,_) -> mk_abs(to_term v,to_term b)
< 
<     let dummy = Var_("",aty)
< 
<     let rec find_term p t =
<       if p t then t else
<         match t with
<         |Abs_(_,b,_) -> find_term p b
<         |Comb_(u,v,_) -> try find_term p u with Failure _ -> find_term p v
<         |_ -> failwith "Annot.find_term"
<   end in
---
> module Tset = struct
>   (*type t = term list*) (* TODO Makes CakeML pretty printer system dizzy *)
>   let lift f = List.sort Term.(<) o f
>   let of_list = lift I
>   let insert ts t =
>     let rec self xs = match xs with
>       |[] -> [t]
>       |x::xs when Term.(<) x t -> x::self xs
>       |x::_ as xs when x = t -> xs
>       |xs -> t::xs
>     in
>     if t = T_Tm then ts else self ts
>   let remove ts t =
>     let rec self xs = match xs with
>       |[] -> []
>       |x::xs when Term.(<) x t -> x::self xs
>       |x::xs when x = t -> xs
>       |_::_ as xs -> xs
>     in
>     self ts
>   let strip_conj =
>     let rec self acc t =
>       try
>         let t1,t2 = dest_conj t in
>         self (self acc t1) t2
>       with Failure _ -> insert acc t
>     in
>     self []
>   let rec union l1 l2 =
>     match l1 with
>     |[] -> l2
>     |h1::t1 ->
>         match l2 with
>         |[] -> l1
>         |h2::t2 when Term.(<) h1 h2 -> h1::union t1 l2
>         |h2::t2 when h1 = h2 -> h1::union t1 t2
>         |h2::t2 -> h2::union l1 t2
>   let rec mem x = function
>     |x'::xs when x' = x -> true
>     |x'::xs when Term.(<) x' x -> mem x xs
>     |_ -> false
>   let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1
>   let empty = []
>   let flat_revmap f =
>     let rec self acc = function
>       |[] -> acc
>       |x::xs -> self (union (f x) acc) xs
>     in
>     self []
>   let flat_map f = flat_revmap f o rev
>   let rec frees acc = function
>     |Var (_,_) as t -> insert acc t
>     |Const (_,_) -> acc
>     |Abs(v,b) -> remove (frees acc b) v
>     |Comb(u,v) -> frees (frees acc u) v
>   let freesl ts = itlist (C frees) ts empty
>   let frees = frees empty
> end ;;
> 
> module Annot = struct
>   type t =
>     |Var_ of string * hol_type
>     |Const_ of string * hol_type * term
>     |Comb_ of t * t * hol_type
>     |Abs_ of t * t * hol_type
> 
>   let type_of = function
>     |Var_(_,ty) -> ty
>     |Const_(_,ty,_) -> ty
>     |Comb_(_,_,ty) -> ty
>     |Abs_(_,_,ty) -> ty
> 
>   let rec of_term tm = match tm with
>     |Var(s,ty) -> Var_(s,ty)
>     |Const(s,ty) as t -> Const_(s,ty,t)
>     |Comb(u,v) ->
>         let u' = of_term u and v' = of_term v in
>         Comb_(u',v',snd (dest_fun_ty (type_of u')))
>     |Abs(x,b) ->
>         let x' = of_term x and b' = of_term b in
>         Abs_(x',b',mk_fun_ty (type_of x') (type_of b'))
> 
>   let rec equal t1 t2 =
>     match t1,t2 with
>     |Var_(s1,ty1),Var_(s2,ty2)
>     |Const_(s1,ty1,_),Const_(s2,ty2,_) -> s1 = s2 && ty1 = ty2
>     |Comb_(u1,v1,_),Comb_(u2,v2,_) -> equal u1 u2 && equal v1 v2
>     |Abs_(v1,b1,_),Abs_(v2,b2,_) -> equal v1 v2 && equal b1 b2
>     |_ -> false
> 
>   let rec to_term tm = match tm with
>     |Var_(s,ty) -> mk_var(s,ty)
>     |Const_(_,_,t) -> t
>     |Comb_(u,v,_) -> mk_comb(to_term u,to_term v)
>     |Abs_(v,b,_) -> mk_abs(to_term v,to_term b)
321c310,318
< let module Annot = Type_annoted_term in
---
>   let dummy = Var_("",aty)
> 
>   let rec find_term p t =
>     if p t then t else
>       match t with
>       |Abs_(_,b,_) -> find_term p b
>       |Comb_(u,v,_) -> try find_term p u with Failure _ -> find_term p v
>       |_ -> failwith "Annot.find_term"
> end ;;
332a330,336
> let rec rev_map acc f xs =
>   match xs with
>   | [] -> acc
>   | x::xs -> rev_map (f x::acc) f xs;;
> 
> let rev_map f xs = rev_map [] f xs;;
> 
335c339
<   let rec self bnds (tenv,tyenv as env) p t =
---
>   let rec self bnds ((tenv,tyenv) as env) p t =
346c350
<     |Var(n,ty) as v,t ->
---
>     | (Var(n,ty) as v),t ->
366c370
<   List.rev_map (fun t,v -> Annot.to_term t,inst v) tenv,tyenv in
---
>   rev_map (fun t,v -> Annot.to_term t,inst v) tenv,tyenv ;;
395c399
<       if Pervasives.compare tm' tm = 0 then fth else
---
>       if tm' = tm then fth else
397c401
<       with Failure _ -> failwith "PART_MATCH: Sanity check failure" in
---
>       with Failure _ -> failwith "PART_MATCH: Sanity check failure" ;;
399,434c403,437
< let module Fo_nets =
<   struct
<     type term_label =
<       |Vnet of int
<       |Lcnet of string * int
<       |Cnet of string * int
<       |Lnet of int
< 
<     type 'a t = Netnode of (term_label * 'a t) list * 'a list
< 
<     let empty_net = Netnode([],[])
< 
<     let enter =
<       let label_to_store lcs t =
<         let op,args = strip_comb t in
<         let nargs = length args in
<         match op with
<         |Const(n,_) -> Cnet(n,nargs),args
<         |Abs(v,b) ->
<           let b' = if mem v lcs then vsubst [genvar(type_of v),v] b else b in
<           Lnet nargs,b'::args
<         |Var(n,_) when mem op lcs -> Lcnet(n,nargs),args
<         |Var(_,_) -> Vnet nargs,args
<         |_ -> assert false
<       in
<       let rec net_update lcs elem (Netnode(edges,tips)) = function
<         |[] -> Netnode(edges,elem::tips)
<         |t::rts ->
<             let label,nts = label_to_store lcs t in
<             let child,others =
<               try (snd F_F I) (remove (fun (x,y) -> x = label) edges)
<               with Failure _ -> empty_net,edges in
<             let new_child = net_update lcs elem child (nts@rts) in
<             Netnode ((label,new_child)::others,tips)
<       in
<       fun lcs (t,elem) net -> net_update lcs elem net [t]
---
> module Fo_nets = struct
>   type term_label =
>     |Vnet of int
>     |Lcnet of string * int
>     |Cnet of string * int
>     |Lnet of int
> 
>   type 'a t = Netnode of (term_label * 'a t) list * 'a list
> 
>   let empty_net = Netnode([],[])
> 
>   let enter lcs =
>     let label_to_store lcs t =
>       let op,args = strip_comb t in
>       let nargs = length args in
>       match op with
>       |Const(n,_) -> Cnet(n,nargs),args
>       |Abs(v,b) ->
>         let b' = if mem v lcs then vsubst [genvar(type_of v),v] b else b in
>         Lnet nargs,b'::args
>       |Var(n,_) when mem op lcs -> Lcnet(n,nargs),args
>       |Var(_,_) -> Vnet nargs,args
>       |_ -> raise Bind (* assert false *)
>     in
>     let rec net_update lcs elem (Netnode(edges,tips)) = function
>       |[] -> Netnode(edges,elem::tips)
>       |t::rts ->
>           let label,nts = label_to_store lcs t in
>           let child,others =
>             try (snd F_F I) (remove (fun (x,y) -> x = label) edges)
>             with Failure _ -> empty_net,edges in
>           let new_child = net_update lcs elem child (nts@rts) in
>           Netnode ((label,new_child)::others,tips)
>     in
>     fun (t,elem) net -> net_update lcs elem net [t]
436,463c439,464
<     let lookup =
<       let label_for_lookup t =
<         let op,args = strip_comb t in
<         let nargs = length args in
<         match op with
<         |Const(n,_) -> Cnet(n,nargs),args
<         |Abs(_,b) -> Lnet nargs,b::args
<         |Var(n,_) -> Lcnet(n,nargs),args
<         |Comb _ -> assert false
<       in
<       let rec follow (Netnode(edges,tips)) = function
<         |[] -> tips
<         |t::rts ->
<             let label,nts = label_for_lookup t in
<             let collection =
<               try follow (assoc label edges) (nts@rts) with Failure _ -> []
<             in
<             let rec support = function
<               |[] -> [0,rts]
<               |t::ts ->
<                   let ((k,nts')::res') as res = support ts in
<                   (k+1,(t::nts'))::res
<             in
<             let follows =
<               let f (k,nts) =
<                 try follow (assoc (Vnet k) edges) nts with Failure _ -> []
<               in
<               map f (support nts)
---
>   let lookup t =
>     let label_for_lookup t =
>       let op,args = strip_comb t in
>       let nargs = length args in
>       match op with
>       |Const(n,_) -> Cnet(n,nargs),args
>       |Abs(_,b) -> Lnet nargs,b::args
>       |Var(n,_) -> Lcnet(n,nargs),args
>       |Comb (_,_) -> raise Bind (* assert false *)
>     in
>     let rec follow (Netnode(edges,tips)) = function
>       |[] -> tips
>       |t::rts ->
>           let label,nts = label_for_lookup t in
>           let collection =
>             try follow (assoc label edges) (nts@rts) with Failure _ -> []
>           in
>           let rec support xs = match xs with
>             |[] -> [0,rts]
>             |t::ts ->
>                 let ((k,nts')::res') as res = support ts in
>                 (k+1,(t::nts'))::res
>           in
>           let follows =
>             let f (k,nts) =
>               try follow (assoc (Vnet k) edges) nts with Failure _ -> []
465,467c466,470
<             collection @ flat follows
<       in
<       fun t net -> follow net [t]
---
>             map f (support nts)
>           in
>           collection @ flat follows
>     in
>     fun net -> follow net [t]
469,479c472,481
<     let rec filter p (Netnode(edges,tips)) =
<       Netnode(
<         List.map (fun l,n -> l,filter p n) edges,
<         List.filter p tips)
<   end in
< 
< let module Variance =
<   struct
<     type t = Co | Contra
<     let neg = function Co -> Contra | Contra -> Co
<   end in
---
>   let rec filter p (Netnode(edges,tips)) =
>     Netnode(
>       List.map (fun l,n -> l,filter p n) edges,
>       List.filter p tips)
> end ;;
> 
> module Variance = struct
>   type t = Co | Contra
>   let neg = function Co -> Contra | Contra -> Co
> end ;;
487,488d488
< let module Impconv =
<   struct
492c492
<   MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>   MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
518c518
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
531c531
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
538c538
<     MP (INST [a,A_;b,B_;c,C_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm] lem) th
547c547
<     MP (INST [a,A_;b,B_;d,D_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;d,D_Tm] lem) th
556c556
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
565c565
<     MP (INST [a,A_;b,B_;c,C_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm] lem) th
572c572
<     MP (INST [a,A_;b,B_;d,D_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;d,D_Tm] lem) th
579c579
<   MP (INST [a,A_;b,B_;c,C_;d,D_] MONO_IMP) (CONJ th1 th2)
---
>   MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] MONO_IMP) (CONJ th1 th2)
582c582
<   let lem' = REWRITE_RULE[] (INST [C_,D_] lem) in
---
>   let lem' = REWRITE_RULE[] (INST [C_Tm,D_Tm] lem) in
585c585
<     MP (INST [a,A_;b,B_;t,C_] lem') th
---
>     MP (INST [a,A_Tm;b,B_Tm;t,C_Tm] lem') th
601c601
<   let MONO_IMP' = REWRITE_RULE[] (INST [C_,D_] MONO_IMP) in
---
>   let MONO_IMP' = REWRITE_RULE[] (INST [C_Tm,D_Tm] MONO_IMP) in
604c604
<     MP (INST [a,A_;b,B_;t,C_] MONO_IMP') th
---
>     MP (INST [a,A_Tm;b,B_Tm;t,C_Tm] MONO_IMP') th
607c607
<   let lem' = REWRITE_RULE[] (INST [A_,B_] lem) in
---
>   let lem' = REWRITE_RULE[] (INST [A_Tm,B_Tm] lem) in
610c610
<     MP (INST [c,C_;d,D_;t,A_] lem') th
---
>     MP (INST [c,C_Tm;d,D_Tm;t,A_Tm] lem') th
630c630
<   MP (INST [a,A_;b,B_] MONO_NOT) th
---
>   MP (INST [a,A_Tm;b,B_Tm] MONO_NOT) th
660c660
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
668c668
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
679c679
<     MP (INST [c,C_;d,D_;a,A_] lem) th
---
>     MP (INST [c,C_Tm;d,D_Tm;a,A_Tm] lem) th
691c691
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
698c698
<     MP (INST [a,A_;b,B_;c,C_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm] lem) th
705c705
<     MP (INST [a,A_;c,C_;d,D_] lem) th
---
>     MP (INST [a,A_Tm;c,C_Tm;d,D_Tm] lem) th
712c712
<     MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2)
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm;d,D_Tm] lem) (CONJ th1 th2)
718c718
<     fun c -> MP (INST [a,A_;b,B_;c,C_] lem) th
---
>     fun c -> MP (INST [a,A_Tm;b,B_Tm;c,C_Tm] lem) th
725c725
<     MP (INST [a,A_;b,B_;c,C_] lem) th
---
>     MP (INST [a,A_Tm;b,B_Tm;c,C_Tm] lem) th
734c734
< open Variance
---
> (*open Variance*)
743c743
< let imp_conv_of_conv:conv->imp_conv =
---
> let (imp_conv_of_conv:conv->imp_conv) =
746c746
<     match v with Co -> th2 | Contra -> th1
---
>     match v with Variance.Co -> th2 | Variance.Contra -> th1
751c751
<   match v with Co -> t1 | Contra -> t2
---
>   match v with Variance.Co -> t1 | Variance.Contra -> t2
754c754
< let ALL_IMPCONV:imp_conv = fun _ -> IMP_REFL
---
> let (ALL_IMPCONV:imp_conv) = fun _ -> IMP_REFL
757c757
< let NO_IMPCONV:imp_conv = fun _ _ -> failwith "NO_IMPCONV"
---
> let (NO_IMPCONV:imp_conv) = fun _ _ -> failwith "NO_IMPCONV"
762,763c762,763
<   |Co -> IMP_TRANS (c v t1) th
<   |Contra -> IMP_TRANS th (c v t2)
---
>   |Variance.Co -> IMP_TRANS (c v t1) th
>   |Variance.Contra -> IMP_TRANS th (c v t2)
778c778
< let MATCH_MP_IMPCONV:thm->imp_conv =
---
> let (MATCH_MP_IMPCONV:thm->imp_conv) =
780,781c780,781
<     |Co -> GEN_PART_MATCH rand th
<     |Contra -> GEN_PART_MATCH lhand th
---
>     |Variance.Co -> GEN_PART_MATCH rand th
>     |Variance.Contra -> GEN_PART_MATCH lhand th
791c791
< let IMPCONV_RULE:imp_conv->thm->thm =
---
> let (IMPCONV_RULE:imp_conv->thm->thm) =
794c794
<     MATCH_MP (c Contra t) th
---
>     MATCH_MP (c Variance.Contra t) th
797,799c797,799
< let IMPCONV_TAC:imp_conv->tactic =
<   fun cnv (_,c as g) ->
<     (MATCH_MP_TAC (cnv Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
---
> let (IMPCONV_TAC:imp_conv->tactic) =
>   fun cnv ((_,c) as g) ->
>     (MATCH_MP_TAC (cnv Variance.Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
808c808
<   With_context of 'a * (Tset.t -> 'a with_context) * (term -> 'a with_context)
---
>   With_context of 'a * ((*Tset.t*) term list -> 'a with_context) * (term -> 'a with_context)
821,824c821,824
<  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C],
<  * then [CONJ_IMPCONV ic1 ic2 Co (A /\ C)] returns [B /\ D ==> A /\ C].
<  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns
<  * [C ==> D], then [CONJ_IMPCONV ic1 ic2 Contra (A /\ B)]
---
>  * Suppose [ic1 Variance.Co A] returns [B ==> A], and [ic2 Variance.Co C] returns [D ==> C],
>  * then [CONJ_IMPCONV ic1 ic2 Variance.Co (A /\ C)] returns [B /\ D ==> A /\ C].
>  * Suppose [ic1 Variance.Contra A] returns [A ==> B], and [ic2 Variance.Contra C] returns
>  * [C ==> D], then [CONJ_IMPCONV ic1 ic2 Variance.Contra (A /\ B)]
827c827
<  * Additionally takes the context into account, i.e., if [ic2 Co C] returns
---
>  * Additionally takes the context into account, i.e., if [ic2 Variance.Co C] returns
829c829
<  * then [CONJ_IMPCONV ic1 ic2 Co (A /\ B)] returns [|- C /\ D ==> A /\ B]
---
>  * then [CONJ_IMPCONV ic1 ic2 Variance.Co (A /\ B)] returns [|- C /\ D ==> A /\ B]
837c837
<       |Co ->
---
>       |Variance.Co ->
839c839
<             let th1 = apply c Co t1 in
---
>             let th1 = apply c Variance.Co t1 in
841,842c841,842
<               let t1' = imp_conv_outcome th1 Co in
<               MKIMP_CONJ_CO_CTXT th1 (apply_with_context c t1' Co t2)
---
>               let t1' = imp_conv_outcome th1 Variance.Co in
>               MKIMP_CONJ_CO_CTXT th1 (apply_with_context c t1' Variance.Co t2)
844,845c844,845
<           with Failure _ -> MKIMPR_CONJ_CO_CTXT (apply_with_context c t1 Co t2))
<       |Contra ->
---
>           with Failure _ -> MKIMPR_CONJ_CO_CTXT (apply_with_context c t1 Variance.Co t2))
>       |Variance.Contra ->
851c851
<             let th1 = apply (augment c t2s) Contra t1 in
---
>             let th1 = apply (augment c t2s) Variance.Contra t1 in
853c853
<                 let t1' = imp_conv_outcome th1 Contra in
---
>                 let t1' = imp_conv_outcome th1 Variance.Contra in
856c856
<                 let th2 = apply (augment c t1s'') Contra t2 in
---
>                 let th2 = apply (augment c t1s'') Variance.Contra t2 in
861c861
<               MKIMPR_CONJ_CONTRA_CTXT (apply_with_context c t1 Contra t2))
---
>               MKIMPR_CONJ_CONTRA_CTXT (apply_with_context c t1 Variance.Contra t2))
867,870c867,870
<  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C],
<  * then [DISJ_IMPCONV ic1 ic2 Co (A \/ C)] returns [B \/ D ==> A \/ C].
<  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns
<  * [C ==> D], then [DISJ_IMPCONV ic1 ic2 Contra (A \/ B)]
---
>  * Suppose [ic1 Variance.Co A] returns [B ==> A], and [ic2 Variance.Co C] returns [D ==> C],
>  * then [DISJ_IMPCONV ic1 ic2 Variance.Co (A \/ C)] returns [B \/ D ==> A \/ C].
>  * Suppose [ic1 Variance.Contra A] returns [A ==> B], and [ic2 Variance.Contra C] returns
>  * [C ==> D], then [DISJ_IMPCONV ic1 ic2 Variance.Contra (A \/ B)]
885,888c885,888
<  * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Co C] returns [D ==> C],
<  * then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns [(B ==> D) ==> (A ==> C)].
<  * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Contra C] returns
<  * [C ==> D], then [IMP_IMPCONV ic1 ic2 Contra (A ==> C)]
---
>  * Suppose [ic1 Variance.Contra A] returns [A ==> B], and [ic2 Variance.Co C] returns [D ==> C],
>  * then [IMP_IMPCONV ic1 ic2 Variance.Co (A ==> C)] returns [(B ==> D) ==> (A ==> C)].
>  * Suppose [ic1 Variance.Co A] returns [B ==> A], and [ic2 Variance.Contra C] returns
>  * [C ==> D], then [IMP_IMPCONV ic1 ic2 Variance.Contra (A ==> C)]
891,892c891,892
<  * Additionally takes the context into account, i.e., if [ic2 Co C] returns
<  * [B |- D ==> C], then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns
---
>  * Additionally takes the context into account, i.e., if [ic2 Variance.Co C] returns
>  * [B |- D ==> C], then [IMP_IMPCONV ic1 ic2 Variance.Co (A ==> C)] returns
906c906
<           match v with Co -> MKIMP_IMP_CO_CTXT | Contra -> MKIMP_IMP_CONTRA_CTXT
---
>           match v with Variance.Co -> MKIMP_IMP_CO_CTXT | Variance.Contra -> MKIMP_IMP_CONTRA_CTXT
921,922c921,922
<         |Co -> MKIMP_CO_IFF,MKIMPL_CO_IFF,MKIMPR_CO_IFF
<         |Contra -> MKIMP_CONTRA_IFF,MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
---
>         |Variance.Co -> MKIMP_CO_IFF,MKIMPL_CO_IFF,MKIMPR_CO_IFF
>         |Variance.Contra -> MKIMP_CONTRA_IFF,MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
935,938c935,938
<  * Suppose [ic Contra A] returns [A ==> B]
<  * then [NOT_IMPCONV ic Co ~A] returns [~B ==> ~A].
<  * Suppose [ic Co A] returns [B ==> A]
<  * then [NOT_IMPCONV ic Contra ~A] returns [~A ==> ~B].
---
>  * Suppose [ic Variance.Contra A] returns [A ==> B]
>  * then [NOT_IMPCONV ic Variance.Co ~A] returns [~B ==> ~A].
>  * Suppose [ic Variance.Co A] returns [B ==> A]
>  * then [NOT_IMPCONV ic Variance.Contra ~A] returns [~A ==> ~B].
956,959c956,959
<  * Suppose [ic Co A] returns [B ==> A]
<  * then [FORALL_IMPCONV ic Co (!x.A)] returns [(!x.B) ==> (!x.A)].
<  * Suppose [ic Contra A] returns [A ==> B]
<  * then [FORALL_IMPCONV ic Contra (!x.A)] returns [(!x.A) ==> (!x.B)].
---
>  * Suppose [ic Variance.Co A] returns [B ==> A]
>  * then [FORALL_IMPCONV ic Variance.Co (!x.A)] returns [(!x.B) ==> (!x.A)].
>  * Suppose [ic Variance.Contra A] returns [A ==> B]
>  * then [FORALL_IMPCONV ic Variance.Contra (!x.A)] returns [(!x.A) ==> (!x.B)].
964,967c964,967
<  * Suppose [ic Co A] returns [B ==> A]
<  * then [EXISTS_IMPCONV ic Co (?x.A)] returns [(?x.B) ==> (?x.A)].
<  * Suppose [ic Contra A] returns [A ==> B]
<  * then [EXISTS_IMPCONV ic Contra (?x.A)] returns [(?x.A) ==> (?x.B)].
---
>  * Suppose [ic Variance.Co A] returns [B ==> A]
>  * then [EXISTS_IMPCONV ic Variance.Co (?x.A)] returns [(?x.B) ==> (?x.A)].
>  * Suppose [ic Variance.Contra A] returns [A ==> B]
>  * then [EXISTS_IMPCONV ic Variance.Contra (?x.A)] returns [(?x.A) ==> (?x.B)].
972c972
< let rec SUB_CTXIMPCONV =
---
> let SUB_CTXIMPCONV  =
974c974
<   fun c ->
---
>   let rec SUB_CTXIMPCONV c =
990a991
>   in SUB_CTXIMPCONV;;
998,999c999,1000
<   |Co -> IMP_TRANS (apply c v t1) th
<   |Contra -> IMP_TRANS th (apply c v t2)
---
>   |Variance.Co -> IMP_TRANS (apply c v t1) th
>   |Variance.Contra -> IMP_TRANS th (apply c v t2)
1051,1072c1052,1070
< let rec REPEAT_UNCHANGED_CTXIMPCONV =
<   let rec map_all f xs x =
<     match xs with
<     |[] -> []
<     |y::ys -> f y x :: map_all f ys x
<   in
<   fun (cs:imp_conv with_context list) ->
<     With_context(
<       ((fun v t ->
<         let rec loop changed acc = function
<           |[] when changed -> loop false acc cs
<           |[] -> acc
<           |c::cs' ->
<               try
<                 let acc' = bind_ctximpconv c v acc in
<                 loop true acc' cs'
<               with Unchanged -> loop changed acc cs'
<         in
<         loop false (IMP_REFL t) cs):imp_conv),
<       REPEAT_UNCHANGED_CTXIMPCONV o map_all augment cs,
<       REPEAT_UNCHANGED_CTXIMPCONV o map_all diminish cs)
< 
---
> let rec map_all f xs x =
>   match xs with
>   |[] -> []
>   |y::ys -> f y x :: map_all f ys x ;;
> let rec REPEAT_UNCHANGED_CTXIMPCONV (cs:imp_conv with_context list) =
>   With_context(
>     ((fun v t ->
>       let rec loop changed acc = function
>         |[] when changed -> loop false acc cs
>         |[] -> acc
>         |c::cs' ->
>             try
>               let acc' = bind_ctximpconv c v acc in
>               loop true acc' cs'
>             with Unchanged -> loop changed acc cs'
>       in
>       loop false (IMP_REFL t) cs):imp_conv),
>     REPEAT_UNCHANGED_CTXIMPCONV o map_all augment cs,
>     REPEAT_UNCHANGED_CTXIMPCONV o map_all diminish cs);;
1080,1081c1078,1079
<     |Co -> IMP_TRANS (apply c na v t1) th
<     |Contra -> IMP_TRANS th (apply c na v t2)
---
>     |Variance.Co -> IMP_TRANS (apply c na v t1) th
>     |Variance.Contra -> IMP_TRANS th (apply c na v t2)
1127c1125
<   MATCH_MP (apply c Contra (concl th)) th
---
>   MATCH_MP (apply c Variance.Contra (concl th)) th
1130c1128
<   fun (asms,c as g) ->
---
>   fun ((asms,c) as g) ->
1132c1130
<     (MATCH_MP_TAC (apply cnv' Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
---
>     (MATCH_MP_TAC (apply cnv' Variance.Co c) THEN TRY (ACCEPT_TAC TRUTH)) g
1186c1184
< let IMPREWR_CONV:Tset.t->thm->annot_conv =
---
> let (IMPREWR_CONV:(*Tset.t*)term list->thm->annot_conv) =
1202c1200
<   let th,_,_ as res = cnv t in
---
>   let (th,_,_) as res = cnv t in
1258c1256
<   (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t =
---
>   (net:((term list -> annot_conv) * (*Tset.t*)term list * thm) Fo_nets.t) avs t =
1264c1262
< let IMPREWR_CTXCONV :thm list -> (atomic->annot_conv) with_context =
---
> let (IMPREWR_CTXCONV :thm list -> (atomic->annot_conv) with_context) =
1268,1269c1266,1267
<       |_,Some _,_ as c1t -> c1t
<       |th1,None,vs1 as c1t ->
---
>       |(_,Some _,_) as c1t -> c1t
>       |(th1,None,vs1) as c1t ->
1298c1296
<           res,!ho,!vs
---
>           res,(!ho),(!vs)
1301,1302c1299,1300
<     let rec (!) c avs t = (c ++ !c) avs t in
<     (!c + (SUB_QCONV (top_depth c) ++ top_depth c)) avs t
---
>     let rec (!) c avs t = (c ++ (!c)) avs t in
>     ((!c) + (SUB_QCONV (top_depth c) ++ top_depth c)) avs t
1324c1322
<           if not (Tset.mem v vs) then (ths := th :: !ths; true) else false
---
>           if not (Tset.mem v vs) then (ths := th :: (!ths); true) else false
1327c1325
<         self net' !ths))
---
>         self net' (!ths)))
1342c1340
< let rec REWR_IMPCONV_OF_CONV =
---
> let REWR_IMPCONV_OF_CONV =
1346c1344
<   fun (c:(atomic -> annot_conv) with_context) ->
---
>   let rec REWR_IMPCONV_OF_CONV (c:(atomic -> annot_conv) with_context) =
1353c1351
<           |Co ->
---
>           |Variance.Co ->
1355c1353
<               let rec exists_intro = function
---
>               let rec exists_intro vs = match vs with
1362c1360
<           |Contra ->
---
>           |Variance.Contra ->
1373c1371,1372
<       REWR_IMPCONV_OF_CONV o diminish c)
---
>       REWR_IMPCONV_OF_CONV o diminish c) in
>   REWR_IMPCONV_OF_CONV;;
1413c1412
< let rec CASE_REWR_IMPCONV_OF_CONV =
---
> let CASE_REWR_IMPCONV_OF_CONV =
1417c1416
<   fun (c:(atomic -> annot_conv) with_context) ->
---
>   let rec CASE_REWR_IMPCONV_OF_CONV (c:(atomic -> annot_conv) with_context) =
1427c1426,1427
<       CASE_REWR_IMPCONV_OF_CONV o diminish c)
---
>       CASE_REWR_IMPCONV_OF_CONV o diminish c) in
>   CASE_REWR_IMPCONV_OF_CONV;;
1446,1448c1446,1448
<  * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A],
<  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
<  * then [CONJ_IMPMCONV ic1 ic2 Co (A /\ C)] returns
---
>  * Suppose [ic1 Variance.Co A] returns a list [B1 ==> A; ...; Bk ==> A],
>  * and [ic2 Variance.Co C] returns [D1 ==> C; ...; Dn ==> C],
>  * then [CONJ_IMPMCONV ic1 ic2 Variance.Co (A /\ C)] returns
1461,1462c1461,1462
<         |Co -> MKIMPL_CONJ_CO2_CTXT,MKIMPR_CONJ_CO_CTXT
<         |Contra -> MKIMPL_CONJ_CONTRA_CTXT,MKIMPR_CONJ_CONTRA_CTXT
---
>         |Variance.Co -> MKIMPL_CONJ_CO2_CTXT,MKIMPR_CONJ_CO_CTXT
>         |Variance.Contra -> MKIMPL_CONJ_CONTRA_CTXT,MKIMPR_CONJ_CONTRA_CTXT
1471,1473c1471,1473
<  * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A],
<  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
<  * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns
---
>  * Suppose [ic1 Variance.Co A] returns a list [B1 ==> A; ...; Bk ==> A],
>  * and [ic2 Variance.Co C] returns [D1 ==> C; ...; Dn ==> C],
>  * then [DISJ_IMPMCONV ic1 ic2 Variance.Co (A \/ C)] returns
1491,1493c1491,1493
<  * Suppose [ic1 Contra A] returns a list [A ==> B1; ...; A ==> Bk],
<  * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C],
<  * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns
---
>  * Suppose [ic1 Variance.Contra A] returns a list [A ==> B1; ...; A ==> Bk],
>  * and [ic2 Variance.Co C] returns [D1 ==> C; ...; Dn ==> C],
>  * then [DISJ_IMPMCONV ic1 ic2 Variance.Co (A \/ C)] returns
1516,1517c1516,1517
<         |Co -> MKIMPL_CO_IFF,MKIMPR_CO_IFF
<         |Contra -> MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
---
>         |Variance.Co -> MKIMPL_CO_IFF,MKIMPR_CO_IFF
>         |Variance.Contra -> MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF
1526,1527c1526,1527
<  * Suppose [ic Contra A] returns a list [A ==> B1; ...; A ==> Bk],
<  * then [NOT_IMPMCONV ic Co ~A] returns [~B1 ==> ~A; ...; ~Bk ==> ~A].
---
>  * Suppose [ic Variance.Contra A] returns a list [A ==> B1; ...; A ==> Bk],
>  * then [NOT_IMPMCONV ic Variance.Co ~A] returns [~B1 ==> ~A; ...; ~Bk ==> ~A].
1549,1550c1549,1550
<  * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A],
<  * then [FORALL_IMPMCONV ic Co (!x.A)] returns [(!x.B1) ==> (!x.A); ...;
---
>  * Suppose [ic Variance.Co A] returns a list [B1 ==> A; ...; Bk ==> A],
>  * then [FORALL_IMPMCONV ic Variance.Co (!x.A)] returns [(!x.B1) ==> (!x.A); ...;
1558,1559c1558,1559
<  * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A],
<  * then [EXISTS_IMPMCONV ic Co (?x.A)] returns [(?x.B1) ==> (?x.A); ...;
---
>  * Suppose [ic Variance.Co A] returns a list [B1 ==> A; ...; Bk ==> A],
>  * then [EXISTS_IMPMCONV ic Variance.Co (?x.A)] returns [(?x.B1) ==> (?x.A); ...;
1569c1569
< let rec SUB_CTXIMPMCONV =
---
> let SUB_CTXIMPMCONV =
1571c1571
<   fun c ->
---
>   let rec SUB_CTXIMPMCONV c =
1586,1587c1586,1587
<     SUB_CTXIMPMCONV o diminish c)
< 
---
>     SUB_CTXIMPMCONV o diminish c) in
>   SUB_CTXIMPMCONV;;
1653c1653
< let DEEP_IMP_REWR_MCONV:thm list->(atomic->annot_mconv) with_context =
---
> let (DEEP_IMP_REWR_MCONV:thm list->(atomic->annot_mconv) with_context) =
1675c1675
<     |Const _ | Var _ -> []
---
>     |Const (_,_) | Var (_,_) -> []
1678c1678
<   let REWRITES_IMPCONV (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t =
---
>   let REWRITES_IMPCONV (net:((term list -> annot_conv) * (*Tset.t*) term list * thm) Fo_nets.t) avs t =
1697c1697
<           if not (Tset.mem v vs) then (ths := th :: !ths; true) else false
---
>           if not (Tset.mem v vs) then (ths := th :: (!ths); true) else false
1700c1700
<         self net' !ths))
---
>         self net' (!ths)))
1711c1711
< let rec REWR_IMPMCONV_OF_MCONV =
---
> let REWR_IMPMCONV_OF_MCONV =
1715c1715
<   fun (c:(atomic -> annot_mconv) with_context) ->
---
>   let rec REWR_IMPMCONV_OF_MCONV (c:(atomic -> annot_mconv) with_context) =
1721c1721
<           |Co ->
---
>           |Variance.Co ->
1723c1723
<               let rec exists_intro = function
---
>               let rec exists_intro xs = match xs with
1730c1730
<           |Contra ->
---
>           |Variance.Contra ->
1740c1740,1741
<       REWR_IMPMCONV_OF_MCONV o diminish c)
---
>       REWR_IMPMCONV_OF_MCONV o diminish c) in
>   REWR_IMPMCONV_OF_MCONV;;
1747c1748
< let EXISTS_CTXIMPCONV:imp_conv with_context =
---
> let (EXISTS_CTXIMPCONV:imp_conv with_context) =
1759c1760
<       |Co,Comb(Const("?",_),_) ->
---
>       |Variance.Co,Comb(Const("?",_),_) ->
1765c1766
<             |_::_ as lvs,lcs ->
---
>             |(_::_ as lvs),lcs ->
1777,1778c1778,1779
<           |[] -> assert false
<           |[h] -> DISCH T_ th
---
>           |[] -> raise Bind (* assert false *)
>           |[h] -> DISCH T_Tm th
1799,1800c1800,1801
<   |Co -> map (C IMP_TRANS th) (c v t1)
<   |Contra -> map (IMP_TRANS th) (c v t2)
---
>   |Variance.Co -> map (C IMP_TRANS th) (c v t1)
>   |Variance.Contra -> map (IMP_TRANS th) (c v t2)
1811c1812
< let TARGET_REWRITE_IMPCONV : thm list -> term list -> imp_conv =
---
> let (TARGET_REWRITE_IMPCONV : thm list -> term list -> imp_conv) =
1852c1853,1861
< end in
---
> end;;
> 
> let IMP_REWRITE_TAC,TARGET_REWRITE_TAC,HINT_EXISTS_TAC,
>     SEQ_IMP_REWRITE_TAC,CASE_REWRITE_TAC =
>   Impconv.IMP_REWRITE_TAC,
>   Impconv.TARGET_REWRITE_TAC,
>   Impconv.HINT_EXISTS_TAC,
>   Impconv.SEQ_IMP_REWRITE_TAC,
>   Impconv.CASE_REWRITE_TAC;;
1854,1858d1862
< Impconv.IMP_REWRITE_TAC,
< Impconv.TARGET_REWRITE_TAC,
< Impconv.HINT_EXISTS_TAC,
< Impconv.SEQ_IMP_REWRITE_TAC,
< Impconv.CASE_REWRITE_TAC;;