do not open ML structures;
authorwenzelm
Fri Jan 07 21:26:49 2011 +0100 (2011-01-07)
changeset 41451892e67be8304
parent 41450 3a62f88d9650
child 41452 c291e0826902
do not open ML structures;
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 20:42:25 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 21:26:49 2011 +0100
     1.3 @@ -19,9 +19,6 @@
     1.4  structure Quotient_Def: QUOTIENT_DEF =
     1.5  struct
     1.6  
     1.7 -open Quotient_Info;
     1.8 -open Quotient_Term;
     1.9 -
    1.10  (** Interface and Syntax Setup **)
    1.11  
    1.12  (* The ML-interface for a quotient definition takes
    1.13 @@ -60,7 +57,7 @@
    1.14      val _ = sanity_test optbind lhs_str
    1.15  
    1.16      val qconst_bname = Binding.name lhs_str
    1.17 -    val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
    1.18 +    val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
    1.19      val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    1.20      val (_, prop') = Local_Defs.cert_def lthy prop
    1.21      val (_, newrhs) = Local_Defs.abs_def prop'
    1.22 @@ -70,10 +67,11 @@
    1.23      (* data storage *)
    1.24      val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    1.25  
    1.26 -    fun qcinfo phi = transform_qconsts phi qconst_data
    1.27 +    fun qcinfo phi = Quotient_Info.transform_qconsts phi qconst_data
    1.28      fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    1.29 -    val lthy'' = Local_Theory.declaration true
    1.30 -                   (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
    1.31 +    val lthy'' =
    1.32 +      Local_Theory.declaration true
    1.33 +        (fn phi => Quotient_Info.qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
    1.34    in
    1.35      (qconst_data, lthy'')
    1.36    end
    1.37 @@ -92,7 +90,7 @@
    1.38  fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
    1.39    let
    1.40      val rty = fastype_of rconst
    1.41 -    val qty = derive_qtyp ctxt qtys rty
    1.42 +    val qty = Quotient_Term.derive_qtyp ctxt qtys rty
    1.43      val lhs = Free (qconst_name, qty)
    1.44    in
    1.45      quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 20:42:25 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 21:26:49 2011 +0100
     2.3 @@ -4,6 +4,8 @@
     2.4  Data slots for the quotient package.
     2.5  *)
     2.6  
     2.7 +(* FIXME odd names/signatures of data access operations *)
     2.8 +
     2.9  signature QUOTIENT_INFO =
    2.10  sig
    2.11    exception NotFound  (* FIXME complicates signatures unnecessarily *)
    2.12 @@ -44,7 +46,6 @@
    2.13    val quotient_rules_add: attribute
    2.14  end;
    2.15  
    2.16 -
    2.17  structure Quotient_Info: QUOTIENT_INFO =
    2.18  struct
    2.19  
     3.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 20:42:25 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 21:26:49 2011 +0100
     3.3 @@ -25,10 +25,6 @@
     3.4  structure Quotient_Tacs: QUOTIENT_TACS =
     3.5  struct
     3.6  
     3.7 -open Quotient_Info;
     3.8 -open Quotient_Term;
     3.9 -
    3.10 -
    3.11  (** various helper fuctions **)
    3.12  
    3.13  (* Since HOL_basic_ss is too "big" for us, we *)
    3.14 @@ -56,7 +52,7 @@
    3.15  (** solvers for equivp and quotient assumptions **)
    3.16  
    3.17  fun equiv_tac ctxt =
    3.18 -  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
    3.19 +  REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
    3.20  
    3.21  fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
    3.22  val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
    3.23 @@ -64,7 +60,7 @@
    3.24  fun quotient_tac ctxt =
    3.25    (REPEAT_ALL_NEW (FIRST'
    3.26      [rtac @{thm identity_quotient},
    3.27 -     resolve_tac (quotient_rules_get ctxt)]))
    3.28 +     resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
    3.29  
    3.30  fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    3.31  val quotient_solver =
    3.32 @@ -152,11 +148,11 @@
    3.33  
    3.34  fun reflp_get ctxt =
    3.35    map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
    3.36 -    handle THM _ => NONE) (equiv_rules_get ctxt)
    3.37 +    handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt)
    3.38  
    3.39  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
    3.40  
    3.41 -fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
    3.42 +fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
    3.43  
    3.44  fun regularize_tac ctxt =
    3.45    let
    3.46 @@ -379,7 +375,7 @@
    3.47  
    3.48       (* respectfulness of constants; in particular of a simple relation *)
    3.49    | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
    3.50 -      => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
    3.51 +      => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
    3.52  
    3.53        (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
    3.54        (* observe map_fun *)
    3.55 @@ -527,18 +523,19 @@
    3.56  *)
    3.57  fun clean_tac lthy =
    3.58    let
    3.59 -    val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
    3.60 -    val prs = prs_rules_get lthy
    3.61 -    val ids = id_simps_get lthy
    3.62 +    val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy)
    3.63 +    val prs = Quotient_Info.prs_rules_get lthy
    3.64 +    val ids = Quotient_Info.id_simps_get lthy
    3.65      val thms =
    3.66        @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    3.67  
    3.68      val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
    3.69    in
    3.70 -    EVERY' [map_fun_tac lthy,
    3.71 -            lambda_prs_tac lthy,
    3.72 -            simp_tac ss,
    3.73 -            TRY o rtac refl]
    3.74 +    EVERY' [
    3.75 +      map_fun_tac lthy,
    3.76 +      lambda_prs_tac lthy,
    3.77 +      simp_tac ss,
    3.78 +      TRY o rtac refl]
    3.79    end
    3.80  
    3.81  
    3.82 @@ -606,10 +603,10 @@
    3.83      val thy = ProofContext.theory_of ctxt
    3.84      val rtrm' = HOLogic.dest_Trueprop rtrm
    3.85      val qtrm' = HOLogic.dest_Trueprop qtrm
    3.86 -    val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
    3.87 -      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    3.88 -    val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
    3.89 -      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    3.90 +    val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
    3.91 +      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    3.92 +    val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
    3.93 +      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    3.94    in
    3.95      Drule.instantiate' []
    3.96        [SOME (cterm_of thy rtrm'),
    3.97 @@ -638,7 +635,7 @@
    3.98      THEN' SUBGOAL (fn (goal, i) =>
    3.99        let
   3.100          val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   3.101 -        val rtrm = derive_rtrm ctxt qtys goal
   3.102 +        val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
   3.103          val rule = procedure_inst ctxt rtrm  goal
   3.104        in
   3.105          rtac rule i
   3.106 @@ -703,7 +700,7 @@
   3.107  fun lifted ctxt qtys simps rthm =
   3.108    let
   3.109      val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
   3.110 -    val goal = derive_qtrm ctxt' qtys (prop_of rthm')
   3.111 +    val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm')
   3.112    in
   3.113      Goal.prove ctxt' [] [] goal
   3.114        (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
     4.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 20:42:25 2011 +0100
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 21:26:49 2011 +0100
     4.3 @@ -35,8 +35,6 @@
     4.4  structure Quotient_Term: QUOTIENT_TERM =
     4.5  struct
     4.6  
     4.7 -open Quotient_Info;
     4.8 -
     4.9  exception LIFT_MATCH of string
    4.10  
    4.11  
    4.12 @@ -67,7 +65,7 @@
    4.13  fun get_mapfun ctxt s =
    4.14    let
    4.15      val thy = ProofContext.theory_of ctxt
    4.16 -    val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
    4.17 +    val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    4.18        raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    4.19    in
    4.20      Const (mapfun, dummyT)
    4.21 @@ -104,7 +102,7 @@
    4.22  fun get_rty_qty ctxt s =
    4.23    let
    4.24      val thy = ProofContext.theory_of ctxt
    4.25 -    val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
    4.26 +    val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound =>
    4.27        raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    4.28    in
    4.29      (#rtyp qdata, #qtyp qdata)
    4.30 @@ -276,7 +274,7 @@
    4.31  fun get_relmap ctxt s =
    4.32    let
    4.33      val thy = ProofContext.theory_of ctxt
    4.34 -    val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
    4.35 +    val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    4.36        raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    4.37    in
    4.38      Const (relmap, dummyT)
    4.39 @@ -300,7 +298,7 @@
    4.40    let
    4.41      val thy = ProofContext.theory_of ctxt
    4.42    in
    4.43 -    #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
    4.44 +    #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound =>
    4.45        raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
    4.46    end
    4.47  
    4.48 @@ -437,7 +435,7 @@
    4.49            if length rtys <> length qtys then false
    4.50            else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
    4.51          else
    4.52 -          (case quotdata_lookup_raw thy qs of
    4.53 +          (case Quotient_Info.quotdata_lookup_raw thy qs of
    4.54              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
    4.55            | NONE => false)
    4.56      | _ => false)
    4.57 @@ -563,7 +561,7 @@
    4.58          if same_const rtrm qtrm then rtrm
    4.59          else
    4.60            let
    4.61 -            val rtrm' = #rconst (qconsts_lookup thy qtrm)
    4.62 +            val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
    4.63                handle Quotient_Info.NotFound =>
    4.64                  term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
    4.65            in
    4.66 @@ -753,7 +751,7 @@
    4.67    let
    4.68      val thy = ProofContext.theory_of ctxt
    4.69    in
    4.70 -    quotdata_dest ctxt
    4.71 +    Quotient_Info.quotdata_dest ctxt
    4.72      |> map (fn x => (#rtyp x, #qtyp x))
    4.73      |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
    4.74      |> map (if direction then swap else I)
    4.75 @@ -765,12 +763,12 @@
    4.76      fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
    4.77  
    4.78      val const_substs =
    4.79 -      qconsts_dest ctxt
    4.80 +      Quotient_Info.qconsts_dest ctxt
    4.81        |> map (fn x => (#rconst x, #qconst x))
    4.82        |> map (if direction then swap else I)
    4.83  
    4.84      val rel_substs =
    4.85 -      quotdata_dest ctxt
    4.86 +      Quotient_Info.quotdata_dest ctxt
    4.87        |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
    4.88        |> map (if direction then swap else I)
    4.89    in
     5.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 20:42:25 2011 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 21:26:49 2011 +0100
     5.3 @@ -20,9 +20,8 @@
     5.4  structure Quotient_Type: QUOTIENT_TYPE =
     5.5  struct
     5.6  
     5.7 -open Quotient_Info;
     5.8 +(* wrappers for define, note, Attrib.internal and theorem_i *)  (* FIXME !? *)
     5.9  
    5.10 -(* wrappers for define, note, Attrib.internal and theorem_i *)
    5.11  fun define (name, mx, rhs) lthy =
    5.12    let
    5.13      val ((rhs, (_ , thm)), lthy') =
    5.14 @@ -160,12 +159,15 @@
    5.15      (* storing the quotdata *)
    5.16      val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
    5.17  
    5.18 -    fun qinfo phi = transform_quotdata phi quotdata
    5.19 +    fun qinfo phi = Quotient_Info.transform_quotdata phi quotdata
    5.20  
    5.21      val lthy4 = lthy3
    5.22 -      |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
    5.23 -      |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
    5.24 -      |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
    5.25 +      |> Local_Theory.declaration true
    5.26 +        (fn phi => Quotient_Info.quotdata_update_gen qty_full_name (qinfo phi))
    5.27 +      |> note
    5.28 +        (equiv_thm_name, equiv_thm,
    5.29 +          if partial then [] else [intern_attr Quotient_Info.equiv_rules_add])
    5.30 +      |> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add])
    5.31    in
    5.32      (quotdata, lthy4)
    5.33    end
    5.34 @@ -218,7 +220,7 @@
    5.35      fun map_check_aux rty warns =
    5.36        case rty of
    5.37          Type (_, []) => warns
    5.38 -      | Type (s, _) => if maps_defined thy s then warns else s::warns
    5.39 +      | Type (s, _) => if Quotient_Info.maps_defined thy s then warns else s::warns
    5.40        | _ => warns
    5.41  
    5.42      val warns = map_check_aux rty []