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