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--
```     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
```