Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
authorkrauss
Tue Apr 10 14:11:01 2007 +0200 (2007-04-10)
changeset 2262225693088396b
parent 22621 6aa55c562ae7
child 22623 5fcee5b319a2
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
src/HOL/FunDef.thy
src/HOL/Recdef.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/sum_tools.ML
     1.1 --- a/src/HOL/FunDef.thy	Tue Apr 10 11:55:23 2007 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Tue Apr 10 14:11:01 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  
     1.6  theory FunDef
     1.7 -imports Accessible_Part Datatype Recdef
     1.8 +imports Accessible_Part 
     1.9  uses 
    1.10  ("Tools/function_package/sum_tools.ML")
    1.11  ("Tools/function_package/fundef_common.ML")
    1.12 @@ -83,25 +83,6 @@
    1.13  
    1.14  
    1.15  
    1.16 -section {* Projections *}
    1.17 -
    1.18 -inductive2 lpg :: "('a + 'b) \<Rightarrow> 'a \<Rightarrow> bool"
    1.19 -where
    1.20 -  "lpg (Inl x) x"
    1.21 -inductive2 rpg :: "('a + 'b) \<Rightarrow> 'b \<Rightarrow> bool"
    1.22 -where
    1.23 -  "rpg (Inr y) y"
    1.24 -
    1.25 -definition "lproj x = (THE y. lpg x y)"
    1.26 -definition "rproj x = (THE y. rpg x y)"
    1.27 -
    1.28 -lemma lproj_inl:
    1.29 -  "lproj (Inl x) = x"
    1.30 -  by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
    1.31 -lemma rproj_inr:
    1.32 -  "rproj (Inr x) = x"
    1.33 -  by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
    1.34 -
    1.35  use "Tools/function_package/sum_tools.ML"
    1.36  use "Tools/function_package/fundef_common.ML"
    1.37  use "Tools/function_package/fundef_lib.ML"
    1.38 @@ -115,6 +96,10 @@
    1.39  
    1.40  setup FundefPackage.setup
    1.41  
    1.42 +lemma let_cong:
    1.43 +    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
    1.44 +  by (unfold Let_def) blast
    1.45 +
    1.46  lemmas [fundef_cong] = 
    1.47    let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.48  
     2.1 --- a/src/HOL/Recdef.thy	Tue Apr 10 11:55:23 2007 +0200
     2.2 +++ b/src/HOL/Recdef.thy	Tue Apr 10 14:11:01 2007 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* TFL: recursive function definitions *}
     2.5  
     2.6  theory Recdef
     2.7 -imports Wellfounded_Relations
     2.8 +imports Wellfounded_Relations FunDef
     2.9  uses
    2.10    ("../TFL/casesplit.ML")
    2.11    ("../TFL/utils.ML")
    2.12 @@ -64,11 +64,7 @@
    2.13    less_Suc_eq [THEN iffD2]
    2.14  
    2.15  lemmas [recdef_cong] = 
    2.16 -  if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    2.17 -
    2.18 -lemma let_cong [recdef_cong]:
    2.19 -    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
    2.20 -  by (unfold Let_def) blast
    2.21 +  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    2.22  
    2.23  lemmas [recdef_wf] =
    2.24    wf_trancl
     3.1 --- a/src/HOL/Sum_Type.thy	Tue Apr 10 11:55:23 2007 +0200
     3.2 +++ b/src/HOL/Sum_Type.thy	Tue Apr 10 14:11:01 2007 +0200
     3.3 @@ -119,6 +119,29 @@
     3.4  by (blast dest!: Inr_inject)
     3.5  
     3.6  
     3.7 +subsection {* Projections *}
     3.8 +
     3.9 +definition 
    3.10 +  "sum_case f g x =
    3.11 +  (if (\<exists>!y. x = Inl y) 
    3.12 +  then f (THE y. x = Inl y) 
    3.13 +  else g (THE y. x = Inr y))"
    3.14 +definition "Projl x = sum_case id arbitrary x"
    3.15 +definition "Projr x = sum_case arbitrary id x"
    3.16 +
    3.17 +lemma sum_cases[simp]: 
    3.18 +  "sum_case f g (Inl x) = f x"
    3.19 +  "sum_case f g (Inr y) = g y"
    3.20 +  unfolding sum_case_def
    3.21 +  by auto
    3.22 +
    3.23 +lemma Projl_Inl[simp]: "Projl (Inl x) = x"
    3.24 +  unfolding Projl_def by simp
    3.25 +
    3.26 +lemma Projr_Inr[simp]: "Projr (Inr x) = x"
    3.27 +  unfolding Projr_def by simp
    3.28 +
    3.29 +
    3.30  subsection{*The Disjoint Sum of Sets*}
    3.31  
    3.32  (** Introduction rules for the injections **)
     4.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 11:55:23 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 14:11:01 2007 +0200
     4.3 @@ -30,7 +30,7 @@
     4.4  open FundefCommon
     4.5  
     4.6  (* Theory dependencies *)
     4.7 -val sum_case_rules = thms "Datatype.sum.cases"
     4.8 +val sum_case_rules = thms "Sum_Type.sum_cases"
     4.9  val split_apply = thm "Product_Type.split"
    4.10  
    4.11  type qgar = string * (string * typ) list * term list * term list * term
    4.12 @@ -250,7 +250,7 @@
    4.13                   (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
    4.14                   (fn _ => SIMPSET (unfold_tac all_orig_fdefs)
    4.15                            THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    4.16 -                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps [@{thm "lproj_inl"}, @{thm "rproj_inr"}])) 1)
    4.17 +                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps [SumTools.projl_inl, SumTools.projr_inr])) 1)
    4.18          |> restore_cond 
    4.19          |> export
    4.20      end
    4.21 @@ -324,7 +324,7 @@
    4.22                          termination,domintros} = result
    4.23                                                                                                                 
    4.24        val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
    4.25 -                               mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
    4.26 +                               mk_applied_form lthy cargTs (symmetric f_def))
    4.27                             parts
    4.28  
    4.29        val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
     5.1 --- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 11:55:23 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Apr 10 14:11:01 2007 +0200
     5.3 @@ -31,12 +31,12 @@
     5.4  
     5.5  val inlN = "Sum_Type.Inl"
     5.6  val inrN = "Sum_Type.Inr"
     5.7 -val sumcaseN = "Datatype.sum.sum_case"
     5.8 +val sumcaseN = "Sum_Type.sum_case"
     5.9  
    5.10 -val projlN = "FunDef.lproj"
    5.11 -val projrN = "FunDef.rproj"
    5.12 -val projl_inl = thm "FunDef.lproj_inl"
    5.13 -val projr_inr = thm "FunDef.rproj_inr"
    5.14 +val projlN = "Sum_Type.Projl"
    5.15 +val projrN = "Sum_Type.Projr"
    5.16 +val projl_inl = thm "Sum_Type.Projl_Inl"
    5.17 +val projr_inr = thm "Sum_Type.Projr_Inr"
    5.18  
    5.19  fun mk_sumT LT RT = Type ("+", [LT, RT])
    5.20  fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r