quot_del attribute, it allows us to deregister quotient types
authorkuncar
Mon May 21 16:36:48 2012 +0200 (2012-05-21)
changeset 479518c8a03765de7
parent 47950 9cb132898ac8
child 47952 36a8c477dae8
quot_del attribute, it allows us to deregister quotient types
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon May 21 11:31:52 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon May 21 16:36:48 2012 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  *)
     1.5  
     1.6  fun can_generate_code_cert quot_thm  =
     1.7 -  case Lifting_Term.quot_thm_rel quot_thm of
     1.8 +  case quot_thm_rel quot_thm of
     1.9      Const (@{const_name HOL.eq}, _) => true
    1.10      | Const (@{const_name invariant}, _) $ _  => true
    1.11      | _ => false
    1.12 @@ -136,7 +136,7 @@
    1.13          | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
    1.14      val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
    1.15      val unabs_def = unabs_all_def ctxt unfolded_def
    1.16 -    val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
    1.17 +    val rep = (cterm_of thy o quot_thm_rep) quot_thm
    1.18      val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
    1.19      val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
    1.20      val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
    1.21 @@ -195,8 +195,8 @@
    1.22  
    1.23      val abs_eq_with_assms =
    1.24        let
    1.25 -        val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    1.26 -        val rel = Lifting_Term.quot_thm_rel quot_thm
    1.27 +        val (rty, qty) = quot_thm_rty_qty quot_thm
    1.28 +        val rel = quot_thm_rel quot_thm
    1.29          val ty_args = get_binder_types_by_rel rel (rty, qty)
    1.30          val body_type = get_body_type_by_rel rel (rty, qty)
    1.31          val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
    1.32 @@ -248,7 +248,7 @@
    1.33  fun has_constr ctxt quot_thm =
    1.34    let
    1.35      val thy = Proof_Context.theory_of ctxt
    1.36 -    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
    1.37 +    val abs_fun = quot_thm_abs quot_thm
    1.38    in
    1.39      if is_Const abs_fun then
    1.40        Code.is_constr thy ((fst o dest_Const) abs_fun)
    1.41 @@ -259,7 +259,7 @@
    1.42  fun has_abstr ctxt quot_thm =
    1.43    let
    1.44      val thy = Proof_Context.theory_of ctxt
    1.45 -    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
    1.46 +    val abs_fun = quot_thm_abs quot_thm
    1.47    in
    1.48      if is_Const abs_fun then
    1.49        Code.is_abstr thy ((fst o dest_Const) abs_fun)
    1.50 @@ -304,7 +304,7 @@
    1.51    let
    1.52      val rty = fastype_of rhs
    1.53      val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
    1.54 -    val absrep_trm =  Lifting_Term.quot_thm_abs quot_thm
    1.55 +    val absrep_trm =  quot_thm_abs quot_thm
    1.56      val rty_forced = (domain_type o fastype_of) absrep_trm
    1.57      val forced_rhs = force_rty_type lthy rty_forced rhs
    1.58      val lhs = Free (Binding.print (#1 var), qty)
     2.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon May 21 11:31:52 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon May 21 16:36:48 2012 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4      Quotmaps.map (Symtab.update (relatorT_name, minfo)) ctxt
     2.5    end    
     2.6  
     2.7 -val quotmaps_attribute_setup =
     2.8 +val quot_map_attribute_setup =
     2.9    Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
    2.10      "declaration of the Quotient map theorem"
    2.11  
    2.12 @@ -136,6 +136,22 @@
    2.13  
    2.14  fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
    2.15  
    2.16 +fun delete_quotients quot_thm ctxt =
    2.17 +  let
    2.18 +    val (_, qtyp) = quot_thm_rty_qty quot_thm
    2.19 +    val qty_full_name = (fst o dest_Type) qtyp
    2.20 +    val symtab = Quotients.get ctxt
    2.21 +    val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
    2.22 +  in
    2.23 +    case maybe_stored_quot_thm of
    2.24 +      SOME {quot_thm = stored_quot_thm} => 
    2.25 +        if Thm.eq_thm_prop (stored_quot_thm, quot_thm) then
    2.26 +          Quotients.map (Symtab.delete qty_full_name) ctxt
    2.27 +        else
    2.28 +          ctxt
    2.29 +      | NONE => ctxt
    2.30 +  end
    2.31 +
    2.32  fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
    2.33    map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
    2.34  
    2.35 @@ -153,6 +169,10 @@
    2.36      |> Pretty.writeln
    2.37    end
    2.38  
    2.39 +val quot_del_attribute_setup =
    2.40 +  Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
    2.41 +    "deletes the Quotient theorem"
    2.42 +
    2.43  structure Invariant_Commute = Named_Thms
    2.44  (
    2.45    val name = @{binding invariant_commute}
    2.46 @@ -174,7 +194,8 @@
    2.47  (* theory setup *)
    2.48  
    2.49  val setup =
    2.50 -  quotmaps_attribute_setup
    2.51 +  quot_map_attribute_setup
    2.52 +  #> quot_del_attribute_setup
    2.53    #> Invariant_Commute.setup
    2.54    #> Reflp_Preserve.setup
    2.55  
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 21 11:31:52 2012 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 21 16:36:48 2012 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  
     3.5  fun define_code_constr gen_code quot_thm lthy =
     3.6    let
     3.7 -    val abs = Lifting_Term.quot_thm_abs quot_thm
     3.8 +    val abs = quot_thm_abs quot_thm
     3.9      val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
    3.10    in
    3.11      if gen_code andalso is_Const abs_background then
    3.12 @@ -71,7 +71,7 @@
    3.13  fun quot_thm_sanity_check ctxt quot_thm =
    3.14    let
    3.15      val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
    3.16 -    val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
    3.17 +    val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
    3.18      val rty_tfreesT = Term.add_tfree_namesT rty []
    3.19      val qty_tfreesT = Term.add_tfree_namesT qty []
    3.20      val extra_rty_tfrees =
    3.21 @@ -97,7 +97,7 @@
    3.22  fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
    3.23    let
    3.24      val _ = quot_thm_sanity_check lthy quot_thm
    3.25 -    val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    3.26 +    val (_, qtyp) = quot_thm_rty_qty quot_thm
    3.27      val qty_full_name = (fst o dest_Type) qtyp
    3.28      val quotients = { quot_thm = quot_thm }
    3.29      fun quot_info phi = Lifting_Info.transform_quotients phi quotients
    3.30 @@ -127,7 +127,7 @@
    3.31  fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
    3.32    let
    3.33      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    3.34 -    val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    3.35 +    val (_, qty) = quot_thm_rty_qty quot_thm
    3.36      val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
    3.37      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
    3.38      fun qualify suffix = Binding.qualified true suffix qty_name
    3.39 @@ -183,7 +183,7 @@
    3.40        | _ => 
    3.41          [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
    3.42  
    3.43 -    val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    3.44 +    val (_, qty) = quot_thm_rty_qty quot_thm
    3.45      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
    3.46      fun qualify suffix = Binding.qualified true suffix qty_name
    3.47      val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
     4.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon May 21 11:31:52 2012 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon May 21 16:36:48 2012 +0200
     4.3 @@ -14,11 +14,6 @@
     4.4    val abs_fun: Proof.context -> typ * typ -> term
     4.5  
     4.6    val equiv_relation: Proof.context -> typ * typ -> term
     4.7 -
     4.8 -  val quot_thm_rel: thm -> term
     4.9 -  val quot_thm_abs: thm -> term
    4.10 -  val quot_thm_rep: thm -> term
    4.11 -  val quot_thm_rty_qty: thm -> typ * typ
    4.12  end
    4.13  
    4.14  structure Lifting_Term: LIFTING_TERM =
    4.15 @@ -79,31 +74,6 @@
    4.16  
    4.17  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    4.18  
    4.19 -(*
    4.20 -  quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
    4.21 -    for destructing quotient theorems (Quotient R Abs Rep T).
    4.22 -*)
    4.23 -
    4.24 -fun quot_thm_rel quot_thm =
    4.25 -  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    4.26 -    (rel, _, _, _) => rel
    4.27 -
    4.28 -fun quot_thm_abs quot_thm =
    4.29 -  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    4.30 -    (_, abs, _, _) => abs
    4.31 -
    4.32 -fun quot_thm_rep quot_thm =
    4.33 -  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    4.34 -    (_, _, rep, _) => rep
    4.35 -
    4.36 -fun quot_thm_rty_qty quot_thm =
    4.37 -  let
    4.38 -    val abs = quot_thm_abs quot_thm
    4.39 -    val abs_type = fastype_of abs  
    4.40 -  in
    4.41 -    (domain_type abs_type, range_type abs_type)
    4.42 -  end
    4.43 -
    4.44  fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
    4.45    if provided_rty_name <> rty_of_qty_name then
    4.46      raise QUOT_THM_INTERNAL (Pretty.block 
     5.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Mon May 21 11:31:52 2012 +0200
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Mon May 21 16:36:48 2012 +0200
     5.3 @@ -9,6 +9,11 @@
     5.4    val MRSL: thm list * thm -> thm
     5.5    val Trueprop_conv: conv -> conv
     5.6    val dest_Quotient: term -> term * term * term * term
     5.7 +
     5.8 +  val quot_thm_rel: thm -> term
     5.9 +  val quot_thm_abs: thm -> term
    5.10 +  val quot_thm_rep: thm -> term
    5.11 +  val quot_thm_rty_qty: thm -> typ * typ
    5.12  end;
    5.13  
    5.14  
    5.15 @@ -28,4 +33,29 @@
    5.16        = (rel, abs, rep, cr)
    5.17    | dest_Quotient t = raise TERM ("dest_Quotient", [t])
    5.18  
    5.19 +(*
    5.20 +  quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
    5.21 +    for destructing quotient theorems (Quotient R Abs Rep T).
    5.22 +*)
    5.23 +
    5.24 +fun quot_thm_rel quot_thm =
    5.25 +  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    5.26 +    (rel, _, _, _) => rel
    5.27 +
    5.28 +fun quot_thm_abs quot_thm =
    5.29 +  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    5.30 +    (_, abs, _, _) => abs
    5.31 +
    5.32 +fun quot_thm_rep quot_thm =
    5.33 +  case (dest_Quotient o HOLogic.dest_Trueprop o prop_of) quot_thm of
    5.34 +    (_, _, rep, _) => rep
    5.35 +
    5.36 +fun quot_thm_rty_qty quot_thm =
    5.37 +  let
    5.38 +    val abs = quot_thm_abs quot_thm
    5.39 +    val abs_type = fastype_of abs  
    5.40 +  in
    5.41 +    (domain_type abs_type, range_type abs_type)
    5.42 +  end
    5.43 +
    5.44  end;