1) all theorems in Orderings can now be given as a parameter
authorobua
Thu Jul 07 19:01:04 2005 +0200 (2005-07-07)
changeset 1674321dbff595bf6
parent 16742 d1641dba61e5
child 16744 d0b61beefa49
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
src/HOL/Orderings.thy
src/Provers/order.ML
src/Pure/defs.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Orderings.thy	Thu Jul 07 18:38:00 2005 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Jul 07 19:01:04 2005 +0200
     1.3 @@ -346,6 +346,7 @@
     1.4      val neq_le_trans = thm "order_neq_le_trans";
     1.5      val less_imp_neq = thm "less_imp_neq";
     1.6      val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
     1.7 +    val not_sym = thm "not_sym";
     1.8      val decomp_part = decomp_gen ["Orderings.order"];
     1.9      val decomp_lin = decomp_gen ["Orderings.linorder"];
    1.10  
     2.1 --- a/src/Provers/order.ML	Thu Jul 07 18:38:00 2005 +0200
     2.2 +++ b/src/Provers/order.ML	Thu Jul 07 19:01:04 2005 +0200
     2.3 @@ -44,6 +44,7 @@
     2.4    val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
     2.5    val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
     2.6    val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
     2.7 +  val not_sym : thm (* x ~= y ==> y ~= x *)
     2.8  
     2.9    (* Additional theorems for linear orders *)
    2.10    val not_lessD: thm (* ~(x < y) ==> y <= x *)
    2.11 @@ -137,7 +138,7 @@
    2.12      | "~="  => if (x aconv y) then 
    2.13                    raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
    2.14                 else [ NotEq (x, y, Asm n),
    2.15 -                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
    2.16 +                      NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
    2.17      | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
    2.18                   "''returned by decomp_part."))
    2.19    | NONE => [];
    2.20 @@ -167,7 +168,7 @@
    2.21      | "~="  => if (x aconv y) then 
    2.22                    raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
    2.23                 else [ NotEq (x, y, Asm n),
    2.24 -                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
    2.25 +                      NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
    2.26      | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
    2.27                   "''returned by decomp_lin."))
    2.28    | NONE => [];
    2.29 @@ -785,10 +786,10 @@
    2.30       (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
    2.31         ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
    2.32            if  (x aconv x' andalso y aconv y') then p 
    2.33 -	  else Thm ([p], thm "not_sym")
    2.34 +	  else Thm ([p], Less.not_sym)
    2.35       | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 
    2.36            if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq))
    2.37 -          else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym"))
    2.38 +          else (Thm ([(Thm ([p], Less.less_imp_neq))], Less.not_sym))
    2.39       | _ => raise Cannot) 
    2.40     ) else (
    2.41     
    2.42 @@ -810,11 +811,11 @@
    2.43  	    	if e subsumes subgoal then (
    2.44  		     case e of (Less (u, v, q)) => (
    2.45  		       if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq))
    2.46 -		       else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym"))
    2.47 +		       else (Thm ([(Thm ([q], Less.less_imp_neq))], Less.not_sym))
    2.48  		     )
    2.49  		     |    (NotEq (u,v, q)) => (
    2.50  		       if u aconv x andalso v aconv y then q
    2.51 -		       else (Thm ([q],  thm "not_sym"))
    2.52 +		       else (Thm ([q],  Less.not_sym))
    2.53  		     )
    2.54  		 )
    2.55                  (* if SCC_x is linked to SCC_y via edge e *)
    2.56 @@ -843,7 +844,7 @@
    2.57  		     case e of (Less (_, _,_)) => (
    2.58  		        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
    2.59  			    val xyLesss = transPath (tl xypath, hd xypath)
    2.60 -			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
    2.61 +			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , Less.not_sym)) end ) 
    2.62  		     | _ => (
    2.63  		        
    2.64  			let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
    2.65 @@ -857,7 +858,7 @@
    2.66  			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI))
    2.67  			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI))
    2.68  			in
    2.69 -			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym"))
    2.70 +			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], Less.not_sym))
    2.71  		        end
    2.72  		       )
    2.73  		  ) else (
    2.74 @@ -871,7 +872,7 @@
    2.75  	                        val xr = dfs_int_reachable sccGraph_transpose xi
    2.76  		               in 
    2.77  		                case  (findLess e y x yi xi yr xr) of 
    2.78 -		                      (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) 
    2.79 +		                      (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], Less.not_sym)) 
    2.80                                        | _ => processNeqEdges es
    2.81  		               end)
    2.82  		 ) end) 
     3.1 --- a/src/Pure/defs.ML	Thu Jul 07 18:38:00 2005 +0200
     3.2 +++ b/src/Pure/defs.ML	Thu Jul 07 19:01:04 2005 +0200
     3.3 @@ -35,6 +35,10 @@
     3.4    val set_chain_history : bool -> unit
     3.5    val chain_history : unit -> bool
     3.6  
     3.7 +  datatype overloadingstate = Open | Closed | Final
     3.8 +  val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
     3.9 +  val is_overloaded : graph -> string -> bool
    3.10 +
    3.11  end
    3.12  
    3.13  structure Defs :> DEFS = struct
    3.14 @@ -42,7 +46,7 @@
    3.15  type tyenv = Type.tyenv
    3.16  type edgelabel = (int * typ * typ * (typ * string * string) list)
    3.17  
    3.18 -datatype forwardstate = Open | Closed | Final
    3.19 +datatype overloadingstate = Open | Closed | Final
    3.20  
    3.21  datatype node = Node of
    3.22           typ  (* most general type of constant *)
    3.23 @@ -53,7 +57,7 @@
    3.24               (* a table of all back referencing defnodes to this node, 
    3.25                  indexed by node name of the defnodes *)
    3.26           * typ list (* a list of all finalized types *)
    3.27 -         * forwardstate
    3.28 +         * overloadingstate
    3.29       
    3.30       and defnode = Defnode of
    3.31           typ  (* type of the constant in this particular definition *)
    3.32 @@ -653,6 +657,21 @@
    3.33            Symtab.update_new ((name, ftys), finals)) 
    3.34        (Symtab.empty, graph)
    3.35  
    3.36 +fun overloading_info (_, axmap, _, graph) c = 
    3.37 +    let
    3.38 +      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
    3.39 +    in
    3.40 +      case Symtab.lookup (graph, c) of
    3.41 +        NONE => NONE
    3.42 +      | SOME (Node (ty, defnodes, _, _, state)) =>
    3.43 +        SOME (ty, map translate (Symtab.dest defnodes), state)
    3.44 +    end
    3.45 +      
    3.46 +fun is_overloaded g c = 
    3.47 +    case overloading_info g c of
    3.48 +      NONE => false
    3.49 +    | SOME (_, l, _) => length l >= 2
    3.50 +
    3.51  end;
    3.52  		
    3.53  (*
     4.1 --- a/src/Pure/theory.ML	Thu Jul 07 18:38:00 2005 +0200
     4.2 +++ b/src/Pure/theory.ML	Thu Jul 07 19:01:04 2005 +0200
     4.3 @@ -38,6 +38,7 @@
     4.4    val oracle_space: theory -> NameSpace.T
     4.5    val axioms_of: theory -> (string * term) list
     4.6    val all_axioms_of: theory -> (string * term) list
     4.7 +  val defs_of : theory -> Defs.graph
     4.8    val self_ref: theory -> theory_ref
     4.9    val deref: theory_ref -> theory
    4.10    val merge: theory * theory -> theory                     (*exception TERM*)
    4.11 @@ -178,6 +179,8 @@
    4.12  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    4.13  fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
    4.14  
    4.15 +fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
    4.16 +
    4.17  fun requires thy name what =
    4.18    if Context.exists_name name thy then ()
    4.19    else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);