src/CTT/ex/Elimination.thy
author wenzelm
Wed, 26 Jul 2006 00:44:44 +0200
changeset 20207 4c57e850e8d5
parent 19761 5cd82054c2c6
child 35762 af3ff2ba4c54
permissions -rw-r--r--
added Pure/subgoal.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     1
(*  Title:      CTT/ex/Elimination.thy
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     6
Some examples taken from P. Martin-L\"of, Intuitionistic type theory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
        (Bibliopolis, 1984).
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     9
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
header "Examples with elimination rules"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
theory Elimination
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
imports CTT
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    14
begin
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
text "This finds the functions fst and snd!"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    18
lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
apply (tactic {* pc_tac [] 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
apply (tactic {* pc_tac [] 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
back
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    25
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
text "Double negation of the Excluded Middle"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    28
lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
apply (rule ProdE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
apply assumption
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    36
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    37
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
(*The sequent version (ITT) could produce an interesting alternative
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
  by backtracking.  No longer.*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    41
text "Binary sums and products"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    42
lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    44
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    45
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
(*A distributive law*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    48
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    49
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
(*more general version, same proof*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    54
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
    and "!!x. x:A ==> C(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
  shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    58
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
text "Construction of the currying functional"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    63
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    64
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
(*more general goal with same proof*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    68
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
    and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    70
  shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
                      (PROD x:A . PROD y:B(x) . C(<x,y>))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    72
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    73
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    74
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    75
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    76
lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    77
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    78
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    79
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    80
(*more general goal with same proof*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    81
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    82
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    83
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    84
    and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    85
  shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    86
        --> (PROD z : (SUM x:A . B(x)) . C(z))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    87
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    88
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    89
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    90
text "Function application"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    91
lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    92
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    93
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    94
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    95
text "Basic test of quantifier reasoning"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    96
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    97
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    98
    and "B type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    99
    and "!!x y.[| x:A;  y:B |] ==> C(x,y) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   100
  shows
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   101
    "?a :     (SUM y:B . PROD x:A . C(x,y))
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   102
          --> (PROD x:A . SUM y:B . C(x,y))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   103
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   104
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   105
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   106
text "Martin-Lof (1984) pages 36-7: the combinator S"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   107
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   108
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   109
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   110
    and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   111
  shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   112
             --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   113
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   114
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   115
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   116
text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   117
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   118
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   119
    and "B type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   120
    and "!!z. z: A+B ==> C(z) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   121
  shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   122
          --> (PROD z: A+B. C(z))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   123
apply (tactic {* pc_tac (thms "prems") 1 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   124
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   125
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   126
(*towards AXIOM OF CHOICE*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   127
lemma [folded basic_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   128
  "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   129
apply (tactic "pc_tac [] 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   130
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   131
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   132
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   133
(*Martin-Lof (1984) page 50*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   134
text "AXIOM OF CHOICE!  Delicate use of elimination rules"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   135
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   136
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   137
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   138
    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   139
  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   140
                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   141
apply (tactic {* intr_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   142
apply (tactic "add_mp_tac 2")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   143
apply (tactic "add_mp_tac 1")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   144
apply (erule SumE_fst)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   145
apply (rule replace_type)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   146
apply (rule subst_eqtyparg)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   147
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   148
apply (rule_tac [4] SumE_snd)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   149
apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   150
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   151
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   152
text "Axiom of choice.  Proof without fst, snd.  Harder still!"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   153
lemma [folded basic_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   154
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   155
    and "!!x. x:A ==> B(x) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   156
    and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   157
  shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   158
                         (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   159
apply (tactic {* intr_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   160
(*Must not use add_mp_tac as subst_prodE hides the construction.*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   161
apply (rule ProdE [THEN SumE], assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   162
apply (tactic "TRYALL assume_tac")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   163
apply (rule replace_type)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   164
apply (rule subst_eqtyparg)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   165
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   166
apply (erule_tac [4] ProdE [THEN SumE])
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   167
apply (tactic {* typechk_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   168
apply (rule replace_type)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   169
apply (rule subst_eqtyparg)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   170
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   171
apply (tactic {* typechk_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   172
apply assumption
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   173
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   174
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   175
text "Example of sequent_style deduction"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   176
(*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   177
    lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   178
lemma
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   179
  assumes "A type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   180
    and "B type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   181
    and "!!z. z:A*B ==> C(z) type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   182
  shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   183
apply (rule intr_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   184
apply (tactic {* biresolve_tac safe_brls 2 *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   185
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   186
apply (rule_tac [2] a = "y" in ProdE)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   187
apply (tactic {* typechk_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   188
apply (rule SumE, assumption)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   189
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   190
apply (tactic "TRYALL assume_tac")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   191
apply (tactic {* typechk_tac (thms "prems") *})
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   192
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   193
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   194
end