author kuncar Fri Mar 23 14:03:58 2012 +0100 (2012-03-23) changeset 47091 d5cd13aca90b 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 file | annotate | diff | revisions src/HOL/Tools/Quotient/quotient_def.ML file | annotate | diff | revisions src/HOL/Tools/Quotient/quotient_type.ML file | annotate | diff | revisions
```     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.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.150 +    val maybe_proven_rsp_thm = try_to_prove_refl 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;
```