src/HOL/Prolog/Test.thy
changeset 21425 c11ab38b78a7
parent 17311 5b1d47d920ce
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Prolog/Test.thy	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ b/src/HOL/Prolog/Test.thy	Mon Nov 20 21:23:12 2006 +0100
     1.3 @@ -80,6 +80,202 @@
     1.4                                  remove Y S4 S5 &
     1.5                                  empty    S5)"
     1.6  
     1.7 -ML {* use_legacy_bindings (the_context ()) *}
     1.8 +lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
     1.9 +
    1.10 +lemma "append ?x ?y [a,b,c,d]"
    1.11 +  apply (prolog prog_Test)
    1.12 +  back
    1.13 +  back
    1.14 +  back
    1.15 +  back
    1.16 +  done
    1.17 +
    1.18 +lemma "append [a,b] y ?L"
    1.19 +  apply (prolog prog_Test)
    1.20 +  done
    1.21 +
    1.22 +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 +  apply (prolog prog_Test)
    1.28 +  done
    1.29 +
    1.30 +lemma "reverse [23] ?L"
    1.31 +  apply (prolog prog_Test)
    1.32 +  done
    1.33 +
    1.34 +lemma "reverse [23,24,?x] ?L"
    1.35 +  apply (prolog prog_Test)
    1.36 +  done
    1.37 +
    1.38 +lemma "reverse ?L [23,24,?x]"
    1.39 +  apply (prolog prog_Test)
    1.40 +  done
    1.41 +
    1.42 +lemma "mappred age ?x [23,24]"
    1.43 +  apply (prolog prog_Test)
    1.44 +  back
    1.45 +  done
    1.46 +
    1.47 +lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
    1.48 +  apply (prolog prog_Test)
    1.49 +  done
    1.50 +
    1.51 +lemma "mappred ?P [bob,sue] [24,23]"
    1.52 +  apply (prolog prog_Test)
    1.53 +  done
    1.54 +
    1.55 +lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
    1.56 +  apply (prolog prog_Test)
    1.57 +  done
    1.58 +
    1.59 +lemma "mapfun (%x. h x 25) [bob,sue] ?L"
    1.60 +  apply (prolog prog_Test)
    1.61 +  done
    1.62 +
    1.63 +lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
    1.64 +  apply (prolog prog_Test)
    1.65 +  done
    1.66 +
    1.67 +lemma "mapfun ?F [24] [h 24 24]"
    1.68 +  apply (prolog prog_Test)
    1.69 +  back
    1.70 +  back
    1.71 +  back
    1.72 +  done
    1.73 +
    1.74 +lemma "True"
    1.75 +  apply (prolog prog_Test)
    1.76 +  done
    1.77 +
    1.78 +lemma "age ?x 24 & age ?y 23"
    1.79 +  apply (prolog prog_Test)
    1.80 +  back
    1.81 +  done
    1.82 +
    1.83 +lemma "age ?x 24 | age ?x 23"
    1.84 +  apply (prolog prog_Test)
    1.85 +  back
    1.86 +  back
    1.87 +  done
    1.88 +
    1.89 +lemma "? x y. age x y"
    1.90 +  apply (prolog prog_Test)
    1.91 +  done
    1.92 +
    1.93 +lemma "!x y. append [] x x"
    1.94 +  apply (prolog prog_Test)
    1.95 +  done
    1.96 +
    1.97 +lemma "age sue 24 .. age bob 23 => age ?x ?y"
    1.98 +  apply (prolog prog_Test)
    1.99 +  back
   1.100 +  back
   1.101 +  back
   1.102 +  back
   1.103 +  done
   1.104 +
   1.105 +(*set trace_DEPTH_FIRST;*)
   1.106 +lemma "age bob 25 :- age bob 24 => age bob 25"
   1.107 +  apply (prolog prog_Test)
   1.108 +  done
   1.109 +(*reset trace_DEPTH_FIRST;*)
   1.110 +
   1.111 +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 +  back
   1.116 +  done
   1.117 +
   1.118 +lemma "!x. ? y. eq x y"
   1.119 +  apply (prolog prog_Test)
   1.120 +  done
   1.121 +
   1.122 +lemma "? P. P & eq P ?x"
   1.123 +  apply (prolog prog_Test)
   1.124 +(*
   1.125 +  back
   1.126 +  back
   1.127 +  back
   1.128 +  back
   1.129 +  back
   1.130 +  back
   1.131 +  back
   1.132 +  back
   1.133 +*)
   1.134 +  done
   1.135 +
   1.136 +lemma "? P. eq P (True & True) & P"
   1.137 +  apply (prolog prog_Test)
   1.138 +  done
   1.139 +
   1.140 +lemma "? P. eq P op | & P k True"
   1.141 +  apply (prolog prog_Test)
   1.142 +  done
   1.143 +
   1.144 +lemma "? P. eq P (Q => True) & P"
   1.145 +  apply (prolog prog_Test)
   1.146 +  done
   1.147 +
   1.148 +(* P flexible: *)
   1.149 +lemma "(!P k l. P k l :- eq P Q) => Q a b"
   1.150 +  apply (prolog prog_Test)
   1.151 +  done
   1.152 +(*
   1.153 +loops:
   1.154 +lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
   1.155 +*)
   1.156 +
   1.157 +(* implication and disjunction in atom: *)
   1.158 +lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
   1.159 +  by fast
   1.160 +
   1.161 +(* disjunction in atom: *)
   1.162 +lemma "(!P. g P :- (P => b | a)) => g(a | b)"
   1.163 +  apply (tactic "step_tac HOL_cs 1")
   1.164 +  apply (tactic "step_tac HOL_cs 1")
   1.165 +  apply (tactic "step_tac HOL_cs 1")
   1.166 +   prefer 2
   1.167 +   apply fast
   1.168 +  apply fast
   1.169 +  done
   1.170 +
   1.171 +(*
   1.172 +hangs:
   1.173 +lemma "(!P. g P :- (P => b | a)) => g(a | b)"
   1.174 +  by fast
   1.175 +*)
   1.176 +
   1.177 +lemma "!Emp Stk.(
   1.178 +                       empty    (Emp::'b) .. 
   1.179 +         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
   1.180 +         (!(X::nat) S. remove X ((Stk X S)::'b) S))
   1.181 + => bag_appl 23 24 ?X ?Y"
   1.182 +  oops
   1.183 +
   1.184 +lemma "!Qu. ( 
   1.185 +          (!L.            empty    (Qu L L)) .. 
   1.186 +          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
   1.187 +          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
   1.188 + => bag_appl 23 24 ?X ?Y"
   1.189 +  oops
   1.190 +
   1.191 +lemma "D & (!y. E) :- (!x. True & True) :- True => D"
   1.192 +  apply (prolog prog_Test)
   1.193 +  done
   1.194 +
   1.195 +lemma "P x .. P y => P ?X"
   1.196 +  apply (prolog prog_Test)
   1.197 +  back
   1.198 +  done
   1.199 +(*
   1.200 +back
   1.201 +-> problem with DEPTH_SOLVE:
   1.202 +Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
   1.203 +Exception raised at run-time
   1.204 +*)
   1.205  
   1.206  end