src/CTT/ex/Elimination.thy
author wenzelm
Wed, 17 May 2017 13:47:19 +0200
changeset 65851 c103358a5559
parent 64980 7dc25cf5793e
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned signature;
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
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 41526
diff changeset
     9
section "Examples with elimination rules"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
theory Elimination
58974
cbc2ac19d783 simplifie sessions;
wenzelm
parents: 58972
diff changeset
    12
imports "../CTT"
19761
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
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    17
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    18
apply pc
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    21
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    22
apply pc
19761
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"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    27
schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    28
apply intr
19761
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
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    31
apply pc
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    34
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    35
apply pc
19761
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"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    41
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    42
apply pc
19761
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*)
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    46
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    47
apply pc
19761
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*)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    51
schematic_goal
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    53
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    54
    and "\<And>x. x:A \<Longrightarrow> C(x) type"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    55
  shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    56
apply (pc assms)
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"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    60
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    61
apply pc
19761
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*)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    65
schematic_goal
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    67
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    68
    and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> C(z) type"
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    69
  shows "?a : \<Prod>f: (\<Prod>z : (\<Sum>x:A . B(x)) . C(z)).
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    70
                      (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    71
apply (pc assms)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    72
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    73
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    74
text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    75
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    76
apply pc
19761
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*)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    80
schematic_goal
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    81
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    82
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    83
    and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    84
  shows "?a : (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    85
        \<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    86
apply (pc assms)
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"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    90
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    91
apply pc
19761
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"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    95
schematic_goal
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"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    98
    and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    99
  shows
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   100
    "?a :     (\<Sum>y:B . \<Prod>x:A . C(x,y))
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   101
          \<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   102
apply (pc assms)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   103
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   104
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   105
text "Martin-Löf (1984) pages 36-7: the combinator S"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   106
schematic_goal
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   107
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   108
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   109
    and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   110
  shows "?a :    (\<Prod>x:A. \<Prod>y:B(x). C(x,y))
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   111
             \<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   112
apply (pc assms)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   113
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   114
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   115
text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   116
schematic_goal
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"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   119
    and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   120
  shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   121
          \<longrightarrow> (\<Prod>z: A+B. C(z))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   122
apply (pc assms)
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*)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   126
schematic_goal [folded basic_defs]:
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   127
  "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   128
apply pc
19761
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
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   132
(*Martin-Löf (1984) page 50*)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   133
text "AXIOM OF CHOICE!  Delicate use of elimination rules"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   134
schematic_goal
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   135
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   136
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   137
    and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
64980
7dc25cf5793e misc tuning;
wenzelm
parents: 63505
diff changeset
   138
  shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   139
apply (intr assms)
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   140
prefer 2 apply add_mp
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   141
prefer 2 apply add_mp
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   142
apply (erule SumE_fst)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   143
apply (rule replace_type)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   144
apply (rule subst_eqtyparg)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   145
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   146
apply (rule_tac [4] SumE_snd)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   147
apply (typechk SumE_fst assms)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   148
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   149
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   150
text "Axiom of choice.  Proof without fst, snd.  Harder still!"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   151
schematic_goal [folded basic_defs]:
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   152
  assumes "A type"
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   153
    and "\<And>x. x:A \<Longrightarrow> B(x) type"
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
   154
    and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
64980
7dc25cf5793e misc tuning;
wenzelm
parents: 63505
diff changeset
   155
  shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   156
apply (intr assms)
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   157
(*Must not use add_mp as subst_prodE hides the construction.*)
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   158
apply (rule ProdE [THEN SumE])
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   159
apply assumption
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   160
apply assumption
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   161
apply assumption
19761
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])
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   166
apply (typechk 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)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   170
apply (typechk 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
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents: 61391
diff changeset
   174
text "Example of sequent-style deduction"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   175
(*When splitting z:A \<times> B, the assumption C(z) is affected;  ?a becomes
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   176
    \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w)     *)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
   177
schematic_goal
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"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   180
    and "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
   181
  shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   182
apply (rule intr_rls)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59498
diff changeset
   183
apply (tactic \<open>biresolve_tac @{context} safe_brls 2\<close>)
19761
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)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   186
apply (typechk assms)
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   187
apply (rule SumE, assumption)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   188
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   189
defer 1
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   190
apply assumption+
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   191
apply (typechk assms)
19761
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