src/CTT/ex/Synthesis.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 58889 5b7a9633cfa8
     1.1 --- a/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/CTT/ex/Synthesis.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  begin
     1.5  
     1.6  text "discovery of predecessor function"
     1.7 -lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     1.8 +schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     1.9                    *  (PROD n:N. Eq(N, pred ` succ(n), n))"
    1.10  apply (tactic "intr_tac []")
    1.11  apply (tactic eqintr_tac)
    1.12 @@ -20,7 +20,7 @@
    1.13  done
    1.14  
    1.15  text "the function fst as an element of a function type"
    1.16 -lemma [folded basic_defs]:
    1.17 +schematic_lemma [folded basic_defs]:
    1.18    "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
    1.19  apply (tactic "intr_tac []")
    1.20  apply (tactic eqintr_tac)
    1.21 @@ -34,7 +34,7 @@
    1.22  text "An interesting use of the eliminator, when"
    1.23  (*The early implementation of unification caused non-rigid path in occur check
    1.24    See following example.*)
    1.25 -lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    1.26 +schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    1.27                     * Eq(?A, ?b(inr(i)), <succ(0), i>)"
    1.28  apply (tactic "intr_tac []")
    1.29  apply (tactic eqintr_tac)
    1.30 @@ -46,13 +46,13 @@
    1.31   This prevents the cycle in the first unification (no longer needed).
    1.32   Requires flex-flex to preserve the dependence.
    1.33   Simpler still: make ?A into a constant type N*N.*)
    1.34 -lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    1.35 +schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    1.36                    *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
    1.37  oops
    1.38  
    1.39  text "A tricky combination of when and split"
    1.40  (*Now handled easily, but caused great problems once*)
    1.41 -lemma [folded basic_defs]:
    1.42 +schematic_lemma [folded basic_defs]:
    1.43    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
    1.44                             *  Eq(?A, ?b(inr(<i,j>)), j)"
    1.45  apply (tactic "intr_tac []")
    1.46 @@ -65,18 +65,18 @@
    1.47  done
    1.48  
    1.49  (*similar but allows the type to depend on i and j*)
    1.50 -lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    1.51 +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    1.52                            *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
    1.53  oops
    1.54  
    1.55  (*similar but specifying the type N simplifies the unification problems*)
    1.56 -lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    1.57 +schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    1.58                            *   Eq(N, ?b(inr(<i,j>)), j)"
    1.59  oops
    1.60  
    1.61  
    1.62  text "Deriving the addition operator"
    1.63 -lemma [folded arith_defs]:
    1.64 +schematic_lemma [folded arith_defs]:
    1.65    "?c : PROD n:N. Eq(N, ?f(0,n), n)
    1.66                    *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
    1.67  apply (tactic "intr_tac []")
    1.68 @@ -86,7 +86,7 @@
    1.69  done
    1.70  
    1.71  text "The addition function -- using explicit lambdas"
    1.72 -lemma [folded arith_defs]:
    1.73 +schematic_lemma [folded arith_defs]:
    1.74    "?c : SUM plus : ?A .
    1.75           PROD x:N. Eq(N, plus`0`x, x)
    1.76                  *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"