src/CTT/ex/Typechecking.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 39159 0dec18004e75
     1.1 --- a/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/CTT/ex/Typechecking.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -11,18 +11,18 @@
     1.4  
     1.5  subsection {* Single-step proofs: verifying that a type is well-formed *}
     1.6  
     1.7 -lemma "?A type"
     1.8 +schematic_lemma "?A type"
     1.9  apply (rule form_rls)
    1.10  done
    1.11  
    1.12 -lemma "?A type"
    1.13 +schematic_lemma "?A type"
    1.14  apply (rule form_rls)
    1.15  back
    1.16  apply (rule form_rls)
    1.17  apply (rule form_rls)
    1.18  done
    1.19  
    1.20 -lemma "PROD z:?A . N + ?B(z) type"
    1.21 +schematic_lemma "PROD z:?A . N + ?B(z) type"
    1.22  apply (rule form_rls)
    1.23  apply (rule form_rls)
    1.24  apply (rule form_rls)
    1.25 @@ -37,30 +37,30 @@
    1.26  apply (tactic form_tac)
    1.27  done
    1.28  
    1.29 -lemma "<0, succ(0)> : ?A"
    1.30 +schematic_lemma "<0, succ(0)> : ?A"
    1.31  apply (tactic "intr_tac []")
    1.32  done
    1.33  
    1.34 -lemma "PROD w:N . Eq(?A,w,w) type"
    1.35 +schematic_lemma "PROD w:N . Eq(?A,w,w) type"
    1.36  apply (tactic "typechk_tac []")
    1.37  done
    1.38  
    1.39 -lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    1.40 +schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    1.41  apply (tactic "typechk_tac []")
    1.42  done
    1.43  
    1.44  text "typechecking an application of fst"
    1.45 -lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
    1.46 +schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
    1.47  apply (tactic "typechk_tac []")
    1.48  done
    1.49  
    1.50  text "typechecking the predecessor function"
    1.51 -lemma "lam n. rec(n, 0, %x y. x) : ?A"
    1.52 +schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
    1.53  apply (tactic "typechk_tac []")
    1.54  done
    1.55  
    1.56  text "typechecking the addition function"
    1.57 -lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
    1.58 +schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
    1.59  apply (tactic "typechk_tac []")
    1.60  done
    1.61  
    1.62 @@ -68,18 +68,18 @@
    1.63    For concreteness, every type variable left over is forced to be N*)
    1.64  ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
    1.65  
    1.66 -lemma "lam w. <w,w> : ?A"
    1.67 +schematic_lemma "lam w. <w,w> : ?A"
    1.68  apply (tactic "typechk_tac []")
    1.69  apply (tactic N_tac)
    1.70  done
    1.71  
    1.72 -lemma "lam x. lam y. x : ?A"
    1.73 +schematic_lemma "lam x. lam y. x : ?A"
    1.74  apply (tactic "typechk_tac []")
    1.75  apply (tactic N_tac)
    1.76  done
    1.77  
    1.78  text "typechecking fst (as a function object)"
    1.79 -lemma "lam i. split(i, %j k. j) : ?A"
    1.80 +schematic_lemma "lam i. split(i, %j k. j) : ?A"
    1.81  apply (tactic "typechk_tac []")
    1.82  apply (tactic N_tac)
    1.83  done