respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
authorkuncar
Fri Mar 23 14:03:58 2012 +0100 (2012-03-23)
changeset 47091d5cd13aca90b
parent 47090 6b53d954255b
child 47092 fa3538d6004b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Quotient.thy	Fri Mar 23 12:03:59 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Mar 23 14:03:58 2012 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  keywords
     1.5    "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
     1.6    "quotient_type" :: thy_goal and "/" and
     1.7 -  "quotient_definition" :: thy_decl
     1.8 +  "quotient_definition" :: thy_goal
     1.9  uses
    1.10    ("Tools/Quotient/quotient_info.ML")
    1.11    ("Tools/Quotient/quotient_type.ML")
    1.12 @@ -79,6 +79,10 @@
    1.13    shows "((op =) ===> (op =)) = (op =)"
    1.14    by (auto simp add: fun_eq_iff elim: fun_relE)
    1.15  
    1.16 +lemma fun_rel_eq_rel:
    1.17 +  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    1.18 +  by (simp add: fun_rel_def)
    1.19 +
    1.20  subsection {* set map (vimage) and set relation *}
    1.21  
    1.22  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 23 12:03:59 2012 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 23 14:03:58 2012 +0100
     2.3 @@ -6,13 +6,17 @@
     2.4  
     2.5  signature QUOTIENT_DEF =
     2.6  sig
     2.7 +  val add_quotient_def:
     2.8 +    ((binding * mixfix) * Attrib.binding) * (term * term) -> thm ->
     2.9 +    local_theory -> Quotient_Info.quotconsts * local_theory
    2.10 +
    2.11    val quotient_def:
    2.12      (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
    2.13 -    local_theory -> Quotient_Info.quotconsts * local_theory
    2.14 +    local_theory -> Proof.state
    2.15  
    2.16    val quotient_def_cmd:
    2.17      (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    2.18 -    local_theory -> Quotient_Info.quotconsts * local_theory
    2.19 +    local_theory -> Proof.state
    2.20  
    2.21    val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    2.22      Quotient_Info.quotconsts * local_theory
    2.23 @@ -30,6 +34,7 @@
    2.24      - attributes
    2.25      - the new constant as term
    2.26      - the rhs of the definition as term
    2.27 +    - respectfulness theorem for the rhs
    2.28  
    2.29     It stores the qconst_info in the quotconsts data slot.
    2.30  
    2.31 @@ -45,7 +50,77 @@
    2.32        quote str ^ " differs from declaration " ^ name ^ pos)
    2.33    end
    2.34  
    2.35 -fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
    2.36 +fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy =
    2.37 +  let
    2.38 +    val absrep_trm = 
    2.39 +      Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, fastype_of lhs) $ rhs
    2.40 +    val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
    2.41 +    val (_, prop') = Local_Defs.cert_def lthy prop
    2.42 +    val (_, newrhs) = Local_Defs.abs_def prop'
    2.43 +
    2.44 +    val ((trm, (_ , thm)), lthy') =
    2.45 +      Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
    2.46 +
    2.47 +    (* data storage *)
    2.48 +    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    2.49 +    fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
    2.50 +    
    2.51 +    val lthy'' = lthy'
    2.52 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.53 +        (fn phi =>
    2.54 +          (case Quotient_Info.transform_quotconsts phi qconst_data of
    2.55 +            qcinfo as {qconst = Const (c, _), ...} =>
    2.56 +              Quotient_Info.update_quotconsts c qcinfo
    2.57 +          | _ => I))
    2.58 +      |> (snd oo Local_Theory.note) 
    2.59 +        ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
    2.60 +        [rsp_thm])
    2.61 +
    2.62 +  in
    2.63 +    (qconst_data, lthy'')
    2.64 +  end
    2.65 +
    2.66 +fun mk_readable_rsp_thm_eq tm lthy =
    2.67 +  let
    2.68 +    val ctm = cterm_of (Proof_Context.theory_of lthy) tm
    2.69 +    
    2.70 +    fun norm_fun_eq ctm = 
    2.71 +      let
    2.72 +        fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
    2.73 +        fun erase_quants ctm' =
    2.74 +          case (Thm.term_of ctm') of
    2.75 +            Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
    2.76 +            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv 
    2.77 +              Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
    2.78 +      in
    2.79 +        (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
    2.80 +      end
    2.81 +
    2.82 +    fun simp_arrows_conv ctm =
    2.83 +      let
    2.84 +        val unfold_conv = Conv.rewrs_conv 
    2.85 +          [@{thm fun_rel_eq_rel[THEN eq_reflection]}, @{thm fun_rel_def[THEN eq_reflection]}]
    2.86 +        val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
    2.87 +        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    2.88 +      in
    2.89 +        case (Thm.term_of ctm) of
    2.90 +          Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
    2.91 +            (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
    2.92 +          | _ => Conv.all_conv ctm
    2.93 +      end
    2.94 +
    2.95 +    val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
    2.96 +    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    2.97 +    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
    2.98 +    val eq_thm = 
    2.99 +      (simp_conv then_conv univq_prenex_conv then_conv Thm.beta_conversion true) ctm
   2.100 +  in
   2.101 +    Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
   2.102 +  end
   2.103 +
   2.104 +
   2.105 +
   2.106 +fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
   2.107    let
   2.108      val (vars, ctxt) = prep_vars (the_list raw_var) lthy
   2.109      val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
   2.110 @@ -63,27 +138,50 @@
   2.111            if Variable.check_name binding = lhs_str then (binding, mx)
   2.112            else error_msg binding lhs_str
   2.113        | _ => raise Match)
   2.114 -
   2.115 -    val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
   2.116 -    val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
   2.117 -    val (_, prop') = Local_Defs.cert_def lthy prop
   2.118 -    val (_, newrhs) = Local_Defs.abs_def prop'
   2.119 -
   2.120 -    val ((trm, (_ , thm)), lthy') =
   2.121 -      Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
   2.122 +    
   2.123 +    fun try_to_prove_refl thm = 
   2.124 +      let
   2.125 +        val lhs_eq =
   2.126 +          thm
   2.127 +          |> prop_of
   2.128 +          |> Logic.dest_implies
   2.129 +          |> fst
   2.130 +          |> strip_all_body
   2.131 +          |> try HOLogic.dest_Trueprop
   2.132 +      in
   2.133 +        case lhs_eq of
   2.134 +          SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
   2.135 +          | SOME _ => (case body_type (fastype_of lhs) of
   2.136 +            Type (typ_name, _) => ( SOME
   2.137 +              (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) 
   2.138 +                RS @{thm Equiv_Relations.equivp_reflp} RS thm)
   2.139 +              handle _ => NONE)
   2.140 +            | _ => NONE
   2.141 +            )
   2.142 +          | _ => NONE
   2.143 +      end
   2.144  
   2.145 -    (* data storage *)
   2.146 -    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
   2.147 +    val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty)
   2.148 +    val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs))
   2.149 +    val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
   2.150 +    val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
   2.151 +    val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
   2.152 +  
   2.153 +    fun after_qed thm_list lthy = 
   2.154 +      let
   2.155 +        val internal_rsp_thm =
   2.156 +          case thm_list of
   2.157 +            [] => the maybe_proven_rsp_thm
   2.158 +          | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm 
   2.159 +            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
   2.160 +      in
   2.161 +        snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
   2.162 +      end
   2.163  
   2.164 -    val lthy'' = lthy'
   2.165 -      |> Local_Theory.declaration {syntax = false, pervasive = true}
   2.166 -        (fn phi =>
   2.167 -          (case Quotient_Info.transform_quotconsts phi qconst_data of
   2.168 -            qcinfo as {qconst = Const (c, _), ...} =>
   2.169 -              Quotient_Info.update_quotconsts c qcinfo
   2.170 -          | _ => I));
   2.171    in
   2.172 -    (qconst_data, lthy'')
   2.173 +    case maybe_proven_rsp_thm of
   2.174 +      SOME _ => Proof.theorem NONE after_qed [] lthy
   2.175 +      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
   2.176    end
   2.177  
   2.178  fun check_term' cnstr ctxt =
   2.179 @@ -103,16 +201,19 @@
   2.180      val qty = Quotient_Term.derive_qtyp ctxt qtys rty
   2.181      val lhs = Free (qconst_name, qty)
   2.182    in
   2.183 -    quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
   2.184 +    (*quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt*)
   2.185 +    ({qconst = lhs, rconst = lhs, def = @{thm refl}}, ctxt)
   2.186    end
   2.187  
   2.188 -(* command *)
   2.189 +(* parser and command *)
   2.190 +val quotdef_parser =
   2.191 +  Scan.option Parse_Spec.constdecl --
   2.192 +    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
   2.193  
   2.194  val _ =
   2.195 -  Outer_Syntax.local_theory @{command_spec "quotient_definition"}
   2.196 +  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
   2.197      "definition for constants over the quotient type"
   2.198 -    (Scan.option Parse_Spec.constdecl --
   2.199 -      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
   2.200 -      >> (snd oo quotient_def_cmd))
   2.201 +      (quotdef_parser >> quotient_def_cmd)
   2.202 +
   2.203  
   2.204  end; (* structure *)
     3.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 12:03:59 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:03:58 2012 +0100
     3.3 @@ -264,15 +264,17 @@
     3.4  
     3.5  val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
     3.6  
     3.7 +val quotspec_parser =
     3.8 +  Parse.and_list1
     3.9 +    ((Parse.type_args -- Parse.binding) --
    3.10 +      (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
    3.11 +      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    3.12 +        (@{keyword "/"} |-- (partial -- Parse.term))  --
    3.13 +        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
    3.14 +
    3.15  val _ =
    3.16    Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
    3.17      "quotient type definitions (require equivalence proofs)"
    3.18 -    (Parse.and_list1
    3.19 -      ((Parse.type_args -- Parse.binding) --
    3.20 -        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
    3.21 -        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    3.22 -          (@{keyword "/"} |-- (partial -- Parse.term))  --
    3.23 -          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
    3.24 -    >> quotient_type_cmd)
    3.25 +    (quotspec_parser >> quotient_type_cmd)
    3.26  
    3.27  end;