move MRSL to a separate file
authorkuncar
Mon Apr 23 17:18:18 2012 +0200 (2012-04-23)
changeset 4769818202d3d5832
parent 47697 0622929ca66e
child 47699 bb6b147c6531
move MRSL to a separate file
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Lifting.thy	Mon Apr 23 16:30:43 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Mon Apr 23 17:18:18 2012 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    "lift_definition" :: thy_goal and
     1.5    "setup_lifting" :: thy_decl
     1.6  uses
     1.7 +  ("Tools/Lifting/lifting_util.ML")
     1.8    ("Tools/Lifting/lifting_info.ML")
     1.9    ("Tools/Lifting/lifting_term.ML")
    1.10    ("Tools/Lifting/lifting_def.ML")
    1.11 @@ -354,7 +355,7 @@
    1.12  
    1.13  subsection {* ML setup *}
    1.14  
    1.15 -text {* Auxiliary data for the lifting package *}
    1.16 +use "Tools/Lifting/lifting_util.ML"
    1.17  
    1.18  use "Tools/Lifting/lifting_info.ML"
    1.19  setup Lifting_Info.setup
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 23 16:30:43 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 23 17:18:18 2012 +0200
     2.3 @@ -18,13 +18,11 @@
     2.4  structure Lifting_Def: LIFTING_DEF =
     2.5  struct
     2.6  
     2.7 -(** Interface and Syntax Setup **)
     2.8 -
     2.9 -(* Generation of the code certificate from the rsp theorem *)
    2.10 +open Lifting_Util
    2.11  
    2.12  infix 0 MRSL
    2.13  
    2.14 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    2.15 +(* Generation of the code certificate from the rsp theorem *)
    2.16  
    2.17  fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
    2.18    | get_body_types (U, V)  = (U, V)
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 23 16:30:43 2012 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Apr 23 17:18:18 2012 +0200
     3.3 @@ -18,9 +18,9 @@
     3.4  structure Lifting_Setup: LIFTING_SETUP =
     3.5  struct
     3.6  
     3.7 -infix 0 MRSL
     3.8 +open Lifting_Util
     3.9  
    3.10 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    3.11 +infix 0 MRSL
    3.12  
    3.13  exception SETUP_LIFTING_INFR of string
    3.14  
     4.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Apr 23 16:30:43 2012 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Apr 23 17:18:18 2012 +0200
     4.3 @@ -27,6 +27,10 @@
     4.4  structure Lifting_Term: LIFTING_TERM =
     4.5  struct
     4.6  
     4.7 +open Lifting_Util
     4.8 +
     4.9 +infix 0 MRSL
    4.10 +
    4.11  (* generation of the Quotient theorem  *)
    4.12  
    4.13  exception QUOT_THM_INTERNAL of Pretty.T
    4.14 @@ -81,10 +85,6 @@
    4.15  
    4.16  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    4.17  
    4.18 -infix 0 MRSL
    4.19 -
    4.20 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    4.21 -
    4.22  fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
    4.23        = (rel, abs, rep, cr)
    4.24    | dest_Quotient t = raise TERM ("dest_Quotient", [t])
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon Apr 23 17:18:18 2012 +0200
     5.3 @@ -0,0 +1,20 @@
     5.4 +(*  Title:      HOL/Tools/Lifting/lifting_util.ML
     5.5 +    Author:     Ondrej Kuncar
     5.6 +
     5.7 +General-purpose functions used by the Lifting package.
     5.8 +*)
     5.9 +
    5.10 +signature LIFTING_UTIL =
    5.11 +sig
    5.12 +  val MRSL: thm list * thm -> thm
    5.13 +end;
    5.14 +
    5.15 +
    5.16 +structure Lifting_Util: LIFTING_UTIL =
    5.17 +struct
    5.18 +
    5.19 +infix 0 MRSL
    5.20 +
    5.21 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    5.22 +
    5.23 +end;
     6.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 23 16:30:43 2012 +0200
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Apr 23 17:18:18 2012 +0200
     6.3 @@ -27,9 +27,9 @@
     6.4  
     6.5  (* Generation of the code certificate from the rsp theorem *)
     6.6  
     6.7 -infix 0 MRSL
     6.8 +open Lifting_Util
     6.9  
    6.10 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    6.11 +infix 0 MRSL
    6.12  
    6.13  fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
    6.14    | get_body_types (U, V)  = (U, V)
     7.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Apr 23 16:30:43 2012 +0200
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Apr 23 17:18:18 2012 +0200
     7.3 @@ -358,9 +358,9 @@
     7.4  
     7.5  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3})
     7.6  
     7.7 -infix 0 MRSL
     7.8 +open Lifting_Util
     7.9  
    7.10 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    7.11 +infix 0 MRSL
    7.12  
    7.13  exception NOT_IMPL of string
    7.14  
     8.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 23 16:30:43 2012 +0200
     8.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Apr 23 17:18:18 2012 +0200
     8.3 @@ -99,9 +99,9 @@
     8.4    else
     8.5      lthy
     8.6  
     8.7 -infix 0 MRSL
     8.8 +open Lifting_Util
     8.9  
    8.10 -fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    8.11 +infix 0 MRSL
    8.12  
    8.13  fun define_cr_rel equiv_thm abs_fun lthy =
    8.14    let