--- a/src/CTT/ex/Typechecking.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/CTT/ex/Typechecking.thy Tue Oct 06 15:14:28 2015 +0200
@@ -11,18 +11,18 @@
subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
-schematic_lemma "?A type"
+schematic_goal "?A type"
apply (rule form_rls)
done
-schematic_lemma "?A type"
+schematic_goal "?A type"
apply (rule form_rls)
back
apply (rule form_rls)
apply (rule form_rls)
done
-schematic_lemma "PROD z:?A . N + ?B(z) type"
+schematic_goal "PROD z:?A . N + ?B(z) type"
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
@@ -37,30 +37,30 @@
apply form
done
-schematic_lemma "<0, succ(0)> : ?A"
+schematic_goal "<0, succ(0)> : ?A"
apply intr
done
-schematic_lemma "PROD w:N . Eq(?A,w,w) type"
+schematic_goal "PROD w:N . Eq(?A,w,w) type"
apply typechk
done
-schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+schematic_goal "PROD x:N . PROD y:N . Eq(?A,x,y) type"
apply typechk
done
text "typechecking an application of fst"
-schematic_lemma "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
+schematic_goal "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
apply typechk
done
text "typechecking the predecessor function"
-schematic_lemma "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
+schematic_goal "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
apply typechk
done
text "typechecking the addition function"
-schematic_lemma "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
+schematic_goal "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
apply typechk
done
@@ -69,18 +69,18 @@
method_setup N =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
-schematic_lemma "lam w. <w,w> : ?A"
+schematic_goal "lam w. <w,w> : ?A"
apply typechk
apply N
done
-schematic_lemma "lam x. lam y. x : ?A"
+schematic_goal "lam x. lam y. x : ?A"
apply typechk
apply N
done
text "typechecking fst (as a function object)"
-schematic_lemma "lam i. split(i, \<lambda>j k. j) : ?A"
+schematic_goal "lam i. split(i, \<lambda>j k. j) : ?A"
apply typechk
apply N
done