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