tuned
authorLars Hupel <lars.hupel@mytum.de>
Thu Oct 13 14:41:45 2016 +0200 (2016-10-13)
changeset 64180676763a9c269
parent 64179 ce205d1f8592
child 64181 4d1d2de432fa
tuned
src/HOL/Library/Finite_Map.thy
     1.1 --- a/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:15:34 2016 +0200
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:41:45 2016 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4        then obtain y where "n a = Some y" "A x y"
     1.5          unfolding \<open>m a = _\<close>
     1.6          by cases auto
     1.7 -      thus "\<exists>y \<in> ran n. A x y"
     1.8 +      then show "\<exists>y \<in> ran n. A x y"
     1.9          unfolding ran_def by blast
    1.10      next
    1.11        fix y
    1.12 @@ -49,7 +49,7 @@
    1.13        then obtain x where "m a = Some x" "A x y"
    1.14          unfolding \<open>n a = _\<close>
    1.15          by cases auto
    1.16 -      thus "\<exists>x \<in> ran m. A x y"
    1.17 +      then show "\<exists>x \<in> ran m. A x y"
    1.18          unfolding ran_def by blast
    1.19      qed
    1.20  qed
    1.21 @@ -65,10 +65,10 @@
    1.22      proof -
    1.23        from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
    1.24          unfolding rel_fun_def by auto
    1.25 -      thus ?thesis
    1.26 +      then show ?thesis
    1.27          by cases auto
    1.28      qed
    1.29 -  thus "dom m = dom n"
    1.30 +  then show "dom m = dom n"
    1.31      by auto
    1.32  qed
    1.33  
    1.34 @@ -102,7 +102,7 @@
    1.35    have "dom (map_filter P m) = Set.filter P (dom m)"
    1.36      unfolding map_filter_def Set.filter_def dom_def
    1.37      by auto
    1.38 -  thus ?thesis
    1.39 +  then show ?thesis
    1.40      using assms
    1.41      by (simp add: Set.filter_def)
    1.42  qed
    1.43 @@ -261,7 +261,7 @@
    1.44    have "fmlookup m x = None" if "\<not> P x"
    1.45      using that assms
    1.46      unfolding fmlookup_dom_iff by fastforce
    1.47 -  thus "fmlookup (fmfilter P m) x = fmlookup m x"
    1.48 +  then show "fmlookup (fmfilter P m) x = fmlookup m x"
    1.49      by simp
    1.50  qed
    1.51  
    1.52 @@ -282,7 +282,7 @@
    1.53    have "fmlookup m x = None" if "P x \<noteq> Q x"
    1.54      using that assms
    1.55      unfolding fmlookup_dom_iff by fastforce
    1.56 -  thus "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
    1.57 +  then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
    1.58      by auto
    1.59  qed
    1.60  
    1.61 @@ -292,7 +292,7 @@
    1.62  proof (rule fmfilter_cong)
    1.63    fix x
    1.64    assume "x |\<in>| fmdom m"
    1.65 -  thus "P x = Q x"
    1.66 +  then show "P x = Q x"
    1.67      using assms
    1.68      unfolding fmdom'_alt_def fmember.rep_eq
    1.69      by auto
    1.70 @@ -611,26 +611,36 @@
    1.71        rel: fmrel
    1.72    by auto
    1.73  
    1.74 +text \<open>
    1.75 +  Unfortunately, @{command lift_bnf} doesn't register the definitional theorems. We're doing it
    1.76 +  manually below.
    1.77 +\<close>
    1.78 +
    1.79 +local_setup \<open>fn lthy =>
    1.80 +  let
    1.81 +    val SOME bnf = BNF_Def.bnf_of lthy @{type_name fmap}
    1.82 +  in
    1.83 +    lthy
    1.84 +    |> Local_Theory.note ((@{binding fmmap_def}, []), [BNF_Def.map_def_of_bnf bnf]) |> #2
    1.85 +    |> Local_Theory.note ((@{binding fmran'_def}, []), BNF_Def.set_defs_of_bnf bnf) |> #2
    1.86 +    |> Local_Theory.note ((@{binding fmrel_def}, []), [BNF_Def.rel_def_of_bnf bnf]) |> #2
    1.87 +  end
    1.88 +\<close>
    1.89 +
    1.90  context includes lifting_syntax begin
    1.91  
    1.92  lemma fmmap_transfer[transfer_rule]:
    1.93    "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
    1.94 -apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
    1.95 -apply (rule rel_funI ext)+
    1.96 -apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
    1.97 -done
    1.98 +  unfolding fmmap_def
    1.99 +  by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
   1.100  
   1.101  lemma fmran'_transfer[transfer_rule]:
   1.102    "(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
   1.103 -apply (tactic \<open>Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\<close>)
   1.104 -unfolding fmap.pcr_cr_eq cr_fmap_def
   1.105 -by fastforce
   1.106 +  unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
   1.107  
   1.108  lemma fmrel_transfer[transfer_rule]:
   1.109    "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
   1.110 -apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\<close>)
   1.111 -unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def
   1.112 -  by fastforce
   1.113 +  unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce
   1.114  
   1.115  end
   1.116  
   1.117 @@ -675,7 +685,7 @@
   1.118  proof -
   1.119    from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
   1.120      by auto
   1.121 -  thus thesis
   1.122 +  then show thesis
   1.123      using none some
   1.124      by (cases rule: option.rel_cases) auto
   1.125  qed
   1.126 @@ -711,9 +721,7 @@
   1.127  by simp
   1.128  
   1.129  lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
   1.130 -apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
   1.131 -apply (auto simp: fmap.Abs_fmap_inverse)
   1.132 -done
   1.133 +by transfer' auto
   1.134  
   1.135  lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
   1.136  unfolding fmpred_iff pred_fmap_def fmap.set_map
   1.137 @@ -758,7 +766,7 @@
   1.138    fix m n :: "('a, 'b) fmap"
   1.139    have "fmrel op = m n \<longleftrightarrow> (m = n)"
   1.140      by transfer' (simp add: option.rel_eq rel_fun_eq)
   1.141 -  thus "equal_class.equal m n \<longleftrightarrow> (m = n)"
   1.142 +  then show "equal_class.equal m n \<longleftrightarrow> (m = n)"
   1.143      unfolding equal_fmap_def
   1.144      by (simp add: equal_eq[abs_def])
   1.145  qed