author Lars Hupel Thu Oct 13 14:41:45 2016 +0200 (2016-10-13) changeset 64180 676763a9c269 parent 64179 ce205d1f8592 child 64181 4d1d2de432fa
tuned
```     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
```