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
```