src/CTT/ex/Synthesis.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 58889 5b7a9633cfa8
--- a/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -10,7 +10,7 @@
 begin
 
 text "discovery of predecessor function"
-lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
+schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
                   *  (PROD n:N. Eq(N, pred ` succ(n), n))"
 apply (tactic "intr_tac []")
 apply (tactic eqintr_tac)
@@ -20,7 +20,7 @@
 done
 
 text "the function fst as an element of a function type"
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
   "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
 apply (tactic "intr_tac []")
 apply (tactic eqintr_tac)
@@ -34,7 +34,7 @@
 text "An interesting use of the eliminator, when"
 (*The early implementation of unification caused non-rigid path in occur check
   See following example.*)
-lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
+schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
                    * Eq(?A, ?b(inr(i)), <succ(0), i>)"
 apply (tactic "intr_tac []")
 apply (tactic eqintr_tac)
@@ -46,13 +46,13 @@
  This prevents the cycle in the first unification (no longer needed).
  Requires flex-flex to preserve the dependence.
  Simpler still: make ?A into a constant type N*N.*)
-lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
+schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
                   *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
 oops
 
 text "A tricky combination of when and split"
 (*Now handled easily, but caused great problems once*)
-lemma [folded basic_defs]:
+schematic_lemma [folded basic_defs]:
   "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
                            *  Eq(?A, ?b(inr(<i,j>)), j)"
 apply (tactic "intr_tac []")
@@ -65,18 +65,18 @@
 done
 
 (*similar but allows the type to depend on i and j*)
-lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
+schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
                           *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
 oops
 
 (*similar but specifying the type N simplifies the unification problems*)
-lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
+schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
                           *   Eq(N, ?b(inr(<i,j>)), j)"
 oops
 
 
 text "Deriving the addition operator"
-lemma [folded arith_defs]:
+schematic_lemma [folded arith_defs]:
   "?c : PROD n:N. Eq(N, ?f(0,n), n)
                   *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
 apply (tactic "intr_tac []")
@@ -86,7 +86,7 @@
 done
 
 text "The addition function -- using explicit lambdas"
-lemma [folded arith_defs]:
+schematic_lemma [folded arith_defs]:
   "?c : SUM plus : ?A .
          PROD x:N. Eq(N, plus`0`x, x)
                 *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"