src/HOL/Datatype.ML
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 9108 9fff97d29837
child 11954 3d1780208bf3
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Datatype.ML
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     4
    Copyright   1999  TU Muenchen
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     5
*)
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     6
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     7
(** sum_case -- the selection operator for sums **)
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     8
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
     9
(*compatibility*)
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    10
val [sum_case_Inl, sum_case_Inr] = sum.cases;
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 7293
diff changeset
    11
bind_thm ("sum_case_Inl", sum_case_Inl);
9fff97d29837 bind_thm(s);
wenzelm
parents: 7293
diff changeset
    12
bind_thm ("sum_case_Inr", sum_case_Inr);
7293
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    13
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    14
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    15
by (EVERY1 [res_inst_tac [("s","s")] sumE, 
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    16
            etac ssubst, rtac sum_case_Inl,
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    17
            etac ssubst, rtac sum_case_Inr]);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    18
qed "surjective_sum";
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    19
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    20
(*Prevents simplification of f and g: much faster*)
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    21
Goal "s=t ==> sum_case f g s = sum_case f g t";
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    22
by (etac arg_cong 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    23
qed "sum_case_weak_cong";
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    24
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    25
val [p1,p2] = Goal
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    26
  "[| sum_case f1 f2 = sum_case g1 g2;  \
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    27
\     [| f1 = g1; f2 = g2 |] ==> P |] \
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    28
\  ==> P";
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    29
by (rtac p2 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    30
by (rtac ext 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    31
by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    32
by (Asm_full_simp_tac 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    33
by (rtac ext 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    34
by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    35
by (Asm_full_simp_tac 1);
959e060f4a2f Moved sum_case stuff from Sum to Datatype.
berghofe
parents:
diff changeset
    36
qed "sum_case_inject";