src/HOL/Typedef.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 20426 9ffea7a8b31c child 22846 fb79144af9a3 permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
 wenzelm@11608 ` 1` ```(* Title: HOL/Typedef.thy ``` wenzelm@11608 ` 2` ``` ID: \$Id\$ ``` wenzelm@11608 ` 3` ``` Author: Markus Wenzel, TU Munich ``` wenzelm@11743 ` 4` ```*) ``` wenzelm@11608 ` 5` wenzelm@11979 ` 6` ```header {* HOL type definitions *} ``` wenzelm@11608 ` 7` nipkow@15131 ` 8` ```theory Typedef ``` nipkow@15140 ` 9` ```imports Set ``` haftmann@20426 ` 10` ```uses ``` haftmann@20426 ` 11` ``` ("Tools/typedef_package.ML") ``` haftmann@20426 ` 12` ``` ("Tools/typecopy_package.ML") ``` haftmann@20426 ` 13` ``` ("Tools/typedef_codegen.ML") ``` nipkow@15131 ` 14` ```begin ``` wenzelm@11608 ` 15` wenzelm@13412 ` 16` ```locale type_definition = ``` wenzelm@13412 ` 17` ``` fixes Rep and Abs and A ``` wenzelm@13412 ` 18` ``` assumes Rep: "Rep x \ A" ``` wenzelm@13412 ` 19` ``` and Rep_inverse: "Abs (Rep x) = x" ``` wenzelm@13412 ` 20` ``` and Abs_inverse: "y \ A ==> Rep (Abs y) = y" ``` wenzelm@13412 ` 21` ``` -- {* This will be axiomatized for each typedef! *} ``` wenzelm@11608 ` 22` wenzelm@13412 ` 23` ```lemma (in type_definition) Rep_inject: ``` wenzelm@13412 ` 24` ``` "(Rep x = Rep y) = (x = y)" ``` wenzelm@13412 ` 25` ```proof ``` wenzelm@13412 ` 26` ``` assume "Rep x = Rep y" ``` wenzelm@13412 ` 27` ``` hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) ``` wenzelm@13412 ` 28` ``` also have "Abs (Rep x) = x" by (rule Rep_inverse) ``` wenzelm@13412 ` 29` ``` also have "Abs (Rep y) = y" by (rule Rep_inverse) ``` wenzelm@13412 ` 30` ``` finally show "x = y" . ``` wenzelm@13412 ` 31` ```next ``` wenzelm@13412 ` 32` ``` assume "x = y" ``` wenzelm@13412 ` 33` ``` thus "Rep x = Rep y" by (simp only:) ``` wenzelm@13412 ` 34` ```qed ``` wenzelm@11608 ` 35` wenzelm@13412 ` 36` ```lemma (in type_definition) Abs_inject: ``` wenzelm@13412 ` 37` ``` assumes x: "x \ A" and y: "y \ A" ``` wenzelm@13412 ` 38` ``` shows "(Abs x = Abs y) = (x = y)" ``` wenzelm@13412 ` 39` ```proof ``` wenzelm@13412 ` 40` ``` assume "Abs x = Abs y" ``` wenzelm@13412 ` 41` ``` hence "Rep (Abs x) = Rep (Abs y)" by (simp only:) ``` wenzelm@13412 ` 42` ``` also from x have "Rep (Abs x) = x" by (rule Abs_inverse) ``` wenzelm@13412 ` 43` ``` also from y have "Rep (Abs y) = y" by (rule Abs_inverse) ``` wenzelm@13412 ` 44` ``` finally show "x = y" . ``` wenzelm@13412 ` 45` ```next ``` wenzelm@13412 ` 46` ``` assume "x = y" ``` wenzelm@13412 ` 47` ``` thus "Abs x = Abs y" by (simp only:) ``` wenzelm@11608 ` 48` ```qed ``` wenzelm@11608 ` 49` wenzelm@13412 ` 50` ```lemma (in type_definition) Rep_cases [cases set]: ``` wenzelm@13412 ` 51` ``` assumes y: "y \ A" ``` wenzelm@13412 ` 52` ``` and hyp: "!!x. y = Rep x ==> P" ``` wenzelm@13412 ` 53` ``` shows P ``` wenzelm@13412 ` 54` ```proof (rule hyp) ``` wenzelm@13412 ` 55` ``` from y have "Rep (Abs y) = y" by (rule Abs_inverse) ``` wenzelm@13412 ` 56` ``` thus "y = Rep (Abs y)" .. ``` wenzelm@11608 ` 57` ```qed ``` wenzelm@11608 ` 58` wenzelm@13412 ` 59` ```lemma (in type_definition) Abs_cases [cases type]: ``` wenzelm@13412 ` 60` ``` assumes r: "!!y. x = Abs y ==> y \ A ==> P" ``` wenzelm@13412 ` 61` ``` shows P ``` wenzelm@13412 ` 62` ```proof (rule r) ``` wenzelm@13412 ` 63` ``` have "Abs (Rep x) = x" by (rule Rep_inverse) ``` wenzelm@13412 ` 64` ``` thus "x = Abs (Rep x)" .. ``` wenzelm@13412 ` 65` ``` show "Rep x \ A" by (rule Rep) ``` wenzelm@11608 ` 66` ```qed ``` wenzelm@11608 ` 67` wenzelm@13412 ` 68` ```lemma (in type_definition) Rep_induct [induct set]: ``` wenzelm@13412 ` 69` ``` assumes y: "y \ A" ``` wenzelm@13412 ` 70` ``` and hyp: "!!x. P (Rep x)" ``` wenzelm@13412 ` 71` ``` shows "P y" ``` wenzelm@11608 ` 72` ```proof - ``` wenzelm@13412 ` 73` ``` have "P (Rep (Abs y))" by (rule hyp) ``` wenzelm@13412 ` 74` ``` also from y have "Rep (Abs y) = y" by (rule Abs_inverse) ``` wenzelm@13412 ` 75` ``` finally show "P y" . ``` wenzelm@11608 ` 76` ```qed ``` wenzelm@11608 ` 77` wenzelm@13412 ` 78` ```lemma (in type_definition) Abs_induct [induct type]: ``` wenzelm@13412 ` 79` ``` assumes r: "!!y. y \ A ==> P (Abs y)" ``` wenzelm@13412 ` 80` ``` shows "P x" ``` wenzelm@11608 ` 81` ```proof - ``` wenzelm@13412 ` 82` ``` have "Rep x \ A" by (rule Rep) ``` wenzelm@11608 ` 83` ``` hence "P (Abs (Rep x))" by (rule r) ``` wenzelm@13412 ` 84` ``` also have "Abs (Rep x) = x" by (rule Rep_inverse) ``` wenzelm@13412 ` 85` ``` finally show "P x" . ``` wenzelm@11608 ` 86` ```qed ``` wenzelm@11608 ` 87` wenzelm@11608 ` 88` ```use "Tools/typedef_package.ML" ``` haftmann@20426 ` 89` ```use "Tools/typecopy_package.ML" ``` haftmann@19459 ` 90` ```use "Tools/typedef_codegen.ML" ``` wenzelm@11608 ` 91` haftmann@20426 ` 92` ```setup {* ``` haftmann@20426 ` 93` ``` TypedefPackage.setup ``` haftmann@20426 ` 94` ``` #> TypecopyPackage.setup ``` haftmann@20426 ` 95` ``` #> TypedefCodegen.setup ``` haftmann@20426 ` 96` ```*} ``` berghofe@15260 ` 97` wenzelm@11608 ` 98` ```end ```