src/FOLP/ex/Foundation.thy
changeset 36319 8feb2c4bef1a
parent 35762 af3ff2ba4c54
child 41526 54b4686704af
     1.1 --- a/src/FOLP/ex/Foundation.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOLP/ex/Foundation.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports IFOLP
     1.5  begin
     1.6  
     1.7 -lemma "?p : A&B  --> (C-->A&C)"
     1.8 +schematic_lemma "?p : A&B  --> (C-->A&C)"
     1.9  apply (rule impI)
    1.10  apply (rule impI)
    1.11  apply (rule conjI)
    1.12 @@ -19,7 +19,7 @@
    1.13  done
    1.14  
    1.15  text {*A form of conj-elimination*}
    1.16 -lemma
    1.17 +schematic_lemma
    1.18    assumes "p : A & B"
    1.19      and "!!x y. x : A ==> y : B ==> f(x, y) : C"
    1.20    shows "?p : C"
    1.21 @@ -30,7 +30,7 @@
    1.22  apply (rule prems)
    1.23  done
    1.24  
    1.25 -lemma
    1.26 +schematic_lemma
    1.27    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    1.28    shows "?p : B | ~B"
    1.29  apply (rule prems)
    1.30 @@ -48,7 +48,7 @@
    1.31  apply assumption
    1.32  done
    1.33  
    1.34 -lemma
    1.35 +schematic_lemma
    1.36    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    1.37    shows "?p : B | ~B"
    1.38  apply (rule prems)
    1.39 @@ -63,7 +63,7 @@
    1.40  done
    1.41  
    1.42  
    1.43 -lemma
    1.44 +schematic_lemma
    1.45    assumes "p : A | ~A"
    1.46      and "q : ~ ~A"
    1.47    shows "?p : A"
    1.48 @@ -79,7 +79,7 @@
    1.49  
    1.50  subsection "Examples with quantifiers"
    1.51  
    1.52 -lemma
    1.53 +schematic_lemma
    1.54    assumes "p : ALL z. G(z)"
    1.55    shows "?p : ALL z. G(z)|H(z)"
    1.56  apply (rule allI)
    1.57 @@ -87,20 +87,20 @@
    1.58  apply (rule prems [THEN spec])
    1.59  done
    1.60  
    1.61 -lemma "?p : ALL x. EX y. x=y"
    1.62 +schematic_lemma "?p : ALL x. EX y. x=y"
    1.63  apply (rule allI)
    1.64  apply (rule exI)
    1.65  apply (rule refl)
    1.66  done
    1.67  
    1.68 -lemma "?p : EX y. ALL x. x=y"
    1.69 +schematic_lemma "?p : EX y. ALL x. x=y"
    1.70  apply (rule exI)
    1.71  apply (rule allI)
    1.72  apply (rule refl)?
    1.73  oops
    1.74  
    1.75  text {* Parallel lifting example. *}
    1.76 -lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
    1.77 +schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
    1.78  apply (rule exI allI)
    1.79  apply (rule exI allI)
    1.80  apply (rule exI allI)
    1.81 @@ -108,7 +108,7 @@
    1.82  apply (rule exI allI)
    1.83  oops
    1.84  
    1.85 -lemma
    1.86 +schematic_lemma
    1.87    assumes "p : (EX z. F(z)) & B"
    1.88    shows "?p : EX z. F(z) & B"
    1.89  apply (rule conjE)
    1.90 @@ -122,7 +122,7 @@
    1.91  done
    1.92  
    1.93  text {* A bigger demonstration of quantifiers -- not in the paper. *}
    1.94 -lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.95 +schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    1.96  apply (rule impI)
    1.97  apply (rule allI)
    1.98  apply (rule exE, assumption)