predicate defs via locales;
authorwenzelm
Wed Jul 24 00:10:52 2002 +0200 (2002-07-24)
changeset 13412666137b488a4
parent 13411 181a293aa37a
child 13413 0b60b9e18a26
predicate defs via locales;
src/HOL/HOL.thy
src/HOL/Record.thy
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Jul 24 00:09:44 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Jul 24 00:10:52 2002 +0200
     1.3 @@ -601,15 +601,17 @@
     1.4  
     1.5  subsubsection {* Monotonicity *}
     1.6  
     1.7 -constdefs
     1.8 -  mono :: "['a::ord => 'b::ord] => bool"
     1.9 -  "mono f == ALL A B. A <= B --> f A <= f B"
    1.10 +locale mono =
    1.11 +  fixes f
    1.12 +  assumes mono: "A <= B ==> f A <= f B"
    1.13  
    1.14 -lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f"
    1.15 -  by (unfold mono_def) rules
    1.16 +lemmas monoI [intro?] = mono.intro [OF mono_axioms.intro]
    1.17 +  and monoD [dest?] = mono.mono
    1.18  
    1.19 -lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B"
    1.20 -  by (unfold mono_def) rules
    1.21 +lemma mono_def: "mono f == ALL A B. A <= B --> f A <= f B"
    1.22 +  -- compatibility
    1.23 +  by (simp only: atomize_eq mono_def mono_axioms_def)
    1.24 +
    1.25  
    1.26  constdefs
    1.27    min :: "['a::ord, 'a] => 'a"
     2.1 --- a/src/HOL/Record.thy	Wed Jul 24 00:09:44 2002 +0200
     2.2 +++ b/src/HOL/Record.thy	Wed Jul 24 00:10:52 2002 +0200
     2.3 @@ -11,118 +11,57 @@
     2.4  
     2.5  subsection {* Abstract product types *}
     2.6  
     2.7 -constdefs
     2.8 -  product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
     2.9 -    ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
    2.10 -  "product_type Rep Abs pair dest1 dest2 ==
    2.11 -    type_definition Rep Abs UNIV \<and>
    2.12 -    pair = (\<lambda>a b. Abs (a, b)) \<and>
    2.13 -    dest1 = (\<lambda>p. fst (Rep p)) \<and>
    2.14 -    dest2 = (\<lambda>p. snd (Rep p))"
    2.15 -
    2.16 -lemma product_typeI:
    2.17 -  "type_definition Rep Abs UNIV ==>
    2.18 -    pair == \<lambda>a b. Abs (a, b) ==>
    2.19 -    dest1 == (\<lambda>p. fst (Rep p)) ==>
    2.20 -    dest2 == (\<lambda>p. snd (Rep p)) ==>
    2.21 -    product_type Rep Abs pair dest1 dest2"
    2.22 -  by (simp add: product_type_def)
    2.23 +locale product_type =
    2.24 +  fixes Rep and Abs and pair and dest1 and dest2
    2.25 +  assumes "typedef": "type_definition Rep Abs UNIV"
    2.26 +    and pair: "pair == (\<lambda>a b. Abs (a, b))"
    2.27 +    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
    2.28 +    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
    2.29  
    2.30 -lemma product_type_typedef:
    2.31 -    "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
    2.32 -  by (unfold product_type_def) blast
    2.33 -
    2.34 -lemma product_type_pair:
    2.35 -    "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
    2.36 -  by (unfold product_type_def) blast
    2.37 +lemmas product_typeI =
    2.38 +  product_type.intro [OF product_type_axioms.intro]
    2.39  
    2.40 -lemma product_type_dest1:
    2.41 -    "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
    2.42 -  by (unfold product_type_def) blast
    2.43 -
    2.44 -lemma product_type_dest2:
    2.45 -    "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
    2.46 -  by (unfold product_type_def) blast
    2.47 -
    2.48 +lemma (in product_type)
    2.49 +    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    2.50 +  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    2.51  
    2.52 -theorem product_type_inject:
    2.53 -  "product_type Rep Abs pair dest1 dest2 ==>
    2.54 -    (pair x y = pair x' y') = (x = x' \<and> y = y')"
    2.55 -proof -
    2.56 -  case rule_context
    2.57 -  show ?thesis
    2.58 -    by (simp add: product_type_pair [OF rule_context]
    2.59 -      Abs_inject [OF product_type_typedef [OF rule_context]])
    2.60 -qed
    2.61 +lemma (in product_type) conv1: "dest1 (pair x y) = x"
    2.62 +  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    2.63  
    2.64 -theorem product_type_conv1:
    2.65 -  "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
    2.66 -proof -
    2.67 -  case rule_context
    2.68 -  show ?thesis
    2.69 -    by (simp add: product_type_pair [OF rule_context]
    2.70 -      product_type_dest1 [OF rule_context]
    2.71 -      Abs_inverse [OF product_type_typedef [OF rule_context]])
    2.72 -qed
    2.73 +lemma (in product_type) conv2: "dest2 (pair x y) = y"
    2.74 +  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    2.75  
    2.76 -theorem product_type_conv2:
    2.77 -  "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
    2.78 -proof -
    2.79 -  case rule_context
    2.80 -  show ?thesis
    2.81 -    by (simp add: product_type_pair [OF rule_context]
    2.82 -      product_type_dest2 [OF rule_context]
    2.83 -      Abs_inverse [OF product_type_typedef [OF rule_context]])
    2.84 -qed
    2.85 -
    2.86 -theorem product_type_induct [induct set: product_type]:
    2.87 -  "product_type Rep Abs pair dest1 dest2 ==>
    2.88 -    (!!x y. P (pair x y)) ==> P p"
    2.89 -proof -
    2.90 -  assume hyp: "!!x y. P (pair x y)"
    2.91 -  assume prod_type: "product_type Rep Abs pair dest1 dest2"
    2.92 -  show "P p"
    2.93 -  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
    2.94 -    fix pair show "P (Abs pair)"
    2.95 -    proof (rule prod_induct)
    2.96 -      fix x y from hyp show "P (Abs (x, y))"
    2.97 -        by (simp only: product_type_pair [OF prod_type])
    2.98 -    qed
    2.99 +lemma (in product_type) induct [induct type]:
   2.100 +  assumes hyp: "!!x y. P (pair x y)"
   2.101 +  shows "P p"
   2.102 +proof (rule type_definition.Abs_induct [OF "typedef"])
   2.103 +  fix q show "P (Abs q)"
   2.104 +  proof (induct q)
   2.105 +    fix x y have "P (pair x y)" by (rule hyp)
   2.106 +    also have "pair x y = Abs (x, y)" by (simp only: pair)
   2.107 +    finally show "P (Abs (x, y))" .
   2.108    qed
   2.109  qed
   2.110  
   2.111 -theorem product_type_cases [cases set: product_type]:
   2.112 -  "product_type Rep Abs pair dest1 dest2 ==>
   2.113 -    (!!x y. p = pair x y ==> C) ==> C"
   2.114 -proof -
   2.115 -  assume prod_type: "product_type Rep Abs pair dest1 dest2"
   2.116 -  assume "!!x y. p = pair x y ==> C"
   2.117 -  with prod_type show C
   2.118 -    by (induct p) (simp only: product_type_inject [OF prod_type], blast)
   2.119 -qed
   2.120 +lemma (in product_type) cases [cases type]:
   2.121 +    "(!!x y. p = pair x y ==> C) ==> C"
   2.122 +  by (induct p) (auto simp add: "inject")
   2.123  
   2.124 -theorem product_type_surjective_pairing:
   2.125 -  "product_type Rep Abs pair dest1 dest2 ==>
   2.126 -    p = pair (dest1 p) (dest2 p)"
   2.127 -proof -
   2.128 -  case rule_context
   2.129 -  thus ?thesis by (induct p)
   2.130 -    (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
   2.131 -qed
   2.132 +lemma (in product_type) surjective_pairing:
   2.133 +    "p = pair (dest1 p) (dest2 p)"
   2.134 +  by (induct p) (simp only: conv1 conv2)
   2.135  
   2.136 -theorem product_type_split_paired_all:
   2.137 -  "product_type Rep Abs pair dest1 dest2 ==>
   2.138 -  (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
   2.139 +lemma (in product_type) split_paired_all:
   2.140 +  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
   2.141  proof
   2.142    fix a b
   2.143    assume "!!x. PROP P x"
   2.144    thus "PROP P (pair a b)" .
   2.145  next
   2.146 -  case rule_context
   2.147    fix x
   2.148    assume "!!a b. PROP P (pair a b)"
   2.149    hence "PROP P (pair (dest1 x) (dest2 x))" .
   2.150 -  thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
   2.151 +  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
   2.152  qed
   2.153  
   2.154  
     3.1 --- a/src/HOL/Typedef.thy	Wed Jul 24 00:09:44 2002 +0200
     3.2 +++ b/src/HOL/Typedef.thy	Wed Jul 24 00:10:52 2002 +0200
     3.3 @@ -8,105 +8,79 @@
     3.4  theory Typedef = Set
     3.5  files ("Tools/typedef_package.ML"):
     3.6  
     3.7 -constdefs
     3.8 -  type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
     3.9 -  "type_definition Rep Abs A ==
    3.10 -    (\<forall>x. Rep x \<in> A) \<and>
    3.11 -    (\<forall>x. Abs (Rep x) = x) \<and>
    3.12 -    (\<forall>y \<in> A. Rep (Abs y) = y)"
    3.13 -  -- {* This will be stated as an axiom for each typedef! *}
    3.14 +locale type_definition =
    3.15 +  fixes Rep and Abs and A
    3.16 +  assumes Rep: "Rep x \<in> A"
    3.17 +    and Rep_inverse: "Abs (Rep x) = x"
    3.18 +    and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
    3.19 +  -- {* This will be axiomatized for each typedef! *}
    3.20  
    3.21 -lemma type_definitionI [intro]:
    3.22 -  "(!!x. Rep x \<in> A) ==>
    3.23 -    (!!x. Abs (Rep x) = x) ==>
    3.24 -    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    3.25 -    type_definition Rep Abs A"
    3.26 -  by (unfold type_definition_def) blast
    3.27 -
    3.28 -theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    3.29 -  by (unfold type_definition_def) blast
    3.30 +lemmas type_definitionI [intro] =
    3.31 +  type_definition.intro [OF type_definition_axioms.intro]
    3.32  
    3.33 -theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    3.34 -  by (unfold type_definition_def) blast
    3.35 -
    3.36 -theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    3.37 -  by (unfold type_definition_def) blast
    3.38 +lemma (in type_definition) Rep_inject:
    3.39 +  "(Rep x = Rep y) = (x = y)"
    3.40 +proof
    3.41 +  assume "Rep x = Rep y"
    3.42 +  hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    3.43 +  also have "Abs (Rep x) = x" by (rule Rep_inverse)
    3.44 +  also have "Abs (Rep y) = y" by (rule Rep_inverse)
    3.45 +  finally show "x = y" .
    3.46 +next
    3.47 +  assume "x = y"
    3.48 +  thus "Rep x = Rep y" by (simp only:)
    3.49 +qed
    3.50  
    3.51 -theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    3.52 -proof -
    3.53 -  assume tydef: "type_definition Rep Abs A"
    3.54 -  show ?thesis
    3.55 -  proof
    3.56 -    assume "Rep x = Rep y"
    3.57 -    hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    3.58 -    thus "x = y" by (simp only: Rep_inverse [OF tydef])
    3.59 -  next
    3.60 -    assume "x = y"
    3.61 -    thus "Rep x = Rep y" by simp
    3.62 -  qed
    3.63 +lemma (in type_definition) Abs_inject:
    3.64 +  assumes x: "x \<in> A" and y: "y \<in> A"
    3.65 +  shows "(Abs x = Abs y) = (x = y)"
    3.66 +proof
    3.67 +  assume "Abs x = Abs y"
    3.68 +  hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    3.69 +  also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
    3.70 +  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    3.71 +  finally show "x = y" .
    3.72 +next
    3.73 +  assume "x = y"
    3.74 +  thus "Abs x = Abs y" by (simp only:)
    3.75  qed
    3.76  
    3.77 -theorem Abs_inject:
    3.78 -  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    3.79 -proof -
    3.80 -  assume tydef: "type_definition Rep Abs A"
    3.81 -  assume x: "x \<in> A" and y: "y \<in> A"
    3.82 -  show ?thesis
    3.83 -  proof
    3.84 -    assume "Abs x = Abs y"
    3.85 -    hence "Rep (Abs x) = Rep (Abs y)" by simp
    3.86 -    moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    3.87 -    moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    3.88 -    ultimately show "x = y" by (simp only:)
    3.89 -  next
    3.90 -    assume "x = y"
    3.91 -    thus "Abs x = Abs y" by simp
    3.92 -  qed
    3.93 +lemma (in type_definition) Rep_cases [cases set]:
    3.94 +  assumes y: "y \<in> A"
    3.95 +    and hyp: "!!x. y = Rep x ==> P"
    3.96 +  shows P
    3.97 +proof (rule hyp)
    3.98 +  from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    3.99 +  thus "y = Rep (Abs y)" ..
   3.100  qed
   3.101  
   3.102 -theorem Rep_cases:
   3.103 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
   3.104 -proof -
   3.105 -  assume tydef: "type_definition Rep Abs A"
   3.106 -  assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
   3.107 -  show P
   3.108 -  proof (rule r)
   3.109 -    from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   3.110 -    thus "y = Rep (Abs y)" ..
   3.111 -  qed
   3.112 +lemma (in type_definition) Abs_cases [cases type]:
   3.113 +  assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
   3.114 +  shows P
   3.115 +proof (rule r)
   3.116 +  have "Abs (Rep x) = x" by (rule Rep_inverse)
   3.117 +  thus "x = Abs (Rep x)" ..
   3.118 +  show "Rep x \<in> A" by (rule Rep)
   3.119  qed
   3.120  
   3.121 -theorem Abs_cases:
   3.122 -  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
   3.123 +lemma (in type_definition) Rep_induct [induct set]:
   3.124 +  assumes y: "y \<in> A"
   3.125 +    and hyp: "!!x. P (Rep x)"
   3.126 +  shows "P y"
   3.127  proof -
   3.128 -  assume tydef: "type_definition Rep Abs A"
   3.129 -  assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
   3.130 -  show P
   3.131 -  proof (rule r)
   3.132 -    have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   3.133 -    thus "x = Abs (Rep x)" ..
   3.134 -    show "Rep x \<in> A" by (rule Rep [OF tydef])
   3.135 -  qed
   3.136 +  have "P (Rep (Abs y))" by (rule hyp)
   3.137 +  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
   3.138 +  finally show "P y" .
   3.139  qed
   3.140  
   3.141 -theorem Rep_induct:
   3.142 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   3.143 +lemma (in type_definition) Abs_induct [induct type]:
   3.144 +  assumes r: "!!y. y \<in> A ==> P (Abs y)"
   3.145 +  shows "P x"
   3.146  proof -
   3.147 -  assume tydef: "type_definition Rep Abs A"
   3.148 -  assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   3.149 -  moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   3.150 -  ultimately show "P y" by (simp only:)
   3.151 -qed
   3.152 -
   3.153 -theorem Abs_induct:
   3.154 -  "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   3.155 -proof -
   3.156 -  assume tydef: "type_definition Rep Abs A"
   3.157 -  assume r: "!!y. y \<in> A ==> P (Abs y)"
   3.158 -  have "Rep x \<in> A" by (rule Rep [OF tydef])
   3.159 +  have "Rep x \<in> A" by (rule Rep)
   3.160    hence "P (Abs (Rep x))" by (rule r)
   3.161 -  moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   3.162 -  ultimately show "P x" by (simp only:)
   3.163 +  also have "Abs (Rep x) = x" by (rule Rep_inverse)
   3.164 +  finally show "P x" .
   3.165  qed
   3.166  
   3.167  use "Tools/typedef_package.ML"