src/HOL/Prolog/Test.thy
changeset 36319 8feb2c4bef1a
parent 35109 0015a0a99ae9
child 41310 65631ca437c9
     1.1 --- a/src/HOL/Prolog/Test.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/Prolog/Test.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
     1.6  
     1.7 -lemma "append ?x ?y [a,b,c,d]"
     1.8 +schematic_lemma "append ?x ?y [a,b,c,d]"
     1.9    apply (prolog prog_Test)
    1.10    back
    1.11    back
    1.12 @@ -89,56 +89,56 @@
    1.13    back
    1.14    done
    1.15  
    1.16 -lemma "append [a,b] y ?L"
    1.17 +schematic_lemma "append [a,b] y ?L"
    1.18    apply (prolog prog_Test)
    1.19    done
    1.20  
    1.21 -lemma "!y. append [a,b] y (?L y)"
    1.22 +schematic_lemma "!y. append [a,b] y (?L y)"
    1.23    apply (prolog prog_Test)
    1.24    done
    1.25  
    1.26 -lemma "reverse [] ?L"
    1.27 +schematic_lemma "reverse [] ?L"
    1.28    apply (prolog prog_Test)
    1.29    done
    1.30  
    1.31 -lemma "reverse [23] ?L"
    1.32 +schematic_lemma "reverse [23] ?L"
    1.33    apply (prolog prog_Test)
    1.34    done
    1.35  
    1.36 -lemma "reverse [23,24,?x] ?L"
    1.37 +schematic_lemma "reverse [23,24,?x] ?L"
    1.38    apply (prolog prog_Test)
    1.39    done
    1.40  
    1.41 -lemma "reverse ?L [23,24,?x]"
    1.42 +schematic_lemma "reverse ?L [23,24,?x]"
    1.43    apply (prolog prog_Test)
    1.44    done
    1.45  
    1.46 -lemma "mappred age ?x [23,24]"
    1.47 +schematic_lemma "mappred age ?x [23,24]"
    1.48    apply (prolog prog_Test)
    1.49    back
    1.50    done
    1.51  
    1.52 -lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
    1.53 +schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
    1.54    apply (prolog prog_Test)
    1.55    done
    1.56  
    1.57 -lemma "mappred ?P [bob,sue] [24,23]"
    1.58 +schematic_lemma "mappred ?P [bob,sue] [24,23]"
    1.59    apply (prolog prog_Test)
    1.60    done
    1.61  
    1.62 -lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
    1.63 +schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
    1.64    apply (prolog prog_Test)
    1.65    done
    1.66  
    1.67 -lemma "mapfun (%x. h x 25) [bob,sue] ?L"
    1.68 +schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L"
    1.69    apply (prolog prog_Test)
    1.70    done
    1.71  
    1.72 -lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
    1.73 +schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
    1.74    apply (prolog prog_Test)
    1.75    done
    1.76  
    1.77 -lemma "mapfun ?F [24] [h 24 24]"
    1.78 +schematic_lemma "mapfun ?F [24] [h 24 24]"
    1.79    apply (prolog prog_Test)
    1.80    back
    1.81    back
    1.82 @@ -149,12 +149,12 @@
    1.83    apply (prolog prog_Test)
    1.84    done
    1.85  
    1.86 -lemma "age ?x 24 & age ?y 23"
    1.87 +schematic_lemma "age ?x 24 & age ?y 23"
    1.88    apply (prolog prog_Test)
    1.89    back
    1.90    done
    1.91  
    1.92 -lemma "age ?x 24 | age ?x 23"
    1.93 +schematic_lemma "age ?x 24 | age ?x 23"
    1.94    apply (prolog prog_Test)
    1.95    back
    1.96    back
    1.97 @@ -168,7 +168,7 @@
    1.98    apply (prolog prog_Test)
    1.99    done
   1.100  
   1.101 -lemma "age sue 24 .. age bob 23 => age ?x ?y"
   1.102 +schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y"
   1.103    apply (prolog prog_Test)
   1.104    back
   1.105    back
   1.106 @@ -182,7 +182,7 @@
   1.107    done
   1.108  (*reset trace_DEPTH_FIRST;*)
   1.109  
   1.110 -lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
   1.111 +schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
   1.112    apply (prolog prog_Test)
   1.113    back
   1.114    back
   1.115 @@ -193,7 +193,7 @@
   1.116    apply (prolog prog_Test)
   1.117    done
   1.118  
   1.119 -lemma "? P. P & eq P ?x"
   1.120 +schematic_lemma "? P. P & eq P ?x"
   1.121    apply (prolog prog_Test)
   1.122  (*
   1.123    back
   1.124 @@ -248,14 +248,14 @@
   1.125    by fast
   1.126  *)
   1.127  
   1.128 -lemma "!Emp Stk.(
   1.129 +schematic_lemma "!Emp Stk.(
   1.130                         empty    (Emp::'b) .. 
   1.131           (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
   1.132           (!(X::nat) S. remove X ((Stk X S)::'b) S))
   1.133   => bag_appl 23 24 ?X ?Y"
   1.134    oops
   1.135  
   1.136 -lemma "!Qu. ( 
   1.137 +schematic_lemma "!Qu. ( 
   1.138            (!L.            empty    (Qu L L)) .. 
   1.139            (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
   1.140            (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
   1.141 @@ -266,7 +266,7 @@
   1.142    apply (prolog prog_Test)
   1.143    done
   1.144  
   1.145 -lemma "P x .. P y => P ?X"
   1.146 +schematic_lemma "P x .. P y => P ?X"
   1.147    apply (prolog prog_Test)
   1.148    back
   1.149    done