src/HOL/Word/Misc_Typedef.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59807 22bc39064290
child 61799 4cf66f21b764
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (* 
     2   Author:     Jeremy Dawson and Gerwin Klein, NICTA
     3 
     4   Consequences of type definition theorems, and of extended type definition.
     5 *)
     6 
     7 section {* Type Definition Theorems *}
     8 
     9 theory Misc_Typedef
    10 imports Main
    11 begin
    12 
    13 section "More lemmas about normal type definitions"
    14 
    15 lemma
    16   tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
    17   tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
    18   tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
    19   by (auto simp: type_definition_def)
    20 
    21 lemma td_nat_int: 
    22   "type_definition int nat (Collect (op <= 0))"
    23   unfolding type_definition_def by auto
    24 
    25 context type_definition
    26 begin
    27 
    28 declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]
    29 
    30 lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
    31   by (simp add: Abs_inject)
    32    
    33 lemma Abs_inverse': 
    34   "r : A ==> Abs r = a ==> Rep a = r"
    35   by (safe elim!: Abs_inverse)
    36 
    37 lemma Rep_comp_inverse: 
    38   "Rep o f = g ==> Abs o g = f"
    39   using Rep_inverse by auto
    40 
    41 lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
    42   by simp
    43 
    44 lemma Rep_inverse': "Rep a = r ==> Abs r = a"
    45   by (safe intro!: Rep_inverse)
    46 
    47 lemma comp_Abs_inverse: 
    48   "f o Abs = g ==> g o Rep = f"
    49   using Rep_inverse by auto
    50 
    51 lemma set_Rep: 
    52   "A = range Rep"
    53 proof (rule set_eqI)
    54   fix x
    55   show "(x \<in> A) = (x \<in> range Rep)"
    56     by (auto dest: Abs_inverse [of x, symmetric])
    57 qed  
    58 
    59 lemma set_Rep_Abs: "A = range (Rep o Abs)"
    60 proof (rule set_eqI)
    61   fix x
    62   show "(x \<in> A) = (x \<in> range (Rep o Abs))"
    63     by (auto dest: Abs_inverse [of x, symmetric])
    64 qed  
    65 
    66 lemma Abs_inj_on: "inj_on Abs A"
    67   unfolding inj_on_def 
    68   by (auto dest: Abs_inject [THEN iffD1])
    69 
    70 lemma image: "Abs ` A = UNIV"
    71   by (auto intro!: image_eqI)
    72 
    73 lemmas td_thm = type_definition_axioms
    74 
    75 lemma fns1: 
    76   "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
    77   by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
    78 
    79 lemmas fns1a = disjI1 [THEN fns1]
    80 lemmas fns1b = disjI2 [THEN fns1]
    81 
    82 lemma fns4:
    83   "Rep o fa o Abs = fr ==> 
    84    Rep o fa = fr o Rep & fa o Abs = Abs o fr"
    85   by auto
    86 
    87 end
    88 
    89 interpretation nat_int: type_definition int nat "Collect (op <= 0)"
    90   by (rule td_nat_int)
    91 
    92 declare
    93   nat_int.Rep_cases [cases del]
    94   nat_int.Abs_cases [cases del]
    95   nat_int.Rep_induct [induct del]
    96   nat_int.Abs_induct [induct del]
    97 
    98 
    99 subsection "Extended form of type definition predicate"
   100 
   101 lemma td_conds:
   102   "norm o norm = norm ==> (fr o norm = norm o fr) = 
   103     (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
   104   apply safe
   105     apply (simp_all add: comp_assoc)
   106    apply (simp_all add: o_assoc)
   107   done
   108 
   109 lemma fn_comm_power:
   110   "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" 
   111   apply (rule ext) 
   112   apply (induct n)
   113    apply (auto dest: fun_cong)
   114   done
   115 
   116 lemmas fn_comm_power' =
   117   ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def]
   118 
   119 
   120 locale td_ext = type_definition +
   121   fixes norm
   122   assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
   123 begin
   124 
   125 lemma Abs_norm [simp]: 
   126   "Abs (norm x) = Abs x"
   127   using eq_norm [of x] by (auto elim: Rep_inverse')
   128 
   129 lemma td_th:
   130   "g o Abs = f ==> f (Rep x) = g x"
   131   by (drule comp_Abs_inverse [symmetric]) simp
   132 
   133 lemma eq_norm': "Rep o Abs = norm"
   134   by (auto simp: eq_norm)
   135 
   136 lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
   137   by (auto simp: eq_norm' intro: td_th)
   138 
   139 lemmas td = td_thm
   140 
   141 lemma set_iff_norm: "w : A <-> w = norm w"
   142   by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
   143 
   144 lemma inverse_norm: 
   145   "(Abs n = w) = (Rep w = norm n)"
   146   apply (rule iffI)
   147    apply (clarsimp simp add: eq_norm)
   148   apply (simp add: eq_norm' [symmetric])
   149   done
   150 
   151 lemma norm_eq_iff: 
   152   "(norm x = norm y) = (Abs x = Abs y)"
   153   by (simp add: eq_norm' [symmetric])
   154 
   155 lemma norm_comps: 
   156   "Abs o norm = Abs" 
   157   "norm o Rep = Rep" 
   158   "norm o norm = norm"
   159   by (auto simp: eq_norm' [symmetric] o_def)
   160 
   161 lemmas norm_norm [simp] = norm_comps
   162 
   163 lemma fns5: 
   164   "Rep o fa o Abs = fr ==> 
   165   fr o norm = fr & norm o fr = fr"
   166   by (fold eq_norm') auto
   167 
   168 (* following give conditions for converses to td_fns1
   169   the condition (norm o fr o norm = fr o norm) says that 
   170   fr takes normalised arguments to normalised results,
   171   (norm o fr o norm = norm o fr) says that fr 
   172   takes norm-equivalent arguments to norm-equivalent results,
   173   (fr o norm = fr) says that fr 
   174   takes norm-equivalent arguments to the same result, and 
   175   (norm o fr = fr) says that fr takes any argument to a normalised result 
   176   *)
   177 lemma fns2: 
   178   "Abs o fr o Rep = fa ==> 
   179    (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)"
   180   apply (fold eq_norm')
   181   apply safe
   182    prefer 2
   183    apply (simp add: o_assoc)
   184   apply (rule ext)
   185   apply (drule_tac x="Rep x" in fun_cong)
   186   apply auto
   187   done
   188 
   189 lemma fns3: 
   190   "Abs o fr o Rep = fa ==> 
   191    (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)"
   192   apply (fold eq_norm')
   193   apply safe
   194    prefer 2
   195    apply (simp add: comp_assoc)
   196   apply (rule ext)
   197   apply (drule_tac f="a o b" for a b in fun_cong)
   198   apply simp
   199   done
   200 
   201 lemma fns: 
   202   "fr o norm = norm o fr ==> 
   203     (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)"
   204   apply safe
   205    apply (frule fns1b)
   206    prefer 2 
   207    apply (frule fns1a) 
   208    apply (rule fns3 [THEN iffD1])
   209      prefer 3
   210      apply (rule fns2 [THEN iffD1])
   211        apply (simp_all add: comp_assoc)
   212    apply (simp_all add: o_assoc)
   213   done
   214 
   215 lemma range_norm:
   216   "range (Rep o Abs) = A"
   217   by (simp add: set_Rep_Abs)
   218 
   219 end
   220 
   221 lemmas td_ext_def' =
   222   td_ext_def [unfolded type_definition_def td_ext_axioms_def]
   223 
   224 end
   225