# HG changeset patch # User obua # Date 1120755664 -7200 # Node ID 21dbff595bf6323b1eba6773505f15c98b1e2786 # Parent d1641dba61e51bf9c6c0ff9692d68809b4b74c15 1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded diff -r d1641dba61e5 -r 21dbff595bf6 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Jul 07 18:38:00 2005 +0200 +++ b/src/HOL/Orderings.thy Thu Jul 07 19:01:04 2005 +0200 @@ -346,6 +346,7 @@ val neq_le_trans = thm "order_neq_le_trans"; val less_imp_neq = thm "less_imp_neq"; val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; + val not_sym = thm "not_sym"; val decomp_part = decomp_gen ["Orderings.order"]; val decomp_lin = decomp_gen ["Orderings.linorder"]; diff -r d1641dba61e5 -r 21dbff595bf6 src/Provers/order.ML --- a/src/Provers/order.ML Thu Jul 07 18:38:00 2005 +0200 +++ b/src/Provers/order.ML Thu Jul 07 19:01:04 2005 +0200 @@ -44,6 +44,7 @@ val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) + val not_sym : thm (* x ~= y ==> y ~= x *) (* Additional theorems for linear orders *) val not_lessD: thm (* ~(x < y) ==> y <= x *) @@ -137,7 +138,7 @@ | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] + NotEq (y, x,Thm ( [Asm n], Less.not_sym))] | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_part.")) | NONE => []; @@ -167,7 +168,7 @@ | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] + NotEq (y, x,Thm ( [Asm n], Less.not_sym))] | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_lin.")) | NONE => []; @@ -785,10 +786,10 @@ (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) => if (x aconv x' andalso y aconv y') then p - else Thm ([p], thm "not_sym") + else Thm ([p], Less.not_sym) | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq)) - else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym")) + else (Thm ([(Thm ([p], Less.less_imp_neq))], Less.not_sym)) | _ => raise Cannot) ) else ( @@ -810,11 +811,11 @@ if e subsumes subgoal then ( case e of (Less (u, v, q)) => ( if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq)) - else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) + else (Thm ([(Thm ([q], Less.less_imp_neq))], Less.not_sym)) ) | (NotEq (u,v, q)) => ( if u aconv x andalso v aconv y then q - else (Thm ([q], thm "not_sym")) + else (Thm ([q], Less.not_sym)) ) ) (* if SCC_x is linked to SCC_y via edge e *) @@ -843,7 +844,7 @@ case e of (Less (_, _,_)) => ( let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) val xyLesss = transPath (tl xypath, hd xypath) - in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) + in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , Less.not_sym)) end ) | _ => ( let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) @@ -857,7 +858,7 @@ val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI)) val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI)) in - (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym")) + (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], Less.not_sym)) end ) ) else ( @@ -871,7 +872,7 @@ val xr = dfs_int_reachable sccGraph_transpose xi in case (findLess e y x yi xi yr xr) of - (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) + (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], Less.not_sym)) | _ => processNeqEdges es end) ) end) diff -r d1641dba61e5 -r 21dbff595bf6 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Jul 07 18:38:00 2005 +0200 +++ b/src/Pure/defs.ML Thu Jul 07 19:01:04 2005 +0200 @@ -35,6 +35,10 @@ val set_chain_history : bool -> unit val chain_history : unit -> bool + datatype overloadingstate = Open | Closed | Final + val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option + val is_overloaded : graph -> string -> bool + end structure Defs :> DEFS = struct @@ -42,7 +46,7 @@ type tyenv = Type.tyenv type edgelabel = (int * typ * typ * (typ * string * string) list) -datatype forwardstate = Open | Closed | Final +datatype overloadingstate = Open | Closed | Final datatype node = Node of typ (* most general type of constant *) @@ -53,7 +57,7 @@ (* a table of all back referencing defnodes to this node, indexed by node name of the defnodes *) * typ list (* a list of all finalized types *) - * forwardstate + * overloadingstate and defnode = Defnode of typ (* type of the constant in this particular definition *) @@ -653,6 +657,21 @@ Symtab.update_new ((name, ftys), finals)) (Symtab.empty, graph) +fun overloading_info (_, axmap, _, graph) c = + let + fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty) + in + case Symtab.lookup (graph, c) of + NONE => NONE + | SOME (Node (ty, defnodes, _, _, state)) => + SOME (ty, map translate (Symtab.dest defnodes), state) + end + +fun is_overloaded g c = + case overloading_info g c of + NONE => false + | SOME (_, l, _) => length l >= 2 + end; (* diff -r d1641dba61e5 -r 21dbff595bf6 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Jul 07 18:38:00 2005 +0200 +++ b/src/Pure/theory.ML Thu Jul 07 19:01:04 2005 +0200 @@ -38,6 +38,7 @@ val oracle_space: theory -> NameSpace.T val axioms_of: theory -> (string * term) list val all_axioms_of: theory -> (string * term) list + val defs_of : theory -> Defs.graph val self_ref: theory -> theory_ref val deref: theory_ref -> theory val merge: theory * theory -> theory (*exception TERM*) @@ -178,6 +179,8 @@ val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy)); +fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D) + fun requires thy name what = if Context.exists_name name thy then () else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);