src/CTT/ex/Elimination.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 39159 0dec18004e75
     1.1 --- a/src/CTT/ex/Elimination.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/CTT/ex/Elimination.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -14,41 +14,41 @@
     1.4  
     1.5  text "This finds the functions fst and snd!"
     1.6  
     1.7 -lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
     1.8 +schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
     1.9  apply (tactic {* pc_tac [] 1 *})
    1.10  done
    1.11  
    1.12 -lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
    1.13 +schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
    1.14  apply (tactic {* pc_tac [] 1 *})
    1.15  back
    1.16  done
    1.17  
    1.18  text "Double negation of the Excluded Middle"
    1.19 -lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
    1.20 +schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
    1.21  apply (tactic "intr_tac []")
    1.22  apply (rule ProdE)
    1.23  apply assumption
    1.24  apply (tactic "pc_tac [] 1")
    1.25  done
    1.26  
    1.27 -lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
    1.28 +schematic_lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
    1.29  apply (tactic "pc_tac [] 1")
    1.30  done
    1.31  (*The sequent version (ITT) could produce an interesting alternative
    1.32    by backtracking.  No longer.*)
    1.33  
    1.34  text "Binary sums and products"
    1.35 -lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    1.36 +schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    1.37  apply (tactic "pc_tac [] 1")
    1.38  done
    1.39  
    1.40  (*A distributive law*)
    1.41 -lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
    1.42 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
    1.43  apply (tactic "pc_tac [] 1")
    1.44  done
    1.45  
    1.46  (*more general version, same proof*)
    1.47 -lemma
    1.48 +schematic_lemma
    1.49    assumes "A type"
    1.50      and "!!x. x:A ==> B(x) type"
    1.51      and "!!x. x:A ==> C(x) type"
    1.52 @@ -57,12 +57,12 @@
    1.53  done
    1.54  
    1.55  text "Construction of the currying functional"
    1.56 -lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
    1.57 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
    1.58  apply (tactic "pc_tac [] 1")
    1.59  done
    1.60  
    1.61  (*more general goal with same proof*)
    1.62 -lemma
    1.63 +schematic_lemma
    1.64    assumes "A type"
    1.65      and "!!x. x:A ==> B(x) type"
    1.66      and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
    1.67 @@ -72,12 +72,12 @@
    1.68  done
    1.69  
    1.70  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    1.71 -lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
    1.72 +schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
    1.73  apply (tactic "pc_tac [] 1")
    1.74  done
    1.75  
    1.76  (*more general goal with same proof*)
    1.77 -lemma
    1.78 +schematic_lemma
    1.79    assumes "A type"
    1.80      and "!!x. x:A ==> B(x) type"
    1.81      and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
    1.82 @@ -87,12 +87,12 @@
    1.83  done
    1.84  
    1.85  text "Function application"
    1.86 -lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
    1.87 +schematic_lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
    1.88  apply (tactic "pc_tac [] 1")
    1.89  done
    1.90  
    1.91  text "Basic test of quantifier reasoning"
    1.92 -lemma
    1.93 +schematic_lemma
    1.94    assumes "A type"
    1.95      and "B type"
    1.96      and "!!x y.[| x:A;  y:B |] ==> C(x,y) type"
    1.97 @@ -103,7 +103,7 @@
    1.98  done
    1.99  
   1.100  text "Martin-Lof (1984) pages 36-7: the combinator S"
   1.101 -lemma
   1.102 +schematic_lemma
   1.103    assumes "A type"
   1.104      and "!!x. x:A ==> B(x) type"
   1.105      and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
   1.106 @@ -113,7 +113,7 @@
   1.107  done
   1.108  
   1.109  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
   1.110 -lemma
   1.111 +schematic_lemma
   1.112    assumes "A type"
   1.113      and "B type"
   1.114      and "!!z. z: A+B ==> C(z) type"
   1.115 @@ -123,7 +123,7 @@
   1.116  done
   1.117  
   1.118  (*towards AXIOM OF CHOICE*)
   1.119 -lemma [folded basic_defs]:
   1.120 +schematic_lemma [folded basic_defs]:
   1.121    "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
   1.122  apply (tactic "pc_tac [] 1")
   1.123  done
   1.124 @@ -131,7 +131,7 @@
   1.125  
   1.126  (*Martin-Lof (1984) page 50*)
   1.127  text "AXIOM OF CHOICE!  Delicate use of elimination rules"
   1.128 -lemma
   1.129 +schematic_lemma
   1.130    assumes "A type"
   1.131      and "!!x. x:A ==> B(x) type"
   1.132      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   1.133 @@ -149,7 +149,7 @@
   1.134  done
   1.135  
   1.136  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
   1.137 -lemma [folded basic_defs]:
   1.138 +schematic_lemma [folded basic_defs]:
   1.139    assumes "A type"
   1.140      and "!!x. x:A ==> B(x) type"
   1.141      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   1.142 @@ -174,7 +174,7 @@
   1.143  text "Example of sequent_style deduction"
   1.144  (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   1.145      lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
   1.146 -lemma
   1.147 +schematic_lemma
   1.148    assumes "A type"
   1.149      and "B type"
   1.150      and "!!z. z:A*B ==> C(z) type"