Moved sum_case stuff from Sum to Datatype.
authorberghofe
Thu Aug 19 19:00:42 1999 +0200 (1999-08-19)
changeset 7293959e060f4a2f
parent 7292 dff3470c5c62
child 7294 5a50de9141b5
Moved sum_case stuff from Sum to Datatype.
src/HOL/Datatype.ML
src/HOL/Sum.ML
src/HOL/Sum.thy
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype.ML	Thu Aug 19 19:00:42 1999 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(*  Title:      HOL/Datatype.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer
     1.7 +    Copyright   1999  TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +(** sum_case -- the selection operator for sums **)
    1.11 +
    1.12 +(*compatibility*)
    1.13 +val [sum_case_Inl, sum_case_Inr] = sum.cases;
    1.14 +
    1.15 +Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.16 +by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    1.17 +            etac ssubst, rtac sum_case_Inl,
    1.18 +            etac ssubst, rtac sum_case_Inr]);
    1.19 +qed "surjective_sum";
    1.20 +
    1.21 +(*Prevents simplification of f and g: much faster*)
    1.22 +Goal "s=t ==> sum_case f g s = sum_case f g t";
    1.23 +by (etac arg_cong 1);
    1.24 +qed "sum_case_weak_cong";
    1.25 +
    1.26 +val [p1,p2] = Goal
    1.27 +  "[| sum_case f1 f2 = sum_case g1 g2;  \
    1.28 +\     [| f1 = g1; f2 = g2 |] ==> P |] \
    1.29 +\  ==> P";
    1.30 +by (rtac p2 1);
    1.31 +by (rtac ext 1);
    1.32 +by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
    1.33 +by (Asm_full_simp_tac 1);
    1.34 +by (rtac ext 1);
    1.35 +by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
    1.36 +by (Asm_full_simp_tac 1);
    1.37 +qed "sum_case_inject";
     2.1 --- a/src/HOL/Sum.ML	Thu Aug 19 18:36:41 1999 +0200
     2.2 +++ b/src/HOL/Sum.ML	Thu Aug 19 19:00:42 1999 +0200
     2.3 @@ -114,18 +114,6 @@
     2.4  AddSEs [PlusE];
     2.5  
     2.6  
     2.7 -(** sum_case -- the selection operator for sums **)
     2.8 -
     2.9 -Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
    2.10 -by (Blast_tac 1);
    2.11 -qed "sum_case_Inl";
    2.12 -
    2.13 -Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
    2.14 -by (Blast_tac 1);
    2.15 -qed "sum_case_Inr";
    2.16 -
    2.17 -Addsimps [sum_case_Inl, sum_case_Inr];
    2.18 -
    2.19  (** Exhaustion rule for sums -- a degenerate form of induction **)
    2.20  
    2.21  val prems = Goalw [Inl_def,Inr_def]
    2.22 @@ -143,42 +131,6 @@
    2.23  by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
    2.24  qed "sum_induct";
    2.25  
    2.26 -Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    2.27 -by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    2.28 -            etac ssubst, rtac sum_case_Inl,
    2.29 -            etac ssubst, rtac sum_case_Inr]);
    2.30 -qed "surjective_sum";
    2.31 -
    2.32 -Goal "R(basic_sum_case f g s) = \
    2.33 -\             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
    2.34 -by (res_inst_tac [("s","s")] sumE 1);
    2.35 -by Auto_tac;
    2.36 -qed "split_sum_case";
    2.37 -
    2.38 -Goal "P (basic_sum_case f g s) = \
    2.39 -\     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
    2.40 -by (stac split_sum_case 1);
    2.41 -by (Blast_tac 1);
    2.42 -qed "split_sum_case_asm";
    2.43 -
    2.44 -(*Prevents simplification of f and g: much faster*)
    2.45 -Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
    2.46 -by (etac arg_cong 1);
    2.47 -qed "sum_case_weak_cong";
    2.48 -
    2.49 -val [p1,p2] = Goal
    2.50 -  "[| basic_sum_case f1 f2 = basic_sum_case g1 g2;  \
    2.51 -\     [| f1 = g1; f2 = g2 |] ==> P |] \
    2.52 -\  ==> P";
    2.53 -by (rtac p2 1);
    2.54 -by (rtac ext 1);
    2.55 -by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
    2.56 -by (Asm_full_simp_tac 1);
    2.57 -by (rtac ext 1);
    2.58 -by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
    2.59 -by (Asm_full_simp_tac 1);
    2.60 -qed "sum_case_inject";
    2.61 -
    2.62  
    2.63  (** Rules for the Part primitive **)
    2.64  
    2.65 @@ -222,7 +174,6 @@
    2.66  by (Blast_tac 1);
    2.67  qed "Part_Int";
    2.68  
    2.69 -(*For inductive definitions*)
    2.70  Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
    2.71  by (Blast_tac 1);
    2.72  qed "Part_Collect";
     3.1 --- a/src/HOL/Sum.thy	Thu Aug 19 18:36:41 1999 +0200
     3.2 +++ b/src/HOL/Sum.thy	Thu Aug 19 19:00:42 1999 +0200
     3.3 @@ -29,7 +29,6 @@
     3.4  consts
     3.5    Inl            :: "'a => 'a + 'b"
     3.6    Inr            :: "'b => 'a + 'b"
     3.7 -  basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
     3.8  
     3.9    (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
    3.10    Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
    3.11 @@ -40,8 +39,6 @@
    3.12  defs
    3.13    Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
    3.14    Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
    3.15 -  sum_case_def  "basic_sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
    3.16 -                                      & (!y. p=Inr(y) --> z=g(y))"
    3.17  
    3.18    sum_def       "A Plus B == (Inl``A) Un (Inr``B)"
    3.19  
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 18:36:41 1999 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 19:00:42 1999 +0200
     4.3 @@ -47,16 +47,16 @@
     4.4      val Datatype_thy = theory "Datatype";
     4.5      val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
     4.6      val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
     4.7 -      Funs_name, o_name] =
     4.8 +      Funs_name, o_name, sum_case_name] =
     4.9        map (Sign.intern_const (Theory.sign_of Datatype_thy))
    4.10 -        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
    4.11 +        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"];
    4.12  
    4.13      val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    4.14           In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
    4.15 -         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
    4.16 +         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
    4.17          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
    4.18           "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
    4.19 -         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
    4.20 +         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
    4.21  
    4.22      val Funs_IntE = (Int_lower2 RS Funs_mono RS
    4.23        (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
    4.24 @@ -124,7 +124,7 @@
    4.25            let
    4.26              val n2 = n div 2;
    4.27              val Type (_, [T1, T2]) = T;
    4.28 -            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    4.29 +            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    4.30            in
    4.31              if i <= n2 then
    4.32                sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 19 18:36:41 1999 +0200
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 19 19:00:42 1999 +0200
     5.3 @@ -455,6 +455,10 @@
     5.4  
     5.5      val sign = Theory.sign_of thy;
     5.6  
     5.7 +    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
     5.8 +        None => []
     5.9 +      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
    5.10 +
    5.11      val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    5.12  
    5.13      (* make predicate for instantiation of abstract induction rule *)
    5.14 @@ -463,7 +467,7 @@
    5.15        | mk_ind_pred T Ps =
    5.16           let val n = (length Ps) div 2;
    5.17               val Type (_, [T1, T2]) = T
    5.18 -         in Const ("basic_sum_case",
    5.19 +         in Const ("Datatype.sum.sum_case",
    5.20             [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
    5.21               mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
    5.22           end;
    5.23 @@ -482,8 +486,7 @@
    5.24            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
    5.25             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
    5.26               nth_elem (find_index_eq c cs, preds)))))
    5.27 -        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
    5.28 -           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    5.29 +        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
    5.30            rtac refl 1])) cs;
    5.31  
    5.32      val induct = prove_goalw_cterm [] (cterm_of sign
    5.33 @@ -498,7 +501,7 @@
    5.34             some premise involves disjunction.*)
    5.35           REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
    5.36                       ORELSE' hyp_subst_tac)),
    5.37 -         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    5.38 +         rewrite_goals_tac sum_case_rewrites,
    5.39           EVERY (map (fn prem =>
    5.40             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    5.41  
    5.42 @@ -508,7 +511,7 @@
    5.43           REPEAT (EVERY
    5.44             [REPEAT (resolve_tac [conjI, impI] 1),
    5.45              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
    5.46 -            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
    5.47 +            rewrite_goals_tac sum_case_rewrites,
    5.48              atac 1])])
    5.49  
    5.50    in standard (split_rule (induct RS lemma))