src/Provers/quasi.ML
changeset 15531 08c8dad8e399
parent 15103 79846e8792eb
child 15570 8d8c70b41bab
     1.1 --- a/src/Provers/quasi.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Provers/quasi.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4    val less_imp_neq : thm (* x < y ==> x ~= y *)
     1.5  
     1.6    (* Analysis of premises and conclusion *)
     1.7 -  (* decomp_x (`x Rel y') should yield Some (x, Rel, y)
     1.8 +  (* decomp_x (`x Rel y') should yield SOME (x, Rel, y)
     1.9         where Rel is one of "<", "<=", "=" and "~=",
    1.10         other relation symbols cause an error message *)
    1.11    (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
    1.12 @@ -127,12 +127,12 @@
    1.13  
    1.14  fun mkasm_trans sign (t, n) =
    1.15    case Less.decomp_trans sign t of
    1.16 -    Some (x, rel, y) => 
    1.17 +    SOME (x, rel, y) => 
    1.18      (case rel of
    1.19       "<="  =>  [Le (x, y, Asm n)]
    1.20      | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
    1.21                   "''returned by decomp_trans."))
    1.22 -  | None => [];
    1.23 +  | NONE => [];
    1.24    
    1.25  (* ************************************************************************ *)
    1.26  (*                                                                          *)
    1.27 @@ -146,7 +146,7 @@
    1.28  
    1.29  fun mkasm_quasi sign (t, n) =
    1.30    case Less.decomp_quasi sign t of
    1.31 -    Some (x, rel, y) => (case rel of
    1.32 +    SOME (x, rel, y) => (case rel of
    1.33        "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
    1.34                 else [Less (x, y, Asm n)]
    1.35      | "<="  => [Le (x, y, Asm n)]
    1.36 @@ -158,7 +158,7 @@
    1.37                        NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
    1.38      | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
    1.39                   "''returned by decomp_quasi."))
    1.40 -  | None => [];
    1.41 +  | NONE => [];
    1.42  
    1.43  
    1.44  (* ************************************************************************ *)
    1.45 @@ -173,10 +173,10 @@
    1.46    
    1.47  fun mkconcl_trans sign t =
    1.48    case Less.decomp_trans sign t of
    1.49 -    Some (x, rel, y) => (case rel of
    1.50 +    SOME (x, rel, y) => (case rel of
    1.51       "<="  => (Le (x, y, Asm ~1), Asm 0) 
    1.52      | _  => raise Cannot)
    1.53 -  | None => raise Cannot;
    1.54 +  | NONE => raise Cannot;
    1.55    
    1.56    
    1.57  (* ************************************************************************ *)
    1.58 @@ -190,12 +190,12 @@
    1.59  
    1.60  fun mkconcl_quasi sign t =
    1.61    case Less.decomp_quasi sign t of
    1.62 -    Some (x, rel, y) => (case rel of
    1.63 +    SOME (x, rel, y) => (case rel of
    1.64        "<"   => ([Less (x, y, Asm ~1)], Asm 0)
    1.65      | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
    1.66      | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
    1.67      | _  => raise Cannot)
    1.68 -| None => raise Cannot;
    1.69 +| NONE => raise Cannot;
    1.70    
    1.71    
    1.72  (* ******************************************************************* *)
    1.73 @@ -266,16 +266,16 @@
    1.74  
    1.75  (* ******************************************************************* *)
    1.76  (*                                                                     *)
    1.77 -(* triv_solv less1 : less ->  proof Library.option                     *)
    1.78 +(* triv_solv less1 : less ->  proof option                     *)
    1.79  (*                                                                     *)
    1.80  (* Solves trivial goal x <= x.                                         *)
    1.81  (*                                                                     *)
    1.82  (* ******************************************************************* *)
    1.83  
    1.84  fun triv_solv (Le (x, x', _)) =
    1.85 -    if x aconv x' then  Some (Thm ([], Less.le_refl)) 
    1.86 -    else None
    1.87 -|   triv_solv _ = None;
    1.88 +    if x aconv x' then  SOME (Thm ([], Less.le_refl)) 
    1.89 +    else NONE
    1.90 +|   triv_solv _ = NONE;
    1.91  
    1.92  (* ********************************************************************* *)
    1.93  (* Graph functions                                                       *)
    1.94 @@ -463,15 +463,15 @@
    1.95     end )
    1.96    | (Less (x,y,_))  => (
    1.97     let 
    1.98 -    fun findParallelNeq []  = None
    1.99 +    fun findParallelNeq []  = NONE
   1.100      |   findParallelNeq (e::es)  =
   1.101 -     if      (x aconv (lower e) andalso y aconv (upper e)) then Some e
   1.102 -     else if (y aconv (lower e) andalso x aconv (upper e)) then Some (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   1.103 +     if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
   1.104 +     else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   1.105       else findParallelNeq es ;  
   1.106     in
   1.107     (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   1.108     (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
   1.109 -    (case findParallelNeq neqE of (Some e) => 
   1.110 +    (case findParallelNeq neqE of (SOME e) => 
   1.111        let 
   1.112         val (xyLeFound,xyLePath) = findPath x y leG 
   1.113        in
   1.114 @@ -487,7 +487,7 @@
   1.115   | (NotEq (x,y,_)) => 
   1.116    (* First check if a single premiss is sufficient *)
   1.117    (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   1.118 -    (Some (NotEq (x, y, p)), NotEq (x', y', _)) =>
   1.119 +    (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   1.120        if  (x aconv x' andalso y aconv y') then p 
   1.121        else Thm ([p], thm "not_sym")
   1.122      | _  => raise Cannot 
   1.123 @@ -540,8 +540,8 @@
   1.124     let 
   1.125     val (subgoals, prf) = mkconcl_quasi sign concl
   1.126     fun solve facts less =
   1.127 -       (case triv_solv less of None => findQuasiProof (leG, neqE) less
   1.128 -       | Some prf => prf )
   1.129 +       (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
   1.130 +       | SOME prf => prf )
   1.131    in   map (solve asms) subgoals end
   1.132   end;
   1.133