transfer package: more flexible handling of equality relations using is_equality predicate
authorhuffman
Wed Oct 24 18:43:25 2012 +0200 (2012-10-24)
changeset 49975faf4afed009f
parent 49974 791157a4179a
child 49976 e1c45d8ec175
transfer package: more flexible handling of equality relations using is_equality predicate
src/HOL/Library/Mapping.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Library/Mapping.thy	Wed Oct 24 17:40:56 2012 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Wed Oct 24 18:43:25 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* An abstract view on maps for code generation. *}
     1.5  
     1.6  theory Mapping
     1.7 -imports Main
     1.8 +imports Main Quotient_Option
     1.9  begin
    1.10  
    1.11  subsection {* Type definition and primitive operations *}
    1.12 @@ -61,10 +61,8 @@
    1.13      | Some v \<Rightarrow> m (k \<mapsto> (f v)))" .
    1.14  
    1.15  lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m
    1.16 -    | Some v \<Rightarrow> update k (f v) m)" 
    1.17 -    apply (cases "lookup m k") 
    1.18 -    apply simp_all 
    1.19 -    by (transfer, simp)+
    1.20 +    | Some v \<Rightarrow> update k (f v) m)"
    1.21 +  by transfer rule
    1.22  
    1.23  definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.24    "map_default k v f m = map_entry k f (default k v m)" 
    1.25 @@ -274,4 +272,4 @@
    1.26  hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
    1.27    replace default map_entry map_default tabulate bulkload map
    1.28  
    1.29 -end
    1.30 \ No newline at end of file
    1.31 +end
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Oct 24 17:40:56 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Oct 24 18:43:25 2012 +0200
     2.3 @@ -316,10 +316,8 @@
     2.4        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
     2.5  
     2.6      fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
     2.7 -    val expand_rel_conv = Trueprop_conv (Conv.fun2_conv(top_rewr_conv (Transfer.get_sym_relator_eq lthy')))
     2.8      val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
     2.9 -        |> Conv.fconv_rule expand_rel_conv
    2.10 -     
    2.11 +
    2.12      val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
    2.13      val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
    2.14  
     3.1 --- a/src/HOL/Tools/transfer.ML	Wed Oct 24 17:40:56 2012 +0200
     3.2 +++ b/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
     3.3 @@ -85,20 +85,6 @@
     3.4  
     3.5  fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
     3.6  
     3.7 -val relator_eq_setup =
     3.8 -  let
     3.9 -    val name = @{binding relator_eq}
    3.10 -    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
    3.11 -    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
    3.12 -    val add = Thm.declaration_attribute add_thm
    3.13 -    val del = Thm.declaration_attribute del_thm
    3.14 -    val text = "declaration of relator equality rule (used by transfer method)"
    3.15 -    val content = Item_Net.content o #relator_eq o Data.get
    3.16 -  in
    3.17 -    Attrib.setup name (Attrib.add_del add del) text
    3.18 -    #> Global_Theory.add_thms_dynamic (name, content)
    3.19 -  end
    3.20 -
    3.21  (** Conversions **)
    3.22  
    3.23  val Rel_rule = Thm.symmetric @{thm Rel_def}
    3.24 @@ -125,22 +111,60 @@
    3.25        else_conv
    3.26        Conv.all_conv) ct
    3.27  
    3.28 -(** Transfer proof method **)
    3.29 +(** Replacing explicit equalities with is_equality premises **)
    3.30 +
    3.31 +fun mk_is_equality t =
    3.32 +  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
    3.33  
    3.34 -fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
    3.35 -  | RelT t = raise TERM ("RelT", [t])
    3.36 +val is_equality_lemma =
    3.37 +  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
    3.38 +    by (unfold is_equality_def, rule, drule meta_spec,
    3.39 +      erule meta_mp, rule refl, simp)}
    3.40  
    3.41 -(* Tactic to correspond a value to itself *)
    3.42 -fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
    3.43 +fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
    3.44    let
    3.45 -    val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
    3.46 -    val cT = ctyp_of (Proof_Context.theory_of ctxt) T
    3.47 -    val rews = get_sym_relator_eq ctxt
    3.48 -    val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
    3.49 -    val thm2 = Raw_Simplifier.rewrite_rule rews thm1
    3.50 +    val thy = Thm.theory_of_thm thm
    3.51 +    val prop = Thm.prop_of thm
    3.52 +    val (t, mk_prop') = dest prop
    3.53 +    val add_eqs = Term.fold_aterms
    3.54 +      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
    3.55 +    val eq_consts = rev (add_eqs t [])
    3.56 +    val eqTs = map (snd o dest_Const) eq_consts
    3.57 +    val used = Term.add_free_names prop []
    3.58 +    val names = map (K "") eqTs |> Name.variant_list used
    3.59 +    val frees = map Free (names ~~ eqTs)
    3.60 +    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
    3.61 +    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
    3.62 +    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
    3.63 +    val cprop = Thm.cterm_of thy prop2
    3.64 +    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
    3.65 +    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
    3.66    in
    3.67 -    rtac thm2 i
    3.68 -  end handle Match => no_tac | TERM _ => no_tac)
    3.69 +    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
    3.70 +  end
    3.71 +    handle TERM _ => thm
    3.72 +
    3.73 +fun abstract_equalities_transfer thm =
    3.74 +  let
    3.75 +    fun dest prop =
    3.76 +      let
    3.77 +        val prems = Logic.strip_imp_prems prop
    3.78 +        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
    3.79 +        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
    3.80 +      in
    3.81 +        (rel, fn rel' =>
    3.82 +          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
    3.83 +      end
    3.84 +  in
    3.85 +    gen_abstract_equalities dest thm
    3.86 +  end
    3.87 +
    3.88 +fun abstract_equalities_relator_eq rel_eq_thm =
    3.89 +  gen_abstract_equalities (fn x => (x, I))
    3.90 +    (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
    3.91 +
    3.92 +
    3.93 +(** Transfer proof method **)
    3.94  
    3.95  val post_simps =
    3.96    @{thms transfer_forall_eq [symmetric]
    3.97 @@ -273,7 +297,7 @@
    3.98           (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
    3.99             THEN_ALL_NEW
   3.100               (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
   3.101 -               ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i,
   3.102 +               ORELSE' end_tac)) (i + 1)) i,
   3.103         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
   3.104         rewrite_goal_tac post_simps i,
   3.105         rtac @{thm _} i]
   3.106 @@ -289,8 +313,7 @@
   3.107        [CONVERSION prep_conv i,
   3.108         rtac @{thm transfer_prover_start} i,
   3.109         (rtac rule1 THEN_ALL_NEW
   3.110 -         REPEAT_ALL_NEW
   3.111 -           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
   3.112 +         REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
   3.113         rtac @{thm refl} i]
   3.114    end)
   3.115  
   3.116 @@ -311,7 +334,7 @@
   3.117  
   3.118  (* Attribute for transfer rules *)
   3.119  
   3.120 -val prep_rule = Conv.fconv_rule prep_conv
   3.121 +val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
   3.122  
   3.123  val transfer_add =
   3.124    Thm.declaration_attribute (add_transfer_thm o prep_rule)
   3.125 @@ -324,6 +347,22 @@
   3.126  
   3.127  (* Theory setup *)
   3.128  
   3.129 +val relator_eq_setup =
   3.130 +  let
   3.131 +    val name = @{binding relator_eq}
   3.132 +    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
   3.133 +      #> add_transfer_thm (abstract_equalities_relator_eq thm)
   3.134 +    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
   3.135 +      #> del_transfer_thm (abstract_equalities_relator_eq thm)
   3.136 +    val add = Thm.declaration_attribute add_thm
   3.137 +    val del = Thm.declaration_attribute del_thm
   3.138 +    val text = "declaration of relator equality rule (used by transfer method)"
   3.139 +    val content = Item_Net.content o #relator_eq o Data.get
   3.140 +  in
   3.141 +    Attrib.setup name (Attrib.add_del add del) text
   3.142 +    #> Global_Theory.add_thms_dynamic (name, content)
   3.143 +  end
   3.144 +
   3.145  val setup =
   3.146    relator_eq_setup
   3.147    #> Attrib.setup @{binding transfer_rule} transfer_attribute
     4.1 --- a/src/HOL/Transfer.thy	Wed Oct 24 17:40:56 2012 +0200
     4.2 +++ b/src/HOL/Transfer.thy	Wed Oct 24 18:43:25 2012 +0200
     4.3 @@ -52,6 +52,11 @@
     4.4  definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
     4.5    where "Rel r \<equiv> r"
     4.6  
     4.7 +text {* Handling of equality relations *}
     4.8 +
     4.9 +definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    4.10 +  where "is_equality R \<longleftrightarrow> R = (op =)"
    4.11 +
    4.12  text {* Handling of meta-logic connectives *}
    4.13  
    4.14  definition transfer_forall where
    4.15 @@ -98,6 +103,8 @@
    4.16  ML_file "Tools/transfer.ML"
    4.17  setup Transfer.setup
    4.18  
    4.19 +declare refl [transfer_rule]
    4.20 +
    4.21  declare fun_rel_eq [relator_eq]
    4.22  
    4.23  hide_const (open) Rel
    4.24 @@ -172,6 +179,9 @@
    4.25  
    4.26  subsection {* Properties of relators *}
    4.27  
    4.28 +lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
    4.29 +  unfolding is_equality_def by simp
    4.30 +
    4.31  lemma right_total_eq [transfer_rule]: "right_total (op =)"
    4.32    unfolding right_total_def by simp
    4.33