src/HOL/Product_Type.thy
changeset 24699 c6674504103f
parent 24286 7619080e49f0
child 24844 98c006a30218
     1.1 --- a/src/HOL/Product_Type.thy	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -7,10 +7,24 @@
     1.4  header {* Cartesian products *}
     1.5  
     1.6  theory Product_Type
     1.7 -imports Typedef Fun
     1.8 -uses ("Tools/split_rule.ML")
     1.9 +imports Inductive
    1.10 +uses
    1.11 +  ("Tools/split_rule.ML")
    1.12 +  ("Tools/inductive_set_package.ML")
    1.13 +  ("Tools/inductive_realizer.ML")
    1.14 +  ("Tools/datatype_realizer.ML")
    1.15  begin
    1.16  
    1.17 +subsection {* @{typ bool} is a datatype *}
    1.18 +
    1.19 +rep_datatype bool
    1.20 +  distinct True_not_False False_not_True
    1.21 +  induction bool_induct
    1.22 +
    1.23 +declare case_split [cases type: bool]
    1.24 +  -- "prefer plain propositional version"
    1.25 +
    1.26 +
    1.27  subsection {* Unit *}
    1.28  
    1.29  typedef unit = "{True}"
    1.30 @@ -18,9 +32,10 @@
    1.31    show "True : ?unit" ..
    1.32  qed
    1.33  
    1.34 -constdefs
    1.35 +definition
    1.36    Unity :: unit    ("'(')")
    1.37 -  "() == Abs_unit True"
    1.38 +where
    1.39 +  "() = Abs_unit True"
    1.40  
    1.41  lemma unit_eq [noatp]: "u = ()"
    1.42    by (induct u) (simp add: unit_def Unity_def)
    1.43 @@ -32,23 +47,26 @@
    1.44  
    1.45  ML_setup {*
    1.46    val unit_eq_proc =
    1.47 -    let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
    1.48 -      Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"]
    1.49 +    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
    1.50 +      Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
    1.51        (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
    1.52      end;
    1.53  
    1.54    Addsimprocs [unit_eq_proc];
    1.55  *}
    1.56  
    1.57 +lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
    1.58 +  by simp
    1.59 +
    1.60 +rep_datatype unit
    1.61 +  induction unit_induct
    1.62 +
    1.63  lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
    1.64    by simp
    1.65  
    1.66  lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
    1.67    by (rule triv_forall_equality)
    1.68  
    1.69 -lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
    1.70 -  by simp
    1.71 -
    1.72  text {*
    1.73    This rewrite counters the effect of @{text unit_eq_proc} on @{term
    1.74    [source] "%u::unit. f u"}, replacing it by @{term [source]
    1.75 @@ -84,7 +102,6 @@
    1.76  
    1.77  local
    1.78  
    1.79 -
    1.80  subsubsection {* Definitions *}
    1.81  
    1.82  global
    1.83 @@ -343,6 +360,10 @@
    1.84  lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
    1.85    by fast
    1.86  
    1.87 +rep_datatype prod
    1.88 +  inject Pair_eq
    1.89 +  induction prod_induct
    1.90 +
    1.91  lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
    1.92    by fast
    1.93  
    1.94 @@ -765,6 +786,77 @@
    1.95  setup SplitRule.setup
    1.96  
    1.97  
    1.98 +
    1.99 +lemmas prod_caseI = prod.cases [THEN iffD2, standard]
   1.100 +
   1.101 +lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
   1.102 +  by auto
   1.103 +
   1.104 +lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
   1.105 +  by (auto simp: split_tupled_all)
   1.106 +
   1.107 +lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   1.108 +  by (induct p) auto
   1.109 +
   1.110 +lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   1.111 +  by (induct p) auto
   1.112 +
   1.113 +lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
   1.114 +  by (simp add: expand_fun_eq)
   1.115 +
   1.116 +declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
   1.117 +declare prod_caseE' [elim!] prod_caseE [elim!]
   1.118 +
   1.119 +lemma prod_case_split [code post]:
   1.120 +  "prod_case = split"
   1.121 +  by (auto simp add: expand_fun_eq)
   1.122 +
   1.123 +lemmas [code inline] = prod_case_split [symmetric]
   1.124 +
   1.125 +
   1.126 +subsection {* Further cases/induct rules for tuples *}
   1.127 +
   1.128 +lemma prod_cases3 [cases type]:
   1.129 +  obtains (fields) a b c where "y = (a, b, c)"
   1.130 +  by (cases y, case_tac b) blast
   1.131 +
   1.132 +lemma prod_induct3 [case_names fields, induct type]:
   1.133 +    "(!!a b c. P (a, b, c)) ==> P x"
   1.134 +  by (cases x) blast
   1.135 +
   1.136 +lemma prod_cases4 [cases type]:
   1.137 +  obtains (fields) a b c d where "y = (a, b, c, d)"
   1.138 +  by (cases y, case_tac c) blast
   1.139 +
   1.140 +lemma prod_induct4 [case_names fields, induct type]:
   1.141 +    "(!!a b c d. P (a, b, c, d)) ==> P x"
   1.142 +  by (cases x) blast
   1.143 +
   1.144 +lemma prod_cases5 [cases type]:
   1.145 +  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
   1.146 +  by (cases y, case_tac d) blast
   1.147 +
   1.148 +lemma prod_induct5 [case_names fields, induct type]:
   1.149 +    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
   1.150 +  by (cases x) blast
   1.151 +
   1.152 +lemma prod_cases6 [cases type]:
   1.153 +  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
   1.154 +  by (cases y, case_tac e) blast
   1.155 +
   1.156 +lemma prod_induct6 [case_names fields, induct type]:
   1.157 +    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   1.158 +  by (cases x) blast
   1.159 +
   1.160 +lemma prod_cases7 [cases type]:
   1.161 +  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
   1.162 +  by (cases y, case_tac f) blast
   1.163 +
   1.164 +lemma prod_induct7 [case_names fields, induct type]:
   1.165 +    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.166 +  by (cases x) blast
   1.167 +
   1.168 +
   1.169  subsection {* Further lemmas *}
   1.170  
   1.171  lemma
   1.172 @@ -914,6 +1006,9 @@
   1.173  end
   1.174  *}
   1.175  
   1.176 +
   1.177 +subsection {* Legacy bindings *}
   1.178 +
   1.179  ML {*
   1.180  val Collect_split = thm "Collect_split";
   1.181  val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
   1.182 @@ -1011,4 +1106,16 @@
   1.183  val unit_induct = thm "unit_induct";
   1.184  *}
   1.185  
   1.186 +
   1.187 +subsection {* Further inductive packages *}
   1.188 +
   1.189 +use "Tools/inductive_realizer.ML"
   1.190 +setup InductiveRealizer.setup
   1.191 +
   1.192 +use "Tools/inductive_set_package.ML"
   1.193 +setup InductiveSetPackage.setup
   1.194 +
   1.195 +use "Tools/datatype_realizer.ML"
   1.196 +setup DatatypeRealizer.setup
   1.197 +
   1.198  end