# HG changeset patch # User berghofe # Date 935082042 -7200 # Node ID 959e060f4a2fcdfdb269ef93b9fa16a0d5e6aa62 # Parent dff3470c5c62669b1c688796f12fc46ad0baae91 Moved sum_case stuff from Sum to Datatype. diff -r dff3470c5c62 -r 959e060f4a2f src/HOL/Datatype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Datatype.ML Thu Aug 19 19:00:42 1999 +0200 @@ -0,0 +1,34 @@ +(* Title: HOL/Datatype.ML + ID: $Id$ + Author: Stefan Berghofer + Copyright 1999 TU Muenchen +*) + +(** sum_case -- the selection operator for sums **) + +(*compatibility*) +val [sum_case_Inl, sum_case_Inr] = sum.cases; + +Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; +by (EVERY1 [res_inst_tac [("s","s")] sumE, + etac ssubst, rtac sum_case_Inl, + etac ssubst, rtac sum_case_Inr]); +qed "surjective_sum"; + +(*Prevents simplification of f and g: much faster*) +Goal "s=t ==> sum_case f g s = sum_case f g t"; +by (etac arg_cong 1); +qed "sum_case_weak_cong"; + +val [p1,p2] = Goal + "[| sum_case f1 f2 = sum_case g1 g2; \ +\ [| f1 = g1; f2 = g2 |] ==> P |] \ +\ ==> P"; +by (rtac p2 1); +by (rtac ext 1); +by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1); +by (Asm_full_simp_tac 1); +by (rtac ext 1); +by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1); +by (Asm_full_simp_tac 1); +qed "sum_case_inject"; diff -r dff3470c5c62 -r 959e060f4a2f src/HOL/Sum.ML --- a/src/HOL/Sum.ML Thu Aug 19 18:36:41 1999 +0200 +++ b/src/HOL/Sum.ML Thu Aug 19 19:00:42 1999 +0200 @@ -114,18 +114,6 @@ AddSEs [PlusE]; -(** sum_case -- the selection operator for sums **) - -Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)"; -by (Blast_tac 1); -qed "sum_case_Inl"; - -Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)"; -by (Blast_tac 1); -qed "sum_case_Inr"; - -Addsimps [sum_case_Inl, sum_case_Inr]; - (** Exhaustion rule for sums -- a degenerate form of induction **) val prems = Goalw [Inl_def,Inr_def] @@ -143,42 +131,6 @@ by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems))); qed "sum_induct"; -Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; -by (EVERY1 [res_inst_tac [("s","s")] sumE, - etac ssubst, rtac sum_case_Inl, - etac ssubst, rtac sum_case_Inr]); -qed "surjective_sum"; - -Goal "R(basic_sum_case f g s) = \ -\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; -by (res_inst_tac [("s","s")] sumE 1); -by Auto_tac; -qed "split_sum_case"; - -Goal "P (basic_sum_case f g s) = \ -\ (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"; -by (stac split_sum_case 1); -by (Blast_tac 1); -qed "split_sum_case_asm"; - -(*Prevents simplification of f and g: much faster*) -Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t"; -by (etac arg_cong 1); -qed "sum_case_weak_cong"; - -val [p1,p2] = Goal - "[| basic_sum_case f1 f2 = basic_sum_case g1 g2; \ -\ [| f1 = g1; f2 = g2 |] ==> P |] \ -\ ==> P"; -by (rtac p2 1); -by (rtac ext 1); -by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1); -by (Asm_full_simp_tac 1); -by (rtac ext 1); -by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1); -by (Asm_full_simp_tac 1); -qed "sum_case_inject"; - (** Rules for the Part primitive **) @@ -222,7 +174,6 @@ by (Blast_tac 1); qed "Part_Int"; -(*For inductive definitions*) Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"; by (Blast_tac 1); qed "Part_Collect"; diff -r dff3470c5c62 -r 959e060f4a2f src/HOL/Sum.thy --- a/src/HOL/Sum.thy Thu Aug 19 18:36:41 1999 +0200 +++ b/src/HOL/Sum.thy Thu Aug 19 19:00:42 1999 +0200 @@ -29,7 +29,6 @@ consts Inl :: "'a => 'a + 'b" Inr :: "'b => 'a + 'b" - basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c" (*disjoint sum for sets; the operator + is overloaded with wrong type!*) Plus :: "['a set, 'b set] => ('a + 'b) set" (infixr 65) @@ -40,8 +39,6 @@ defs Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" - sum_case_def "basic_sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) - & (!y. p=Inr(y) --> z=g(y))" sum_def "A Plus B == (Inl``A) Un (Inr``B)" diff -r dff3470c5c62 -r 959e060f4a2f src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Aug 19 18:36:41 1999 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Aug 19 19:00:42 1999 +0200 @@ -47,16 +47,16 @@ val Datatype_thy = theory "Datatype"; val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node"; val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name, - Funs_name, o_name] = + Funs_name, o_name, sum_case_name] = map (Sign.intern_const (Theory.sign_of Datatype_thy)) - ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"]; + ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"]; val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq, In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject, - Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy) + Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy) ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject", - "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"]; + "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"]; val Funs_IntE = (Int_lower2 RS Funs_mono RS (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE; @@ -124,7 +124,7 @@ let val n2 = n div 2; val Type (_, [T1, T2]) = T; - val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT) + val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT) in if i <= n2 then sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT) diff -r dff3470c5c62 -r 959e060f4a2f src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Aug 19 18:36:41 1999 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Aug 19 19:00:42 1999 +0200 @@ -455,6 +455,10 @@ val sign = Theory.sign_of thy; + val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of + None => [] + | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases")); + val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; (* make predicate for instantiation of abstract induction rule *) @@ -463,7 +467,7 @@ | mk_ind_pred T Ps = let val n = (length Ps) div 2; val Type (_, [T1, T2]) = T - in Const ("basic_sum_case", + in Const ("Datatype.sum.sum_case", [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $ mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) end; @@ -482,8 +486,7 @@ (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ nth_elem (find_index_eq c cs, preds))))) - (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac - (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs; val induct = prove_goalw_cterm [] (cterm_of sign @@ -498,7 +501,7 @@ some premise involves disjunction.*) REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] ORELSE' hyp_subst_tac)), - rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + rewrite_goals_tac sum_case_rewrites, EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); @@ -508,7 +511,7 @@ REPEAT (EVERY [REPEAT (resolve_tac [conjI, impI] 1), TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, - rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), + rewrite_goals_tac sum_case_rewrites, atac 1])]) in standard (split_rule (induct RS lemma))