more precise parentheses and indentation;
authorwenzelm
Fri Jan 07 15:35:00 2011 +0100 (2011-01-07)
changeset 414447f40120cd814
parent 41443 6e93dfec9e76
child 41445 1b31460c2e3a
more precise parentheses and indentation;
eliminated trailing whitespace;
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 14:58:15 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 15:35:00 2011 +0100
     1.3 @@ -34,75 +34,75 @@
     1.4  
     1.5     It stores the qconst_info in the qconsts data slot.
     1.6  
     1.7 -   Restriction: At the moment the left- and right-hand 
     1.8 -   side of the definition must be a constant. 
     1.9 +   Restriction: At the moment the left- and right-hand
    1.10 +   side of the definition must be a constant.
    1.11  *)
    1.12 -fun error_msg bind str = 
    1.13 -let 
    1.14 -  val name = Binding.name_of bind
    1.15 -  val pos = Position.str_of (Binding.pos_of bind)
    1.16 -in
    1.17 -  error ("Head of quotient_definition " ^ 
    1.18 -    quote str ^ " differs from declaration " ^ name ^ pos)
    1.19 -end
    1.20 +fun error_msg bind str =
    1.21 +  let
    1.22 +    val name = Binding.name_of bind
    1.23 +    val pos = Position.str_of (Binding.pos_of bind)
    1.24 +  in
    1.25 +    error ("Head of quotient_definition " ^
    1.26 +      quote str ^ " differs from declaration " ^ name ^ pos)
    1.27 +  end
    1.28  
    1.29  fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
    1.30 -let
    1.31 -  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
    1.32 -  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
    1.33 -  val _ = if is_Const rhs then () else warning "The definiens is not a constant"
    1.34 -  
    1.35 -  fun sanity_test NONE _ = true
    1.36 -    | sanity_test (SOME bind) str =
    1.37 -        if Name.of_binding bind = str then true
    1.38 -        else error_msg bind str
    1.39 +  let
    1.40 +    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
    1.41 +    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
    1.42 +    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
    1.43  
    1.44 -  val _ = sanity_test optbind lhs_str
    1.45 +    fun sanity_test NONE _ = true
    1.46 +      | sanity_test (SOME bind) str =
    1.47 +          if Name.of_binding bind = str then true
    1.48 +          else error_msg bind str
    1.49 +
    1.50 +    val _ = sanity_test optbind lhs_str
    1.51  
    1.52 -  val qconst_bname = Binding.name lhs_str
    1.53 -  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
    1.54 -  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    1.55 -  val (_, prop') = Local_Defs.cert_def lthy prop
    1.56 -  val (_, newrhs) = Local_Defs.abs_def prop'
    1.57 +    val qconst_bname = Binding.name lhs_str
    1.58 +    val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
    1.59 +    val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    1.60 +    val (_, prop') = Local_Defs.cert_def lthy prop
    1.61 +    val (_, newrhs) = Local_Defs.abs_def prop'
    1.62  
    1.63 -  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
    1.64 +    val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
    1.65  
    1.66 -  (* data storage *)
    1.67 -  val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    1.68 +    (* data storage *)
    1.69 +    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    1.70  
    1.71 -  fun qcinfo phi = transform_qconsts phi qconst_data
    1.72 -  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    1.73 -  val lthy'' = Local_Theory.declaration true
    1.74 -                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
    1.75 -in
    1.76 -  (qconst_data, lthy'')
    1.77 -end
    1.78 +    fun qcinfo phi = transform_qconsts phi qconst_data
    1.79 +    fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
    1.80 +    val lthy'' = Local_Theory.declaration true
    1.81 +                   (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
    1.82 +  in
    1.83 +    (qconst_data, lthy'')
    1.84 +  end
    1.85  
    1.86  fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
    1.87 -let
    1.88 -  val lhs = Syntax.read_term lthy lhs_str
    1.89 -  val rhs = Syntax.read_term lthy rhs_str
    1.90 -  val lthy' = Variable.declare_term lhs lthy
    1.91 -  val lthy'' = Variable.declare_term rhs lthy'
    1.92 -in
    1.93 -  quotient_def (decl, (attr, (lhs, rhs))) lthy''
    1.94 -end
    1.95 +  let
    1.96 +    val lhs = Syntax.read_term lthy lhs_str
    1.97 +    val rhs = Syntax.read_term lthy rhs_str
    1.98 +    val lthy' = Variable.declare_term lhs lthy
    1.99 +    val lthy'' = Variable.declare_term rhs lthy'
   1.100 +  in
   1.101 +    quotient_def (decl, (attr, (lhs, rhs))) lthy''
   1.102 +  end
   1.103  
   1.104  (* a wrapper for automatically lifting a raw constant *)
   1.105  fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
   1.106 -let
   1.107 -  val rty = fastype_of rconst
   1.108 -  val qty = derive_qtyp ctxt qtys rty
   1.109 -  val lhs = Free (qconst_name, qty)
   1.110 -in
   1.111 -  quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
   1.112 -end
   1.113 +  let
   1.114 +    val rty = fastype_of rconst
   1.115 +    val qty = derive_qtyp ctxt qtys rty
   1.116 +    val lhs = Free (qconst_name, qty)
   1.117 +  in
   1.118 +    quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
   1.119 +  end
   1.120  
   1.121  (* parser and command *)
   1.122  val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
   1.123  
   1.124  val quotdef_parser =
   1.125 -  Scan.optional quotdef_decl (NONE, NoSyn) -- 
   1.126 +  Scan.optional quotdef_decl (NONE, NoSyn) --
   1.127      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
   1.128  
   1.129  val _ =
     2.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 14:58:15 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:35:00 2011 +0100
     2.3 @@ -68,9 +68,9 @@
     2.4    Symtab.defined (MapsData.get thy) s
     2.5  
     2.6  fun maps_lookup thy s =
     2.7 -  case (Symtab.lookup (MapsData.get thy) s) of
     2.8 +  (case Symtab.lookup (MapsData.get thy) s of
     2.9      SOME map_fun => map_fun
    2.10 -  | NONE => raise NotFound
    2.11 +  | NONE => raise NotFound)
    2.12  
    2.13  fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
    2.14  fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo)  (* FIXME *)
    2.15 @@ -80,17 +80,17 @@
    2.16  
    2.17  (* attribute to be used in declare statements *)
    2.18  fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
    2.19 -let
    2.20 -  val thy = ProofContext.theory_of ctxt
    2.21 -  val tyname = Sign.intern_type thy tystr
    2.22 -  val mapname = Sign.intern_const thy mapstr
    2.23 -  val relname = Sign.intern_const thy relstr
    2.24 +  let
    2.25 +    val thy = ProofContext.theory_of ctxt
    2.26 +    val tyname = Sign.intern_type thy tystr
    2.27 +    val mapname = Sign.intern_const thy mapstr
    2.28 +    val relname = Sign.intern_const thy relstr
    2.29  
    2.30 -  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
    2.31 -  val _ = List.app sanity_check [mapname, relname]
    2.32 -in
    2.33 -  maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
    2.34 -end
    2.35 +    fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
    2.36 +    val _ = List.app sanity_check [mapname, relname]
    2.37 +  in
    2.38 +    maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
    2.39 +  end
    2.40  
    2.41  val maps_attr_parser =
    2.42    Args.context -- Scan.lift
    2.43 @@ -103,20 +103,20 @@
    2.44      "declaration of map information"))
    2.45  
    2.46  fun print_mapsinfo ctxt =
    2.47 -let
    2.48 -  fun prt_map (ty_name, {mapfun, relmap}) =
    2.49 -    Pretty.block (Library.separate (Pretty.brk 2)
    2.50 -      (map Pretty.str
    2.51 -        ["type:", ty_name,
    2.52 -        "map:", mapfun,
    2.53 -        "relation map:", relmap]))
    2.54 -in
    2.55 -  MapsData.get (ProofContext.theory_of ctxt)
    2.56 -  |> Symtab.dest
    2.57 -  |> map (prt_map)
    2.58 -  |> Pretty.big_list "maps for type constructors:"
    2.59 -  |> Pretty.writeln
    2.60 -end
    2.61 +  let
    2.62 +    fun prt_map (ty_name, {mapfun, relmap}) =
    2.63 +      Pretty.block (Library.separate (Pretty.brk 2)
    2.64 +        (map Pretty.str
    2.65 +          ["type:", ty_name,
    2.66 +          "map:", mapfun,
    2.67 +          "relation map:", relmap]))
    2.68 +  in
    2.69 +    MapsData.get (ProofContext.theory_of ctxt)
    2.70 +    |> Symtab.dest
    2.71 +    |> map (prt_map)
    2.72 +    |> Pretty.big_list "maps for type constructors:"
    2.73 +    |> Pretty.writeln
    2.74 +  end
    2.75  
    2.76  
    2.77  (* info about quotient types *)
    2.78 @@ -150,24 +150,24 @@
    2.79    map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
    2.80  
    2.81  fun print_quotinfo ctxt =
    2.82 -let
    2.83 -  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
    2.84 -    Pretty.block (Library.separate (Pretty.brk 2)
    2.85 -     [Pretty.str "quotient type:",
    2.86 -      Syntax.pretty_typ ctxt qtyp,
    2.87 -      Pretty.str "raw type:",
    2.88 -      Syntax.pretty_typ ctxt rtyp,
    2.89 -      Pretty.str "relation:",
    2.90 -      Syntax.pretty_term ctxt equiv_rel,
    2.91 -      Pretty.str "equiv. thm:",
    2.92 -      Syntax.pretty_term ctxt (prop_of equiv_thm)])
    2.93 -in
    2.94 -  QuotData.get (ProofContext.theory_of ctxt)
    2.95 -  |> Symtab.dest
    2.96 -  |> map (prt_quot o snd)
    2.97 -  |> Pretty.big_list "quotients:"
    2.98 -  |> Pretty.writeln
    2.99 -end
   2.100 +  let
   2.101 +    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
   2.102 +      Pretty.block (Library.separate (Pretty.brk 2)
   2.103 +       [Pretty.str "quotient type:",
   2.104 +        Syntax.pretty_typ ctxt qtyp,
   2.105 +        Pretty.str "raw type:",
   2.106 +        Syntax.pretty_typ ctxt rtyp,
   2.107 +        Pretty.str "relation:",
   2.108 +        Syntax.pretty_term ctxt equiv_rel,
   2.109 +        Pretty.str "equiv. thm:",
   2.110 +        Syntax.pretty_term ctxt (prop_of equiv_thm)])
   2.111 +  in
   2.112 +    QuotData.get (ProofContext.theory_of ctxt)
   2.113 +    |> Symtab.dest
   2.114 +    |> map (prt_quot o snd)
   2.115 +    |> Pretty.big_list "quotients:"
   2.116 +    |> Pretty.writeln
   2.117 +  end
   2.118  
   2.119  
   2.120  (* info about quotient constants *)
   2.121 @@ -207,32 +207,32 @@
   2.122          name = name' andalso Sign.typ_instance thy (qty, qty')
   2.123        end
   2.124    in
   2.125 -    case Symtab.lookup (QConstsData.get thy) name of
   2.126 +    (case Symtab.lookup (QConstsData.get thy) name of
   2.127        NONE => raise NotFound
   2.128      | SOME l =>
   2.129 -      (case (find_first matches l) of
   2.130 -        SOME x => x
   2.131 -      | NONE => raise NotFound)
   2.132 +        (case find_first matches l of
   2.133 +          SOME x => x
   2.134 +        | NONE => raise NotFound))
   2.135    end
   2.136  
   2.137  fun print_qconstinfo ctxt =
   2.138 -let
   2.139 -  fun prt_qconst {qconst, rconst, def} =
   2.140 -    Pretty.block (separate (Pretty.brk 1)
   2.141 -     [Syntax.pretty_term ctxt qconst,
   2.142 -      Pretty.str ":=",
   2.143 -      Syntax.pretty_term ctxt rconst,
   2.144 -      Pretty.str "as",
   2.145 -      Syntax.pretty_term ctxt (prop_of def)])
   2.146 -in
   2.147 -  QConstsData.get (ProofContext.theory_of ctxt)
   2.148 -  |> Symtab.dest
   2.149 -  |> map snd
   2.150 -  |> flat
   2.151 -  |> map prt_qconst
   2.152 -  |> Pretty.big_list "quotient constants:"
   2.153 -  |> Pretty.writeln
   2.154 -end
   2.155 +  let
   2.156 +    fun prt_qconst {qconst, rconst, def} =
   2.157 +      Pretty.block (separate (Pretty.brk 1)
   2.158 +       [Syntax.pretty_term ctxt qconst,
   2.159 +        Pretty.str ":=",
   2.160 +        Syntax.pretty_term ctxt rconst,
   2.161 +        Pretty.str "as",
   2.162 +        Syntax.pretty_term ctxt (prop_of def)])
   2.163 +  in
   2.164 +    QConstsData.get (ProofContext.theory_of ctxt)
   2.165 +    |> Symtab.dest
   2.166 +    |> map snd
   2.167 +    |> flat
   2.168 +    |> map prt_qconst
   2.169 +    |> Pretty.big_list "quotient constants:"
   2.170 +    |> Pretty.writeln
   2.171 +  end
   2.172  
   2.173  (* equivalence relation theorems *)
   2.174  structure EquivRules = Named_Thms
     3.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 14:58:15 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 15:35:00 2011 +0100
     3.3 @@ -11,10 +11,10 @@
     3.4    val injection_tac: Proof.context -> int -> tactic
     3.5    val all_injection_tac: Proof.context -> int -> tactic
     3.6    val clean_tac: Proof.context -> int -> tactic
     3.7 -  
     3.8 +
     3.9    val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
    3.10    val descend_tac: Proof.context -> thm list -> int -> tactic
    3.11 - 
    3.12 +
    3.13    val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
    3.14    val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
    3.15  
    3.16 @@ -42,12 +42,12 @@
    3.17  fun OF1 thm1 thm2 = thm2 RS thm1
    3.18  
    3.19  fun atomize_thm thm =
    3.20 -let
    3.21 -  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
    3.22 -  val thm'' = Object_Logic.atomize (cprop_of thm')
    3.23 -in
    3.24 -  @{thm equal_elim_rule1} OF [thm'', thm']
    3.25 -end
    3.26 +  let
    3.27 +    val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
    3.28 +    val thm'' = Object_Logic.atomize (cprop_of thm')
    3.29 +  in
    3.30 +    @{thm equal_elim_rule1} OF [thm'', thm']
    3.31 +  end
    3.32  
    3.33  
    3.34  
    3.35 @@ -83,14 +83,14 @@
    3.36    (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
    3.37  
    3.38  fun get_match_inst thy pat trm =
    3.39 -let
    3.40 -  val univ = Unify.matchers thy [(pat, trm)]
    3.41 -  val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *)  (* FIXME fragile *)
    3.42 -  val tenv = Vartab.dest (Envir.term_env env)
    3.43 -  val tyenv = Vartab.dest (Envir.type_env env)
    3.44 -in
    3.45 -  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
    3.46 -end
    3.47 +  let
    3.48 +    val univ = Unify.matchers thy [(pat, trm)]
    3.49 +    val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
    3.50 +    val tenv = Vartab.dest (Envir.term_env env)
    3.51 +    val tyenv = Vartab.dest (Envir.type_env env)
    3.52 +  in
    3.53 +    (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
    3.54 +  end
    3.55  
    3.56  (* Calculates the instantiations for the lemmas:
    3.57  
    3.58 @@ -101,35 +101,35 @@
    3.59     theorem applies and return NONE if it doesn't.
    3.60  *)
    3.61  fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
    3.62 -let
    3.63 -  val thy = ProofContext.theory_of ctxt
    3.64 -  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
    3.65 -  val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
    3.66 -  val trm_inst = map (SOME o cterm_of thy) [R2, R1]
    3.67 -in
    3.68 -  case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
    3.69 -    NONE => NONE
    3.70 -  | SOME thm' =>
    3.71 -      (case try (get_match_inst thy (get_lhs thm')) redex of
    3.72 -        NONE => NONE
    3.73 -      | SOME inst2 => try (Drule.instantiate inst2) thm')
    3.74 -end
    3.75 +  let
    3.76 +    val thy = ProofContext.theory_of ctxt
    3.77 +    fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
    3.78 +    val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
    3.79 +    val trm_inst = map (SOME o cterm_of thy) [R2, R1]
    3.80 +  in
    3.81 +    (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
    3.82 +      NONE => NONE
    3.83 +    | SOME thm' =>
    3.84 +        (case try (get_match_inst thy (get_lhs thm')) redex of
    3.85 +          NONE => NONE
    3.86 +        | SOME inst2 => try (Drule.instantiate inst2) thm'))
    3.87 +  end
    3.88  
    3.89  fun ball_bex_range_simproc ss redex =
    3.90 -let
    3.91 -  val ctxt = Simplifier.the_context ss
    3.92 -in
    3.93 -  case redex of
    3.94 -    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
    3.95 -      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
    3.96 -        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
    3.97 +  let
    3.98 +    val ctxt = Simplifier.the_context ss
    3.99 +  in
   3.100 +    case redex of
   3.101 +      (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
   3.102 +        (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   3.103 +          calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   3.104  
   3.105 -  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
   3.106 -      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   3.107 -        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   3.108 +    | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
   3.109 +        (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   3.110 +          calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   3.111  
   3.112 -  | _ => NONE
   3.113 -end
   3.114 +    | _ => NONE
   3.115 +  end
   3.116  
   3.117  (* Regularize works as follows:
   3.118  
   3.119 @@ -159,25 +159,27 @@
   3.120  fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
   3.121  
   3.122  fun regularize_tac ctxt =
   3.123 -let
   3.124 -  val thy = ProofContext.theory_of ctxt
   3.125 -  val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   3.126 -  val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
   3.127 -  val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   3.128 -  val simpset = (mk_minimal_ss ctxt)
   3.129 -                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   3.130 -                       addsimprocs [simproc]
   3.131 -                       addSolver equiv_solver addSolver quotient_solver
   3.132 -  val eq_eqvs = eq_imp_rel_get ctxt
   3.133 -in
   3.134 -  simp_tac simpset THEN'
   3.135 -  REPEAT_ALL_NEW (CHANGED o FIRST'
   3.136 -    [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
   3.137 -     resolve_tac (Inductive.get_monos ctxt),
   3.138 -     resolve_tac @{thms ball_all_comm bex_ex_comm},
   3.139 -     resolve_tac eq_eqvs,
   3.140 -     simp_tac simpset])
   3.141 -end
   3.142 +  let
   3.143 +    val thy = ProofContext.theory_of ctxt
   3.144 +    val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   3.145 +    val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
   3.146 +    val simproc =
   3.147 +      Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   3.148 +    val simpset =
   3.149 +      mk_minimal_ss ctxt
   3.150 +      addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   3.151 +      addsimprocs [simproc]
   3.152 +      addSolver equiv_solver addSolver quotient_solver
   3.153 +    val eq_eqvs = eq_imp_rel_get ctxt
   3.154 +  in
   3.155 +    simp_tac simpset THEN'
   3.156 +    REPEAT_ALL_NEW (CHANGED o FIRST'
   3.157 +      [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
   3.158 +       resolve_tac (Inductive.get_monos ctxt),
   3.159 +       resolve_tac @{thms ball_all_comm bex_ex_comm},
   3.160 +       resolve_tac eq_eqvs,
   3.161 +       simp_tac simpset])
   3.162 +  end
   3.163  
   3.164  
   3.165  
   3.166 @@ -187,52 +189,52 @@
   3.167     is an application, it returns the function and the argument.
   3.168  *)
   3.169  fun find_qt_asm asms =
   3.170 -let
   3.171 -  fun find_fun trm =
   3.172 -    case trm of
   3.173 -      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
   3.174 -    | _ => false
   3.175 -in
   3.176 - case find_first find_fun asms of
   3.177 -   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
   3.178 - | _ => NONE
   3.179 -end
   3.180 +  let
   3.181 +    fun find_fun trm =
   3.182 +      (case trm of
   3.183 +        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
   3.184 +      | _ => false)
   3.185 +  in
   3.186 +     (case find_first find_fun asms of
   3.187 +       SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
   3.188 +     | _ => NONE)
   3.189 +  end
   3.190  
   3.191  fun quot_true_simple_conv ctxt fnctn ctrm =
   3.192 -  case (term_of ctrm) of
   3.193 +  case term_of ctrm of
   3.194      (Const (@{const_name Quot_True}, _) $ x) =>
   3.195 -    let
   3.196 -      val fx = fnctn x;
   3.197 -      val thy = ProofContext.theory_of ctxt;
   3.198 -      val cx = cterm_of thy x;
   3.199 -      val cfx = cterm_of thy fx;
   3.200 -      val cxt = ctyp_of thy (fastype_of x);
   3.201 -      val cfxt = ctyp_of thy (fastype_of fx);
   3.202 -      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   3.203 -    in
   3.204 -      Conv.rewr_conv thm ctrm
   3.205 -    end
   3.206 +      let
   3.207 +        val fx = fnctn x;
   3.208 +        val thy = ProofContext.theory_of ctxt;
   3.209 +        val cx = cterm_of thy x;
   3.210 +        val cfx = cterm_of thy fx;
   3.211 +        val cxt = ctyp_of thy (fastype_of x);
   3.212 +        val cfxt = ctyp_of thy (fastype_of fx);
   3.213 +        val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   3.214 +      in
   3.215 +        Conv.rewr_conv thm ctrm
   3.216 +      end
   3.217  
   3.218  fun quot_true_conv ctxt fnctn ctrm =
   3.219 -  case (term_of ctrm) of
   3.220 +  (case term_of ctrm of
   3.221      (Const (@{const_name Quot_True}, _) $ _) =>
   3.222        quot_true_simple_conv ctxt fnctn ctrm
   3.223    | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   3.224    | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
   3.225 -  | _ => Conv.all_conv ctrm
   3.226 +  | _ => Conv.all_conv ctrm)
   3.227  
   3.228  fun quot_true_tac ctxt fnctn =
   3.229 -   CONVERSION
   3.230 +  CONVERSION
   3.231      ((Conv.params_conv ~1 (fn ctxt =>
   3.232 -       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
   3.233 +        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
   3.234  
   3.235  fun dest_comb (f $ a) = (f, a)
   3.236  fun dest_bcomb ((_ $ l) $ r) = (l, r)
   3.237  
   3.238  fun unlam t =
   3.239 -  case t of
   3.240 -    (Abs a) => snd (Term.dest_abs a)
   3.241 -  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
   3.242 +  (case t of
   3.243 +    Abs a => snd (Term.dest_abs a)
   3.244 +  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
   3.245  
   3.246  val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
   3.247  
   3.248 @@ -242,53 +244,53 @@
   3.249  *)
   3.250  val apply_rsp_tac =
   3.251    Subgoal.FOCUS (fn {concl, asms, context,...} =>
   3.252 -  let
   3.253 -    val bare_concl = HOLogic.dest_Trueprop (term_of concl)
   3.254 -    val qt_asm = find_qt_asm (map term_of asms)
   3.255 -  in
   3.256 -    case (bare_concl, qt_asm) of
   3.257 -      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
   3.258 -         if fastype_of qt_fun = fastype_of f
   3.259 -         then no_tac
   3.260 -         else
   3.261 -           let
   3.262 -             val ty_x = fastype_of x
   3.263 -             val ty_b = fastype_of qt_arg
   3.264 -             val ty_f = range_type (fastype_of f)
   3.265 -             val thy = ProofContext.theory_of context
   3.266 -             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
   3.267 -             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
   3.268 -             val inst_thm = Drule.instantiate' ty_inst
   3.269 -               ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
   3.270 -           in
   3.271 -             (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
   3.272 -           end
   3.273 -    | _ => no_tac
   3.274 -  end)
   3.275 +    let
   3.276 +      val bare_concl = HOLogic.dest_Trueprop (term_of concl)
   3.277 +      val qt_asm = find_qt_asm (map term_of asms)
   3.278 +    in
   3.279 +      case (bare_concl, qt_asm) of
   3.280 +        (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
   3.281 +          if fastype_of qt_fun = fastype_of f
   3.282 +          then no_tac
   3.283 +          else
   3.284 +            let
   3.285 +              val ty_x = fastype_of x
   3.286 +              val ty_b = fastype_of qt_arg
   3.287 +              val ty_f = range_type (fastype_of f)
   3.288 +              val thy = ProofContext.theory_of context
   3.289 +              val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
   3.290 +              val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
   3.291 +              val inst_thm = Drule.instantiate' ty_inst
   3.292 +                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
   3.293 +            in
   3.294 +              (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
   3.295 +            end
   3.296 +      | _ => no_tac
   3.297 +    end)
   3.298  
   3.299  (* Instantiates and applies 'equals_rsp'. Since the theorem is
   3.300     complex we rely on instantiation to tell us if it applies
   3.301  *)
   3.302  fun equals_rsp_tac R ctxt =
   3.303 -let
   3.304 -  val thy = ProofContext.theory_of ctxt
   3.305 -in
   3.306 -  case try (cterm_of thy) R of (* There can be loose bounds in R *)
   3.307 -    SOME ctm =>
   3.308 -      let
   3.309 -        val ty = domain_type (fastype_of R)
   3.310 -      in
   3.311 -        case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
   3.312 -          [SOME (cterm_of thy R)]) @{thm equals_rsp} of
   3.313 -          SOME thm => rtac thm THEN' quotient_tac ctxt
   3.314 -        | NONE => K no_tac
   3.315 -      end
   3.316 -  | _ => K no_tac
   3.317 -end
   3.318 +  let
   3.319 +    val thy = ProofContext.theory_of ctxt
   3.320 +  in
   3.321 +    case try (cterm_of thy) R of (* There can be loose bounds in R *)
   3.322 +      SOME ctm =>
   3.323 +        let
   3.324 +          val ty = domain_type (fastype_of R)
   3.325 +        in
   3.326 +          case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
   3.327 +              [SOME (cterm_of thy R)]) @{thm equals_rsp} of
   3.328 +            SOME thm => rtac thm THEN' quotient_tac ctxt
   3.329 +          | NONE => K no_tac
   3.330 +        end
   3.331 +    | _ => K no_tac
   3.332 +  end
   3.333  
   3.334  fun rep_abs_rsp_tac ctxt =
   3.335    SUBGOAL (fn (goal, i) =>
   3.336 -    case (try bare_concl goal) of
   3.337 +    (case try bare_concl goal of
   3.338        SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
   3.339      | SOME (rel $ _ $ (rep $ (abs $ _))) =>
   3.340          let
   3.341 @@ -303,7 +305,7 @@
   3.342                | NONE => no_tac)
   3.343            | NONE => no_tac
   3.344          end
   3.345 -    | _ => no_tac)
   3.346 +    | _ => no_tac))
   3.347  
   3.348  
   3.349  
   3.350 @@ -329,67 +331,66 @@
   3.351      - reflexivity of the relation
   3.352  *)
   3.353  fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
   3.354 -(case (bare_concl goal) of
   3.355 -    (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   3.356 -  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   3.357 -      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.358 +  (case bare_concl goal of
   3.359 +      (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   3.360 +    (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   3.361 +        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.362  
   3.363 -    (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   3.364 -| (Const (@{const_name HOL.eq},_) $
   3.365 -    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.366 -    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   3.367 -      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   3.368 +      (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   3.369 +  | (Const (@{const_name HOL.eq},_) $
   3.370 +      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.371 +      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   3.372 +        => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   3.373  
   3.374 -    (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
   3.375 -| (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.376 -    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.377 -    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.378 -      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.379 +      (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
   3.380 +  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.381 +      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.382 +      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.383 +        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.384  
   3.385 -    (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   3.386 -| Const (@{const_name HOL.eq},_) $
   3.387 -    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.388 -    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.389 -      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   3.390 +      (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   3.391 +  | Const (@{const_name HOL.eq},_) $
   3.392 +      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.393 +      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.394 +        => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   3.395  
   3.396 -    (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
   3.397 -| (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.398 -    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.399 -    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.400 -      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.401 +      (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
   3.402 +  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.403 +      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.404 +      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   3.405 +        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
   3.406  
   3.407 -| (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.408 -    (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
   3.409 -      => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
   3.410 +  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   3.411 +      (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
   3.412 +        => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
   3.413  
   3.414 -| (_ $
   3.415 -    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.416 -    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   3.417 -      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
   3.418 +  | (_ $
   3.419 +      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   3.420 +      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   3.421 +        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
   3.422  
   3.423 -| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   3.424 -   (rtac @{thm refl} ORELSE'
   3.425 -    (equals_rsp_tac R ctxt THEN' RANGE [
   3.426 -       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
   3.427 +  | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   3.428 +     (rtac @{thm refl} ORELSE'
   3.429 +      (equals_rsp_tac R ctxt THEN' RANGE [
   3.430 +         quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
   3.431  
   3.432 -    (* reflexivity of operators arising from Cong_tac *)
   3.433 -| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
   3.434 +      (* reflexivity of operators arising from Cong_tac *)
   3.435 +  | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
   3.436  
   3.437 -   (* respectfulness of constants; in particular of a simple relation *)
   3.438 -| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
   3.439 -    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
   3.440 +     (* respectfulness of constants; in particular of a simple relation *)
   3.441 +  | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
   3.442 +      => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
   3.443  
   3.444 -    (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
   3.445 -    (* observe map_fun *)
   3.446 -| _ $ _ $ _
   3.447 -    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
   3.448 -       ORELSE' rep_abs_rsp_tac ctxt
   3.449 +      (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
   3.450 +      (* observe map_fun *)
   3.451 +  | _ $ _ $ _
   3.452 +      => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
   3.453 +         ORELSE' rep_abs_rsp_tac ctxt
   3.454  
   3.455 -| _ => K no_tac
   3.456 -) i)
   3.457 +  | _ => K no_tac) i)
   3.458  
   3.459  fun injection_step_tac ctxt rel_refl =
   3.460 - FIRST' [
   3.461 +  FIRST' [
   3.462      injection_match_tac ctxt,
   3.463  
   3.464      (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
   3.465 @@ -412,11 +413,11 @@
   3.466      resolve_tac rel_refl]
   3.467  
   3.468  fun injection_tac ctxt =
   3.469 -let
   3.470 -  val rel_refl = reflp_get ctxt
   3.471 -in
   3.472 -  injection_step_tac ctxt rel_refl
   3.473 -end
   3.474 +  let
   3.475 +    val rel_refl = reflp_get ctxt
   3.476 +  in
   3.477 +    injection_step_tac ctxt rel_refl
   3.478 +  end
   3.479  
   3.480  fun all_injection_tac ctxt =
   3.481    REPEAT_ALL_NEW (injection_tac ctxt)
   3.482 @@ -427,46 +428,48 @@
   3.483  
   3.484  (* expands all map_funs, except in front of the (bound) variables listed in xs *)
   3.485  fun map_fun_simple_conv xs ctrm =
   3.486 -  case (term_of ctrm) of
   3.487 +  (case term_of ctrm of
   3.488      ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
   3.489          if member (op=) xs h
   3.490          then Conv.all_conv ctrm
   3.491          else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
   3.492 -  | _ => Conv.all_conv ctrm
   3.493 +  | _ => Conv.all_conv ctrm)
   3.494  
   3.495  fun map_fun_conv xs ctxt ctrm =
   3.496 -  case (term_of ctrm) of
   3.497 -      _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
   3.498 -                map_fun_simple_conv xs) ctrm
   3.499 -    | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
   3.500 -    | _ => Conv.all_conv ctrm
   3.501 +  (case term_of ctrm of
   3.502 +    _ $ _ =>
   3.503 +      (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
   3.504 +        map_fun_simple_conv xs) ctrm
   3.505 +  | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
   3.506 +  | _ => Conv.all_conv ctrm)
   3.507  
   3.508  fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
   3.509  
   3.510  (* custom matching functions *)
   3.511  fun mk_abs u i t =
   3.512 -  if incr_boundvars i u aconv t then Bound i else
   3.513 -  case t of
   3.514 -    t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
   3.515 -  | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
   3.516 -  | Bound j => if i = j then error "make_inst" else t
   3.517 -  | _ => t
   3.518 +  if incr_boundvars i u aconv t then Bound i
   3.519 +  else
   3.520 +    case t of
   3.521 +      t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
   3.522 +    | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
   3.523 +    | Bound j => if i = j then error "make_inst" else t
   3.524 +    | _ => t
   3.525  
   3.526  fun make_inst lhs t =
   3.527 -let
   3.528 -  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
   3.529 -  val _ $ (Abs (_, _, (_ $ g))) = t;
   3.530 -in
   3.531 -  (f, Abs ("x", T, mk_abs u 0 g))
   3.532 -end
   3.533 +  let
   3.534 +    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
   3.535 +    val _ $ (Abs (_, _, (_ $ g))) = t;
   3.536 +  in
   3.537 +    (f, Abs ("x", T, mk_abs u 0 g))
   3.538 +  end
   3.539  
   3.540  fun make_inst_id lhs t =
   3.541 -let
   3.542 -  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
   3.543 -  val _ $ (Abs (_, _, g)) = t;
   3.544 -in
   3.545 -  (f, Abs ("x", T, mk_abs u 0 g))
   3.546 -end
   3.547 +  let
   3.548 +    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
   3.549 +    val _ $ (Abs (_, _, g)) = t;
   3.550 +  in
   3.551 +    (f, Abs ("x", T, mk_abs u 0 g))
   3.552 +  end
   3.553  
   3.554  (* Simplifies a redex using the 'lambda_prs' theorem.
   3.555     First instantiates the types and known subterms.
   3.556 @@ -476,7 +479,7 @@
   3.557     make_inst_id is used
   3.558  *)
   3.559  fun lambda_prs_simple_conv ctxt ctrm =
   3.560 -  case (term_of ctrm) of
   3.561 +  (case term_of ctrm of
   3.562      (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
   3.563        let
   3.564          val thy = ProofContext.theory_of ctxt
   3.565 @@ -495,7 +498,7 @@
   3.566        in
   3.567          Conv.rewr_conv thm4 ctrm
   3.568        end
   3.569 -  | _ => Conv.all_conv ctrm
   3.570 +  | _ => Conv.all_conv ctrm)
   3.571  
   3.572  fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
   3.573  fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
   3.574 @@ -523,25 +526,26 @@
   3.575    4. test for refl
   3.576  *)
   3.577  fun clean_tac lthy =
   3.578 -let
   3.579 -  val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
   3.580 -  val prs = prs_rules_get lthy
   3.581 -  val ids = id_simps_get lthy
   3.582 -  val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   3.583 +  let
   3.584 +    val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
   3.585 +    val prs = prs_rules_get lthy
   3.586 +    val ids = id_simps_get lthy
   3.587 +    val thms =
   3.588 +      @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   3.589  
   3.590 -  val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   3.591 -in
   3.592 -  EVERY' [map_fun_tac lthy,
   3.593 -          lambda_prs_tac lthy,
   3.594 -          simp_tac ss,
   3.595 -          TRY o rtac refl]
   3.596 -end
   3.597 +    val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   3.598 +  in
   3.599 +    EVERY' [map_fun_tac lthy,
   3.600 +            lambda_prs_tac lthy,
   3.601 +            simp_tac ss,
   3.602 +            TRY o rtac refl]
   3.603 +  end
   3.604  
   3.605  
   3.606  (* Tactic for Generalising Free Variables in a Goal *)
   3.607  
   3.608  fun inst_spec ctrm =
   3.609 -   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
   3.610 +  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
   3.611  
   3.612  fun inst_spec_tac ctrms =
   3.613    EVERY' (map (dtac o inst_spec) ctrms)
   3.614 @@ -588,31 +592,31 @@
   3.615        by (simp add: Quot_True_def)}
   3.616  
   3.617  fun lift_match_error ctxt msg rtrm qtrm =
   3.618 -let
   3.619 -  val rtrm_str = Syntax.string_of_term ctxt rtrm
   3.620 -  val qtrm_str = Syntax.string_of_term ctxt qtrm
   3.621 -  val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
   3.622 -    "", "does not match with original theorem", rtrm_str]
   3.623 -in
   3.624 -  error msg
   3.625 -end
   3.626 +  let
   3.627 +    val rtrm_str = Syntax.string_of_term ctxt rtrm
   3.628 +    val qtrm_str = Syntax.string_of_term ctxt qtrm
   3.629 +    val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
   3.630 +      "", "does not match with original theorem", rtrm_str]
   3.631 +  in
   3.632 +    error msg
   3.633 +  end
   3.634  
   3.635  fun procedure_inst ctxt rtrm qtrm =
   3.636 -let
   3.637 -  val thy = ProofContext.theory_of ctxt
   3.638 -  val rtrm' = HOLogic.dest_Trueprop rtrm
   3.639 -  val qtrm' = HOLogic.dest_Trueprop qtrm
   3.640 -  val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
   3.641 -    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   3.642 -  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   3.643 -    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   3.644 -in
   3.645 -  Drule.instantiate' []
   3.646 -    [SOME (cterm_of thy rtrm'),
   3.647 -     SOME (cterm_of thy reg_goal),
   3.648 -     NONE,
   3.649 -     SOME (cterm_of thy inj_goal)] lifting_procedure_thm
   3.650 -end
   3.651 +  let
   3.652 +    val thy = ProofContext.theory_of ctxt
   3.653 +    val rtrm' = HOLogic.dest_Trueprop rtrm
   3.654 +    val qtrm' = HOLogic.dest_Trueprop qtrm
   3.655 +    val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
   3.656 +      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   3.657 +    val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   3.658 +      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   3.659 +  in
   3.660 +    Drule.instantiate' []
   3.661 +      [SOME (cterm_of thy rtrm'),
   3.662 +       SOME (cterm_of thy reg_goal),
   3.663 +       NONE,
   3.664 +       SOME (cterm_of thy inj_goal)] lifting_procedure_thm
   3.665 +  end
   3.666  
   3.667  
   3.668  (* Since we use Ball and Bex during the lifting and descending,
   3.669 @@ -625,34 +629,34 @@
   3.670  (** descending as tactic **)
   3.671  
   3.672  fun descend_procedure_tac ctxt simps =
   3.673 -let
   3.674 -  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   3.675 -in
   3.676 -  full_simp_tac ss
   3.677 -  THEN' Object_Logic.full_atomize_tac
   3.678 -  THEN' gen_frees_tac ctxt
   3.679 -  THEN' SUBGOAL (fn (goal, i) =>
   3.680 -        let
   3.681 -          val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   3.682 -          val rtrm = derive_rtrm ctxt qtys goal
   3.683 -          val rule = procedure_inst ctxt rtrm  goal
   3.684 -        in
   3.685 -          rtac rule i
   3.686 -        end)
   3.687 -end
   3.688 +  let
   3.689 +    val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   3.690 +  in
   3.691 +    full_simp_tac ss
   3.692 +    THEN' Object_Logic.full_atomize_tac
   3.693 +    THEN' gen_frees_tac ctxt
   3.694 +    THEN' SUBGOAL (fn (goal, i) =>
   3.695 +      let
   3.696 +        val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   3.697 +        val rtrm = derive_rtrm ctxt qtys goal
   3.698 +        val rule = procedure_inst ctxt rtrm  goal
   3.699 +      in
   3.700 +        rtac rule i
   3.701 +      end)
   3.702 +  end
   3.703  
   3.704  fun descend_tac ctxt simps =
   3.705 -let
   3.706 -  val mk_tac_raw =
   3.707 -    descend_procedure_tac ctxt simps
   3.708 -    THEN' RANGE
   3.709 -      [Object_Logic.rulify_tac THEN' (K all_tac),
   3.710 -       regularize_tac ctxt,
   3.711 -       all_injection_tac ctxt,
   3.712 -       clean_tac ctxt]
   3.713 -in
   3.714 -  Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
   3.715 -end
   3.716 +  let
   3.717 +    val mk_tac_raw =
   3.718 +      descend_procedure_tac ctxt simps
   3.719 +      THEN' RANGE
   3.720 +        [Object_Logic.rulify_tac THEN' (K all_tac),
   3.721 +         regularize_tac ctxt,
   3.722 +         all_injection_tac ctxt,
   3.723 +         clean_tac ctxt]
   3.724 +  in
   3.725 +    Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
   3.726 +  end
   3.727  
   3.728  
   3.729  (** lifting as a tactic **)
   3.730 @@ -660,29 +664,29 @@
   3.731  
   3.732  (* the tactic leaves three subgoals to be proved *)
   3.733  fun lift_procedure_tac ctxt simps rthm =
   3.734 -let
   3.735 -  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   3.736 -in
   3.737 -  full_simp_tac ss
   3.738 -  THEN' Object_Logic.full_atomize_tac
   3.739 -  THEN' gen_frees_tac ctxt
   3.740 -  THEN' SUBGOAL (fn (goal, i) =>
   3.741 -    let
   3.742 -      (* full_atomize_tac contracts eta redexes,
   3.743 -         so we do it also in the original theorem *)
   3.744 -      val rthm' = 
   3.745 -        rthm |> full_simplify ss
   3.746 -             |> Drule.eta_contraction_rule 
   3.747 -             |> Thm.forall_intr_frees
   3.748 -             |> atomize_thm 
   3.749 +  let
   3.750 +    val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   3.751 +  in
   3.752 +    full_simp_tac ss
   3.753 +    THEN' Object_Logic.full_atomize_tac
   3.754 +    THEN' gen_frees_tac ctxt
   3.755 +    THEN' SUBGOAL (fn (goal, i) =>
   3.756 +      let
   3.757 +        (* full_atomize_tac contracts eta redexes,
   3.758 +           so we do it also in the original theorem *)
   3.759 +        val rthm' =
   3.760 +          rthm |> full_simplify ss
   3.761 +               |> Drule.eta_contraction_rule
   3.762 +               |> Thm.forall_intr_frees
   3.763 +               |> atomize_thm
   3.764  
   3.765 -      val rule = procedure_inst ctxt (prop_of rthm') goal
   3.766 -    in
   3.767 -      (rtac rule THEN' rtac rthm') i
   3.768 -    end)
   3.769 -end
   3.770 +        val rule = procedure_inst ctxt (prop_of rthm') goal
   3.771 +      in
   3.772 +        (rtac rule THEN' rtac rthm') i
   3.773 +      end)
   3.774 +  end
   3.775  
   3.776 -fun lift_single_tac ctxt simps rthm = 
   3.777 +fun lift_single_tac ctxt simps rthm =
   3.778    lift_procedure_tac ctxt simps rthm
   3.779    THEN' RANGE
   3.780      [ regularize_tac ctxt,
   3.781 @@ -690,26 +694,26 @@
   3.782        clean_tac ctxt ]
   3.783  
   3.784  fun lift_tac ctxt simps rthms =
   3.785 -  Goal.conjunction_tac 
   3.786 +  Goal.conjunction_tac
   3.787    THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
   3.788  
   3.789  
   3.790  (* automated lifting with pre-simplification of the theorems;
   3.791     for internal usage *)
   3.792  fun lifted ctxt qtys simps rthm =
   3.793 -let
   3.794 -  val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
   3.795 -  val goal = derive_qtrm ctxt' qtys (prop_of rthm')
   3.796 -in
   3.797 -  Goal.prove ctxt' [] [] goal 
   3.798 -    (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
   3.799 -  |> singleton (ProofContext.export ctxt' ctxt)
   3.800 -end
   3.801 +  let
   3.802 +    val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
   3.803 +    val goal = derive_qtrm ctxt' qtys (prop_of rthm')
   3.804 +  in
   3.805 +    Goal.prove ctxt' [] [] goal
   3.806 +      (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
   3.807 +    |> singleton (ProofContext.export ctxt' ctxt)
   3.808 +  end
   3.809  
   3.810  
   3.811  (* lifting as an attribute *)
   3.812  
   3.813 -val lifted_attrib = Thm.rule_attribute (fn context => 
   3.814 +val lifted_attrib = Thm.rule_attribute (fn context =>
   3.815    let
   3.816      val ctxt = Context.proof_of context
   3.817      val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
     4.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 14:58:15 2011 +0100
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 15:35:00 2011 +0100
     4.3 @@ -65,13 +65,13 @@
     4.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     4.5  
     4.6  fun get_mapfun ctxt s =
     4.7 -let
     4.8 -  val thy = ProofContext.theory_of ctxt
     4.9 -  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
    4.10 -    raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    4.11 -in
    4.12 -  Const (mapfun, dummyT)
    4.13 -end
    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 +      raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    4.18 +  in
    4.19 +    Const (mapfun, dummyT)
    4.20 +  end
    4.21  
    4.22  (* makes a Free out of a TVar *)
    4.23  fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    4.24 @@ -85,74 +85,74 @@
    4.25     it produces:     %a b. prod_map (map a) b
    4.26  *)
    4.27  fun mk_mapfun ctxt vs rty =
    4.28 -let
    4.29 -  val vs' = map mk_Free vs
    4.30 +  let
    4.31 +    val vs' = map mk_Free vs
    4.32  
    4.33 -  fun mk_mapfun_aux rty =
    4.34 -    case rty of
    4.35 -      TVar _ => mk_Free rty
    4.36 -    | Type (_, []) => mk_identity rty
    4.37 -    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
    4.38 -    | _ => raise LIFT_MATCH "mk_mapfun (default)"
    4.39 -in
    4.40 -  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
    4.41 -end
    4.42 +    fun mk_mapfun_aux rty =
    4.43 +      case rty of
    4.44 +        TVar _ => mk_Free rty
    4.45 +      | Type (_, []) => mk_identity rty
    4.46 +      | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
    4.47 +      | _ => raise LIFT_MATCH "mk_mapfun (default)"
    4.48 +  in
    4.49 +    fold_rev Term.lambda vs' (mk_mapfun_aux rty)
    4.50 +  end
    4.51  
    4.52  (* looks up the (varified) rty and qty for
    4.53     a quotient definition
    4.54  *)
    4.55  fun get_rty_qty ctxt s =
    4.56 -let
    4.57 -  val thy = ProofContext.theory_of ctxt
    4.58 -  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
    4.59 -    raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    4.60 -in
    4.61 -  (#rtyp qdata, #qtyp qdata)
    4.62 -end
    4.63 +  let
    4.64 +    val thy = ProofContext.theory_of ctxt
    4.65 +    val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
    4.66 +      raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
    4.67 +  in
    4.68 +    (#rtyp qdata, #qtyp qdata)
    4.69 +  end
    4.70  
    4.71  (* takes two type-environments and looks
    4.72     up in both of them the variable v, which
    4.73     must be listed in the environment
    4.74  *)
    4.75  fun double_lookup rtyenv qtyenv v =
    4.76 -let
    4.77 -  val v' = fst (dest_TVar v)
    4.78 -in
    4.79 -  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
    4.80 -end
    4.81 +  let
    4.82 +    val v' = fst (dest_TVar v)
    4.83 +  in
    4.84 +    (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
    4.85 +  end
    4.86  
    4.87  (* matches a type pattern with a type *)
    4.88  fun match ctxt err ty_pat ty =
    4.89 -let
    4.90 -  val thy = ProofContext.theory_of ctxt
    4.91 -in
    4.92 -  Sign.typ_match thy (ty_pat, ty) Vartab.empty
    4.93 -  handle Type.TYPE_MATCH => err ctxt ty_pat ty
    4.94 -end
    4.95 +  let
    4.96 +    val thy = ProofContext.theory_of ctxt
    4.97 +  in
    4.98 +    Sign.typ_match thy (ty_pat, ty) Vartab.empty
    4.99 +      handle Type.TYPE_MATCH => err ctxt ty_pat ty
   4.100 +  end
   4.101  
   4.102  (* produces the rep or abs constant for a qty *)
   4.103  fun absrep_const flag ctxt qty_str =
   4.104 -let
   4.105 -  val qty_name = Long_Name.base_name qty_str
   4.106 -  val qualifier = Long_Name.qualifier qty_str
   4.107 -in
   4.108 -  case flag of
   4.109 -    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
   4.110 -  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
   4.111 -end
   4.112 +  let
   4.113 +    val qty_name = Long_Name.base_name qty_str
   4.114 +    val qualifier = Long_Name.qualifier qty_str
   4.115 +  in
   4.116 +    case flag of
   4.117 +      AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
   4.118 +    | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
   4.119 +  end
   4.120  
   4.121  (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
   4.122  fun absrep_const_chk flag ctxt qty_str =
   4.123    Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
   4.124  
   4.125  fun absrep_match_err ctxt ty_pat ty =
   4.126 -let
   4.127 -  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   4.128 -  val ty_str = Syntax.string_of_typ ctxt ty
   4.129 -in
   4.130 -  raise LIFT_MATCH (space_implode " "
   4.131 -    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   4.132 -end
   4.133 +  let
   4.134 +    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   4.135 +    val ty_str = Syntax.string_of_typ ctxt ty
   4.136 +  in
   4.137 +    raise LIFT_MATCH (space_implode " "
   4.138 +      ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   4.139 +  end
   4.140  
   4.141  
   4.142  (** generation of an aggregate absrep function **)
   4.143 @@ -213,29 +213,29 @@
   4.144      | (Type (s, tys), Type (s', tys')) =>
   4.145          if s = s'
   4.146          then
   4.147 -           let
   4.148 -             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
   4.149 -           in
   4.150 -             list_comb (get_mapfun ctxt s, args)
   4.151 -           end
   4.152 +          let
   4.153 +            val args = map (absrep_fun flag ctxt) (tys ~~ tys')
   4.154 +          in
   4.155 +            list_comb (get_mapfun ctxt s, args)
   4.156 +          end
   4.157          else
   4.158 -           let
   4.159 -             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   4.160 -             val rtyenv = match ctxt absrep_match_err rty_pat rty
   4.161 -             val qtyenv = match ctxt absrep_match_err qty_pat qty
   4.162 -             val args_aux = map (double_lookup rtyenv qtyenv) vs
   4.163 -             val args = map (absrep_fun flag ctxt) args_aux
   4.164 -           in
   4.165 -             if forall is_identity args
   4.166 -             then absrep_const flag ctxt s'
   4.167 -             else 
   4.168 -               let
   4.169 -                 val map_fun = mk_mapfun ctxt vs rty_pat
   4.170 -                 val result = list_comb (map_fun, args)
   4.171 -               in
   4.172 -                 mk_fun_compose flag (absrep_const flag ctxt s', result)
   4.173 -               end
   4.174 -           end
   4.175 +          let
   4.176 +            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   4.177 +            val rtyenv = match ctxt absrep_match_err rty_pat rty
   4.178 +            val qtyenv = match ctxt absrep_match_err qty_pat qty
   4.179 +            val args_aux = map (double_lookup rtyenv qtyenv) vs
   4.180 +            val args = map (absrep_fun flag ctxt) args_aux
   4.181 +          in
   4.182 +            if forall is_identity args
   4.183 +            then absrep_const flag ctxt s'
   4.184 +            else
   4.185 +              let
   4.186 +                val map_fun = mk_mapfun ctxt vs rty_pat
   4.187 +                val result = list_comb (map_fun, args)
   4.188 +              in
   4.189 +                mk_fun_compose flag (absrep_const flag ctxt s', result)
   4.190 +              end
   4.191 +          end
   4.192      | (TFree x, TFree x') =>
   4.193          if x = x'
   4.194          then mk_identity rty
   4.195 @@ -259,13 +259,13 @@
   4.196  
   4.197  (* instantiates TVars so that the term is of type ty *)
   4.198  fun force_typ ctxt trm ty =
   4.199 -let
   4.200 -  val thy = ProofContext.theory_of ctxt
   4.201 -  val trm_ty = fastype_of trm
   4.202 -  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   4.203 -in
   4.204 -  map_types (Envir.subst_type ty_inst) trm
   4.205 -end
   4.206 +  let
   4.207 +    val thy = ProofContext.theory_of ctxt
   4.208 +    val trm_ty = fastype_of trm
   4.209 +    val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   4.210 +  in
   4.211 +    map_types (Envir.subst_type ty_inst) trm
   4.212 +  end
   4.213  
   4.214  fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   4.215    | is_eq _ = false
   4.216 @@ -274,44 +274,44 @@
   4.217    Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
   4.218  
   4.219  fun get_relmap ctxt s =
   4.220 -let
   4.221 -  val thy = ProofContext.theory_of ctxt
   4.222 -  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
   4.223 -    raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   4.224 -in
   4.225 -  Const (relmap, dummyT)
   4.226 -end
   4.227 +  let
   4.228 +    val thy = ProofContext.theory_of ctxt
   4.229 +    val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
   4.230 +      raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   4.231 +  in
   4.232 +    Const (relmap, dummyT)
   4.233 +  end
   4.234  
   4.235  fun mk_relmap ctxt vs rty =
   4.236 -let
   4.237 -  val vs' = map (mk_Free) vs
   4.238 +  let
   4.239 +    val vs' = map (mk_Free) vs
   4.240  
   4.241 -  fun mk_relmap_aux rty =
   4.242 -    case rty of
   4.243 -      TVar _ => mk_Free rty
   4.244 -    | Type (_, []) => HOLogic.eq_const rty
   4.245 -    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   4.246 -    | _ => raise LIFT_MATCH ("mk_relmap (default)")
   4.247 -in
   4.248 -  fold_rev Term.lambda vs' (mk_relmap_aux rty)
   4.249 -end
   4.250 +    fun mk_relmap_aux rty =
   4.251 +      case rty of
   4.252 +        TVar _ => mk_Free rty
   4.253 +      | Type (_, []) => HOLogic.eq_const rty
   4.254 +      | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
   4.255 +      | _ => raise LIFT_MATCH ("mk_relmap (default)")
   4.256 +  in
   4.257 +    fold_rev Term.lambda vs' (mk_relmap_aux rty)
   4.258 +  end
   4.259  
   4.260  fun get_equiv_rel ctxt s =
   4.261 -let
   4.262 -  val thy = ProofContext.theory_of ctxt
   4.263 -in
   4.264 -  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
   4.265 -    raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   4.266 -end
   4.267 +  let
   4.268 +    val thy = ProofContext.theory_of ctxt
   4.269 +  in
   4.270 +    #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
   4.271 +      raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   4.272 +  end
   4.273  
   4.274  fun equiv_match_err ctxt ty_pat ty =
   4.275 -let
   4.276 -  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   4.277 -  val ty_str = Syntax.string_of_typ ctxt ty
   4.278 -in
   4.279 -  raise LIFT_MATCH (space_implode " "
   4.280 -    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   4.281 -end
   4.282 +  let
   4.283 +    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   4.284 +    val ty_str = Syntax.string_of_typ ctxt ty
   4.285 +  in
   4.286 +    raise LIFT_MATCH (space_implode " "
   4.287 +      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   4.288 +  end
   4.289  
   4.290  (* builds the aggregate equivalence relation
   4.291     that will be the argument of Respects
   4.292 @@ -322,34 +322,34 @@
   4.293    else
   4.294      case (rty, qty) of
   4.295        (Type (s, tys), Type (s', tys')) =>
   4.296 -       if s = s'
   4.297 -       then
   4.298 -         let
   4.299 -           val args = map (equiv_relation ctxt) (tys ~~ tys')
   4.300 -         in
   4.301 -           list_comb (get_relmap ctxt s, args)
   4.302 -         end
   4.303 -       else
   4.304 -         let
   4.305 -           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   4.306 -           val rtyenv = match ctxt equiv_match_err rty_pat rty
   4.307 -           val qtyenv = match ctxt equiv_match_err qty_pat qty
   4.308 -           val args_aux = map (double_lookup rtyenv qtyenv) vs
   4.309 -           val args = map (equiv_relation ctxt) args_aux
   4.310 -           val eqv_rel = get_equiv_rel ctxt s'
   4.311 -           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   4.312 -         in
   4.313 -           if forall is_eq args
   4.314 -           then eqv_rel'
   4.315 -           else 
   4.316 -             let 
   4.317 -               val rel_map = mk_relmap ctxt vs rty_pat
   4.318 -               val result = list_comb (rel_map, args)
   4.319 -             in
   4.320 -               mk_rel_compose (result, eqv_rel')
   4.321 -             end
   4.322 -         end
   4.323 -      | _ => HOLogic.eq_const rty
   4.324 +        if s = s'
   4.325 +        then
   4.326 +          let
   4.327 +            val args = map (equiv_relation ctxt) (tys ~~ tys')
   4.328 +          in
   4.329 +            list_comb (get_relmap ctxt s, args)
   4.330 +          end
   4.331 +        else
   4.332 +          let
   4.333 +            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
   4.334 +            val rtyenv = match ctxt equiv_match_err rty_pat rty
   4.335 +            val qtyenv = match ctxt equiv_match_err qty_pat qty
   4.336 +            val args_aux = map (double_lookup rtyenv qtyenv) vs
   4.337 +            val args = map (equiv_relation ctxt) args_aux
   4.338 +            val eqv_rel = get_equiv_rel ctxt s'
   4.339 +            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
   4.340 +          in
   4.341 +            if forall is_eq args
   4.342 +            then eqv_rel'
   4.343 +            else
   4.344 +              let
   4.345 +                val rel_map = mk_relmap ctxt vs rty_pat
   4.346 +                val result = list_comb (rel_map, args)
   4.347 +              in
   4.348 +                mk_rel_compose (result, eqv_rel')
   4.349 +              end
   4.350 +          end
   4.351 +    | _ => HOLogic.eq_const rty
   4.352  
   4.353  fun equiv_relation_chk ctxt (rty, qty) =
   4.354    equiv_relation ctxt (rty, qty)
   4.355 @@ -414,14 +414,14 @@
   4.356    | _ => f (trm1, trm2)
   4.357  
   4.358  fun term_mismatch str ctxt t1 t2 =
   4.359 -let
   4.360 -  val t1_str = Syntax.string_of_term ctxt t1
   4.361 -  val t2_str = Syntax.string_of_term ctxt t2
   4.362 -  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   4.363 -  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   4.364 -in
   4.365 -  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   4.366 -end
   4.367 +  let
   4.368 +    val t1_str = Syntax.string_of_term ctxt t1
   4.369 +    val t2_str = Syntax.string_of_term ctxt t2
   4.370 +    val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
   4.371 +    val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
   4.372 +  in
   4.373 +    raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
   4.374 +  end
   4.375  
   4.376  (* the major type of All and Ex quantifiers *)
   4.377  fun qnt_typ ty = domain_type (domain_type ty)
   4.378 @@ -429,17 +429,18 @@
   4.379  (* Checks that two types match, for example:
   4.380       rty -> rty   matches   qty -> qty *)
   4.381  fun matches_typ thy rT qT =
   4.382 -  if rT = qT then true else
   4.383 -  case (rT, qT) of
   4.384 -    (Type (rs, rtys), Type (qs, qtys)) =>
   4.385 -      if rs = qs then
   4.386 -        if length rtys <> length qtys then false else
   4.387 -        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
   4.388 -      else
   4.389 -        (case quotdata_lookup_raw thy qs of
   4.390 -          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   4.391 -        | NONE => false)
   4.392 -  | _ => false
   4.393 +  if rT = qT then true
   4.394 +  else
   4.395 +    (case (rT, qT) of
   4.396 +      (Type (rs, rtys), Type (qs, qtys)) =>
   4.397 +        if rs = qs then
   4.398 +          if length rtys <> length qtys then false
   4.399 +          else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
   4.400 +        else
   4.401 +          (case quotdata_lookup_raw thy qs of
   4.402 +            SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
   4.403 +          | NONE => false)
   4.404 +    | _ => false)
   4.405  
   4.406  
   4.407  (* produces a regularized version of rtrm
   4.408 @@ -452,124 +453,124 @@
   4.409  fun regularize_trm ctxt (rtrm, qtrm) =
   4.410    case (rtrm, qtrm) of
   4.411      (Abs (x, ty, t), Abs (_, ty', t')) =>
   4.412 -       let
   4.413 -         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   4.414 -       in
   4.415 -         if ty = ty' then subtrm
   4.416 -         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   4.417 -       end
   4.418 +      let
   4.419 +        val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
   4.420 +      in
   4.421 +        if ty = ty' then subtrm
   4.422 +        else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
   4.423 +      end
   4.424    | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
   4.425 -       let
   4.426 -         val subtrm = regularize_trm ctxt (t, t')
   4.427 -         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   4.428 -       in
   4.429 -         if resrel <> needres
   4.430 -         then term_mismatch "regularize (Babs)" ctxt resrel needres
   4.431 -         else mk_babs $ resrel $ subtrm
   4.432 -       end
   4.433 +      let
   4.434 +        val subtrm = regularize_trm ctxt (t, t')
   4.435 +        val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
   4.436 +      in
   4.437 +        if resrel <> needres
   4.438 +        then term_mismatch "regularize (Babs)" ctxt resrel needres
   4.439 +        else mk_babs $ resrel $ subtrm
   4.440 +      end
   4.441  
   4.442    | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
   4.443 -       let
   4.444 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.445 -       in
   4.446 -         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   4.447 -         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.448 -       end
   4.449 +      let
   4.450 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.451 +      in
   4.452 +        if ty = ty' then Const (@{const_name All}, ty) $ subtrm
   4.453 +        else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.454 +      end
   4.455  
   4.456    | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
   4.457 -       let
   4.458 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.459 -       in
   4.460 -         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   4.461 -         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.462 -       end
   4.463 +      let
   4.464 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.465 +      in
   4.466 +        if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
   4.467 +        else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.468 +      end
   4.469  
   4.470    | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
   4.471        (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
   4.472          (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   4.473       Const (@{const_name Ex1}, ty') $ t') =>
   4.474 -       let
   4.475 -         val t_ = incr_boundvars (~1) t
   4.476 -         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   4.477 -         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.478 -       in
   4.479 -         if resrel <> needrel
   4.480 -         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   4.481 -         else mk_bex1_rel $ resrel $ subtrm
   4.482 -       end
   4.483 +      let
   4.484 +        val t_ = incr_boundvars (~1) t
   4.485 +        val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
   4.486 +        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.487 +      in
   4.488 +        if resrel <> needrel
   4.489 +        then term_mismatch "regularize (Bex1)" ctxt resrel needrel
   4.490 +        else mk_bex1_rel $ resrel $ subtrm
   4.491 +      end
   4.492  
   4.493    | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
   4.494 -       let
   4.495 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.496 -       in
   4.497 -         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   4.498 -         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.499 -       end
   4.500 +      let
   4.501 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.502 +      in
   4.503 +        if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
   4.504 +        else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
   4.505 +      end
   4.506  
   4.507    | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   4.508       Const (@{const_name All}, ty') $ t') =>
   4.509 -       let
   4.510 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.511 -         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.512 -       in
   4.513 -         if resrel <> needrel
   4.514 -         then term_mismatch "regularize (Ball)" ctxt resrel needrel
   4.515 -         else mk_ball $ (mk_resp $ resrel) $ subtrm
   4.516 -       end
   4.517 +      let
   4.518 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.519 +        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.520 +      in
   4.521 +        if resrel <> needrel
   4.522 +        then term_mismatch "regularize (Ball)" ctxt resrel needrel
   4.523 +        else mk_ball $ (mk_resp $ resrel) $ subtrm
   4.524 +      end
   4.525  
   4.526    | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
   4.527       Const (@{const_name Ex}, ty') $ t') =>
   4.528 -       let
   4.529 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.530 -         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.531 -       in
   4.532 -         if resrel <> needrel
   4.533 -         then term_mismatch "regularize (Bex)" ctxt resrel needrel
   4.534 -         else mk_bex $ (mk_resp $ resrel) $ subtrm
   4.535 -       end
   4.536 +      let
   4.537 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.538 +        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.539 +      in
   4.540 +        if resrel <> needrel
   4.541 +        then term_mismatch "regularize (Bex)" ctxt resrel needrel
   4.542 +        else mk_bex $ (mk_resp $ resrel) $ subtrm
   4.543 +      end
   4.544  
   4.545    | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
   4.546 -       let
   4.547 -         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.548 -         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.549 -       in
   4.550 -         if resrel <> needrel
   4.551 -         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   4.552 -         else mk_bex1_rel $ resrel $ subtrm
   4.553 -       end
   4.554 +      let
   4.555 +        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
   4.556 +        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
   4.557 +      in
   4.558 +        if resrel <> needrel
   4.559 +        then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
   4.560 +        else mk_bex1_rel $ resrel $ subtrm
   4.561 +      end
   4.562  
   4.563    | (* equalities need to be replaced by appropriate equivalence relations *)
   4.564      (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
   4.565 -         if ty = ty' then rtrm
   4.566 -         else equiv_relation ctxt (domain_type ty, domain_type ty')
   4.567 +        if ty = ty' then rtrm
   4.568 +        else equiv_relation ctxt (domain_type ty, domain_type ty')
   4.569  
   4.570    | (* in this case we just check whether the given equivalence relation is correct *)
   4.571      (rel, Const (@{const_name HOL.eq}, ty')) =>
   4.572 -       let
   4.573 -         val rel_ty = fastype_of rel
   4.574 -         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   4.575 -       in
   4.576 -         if rel' aconv rel then rtrm
   4.577 -         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
   4.578 -       end
   4.579 +      let
   4.580 +        val rel_ty = fastype_of rel
   4.581 +        val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
   4.582 +      in
   4.583 +        if rel' aconv rel then rtrm
   4.584 +        else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
   4.585 +      end
   4.586  
   4.587    | (_, Const _) =>
   4.588 -       let
   4.589 -         val thy = ProofContext.theory_of ctxt
   4.590 -         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
   4.591 -           | same_const _ _ = false
   4.592 -       in
   4.593 -         if same_const rtrm qtrm then rtrm
   4.594 -         else
   4.595 -           let
   4.596 -             val rtrm' = #rconst (qconsts_lookup thy qtrm)
   4.597 -               handle Quotient_Info.NotFound =>
   4.598 +      let
   4.599 +        val thy = ProofContext.theory_of ctxt
   4.600 +        fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
   4.601 +          | same_const _ _ = false
   4.602 +      in
   4.603 +        if same_const rtrm qtrm then rtrm
   4.604 +        else
   4.605 +          let
   4.606 +            val rtrm' = #rconst (qconsts_lookup thy qtrm)
   4.607 +              handle Quotient_Info.NotFound =>
   4.608                  term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
   4.609 -           in
   4.610 -             if Pattern.matches thy (rtrm', rtrm)
   4.611 -             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
   4.612 -           end
   4.613 -       end
   4.614 +          in
   4.615 +            if Pattern.matches thy (rtrm', rtrm)
   4.616 +            then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
   4.617 +          end
   4.618 +      end
   4.619  
   4.620    | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   4.621       ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   4.622 @@ -583,16 +584,16 @@
   4.623         regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
   4.624  
   4.625    | (Bound i, Bound i') =>
   4.626 -       if i = i' then rtrm
   4.627 -       else raise (LIFT_MATCH "regularize (bounds mismatch)")
   4.628 +      if i = i' then rtrm
   4.629 +      else raise (LIFT_MATCH "regularize (bounds mismatch)")
   4.630  
   4.631    | _ =>
   4.632 -       let
   4.633 -         val rtrm_str = Syntax.string_of_term ctxt rtrm
   4.634 -         val qtrm_str = Syntax.string_of_term ctxt qtrm
   4.635 -       in
   4.636 -         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   4.637 -       end
   4.638 +      let
   4.639 +        val rtrm_str = Syntax.string_of_term ctxt rtrm
   4.640 +        val qtrm_str = Syntax.string_of_term ctxt qtrm
   4.641 +      in
   4.642 +        raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
   4.643 +      end
   4.644  
   4.645  fun regularize_trm_chk ctxt (rtrm, qtrm) =
   4.646    regularize_trm ctxt (rtrm, qtrm)
   4.647 @@ -635,12 +636,12 @@
   4.648    absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
   4.649  
   4.650  fun inj_repabs_err ctxt msg rtrm qtrm =
   4.651 -let
   4.652 -  val rtrm_str = Syntax.string_of_term ctxt rtrm
   4.653 -  val qtrm_str = Syntax.string_of_term ctxt qtrm
   4.654 -in
   4.655 -  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   4.656 -end
   4.657 +  let
   4.658 +    val rtrm_str = Syntax.string_of_term ctxt rtrm
   4.659 +    val qtrm_str = Syntax.string_of_term ctxt qtrm
   4.660 +  in
   4.661 +    raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
   4.662 +  end
   4.663  
   4.664  
   4.665  (* bound variables need to be treated properly,
   4.666 @@ -717,8 +718,8 @@
   4.667                  NONE => matches tail
   4.668                | SOME inst => Envir.subst_type inst qty
   4.669        in
   4.670 -        matches ty_subst 
   4.671 -      end 
   4.672 +        matches ty_subst
   4.673 +      end
   4.674    | _ => rty
   4.675  
   4.676  fun subst_trm ctxt ty_subst trm_subst rtrm =
   4.677 @@ -728,7 +729,7 @@
   4.678    | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   4.679    | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   4.680    | Bound i => Bound i
   4.681 -  | Const (a, ty) => 
   4.682 +  | Const (a, ty) =>
   4.683        let
   4.684          val thy = ProofContext.theory_of ctxt
   4.685  
   4.686 @@ -742,43 +743,43 @@
   4.687        end
   4.688  
   4.689  (* generate type and term substitutions out of the
   4.690 -   qtypes involved in a quotient; the direction flag 
   4.691 -   indicates in which direction the substitutions work: 
   4.692 -   
   4.693 +   qtypes involved in a quotient; the direction flag
   4.694 +   indicates in which direction the substitutions work:
   4.695 +
   4.696       true:  quotient -> raw
   4.697       false: raw -> quotient
   4.698  *)
   4.699  fun mk_ty_subst qtys direction ctxt =
   4.700 -let
   4.701 -  val thy = ProofContext.theory_of ctxt  
   4.702 -in
   4.703 -  quotdata_dest ctxt
   4.704 -   |> map (fn x => (#rtyp x, #qtyp x))
   4.705 -   |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
   4.706 -   |> map (if direction then swap else I)
   4.707 -end
   4.708 +  let
   4.709 +    val thy = ProofContext.theory_of ctxt
   4.710 +  in
   4.711 +    quotdata_dest ctxt
   4.712 +    |> map (fn x => (#rtyp x, #qtyp x))
   4.713 +    |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
   4.714 +    |> map (if direction then swap else I)
   4.715 +  end
   4.716  
   4.717  fun mk_trm_subst qtys direction ctxt =
   4.718 -let
   4.719 -  val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
   4.720 -  fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
   4.721 +  let
   4.722 +    val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
   4.723 +    fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
   4.724  
   4.725 -  val const_substs = 
   4.726 -    qconsts_dest ctxt
   4.727 -     |> map (fn x => (#rconst x, #qconst x))
   4.728 -     |> map (if direction then swap else I)
   4.729 +    val const_substs =
   4.730 +      qconsts_dest ctxt
   4.731 +      |> map (fn x => (#rconst x, #qconst x))
   4.732 +      |> map (if direction then swap else I)
   4.733  
   4.734 -  val rel_substs =
   4.735 -    quotdata_dest ctxt
   4.736 -     |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   4.737 -     |> map (if direction then swap else I)
   4.738 -in
   4.739 -  filter proper (const_substs @ rel_substs)
   4.740 -end
   4.741 +    val rel_substs =
   4.742 +      quotdata_dest ctxt
   4.743 +      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
   4.744 +      |> map (if direction then swap else I)
   4.745 +  in
   4.746 +    filter proper (const_substs @ rel_substs)
   4.747 +  end
   4.748  
   4.749  
   4.750  (* derives a qtyp and qtrm out of a rtyp and rtrm,
   4.751 -   respectively 
   4.752 +   respectively
   4.753  *)
   4.754  fun derive_qtyp ctxt qtys rty =
   4.755    subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
   4.756 @@ -787,7 +788,7 @@
   4.757    subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
   4.758  
   4.759  (* derives a rtyp and rtrm out of a qtyp and qtrm,
   4.760 -   respectively 
   4.761 +   respectively
   4.762  *)
   4.763  fun derive_rtyp ctxt qtys qty =
   4.764    subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
     5.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 14:58:15 2011 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 15:35:00 2011 +0100
     5.3 @@ -24,12 +24,12 @@
     5.4  
     5.5  (* wrappers for define, note, Attrib.internal and theorem_i *)
     5.6  fun define (name, mx, rhs) lthy =
     5.7 -let
     5.8 -  val ((rhs, (_ , thm)), lthy') =
     5.9 -     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
    5.10 -in
    5.11 -  ((rhs, thm), lthy')
    5.12 -end
    5.13 +  let
    5.14 +    val ((rhs, (_ , thm)), lthy') =
    5.15 +      Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
    5.16 +  in
    5.17 +    ((rhs, thm), lthy')
    5.18 +  end
    5.19  
    5.20  fun note (name, thm, attrs) lthy =
    5.21    Local_Theory.note ((name, attrs), [thm]) lthy |> snd
    5.22 @@ -38,12 +38,12 @@
    5.23  fun intern_attr at = Attrib.internal (K at)
    5.24  
    5.25  fun theorem after_qed goals ctxt =
    5.26 -let
    5.27 -  val goals' = map (rpair []) goals
    5.28 -  fun after_qed' thms = after_qed (the_single thms)
    5.29 -in
    5.30 -  Proof.theorem NONE after_qed' [goals'] ctxt
    5.31 -end
    5.32 +  let
    5.33 +    val goals' = map (rpair []) goals
    5.34 +    fun after_qed' thms = after_qed (the_single thms)
    5.35 +  in
    5.36 +    Proof.theorem NONE after_qed' [goals'] ctxt
    5.37 +  end
    5.38  
    5.39  
    5.40  
    5.41 @@ -54,178 +54,179 @@
    5.42  
    5.43  (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
    5.44  fun typedef_term rel rty lthy =
    5.45 -let
    5.46 -  val [x, c] =
    5.47 -    [("x", rty), ("c", HOLogic.mk_setT rty)]
    5.48 -    |> Variable.variant_frees lthy [rel]
    5.49 -    |> map Free
    5.50 -in
    5.51 -  lambda c (HOLogic.exists_const rty $
    5.52 -     lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
    5.53 -end
    5.54 +  let
    5.55 +    val [x, c] =
    5.56 +      [("x", rty), ("c", HOLogic.mk_setT rty)]
    5.57 +      |> Variable.variant_frees lthy [rel]
    5.58 +      |> map Free
    5.59 +  in
    5.60 +    lambda c (HOLogic.exists_const rty $
    5.61 +        lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
    5.62 +  end
    5.63  
    5.64  
    5.65  (* makes the new type definitions and proves non-emptyness *)
    5.66  fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
    5.67 -let
    5.68 -  val typedef_tac =
    5.69 -    EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    5.70 -in
    5.71 -(* FIXME: purely local typedef causes at the moment 
    5.72 -   problems with type variables
    5.73 -  
    5.74 -  Typedef.add_typedef false NONE (qty_name, vs, mx) 
    5.75 -    (typedef_term rel rty lthy) NONE typedef_tac lthy
    5.76 -*)
    5.77 -(* FIXME should really use local typedef here *)
    5.78 -   Local_Theory.background_theory_result
    5.79 +  let
    5.80 +    val typedef_tac =
    5.81 +      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    5.82 +  in
    5.83 +  (* FIXME: purely local typedef causes at the moment
    5.84 +     problems with type variables
    5.85 +
    5.86 +    Typedef.add_typedef false NONE (qty_name, vs, mx)
    5.87 +      (typedef_term rel rty lthy) NONE typedef_tac lthy
    5.88 +  *)
    5.89 +  (* FIXME should really use local typedef here *)
    5.90 +    Local_Theory.background_theory_result
    5.91       (Typedef.add_typedef_global false NONE
    5.92         (qty_name, map (rpair dummyS) vs, mx)
    5.93           (typedef_term rel rty lthy)
    5.94             NONE typedef_tac) lthy
    5.95 -end
    5.96 +  end
    5.97  
    5.98  
    5.99  (* tactic to prove the quot_type theorem for the new type *)
   5.100  fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
   5.101 -let
   5.102 -  val rep_thm = #Rep typedef_info RS mem_def1
   5.103 -  val rep_inv = #Rep_inverse typedef_info
   5.104 -  val abs_inv = #Abs_inverse typedef_info
   5.105 -  val rep_inj = #Rep_inject typedef_info
   5.106 -in
   5.107 -  (rtac @{thm quot_type.intro} THEN' RANGE [
   5.108 -    rtac equiv_thm,
   5.109 -    rtac rep_thm,
   5.110 -    rtac rep_inv,
   5.111 -    rtac abs_inv THEN' rtac mem_def2 THEN' atac,
   5.112 -    rtac rep_inj]) 1
   5.113 -end
   5.114 +  let
   5.115 +    val rep_thm = #Rep typedef_info RS mem_def1
   5.116 +    val rep_inv = #Rep_inverse typedef_info
   5.117 +    val abs_inv = #Abs_inverse typedef_info
   5.118 +    val rep_inj = #Rep_inject typedef_info
   5.119 +  in
   5.120 +    (rtac @{thm quot_type.intro} THEN' RANGE [
   5.121 +      rtac equiv_thm,
   5.122 +      rtac rep_thm,
   5.123 +      rtac rep_inv,
   5.124 +      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
   5.125 +      rtac rep_inj]) 1
   5.126 +  end
   5.127  
   5.128  (* proves the quot_type theorem for the new type *)
   5.129  fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
   5.130 -let
   5.131 -  val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
   5.132 -  val goal =
   5.133 -    HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   5.134 -    |> Syntax.check_term lthy
   5.135 -in
   5.136 -  Goal.prove lthy [] [] goal
   5.137 -    (K (typedef_quot_type_tac equiv_thm typedef_info))
   5.138 -end
   5.139 +  let
   5.140 +    val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
   5.141 +    val goal =
   5.142 +      HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   5.143 +      |> Syntax.check_term lthy
   5.144 +  in
   5.145 +    Goal.prove lthy [] [] goal
   5.146 +      (K (typedef_quot_type_tac equiv_thm typedef_info))
   5.147 +  end
   5.148  
   5.149  (* main function for constructing a quotient type *)
   5.150  fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
   5.151 -let
   5.152 -  val part_equiv = 
   5.153 -    if partial 
   5.154 -    then equiv_thm 
   5.155 -    else equiv_thm RS @{thm equivp_implies_part_equivp}
   5.156 +  let
   5.157 +    val part_equiv =
   5.158 +      if partial
   5.159 +      then equiv_thm
   5.160 +      else equiv_thm RS @{thm equivp_implies_part_equivp}
   5.161  
   5.162 -  (* generates the typedef *)
   5.163 -  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
   5.164 +    (* generates the typedef *)
   5.165 +    val ((qty_full_name, typedef_info), lthy1) =
   5.166 +      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
   5.167  
   5.168 -  (* abs and rep functions from the typedef *)
   5.169 -  val Abs_ty = #abs_type (#1 typedef_info)
   5.170 -  val Rep_ty = #rep_type (#1 typedef_info)
   5.171 -  val Abs_name = #Abs_name (#1 typedef_info)
   5.172 -  val Rep_name = #Rep_name (#1 typedef_info)
   5.173 -  val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   5.174 -  val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
   5.175 +    (* abs and rep functions from the typedef *)
   5.176 +    val Abs_ty = #abs_type (#1 typedef_info)
   5.177 +    val Rep_ty = #rep_type (#1 typedef_info)
   5.178 +    val Abs_name = #Abs_name (#1 typedef_info)
   5.179 +    val Rep_name = #Rep_name (#1 typedef_info)
   5.180 +    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   5.181 +    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
   5.182  
   5.183 -  (* more useful abs and rep definitions *)
   5.184 -  val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
   5.185 -  val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
   5.186 -  val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
   5.187 -  val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
   5.188 -  val abs_name = Binding.prefix_name "abs_" qty_name
   5.189 -  val rep_name = Binding.prefix_name "rep_" qty_name
   5.190 +    (* more useful abs and rep definitions *)
   5.191 +    val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
   5.192 +    val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
   5.193 +    val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
   5.194 +    val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
   5.195 +    val abs_name = Binding.prefix_name "abs_" qty_name
   5.196 +    val rep_name = Binding.prefix_name "rep_" qty_name
   5.197  
   5.198 -  val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
   5.199 -  val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
   5.200 +    val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
   5.201 +    val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
   5.202  
   5.203 -  (* quot_type theorem *)
   5.204 -  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
   5.205 +    (* quot_type theorem *)
   5.206 +    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
   5.207  
   5.208 -  (* quotient theorem *)
   5.209 -  val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
   5.210 -  val quotient_thm = 
   5.211 -    (quot_thm RS @{thm quot_type.Quotient})
   5.212 -    |> fold_rule [abs_def, rep_def]
   5.213 +    (* quotient theorem *)
   5.214 +    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
   5.215 +    val quotient_thm =
   5.216 +      (quot_thm RS @{thm quot_type.Quotient})
   5.217 +      |> fold_rule [abs_def, rep_def]
   5.218  
   5.219 -  (* name equivalence theorem *)
   5.220 -  val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
   5.221 +    (* name equivalence theorem *)
   5.222 +    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
   5.223  
   5.224 -  (* storing the quotdata *)
   5.225 -  val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
   5.226 +    (* storing the quotdata *)
   5.227 +    val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
   5.228  
   5.229 -  fun qinfo phi = transform_quotdata phi quotdata
   5.230 +    fun qinfo phi = transform_quotdata phi quotdata
   5.231  
   5.232 -  val lthy4 = lthy3
   5.233 -     |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
   5.234 -     |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
   5.235 -     |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
   5.236 -in
   5.237 -  (quotdata, lthy4)
   5.238 -end
   5.239 +    val lthy4 = lthy3
   5.240 +      |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
   5.241 +      |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
   5.242 +      |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
   5.243 +  in
   5.244 +    (quotdata, lthy4)
   5.245 +  end
   5.246  
   5.247  
   5.248  (* sanity checks for the quotient type specifications *)
   5.249  fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
   5.250 -let
   5.251 -  val rty_tfreesT = map fst (Term.add_tfreesT rty [])
   5.252 -  val rel_tfrees = map fst (Term.add_tfrees rel [])
   5.253 -  val rel_frees = map fst (Term.add_frees rel [])
   5.254 -  val rel_vars = Term.add_vars rel []
   5.255 -  val rel_tvars = Term.add_tvars rel []
   5.256 -  val qty_str = Binding.str_of qty_name ^ ": "
   5.257 +  let
   5.258 +    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
   5.259 +    val rel_tfrees = map fst (Term.add_tfrees rel [])
   5.260 +    val rel_frees = map fst (Term.add_frees rel [])
   5.261 +    val rel_vars = Term.add_vars rel []
   5.262 +    val rel_tvars = Term.add_tvars rel []
   5.263 +    val qty_str = Binding.str_of qty_name ^ ": "
   5.264  
   5.265 -  val illegal_rel_vars =
   5.266 -    if null rel_vars andalso null rel_tvars then []
   5.267 -    else [qty_str ^ "illegal schematic variable(s) in the relation."]
   5.268 +    val illegal_rel_vars =
   5.269 +      if null rel_vars andalso null rel_tvars then []
   5.270 +      else [qty_str ^ "illegal schematic variable(s) in the relation."]
   5.271  
   5.272 -  val dup_vs =
   5.273 -    (case duplicates (op =) vs of
   5.274 -       [] => []
   5.275 -     | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
   5.276 +    val dup_vs =
   5.277 +      (case duplicates (op =) vs of
   5.278 +        [] => []
   5.279 +      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
   5.280  
   5.281 -  val extra_rty_tfrees =
   5.282 -    (case subtract (op =) vs rty_tfreesT of
   5.283 -       [] => []
   5.284 -     | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
   5.285 +    val extra_rty_tfrees =
   5.286 +      (case subtract (op =) vs rty_tfreesT of
   5.287 +        [] => []
   5.288 +      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
   5.289  
   5.290 -  val extra_rel_tfrees =
   5.291 -    (case subtract (op =) vs rel_tfrees of
   5.292 -       [] => []
   5.293 -     | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
   5.294 +    val extra_rel_tfrees =
   5.295 +      (case subtract (op =) vs rel_tfrees of
   5.296 +        [] => []
   5.297 +      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
   5.298  
   5.299 -  val illegal_rel_frees =
   5.300 -    (case rel_frees of
   5.301 -      [] => []
   5.302 -    | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
   5.303 +    val illegal_rel_frees =
   5.304 +      (case rel_frees of
   5.305 +        [] => []
   5.306 +      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
   5.307  
   5.308 -  val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
   5.309 -in
   5.310 -  if null errs then () else error (cat_lines errs)
   5.311 -end
   5.312 +    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
   5.313 +  in
   5.314 +    if null errs then () else error (cat_lines errs)
   5.315 +  end
   5.316  
   5.317  (* check for existence of map functions *)
   5.318  fun map_check ctxt (_, (rty, _, _)) =
   5.319 -let
   5.320 -  val thy = ProofContext.theory_of ctxt
   5.321 +  let
   5.322 +    val thy = ProofContext.theory_of ctxt
   5.323  
   5.324 -  fun map_check_aux rty warns =
   5.325 -    case rty of
   5.326 -      Type (_, []) => warns
   5.327 -    | Type (s, _) => if maps_defined thy s then warns else s::warns
   5.328 -    | _ => warns
   5.329 +    fun map_check_aux rty warns =
   5.330 +      case rty of
   5.331 +        Type (_, []) => warns
   5.332 +      | Type (s, _) => if maps_defined thy s then warns else s::warns
   5.333 +      | _ => warns
   5.334  
   5.335 -  val warns = map_check_aux rty []
   5.336 -in
   5.337 -  if null warns then ()
   5.338 -  else warning ("No map function defined for " ^ commas warns ^
   5.339 -    ". This will cause problems later on.")
   5.340 -end
   5.341 +    val warns = map_check_aux rty []
   5.342 +  in
   5.343 +    if null warns then ()
   5.344 +    else warning ("No map function defined for " ^ commas warns ^
   5.345 +      ". This will cause problems later on.")
   5.346 +  end
   5.347  
   5.348  
   5.349  
   5.350 @@ -246,48 +247,48 @@
   5.351  *)
   5.352  
   5.353  fun quotient_type quot_list lthy =
   5.354 -let
   5.355 -  (* sanity check *)
   5.356 -  val _ = List.app sanity_check quot_list
   5.357 -  val _ = List.app (map_check lthy) quot_list
   5.358 +  let
   5.359 +    (* sanity check *)
   5.360 +    val _ = List.app sanity_check quot_list
   5.361 +    val _ = List.app (map_check lthy) quot_list
   5.362  
   5.363 -  fun mk_goal (rty, rel, partial) =
   5.364 -  let
   5.365 -    val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   5.366 -    val const = 
   5.367 -      if partial then @{const_name part_equivp} else @{const_name equivp}
   5.368 +    fun mk_goal (rty, rel, partial) =
   5.369 +      let
   5.370 +        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   5.371 +        val const =
   5.372 +          if partial then @{const_name part_equivp} else @{const_name equivp}
   5.373 +      in
   5.374 +        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   5.375 +      end
   5.376 +
   5.377 +    val goals = map (mk_goal o snd) quot_list
   5.378 +
   5.379 +    fun after_qed thms lthy =
   5.380 +      fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
   5.381    in
   5.382 -    HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   5.383 +    theorem after_qed goals lthy
   5.384    end
   5.385  
   5.386 -  val goals = map (mk_goal o snd) quot_list
   5.387 -
   5.388 -  fun after_qed thms lthy =
   5.389 -    fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
   5.390 -in
   5.391 -  theorem after_qed goals lthy
   5.392 -end
   5.393 -
   5.394  fun quotient_type_cmd specs lthy =
   5.395 -let
   5.396 -  fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
   5.397    let
   5.398 -    val rty = Syntax.read_typ lthy rty_str
   5.399 -    val lthy1 = Variable.declare_typ rty lthy
   5.400 -    val rel = 
   5.401 -      Syntax.parse_term lthy1 rel_str
   5.402 -      |> Type.constraint (rty --> rty --> @{typ bool}) 
   5.403 -      |> Syntax.check_term lthy1 
   5.404 -    val lthy2 = Variable.declare_term rel lthy1 
   5.405 +    fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
   5.406 +      let
   5.407 +        val rty = Syntax.read_typ lthy rty_str
   5.408 +        val lthy1 = Variable.declare_typ rty lthy
   5.409 +        val rel =
   5.410 +          Syntax.parse_term lthy1 rel_str
   5.411 +          |> Type.constraint (rty --> rty --> @{typ bool})
   5.412 +          |> Syntax.check_term lthy1
   5.413 +        val lthy2 = Variable.declare_term rel lthy1
   5.414 +      in
   5.415 +        (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
   5.416 +      end
   5.417 +
   5.418 +    val (spec', lthy') = fold_map parse_spec specs lthy
   5.419    in
   5.420 -    (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
   5.421 +    quotient_type spec' lthy'
   5.422    end
   5.423  
   5.424 -  val (spec', lthy') = fold_map parse_spec specs lthy
   5.425 -in
   5.426 -  quotient_type spec' lthy'
   5.427 -end
   5.428 -
   5.429  val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   5.430  
   5.431  val quotspec_parser =
   5.432 @@ -299,8 +300,8 @@
   5.433  val _ = Keyword.keyword "/"
   5.434  
   5.435  val _ =
   5.436 -    Outer_Syntax.local_theory_to_proof "quotient_type"
   5.437 -      "quotient type definitions (require equivalence proofs)"
   5.438 -         Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   5.439 +  Outer_Syntax.local_theory_to_proof "quotient_type"
   5.440 +    "quotient type definitions (require equivalence proofs)"
   5.441 +       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   5.442  
   5.443  end; (* structure *)