# HG changeset patch
# User krauss
# Date 1176207061 -7200
# Node ID 25693088396b39390c82002b0bdc0acbee6366d8
# Parent  6aa55c562ae7dfd01eb33c7e8a7ac89988ee1b2a
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.

diff -r 6aa55c562ae7 -r 25693088396b src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/FunDef.thy	Tue Apr 10 14:11:01 2007 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory FunDef
-imports Accessible_Part Datatype Recdef
+imports Accessible_Part 
 uses 
 ("Tools/function_package/sum_tools.ML")
 ("Tools/function_package/fundef_common.ML")
@@ -83,25 +83,6 @@
 
 
 
-section {* Projections *}
-
-inductive2 lpg :: "('a + 'b) \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  "lpg (Inl x) x"
-inductive2 rpg :: "('a + 'b) \<Rightarrow> 'b \<Rightarrow> bool"
-where
-  "rpg (Inr y) y"
-
-definition "lproj x = (THE y. lpg x y)"
-definition "rproj x = (THE y. rpg x y)"
-
-lemma lproj_inl:
-  "lproj (Inl x) = x"
-  by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
-lemma rproj_inr:
-  "rproj (Inr x) = x"
-  by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
-
 use "Tools/function_package/sum_tools.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/fundef_lib.ML"
@@ -115,6 +96,10 @@
 
 setup FundefPackage.setup
 
+lemma let_cong:
+    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
+  by (unfold Let_def) blast
+
 lemmas [fundef_cong] = 
   let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 
diff -r 6aa55c562ae7 -r 25693088396b src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/Recdef.thy	Tue Apr 10 14:11:01 2007 +0200
@@ -6,7 +6,7 @@
 header {* TFL: recursive function definitions *}
 
 theory Recdef
-imports Wellfounded_Relations
+imports Wellfounded_Relations FunDef
 uses
   ("../TFL/casesplit.ML")
   ("../TFL/utils.ML")
@@ -64,11 +64,7 @@
   less_Suc_eq [THEN iffD2]
 
 lemmas [recdef_cong] = 
-  if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
-
-lemma let_cong [recdef_cong]:
-    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
-  by (unfold Let_def) blast
+  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 
 lemmas [recdef_wf] =
   wf_trancl
diff -r 6aa55c562ae7 -r 25693088396b src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/Sum_Type.thy	Tue Apr 10 14:11:01 2007 +0200
@@ -119,6 +119,29 @@
 by (blast dest!: Inr_inject)
 
 
+subsection {* Projections *}
+
+definition 
+  "sum_case f g x =
+  (if (\<exists>!y. x = Inl y) 
+  then f (THE y. x = Inl y) 
+  else g (THE y. x = Inr y))"
+definition "Projl x = sum_case id arbitrary x"
+definition "Projr x = sum_case arbitrary id x"
+
+lemma sum_cases[simp]: 
+  "sum_case f g (Inl x) = f x"
+  "sum_case f g (Inr y) = g y"
+  unfolding sum_case_def
+  by auto
+
+lemma Projl_Inl[simp]: "Projl (Inl x) = x"
+  unfolding Projl_def by simp
+
+lemma Projr_Inr[simp]: "Projr (Inr x) = x"
+  unfolding Projr_def by simp
+
+
 subsection{*The Disjoint Sum of Sets*}
 
 (** Introduction rules for the injections **)
diff -r 6aa55c562ae7 -r 25693088396b src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 14:11:01 2007 +0200
@@ -30,7 +30,7 @@
 open FundefCommon
 
 (* Theory dependencies *)
-val sum_case_rules = thms "Datatype.sum.cases"
+val sum_case_rules = thms "Sum_Type.sum_cases"
 val split_apply = thm "Product_Type.split"
 
 type qgar = string * (string * typ) list * term list * term list * term
@@ -250,7 +250,7 @@
                  (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
                  (fn _ => SIMPSET (unfold_tac all_orig_fdefs)
                           THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps [@{thm "lproj_inl"}, @{thm "rproj_inr"}])) 1)
+                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps [SumTools.projl_inl, SumTools.projr_inr])) 1)
         |> restore_cond 
         |> export
     end
@@ -324,7 +324,7 @@
                         termination,domintros} = result
                                                                                                                
       val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
-                               mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
+                               mk_applied_form lthy cargTs (symmetric f_def))
                            parts
 
       val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
diff -r 6aa55c562ae7 -r 25693088396b src/HOL/Tools/function_package/sum_tools.ML
--- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 11:55:23 2007 +0200
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 14:11:01 2007 +0200
@@ -31,12 +31,12 @@
 
 val inlN = "Sum_Type.Inl"
 val inrN = "Sum_Type.Inr"
-val sumcaseN = "Datatype.sum.sum_case"
+val sumcaseN = "Sum_Type.sum_case"
 
-val projlN = "FunDef.lproj"
-val projrN = "FunDef.rproj"
-val projl_inl = thm "FunDef.lproj_inl"
-val projr_inr = thm "FunDef.rproj_inr"
+val projlN = "Sum_Type.Projl"
+val projrN = "Sum_Type.Projr"
+val projl_inl = thm "Sum_Type.Projl_Inl"
+val projr_inr = thm "Sum_Type.Projr_Inr"
 
 fun mk_sumT LT RT = Type ("+", [LT, RT])
 fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r