src/CTT/ex/Elimination.thy
changeset 39159 0dec18004e75
parent 36319 8feb2c4bef1a
child 41526 54b4686704af
     1.1 --- a/src/CTT/ex/Elimination.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/CTT/ex/Elimination.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4      and "!!x. x:A ==> B(x) type"
     1.5      and "!!x. x:A ==> C(x) type"
     1.6    shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
     1.7 -apply (tactic {* pc_tac (thms "prems") 1 *})
     1.8 +apply (tactic {* pc_tac @{thms assms} 1 *})
     1.9  done
    1.10  
    1.11  text "Construction of the currying functional"
    1.12 @@ -68,7 +68,7 @@
    1.13      and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
    1.14    shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
    1.15                        (PROD x:A . PROD y:B(x) . C(<x,y>))"
    1.16 -apply (tactic {* pc_tac (thms "prems") 1 *})
    1.17 +apply (tactic {* pc_tac @{thms assms} 1 *})
    1.18  done
    1.19  
    1.20  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    1.21 @@ -83,7 +83,7 @@
    1.22      and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
    1.23    shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
    1.24          --> (PROD z : (SUM x:A . B(x)) . C(z))"
    1.25 -apply (tactic {* pc_tac (thms "prems") 1 *})
    1.26 +apply (tactic {* pc_tac @{thms assms} 1 *})
    1.27  done
    1.28  
    1.29  text "Function application"
    1.30 @@ -99,7 +99,7 @@
    1.31    shows
    1.32      "?a :     (SUM y:B . PROD x:A . C(x,y))
    1.33            --> (PROD x:A . SUM y:B . C(x,y))"
    1.34 -apply (tactic {* pc_tac (thms "prems") 1 *})
    1.35 +apply (tactic {* pc_tac @{thms assms} 1 *})
    1.36  done
    1.37  
    1.38  text "Martin-Lof (1984) pages 36-7: the combinator S"
    1.39 @@ -109,7 +109,7 @@
    1.40      and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
    1.41    shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
    1.42               --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    1.43 -apply (tactic {* pc_tac (thms "prems") 1 *})
    1.44 +apply (tactic {* pc_tac @{thms assms} 1 *})
    1.45  done
    1.46  
    1.47  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
    1.48 @@ -119,7 +119,7 @@
    1.49      and "!!z. z: A+B ==> C(z) type"
    1.50    shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
    1.51            --> (PROD z: A+B. C(z))"
    1.52 -apply (tactic {* pc_tac (thms "prems") 1 *})
    1.53 +apply (tactic {* pc_tac @{thms assms} 1 *})
    1.54  done
    1.55  
    1.56  (*towards AXIOM OF CHOICE*)
    1.57 @@ -137,7 +137,7 @@
    1.58      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
    1.59    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
    1.60                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    1.61 -apply (tactic {* intr_tac (thms "prems") *})
    1.62 +apply (tactic {* intr_tac @{thms assms} *})
    1.63  apply (tactic "add_mp_tac 2")
    1.64  apply (tactic "add_mp_tac 1")
    1.65  apply (erule SumE_fst)
    1.66 @@ -145,7 +145,7 @@
    1.67  apply (rule subst_eqtyparg)
    1.68  apply (rule comp_rls)
    1.69  apply (rule_tac [4] SumE_snd)
    1.70 -apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
    1.71 +apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *})
    1.72  done
    1.73  
    1.74  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
    1.75 @@ -155,7 +155,7 @@
    1.76      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
    1.77    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
    1.78                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    1.79 -apply (tactic {* intr_tac (thms "prems") *})
    1.80 +apply (tactic {* intr_tac @{thms assms} *})
    1.81  (*Must not use add_mp_tac as subst_prodE hides the construction.*)
    1.82  apply (rule ProdE [THEN SumE], assumption)
    1.83  apply (tactic "TRYALL assume_tac")
    1.84 @@ -163,11 +163,11 @@
    1.85  apply (rule subst_eqtyparg)
    1.86  apply (rule comp_rls)
    1.87  apply (erule_tac [4] ProdE [THEN SumE])
    1.88 -apply (tactic {* typechk_tac (thms "prems") *})
    1.89 +apply (tactic {* typechk_tac @{thms assms} *})
    1.90  apply (rule replace_type)
    1.91  apply (rule subst_eqtyparg)
    1.92  apply (rule comp_rls)
    1.93 -apply (tactic {* typechk_tac (thms "prems") *})
    1.94 +apply (tactic {* typechk_tac @{thms assms} *})
    1.95  apply assumption
    1.96  done
    1.97  
    1.98 @@ -183,11 +183,11 @@
    1.99  apply (tactic {* biresolve_tac safe_brls 2 *})
   1.100  (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
   1.101  apply (rule_tac [2] a = "y" in ProdE)
   1.102 -apply (tactic {* typechk_tac (thms "prems") *})
   1.103 +apply (tactic {* typechk_tac @{thms assms} *})
   1.104  apply (rule SumE, assumption)
   1.105  apply (tactic "intr_tac []")
   1.106  apply (tactic "TRYALL assume_tac")
   1.107 -apply (tactic {* typechk_tac (thms "prems") *})
   1.108 +apply (tactic {* typechk_tac @{thms assms} *})
   1.109  done
   1.110  
   1.111  end