datatype_record produces simp theorems; contributed in part by Yu Zhang
authorLars Hupel <lars.hupel@mytum.de>
Sat Jul 28 07:28:18 2018 +0200 (11 months ago)
changeset 686867f8db1c4ebec
parent 68685 4b367da119ed
child 68688 3a58abb11840
datatype_record produces simp theorems; contributed in part by Yu Zhang
src/HOL/Library/datatype_records.ML
src/HOL/ex/Datatype_Record_Examples.thy
     1.1 --- a/src/HOL/Library/datatype_records.ML	Wed Jul 25 22:33:04 2018 +0200
     1.2 +++ b/src/HOL/Library/datatype_records.ML	Sat Jul 28 07:28:18 2018 +0200
     1.3 @@ -7,10 +7,10 @@
     1.4  
     1.5    val mk_update_defs: string -> local_theory -> local_theory
     1.6  
     1.7 -  val bnf_record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
     1.8 +  val record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
     1.9      (binding * typ) list -> local_theory -> local_theory
    1.10  
    1.11 -  val bnf_record_cmd: binding -> ctr_options_cmd ->
    1.12 +  val record_cmd: binding -> ctr_options_cmd ->
    1.13      (binding option * (string * string option)) list -> (binding * string) list -> local_theory ->
    1.14      local_theory
    1.15  
    1.16 @@ -35,21 +35,31 @@
    1.17    val extend = I
    1.18  )
    1.19  
    1.20 +fun mk_eq_dummy (lhs, rhs) =
    1.21 +  Const (@{const_name HOL.eq}, dummyT --> dummyT --> @{typ bool}) $ lhs $ rhs
    1.22 +
    1.23 +val dummify = map_types (K dummyT)
    1.24 +fun repeat_split_tac ctxt thm = REPEAT_ALL_NEW (CHANGED o Splitter.split_tac ctxt [thm])
    1.25 +
    1.26  fun mk_update_defs typ_name lthy =
    1.27    let
    1.28      val short_name = Long_Name.base_name typ_name
    1.29 +    val {ctrs, casex, selss, split, sel_thmss, injects, ...} =
    1.30 +      the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
    1.31 +    val ctr = case ctrs of [ctr] => ctr | _ => error "Datatype_Records.mk_update_defs: expected only single constructor"
    1.32 +    val sels = case selss of [sels] => sels | _ => error "Datatype_Records.mk_update_defs: expected selectors"
    1.33 +    val sels_dummy = map dummify sels
    1.34 +    val ctr_dummy = dummify ctr
    1.35 +    val casex_dummy = dummify casex
    1.36 +    val len = length sels
    1.37  
    1.38 -    val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
    1.39 -    val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
    1.40 -    val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
    1.41 -    val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
    1.42 -    val casex_dummy = Const (fst (dest_Const casex), dummyT)
    1.43 -
    1.44 -    val len = length sels
    1.45 +    val simp_thms = flat sel_thmss @ injects
    1.46  
    1.47      fun mk_name sel =
    1.48        Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
    1.49  
    1.50 +    val thms_binding = (@{binding record_simps}, @{attributes [simp]})
    1.51 +
    1.52      fun mk_t idx =
    1.53        let
    1.54          val body =
    1.55 @@ -59,22 +69,143 @@
    1.56          Abs ("f", dummyT, casex_dummy $ body)
    1.57        end
    1.58  
    1.59 -    fun define name t =
    1.60 -      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}), t)) #> snd
    1.61 +    fun simp_only_tac ctxt =
    1.62 +      REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}) THEN'
    1.63 +        asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp_thms)
    1.64 +
    1.65 +    fun prove ctxt defs ts n =
    1.66 +      let
    1.67 +        val t = nth ts n
    1.68 +
    1.69 +        val sel_dummy = nth sels_dummy n
    1.70 +        val t_dummy = dummify t
    1.71 +        fun tac {context = ctxt, ...} =
    1.72 +          Goal.conjunction_tac 1 THEN
    1.73 +            Local_Defs.unfold_tac ctxt defs THEN
    1.74 +            PARALLEL_ALLGOALS (repeat_split_tac ctxt split THEN' simp_only_tac ctxt)
    1.75 +
    1.76 +        val sel_upd_same_thm =
    1.77 +          let
    1.78 +            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
    1.79 +            val f = Free (f, dummyT)
    1.80 +            val x = Free (x, dummyT)
    1.81 +
    1.82 +            val lhs = sel_dummy $ (t_dummy $ f $ x)
    1.83 +            val rhs = f $ (sel_dummy $ x)
    1.84 +            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
    1.85 +          in
    1.86 +            [Goal.prove_future ctxt' [] [] prop tac]
    1.87 +            |> Variable.export ctxt' ctxt
    1.88 +          end
    1.89 +
    1.90 +        val sel_upd_diff_thms =
    1.91 +          let
    1.92 +            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
    1.93 +            val f = Free (f, dummyT)
    1.94 +            val x = Free (x, dummyT)
    1.95 +
    1.96 +            fun lhs sel = sel $ (t_dummy $ f $ x)
    1.97 +            fun rhs sel = sel $ x
    1.98 +            fun eq sel = (lhs sel, rhs sel)
    1.99 +            fun is_n i = i = n
   1.100 +            val props =
   1.101 +              sels_dummy ~~ (0 upto len - 1)
   1.102 +              |> filter_out (is_n o snd)
   1.103 +              |> map (HOLogic.mk_Trueprop o mk_eq_dummy o eq o fst)
   1.104 +              |> Syntax.check_terms ctxt'
   1.105 +          in
   1.106 +            if length props > 0 then
   1.107 +              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
   1.108 +              |> Variable.export ctxt' ctxt
   1.109 +            else
   1.110 +              []
   1.111 +          end
   1.112 +
   1.113 +        val upd_comp_thm =
   1.114 +          let
   1.115 +            val ([f, g, x], ctxt') = Variable.add_fixes ["f", "g", "x"] ctxt
   1.116 +            val f = Free (f, dummyT)
   1.117 +            val g = Free (g, dummyT)
   1.118 +            val x = Free (x, dummyT)
   1.119  
   1.120 -    val lthy' =
   1.121 -      Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy
   1.122 +            val lhs = t_dummy $ f $ (t_dummy $ g $ x)
   1.123 +            val rhs = t_dummy $ Abs ("a", dummyT, f $ (g $ Bound 0)) $ x
   1.124 +            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
   1.125 +          in
   1.126 +            [Goal.prove_future ctxt' [] [] prop tac]
   1.127 +            |> Variable.export ctxt' ctxt
   1.128 +          end
   1.129 +
   1.130 +        val upd_comm_thms =
   1.131 +          let
   1.132 +            fun prop i ctxt =
   1.133 +              let
   1.134 +                val ([f, g, x], ctxt') = Variable.variant_fixes ["f", "g", "x"] ctxt
   1.135 +                val self = t_dummy $ Free (f, dummyT)
   1.136 +                val other = dummify (nth ts i) $ Free (g, dummyT)
   1.137 +                val lhs = other $ (self $ Free (x, dummyT))
   1.138 +                val rhs = self $ (other $ Free (x, dummyT))
   1.139 +              in
   1.140 +                (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)), ctxt')
   1.141 +              end
   1.142 +            val (props, ctxt') = fold_map prop (0 upto n - 1) ctxt
   1.143 +            val props = Syntax.check_terms ctxt' props
   1.144 +          in
   1.145 +            if length props > 0 then
   1.146 +              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
   1.147 +              |> Variable.export ctxt' ctxt
   1.148 +            else
   1.149 +              []
   1.150 +          end
   1.151 +
   1.152 +        val upd_sel_thm =
   1.153 +          let
   1.154 +            val ([x], ctxt') = Variable.add_fixes ["x"] ctxt
   1.155 +
   1.156 +            val lhs = t_dummy $ Abs("_", dummyT, (sel_dummy $ Free(x, dummyT))) $ Free (x, dummyT)
   1.157 +            val rhs = Free (x, dummyT)
   1.158 +            val prop = Syntax.check_term ctxt (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
   1.159 +          in
   1.160 +            [Goal.prove_future ctxt [] [] prop tac]
   1.161 +            |> Variable.export ctxt' ctxt
   1.162 +          end
   1.163 +      in
   1.164 +        sel_upd_same_thm @ sel_upd_diff_thms @ upd_comp_thm @ upd_comm_thms @ upd_sel_thm
   1.165 +      end
   1.166 +
   1.167 +    fun define name t =
   1.168 +      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t))
   1.169 +      #> apfst (apsnd snd)
   1.170 +
   1.171 +    val (updates, (lthy'', lthy')) =
   1.172 +      lthy
   1.173 +      |> Local_Theory.open_target
   1.174 +      |> snd
   1.175 +      |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name))
   1.176 +      |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
   1.177 +      ||> `Local_Theory.close_target
   1.178 +
   1.179 +    val phi = Proof_Context.export_morphism lthy' lthy''
   1.180 +
   1.181 +    val (update_ts, update_defs) =
   1.182 +      split_list updates
   1.183 +      |>> map (Morphism.term phi)
   1.184 +      ||> map (Morphism.thm phi)
   1.185 +
   1.186 +    val thms = flat (map (prove lthy'' update_defs update_ts) (0 upto len-1))
   1.187  
   1.188      fun insert sel =
   1.189        Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
   1.190    in
   1.191 -    lthy'
   1.192 -    |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
   1.193 +    lthy''
   1.194 +    |> Local_Theory.map_background_naming (Name_Space.mandatory_path short_name)
   1.195 +    |> Local_Theory.note (thms_binding, thms)
   1.196 +    |> snd
   1.197 +    |> Local_Theory.restore_background_naming lthy
   1.198      |> Local_Theory.background_theory (Data.map (fold insert sels))
   1.199 -    |> Local_Theory.restore_background_naming lthy
   1.200    end
   1.201  
   1.202 -fun bnf_record binding opts tyargs args lthy =
   1.203 +fun record binding opts tyargs args lthy =
   1.204    let
   1.205      val constructor =
   1.206        (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)
   1.207 @@ -93,8 +224,8 @@
   1.208      lthy'
   1.209    end
   1.210  
   1.211 -fun bnf_record_cmd binding opts tyargs args lthy =
   1.212 -  bnf_record binding (opts lthy)
   1.213 +fun record_cmd binding opts tyargs args lthy =
   1.214 +  record binding (opts lthy)
   1.215      (map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs)
   1.216      (map (apsnd (Syntax.parse_typ lthy)) args) lthy
   1.217  
   1.218 @@ -172,7 +303,7 @@
   1.219      @{command_keyword datatype_record}
   1.220      "Defines a record based on the BNF/datatype machinery"
   1.221      (parser >> (fn (((ctr_options, tyargs), binding), args) =>
   1.222 -      bnf_record_cmd binding ctr_options tyargs args))
   1.223 +      record_cmd binding ctr_options tyargs args))
   1.224  
   1.225  val setup =
   1.226     (Sign.parse_translation
     2.1 --- a/src/HOL/ex/Datatype_Record_Examples.thy	Wed Jul 25 22:33:04 2018 +0200
     2.2 +++ b/src/HOL/ex/Datatype_Record_Examples.thy	Sat Jul 28 07:28:18 2018 +0200
     2.3 @@ -45,4 +45,23 @@
     2.4  lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}"
     2.5    by simp
     2.6  
     2.7 +text \<open>More tests\<close>
     2.8 +
     2.9 +datatype_record ('a, 'b) test1 =
    2.10 +  field_t11 :: 'a
    2.11 +  field_t12 :: 'b
    2.12 +  field_t13 :: nat
    2.13 +  field_t14 :: int
    2.14 +
    2.15 +thm test1.record_simps
    2.16 +
    2.17 +definition ID where "ID x = x"
    2.18 +lemma ID_cong[cong]: "ID x = ID x" by (rule refl)
    2.19 +
    2.20 +lemma "update_field_t11 f (update_field_t12 g (update_field_t11 h x)) = ID (update_field_t12 g (update_field_t11 (\<lambda>x. f (h x)) x))"
    2.21 +  apply (simp only: test1.record_simps)
    2.22 +  apply (subst ID_def)
    2.23 +  apply (rule refl)
    2.24 +  done
    2.25 +
    2.26  end
    2.27 \ No newline at end of file