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