src/HOL/Datatype.thy
changeset 33959 2afc55e8ed27
parent 33633 9f7280e0c231
child 33963 977b94b64905
     1.1 --- a/src/HOL/Datatype.thy	Wed Nov 25 09:14:28 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Nov 25 11:16:57 2009 +0100
     1.3 @@ -8,9 +8,15 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Nat Product_Type
     1.8 +imports Product_Type Sum_Type Nat
     1.9 +uses
    1.10 +  ("Tools/Datatype/datatype_rep_proofs.ML")
    1.11 +  ("Tools/inductive_realizer.ML")
    1.12 +  ("Tools/Datatype/datatype_realizer.ML")
    1.13  begin
    1.14  
    1.15 +subsection {* The datatype universe *}
    1.16 +
    1.17  typedef (Node)
    1.18    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.19      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    1.20 @@ -513,75 +519,12 @@
    1.21  hide (open) type node item
    1.22  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.23  
    1.24 -
    1.25 -section {* Datatypes *}
    1.26 -
    1.27 -subsection {* Representing sums *}
    1.28 -
    1.29 -rep_datatype (sum) Inl Inr
    1.30 -proof -
    1.31 -  fix P
    1.32 -  fix s :: "'a + 'b"
    1.33 -  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    1.34 -  then show "P s" by (auto intro: sumE [of s])
    1.35 -qed simp_all
    1.36 -
    1.37 -lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.38 -  by (rule ext) (simp split: sum.split)
    1.39 -
    1.40 -lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.41 -  apply (rule_tac s = s in sumE)
    1.42 -   apply (erule ssubst)
    1.43 -   apply (rule sum.cases(1))
    1.44 -  apply (erule ssubst)
    1.45 -  apply (rule sum.cases(2))
    1.46 -  done
    1.47 -
    1.48 -lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    1.49 -  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    1.50 -  by simp
    1.51 +use "Tools/Datatype/datatype_rep_proofs.ML"
    1.52  
    1.53 -lemma sum_case_inject:
    1.54 -  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    1.55 -proof -
    1.56 -  assume a: "sum_case f1 f2 = sum_case g1 g2"
    1.57 -  assume r: "f1 = g1 ==> f2 = g2 ==> P"
    1.58 -  show P
    1.59 -    apply (rule r)
    1.60 -     apply (rule ext)
    1.61 -     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    1.62 -    apply (rule ext)
    1.63 -    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    1.64 -    done
    1.65 -qed
    1.66 -
    1.67 -constdefs
    1.68 -  Suml :: "('a => 'c) => 'a + 'b => 'c"
    1.69 -  "Suml == (%f. sum_case f undefined)"
    1.70 -
    1.71 -  Sumr :: "('b => 'c) => 'a + 'b => 'c"
    1.72 -  "Sumr == sum_case undefined"
    1.73 +use "Tools/inductive_realizer.ML"
    1.74 +setup InductiveRealizer.setup
    1.75  
    1.76 -lemma [code]:
    1.77 -  "Suml f (Inl x) = f x"
    1.78 -  by (simp add: Suml_def)
    1.79 -
    1.80 -lemma [code]:
    1.81 -  "Sumr f (Inr x) = f x"
    1.82 -  by (simp add: Sumr_def)
    1.83 -
    1.84 -lemma Suml_inject: "Suml f = Suml g ==> f = g"
    1.85 -  by (unfold Suml_def) (erule sum_case_inject)
    1.86 -
    1.87 -lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    1.88 -  by (unfold Sumr_def) (erule sum_case_inject)
    1.89 -
    1.90 -primrec Projl :: "'a + 'b => 'a"
    1.91 -where Projl_Inl: "Projl (Inl x) = x"
    1.92 -
    1.93 -primrec Projr :: "'a + 'b => 'b"
    1.94 -where Projr_Inr: "Projr (Inr x) = x"
    1.95 -
    1.96 -hide (open) const Suml Sumr Projl Projr
    1.97 +use "Tools/Datatype/datatype_realizer.ML"
    1.98 +setup DatatypeRealizer.setup
    1.99  
   1.100  end