1.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Thu May 27 14:58:45 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Thu May 27 16:29:33 2010 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -2d5ecda945177c32dc13189db42e7a2391a39390 6889 0
     1.5 +b3c5003cf9ccaad1080e68445c705767d58e45ae 6889 0
     1.6  #2 := false
     1.7  decl f11 :: (-> S5 S2 S1)
     1.8  decl ?v1!7 :: (-> S2 S2)

     2.1 --- a/src/HOL/SMT.thy	Thu May 27 14:58:45 2010 +0200
     2.2 +++ b/src/HOL/SMT.thy	Thu May 27 16:29:33 2010 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4  following constant.
     2.5  *}
     2.6  
     2.7 -definition "apply" where "apply f x = f x"
     2.8 +definition fun_app where "fun_app f x = f x"
     2.9  
    2.10  text {*
    2.11  Some solvers support a theory of arrays which can be used to encode
    2.12 @@ -314,7 +314,7 @@
    2.13  
    2.14  
    2.15  hide_type (open) pattern
    2.16 -hide_const Pattern "apply" term_eq
    2.17 -hide_const (open) trigger pat nopat z3div z3mod
    2.18 +hide_const Pattern term_eq
    2.19 +hide_const (open) trigger pat nopat fun_app z3div z3mod
    2.20  
    2.21  end

     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Thu May 27 14:58:45 2010 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Thu May 27 16:29:33 2010 +0200
     3.3 @@ -16193,3 +16193,196 @@
     3.4  #615 := [unit-resolution #638 #1762]: #367
     3.5  [unit-resolution #615 #1764]: false
     3.6  unsat
     3.7 +0906dd207f0c510ad6c7f80b2056a8b625974f5b 192 0
     3.8 +#2 := false
     3.9 +decl f6 :: (-> S3 S2 S4)
    3.10 +decl f3 :: S2
    3.11 +#8 := f3
    3.12 +decl f8 :: S3
    3.13 +#16 := f8
    3.14 +#22 := (f6 f8 f3)
    3.15 +decl f7 :: (-> S3 S2 S4 S3)
    3.16 +decl f10 :: S4
    3.17 +#19 := f10
    3.18 +decl f5 :: S2
    3.19 +#12 := f5
    3.20 +decl f9 :: S4
    3.21 +#17 := f9
    3.22 +decl f4 :: S2
    3.23 +#9 := f4
    3.24 +#18 := (f7 f8 f4 f9)
    3.25 +#20 := (f7 #18 f5 f10)
    3.26 +#21 := (f6 #20 f3)
    3.27 +#23 := (= #21 #22)
    3.28 +#173 := (f6 #18 f4)
    3.29 +#570 := (f7 f8 f4 #173)
    3.30 +#538 := (f6 #570 f3)
    3.31 +#539 := (= #538 #22)
    3.32 +#542 := (= #22 #538)
    3.33 +#533 := (= #173 #538)
    3.34 +#10 := (= f3 f4)
    3.35 +#374 := (ite #10 #533 #542)
    3.36 +#37 := (:var 0 S2)
    3.37 +#35 := (:var 1 S4)
    3.38 +#34 := (:var 2 S2)
    3.39 +#33 := (:var 3 S3)
    3.40 +#36 := (f7 #33 #34 #35)
    3.41 +#38 := (f6 #36 #37)
    3.42 +#599 := (pattern #38)
    3.43 +#40 := (f6 #33 #37)
    3.44 +#100 := (= #38 #40)
    3.45 +#99 := (= #35 #38)
    3.46 +#82 := (= #34 #37)
    3.47 +#107 := (ite #82 #99 #100)
    3.48 +#600 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) (:pat #599) #107)
    3.49 +#95 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #107)
    3.50 +#603 := (iff #95 #600)
    3.51 +#601 := (iff #107 #107)
    3.52 +#602 := [refl]: #601
    3.53 +#604 := [quant-intro #602]: #603
    3.54 +#86 := (ite #82 #35 #40)
    3.55 +#89 := (= #38 #86)
    3.56 +#92 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #89)
    3.57 +#113 := (iff #92 #95)
    3.58 +#108 := (iff #89 #107)
    3.59 +#98 := [rewrite]: #108
    3.60 +#114 := [quant-intro #98]: #113
    3.61 +#105 := (~ #92 #92)
    3.62 +#104 := (~ #89 #89)
    3.63 +#101 := [refl]: #104
    3.64 +#106 := [nnf-pos #101]: #105
    3.65 +#39 := (= #37 #34)
    3.66 +#41 := (ite #39 #35 #40)
    3.67 +#42 := (= #38 #41)
    3.68 +#43 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #42)
    3.69 +#93 := (iff #43 #92)
    3.70 +#90 := (iff #42 #89)
    3.71 +#87 := (= #41 #86)
    3.72 +#84 := (iff #39 #82)
    3.73 +#85 := [rewrite]: #84
    3.74 +#88 := [monotonicity #85]: #87
    3.75 +#91 := [monotonicity #88]: #90
    3.76 +#94 := [quant-intro #91]: #93
    3.77 +#81 := [asserted]: #43
    3.78 +#97 := [mp #81 #94]: #92
    3.79 +#102 := [mp~ #97 #106]: #92
    3.80 +#115 := [mp #102 #114]: #95
    3.81 +#605 := [mp #115 #604]: #600
    3.82 +#251 := (not #600)
    3.83 +#530 := (or #251 #374)
    3.84 +#534 := (= f4 f3)
    3.85 +#540 := (ite #534 #533 #539)
    3.86 +#531 := (or #251 #540)
    3.87 +#532 := (iff #531 #530)
    3.88 +#415 := (iff #530 #530)
    3.89 +#416 := [rewrite]: #415
    3.90 +#527 := (iff #540 #374)
    3.91 +#371 := (iff #539 #542)
    3.92 +#373 := [rewrite]: #371
    3.93 +#541 := (iff #534 #10)
    3.94 +#535 := [rewrite]: #541
    3.95 +#528 := [monotonicity #535 #373]: #527
    3.96 +#414 := [monotonicity #528]: #532
    3.97 +#375 := [trans #414 #416]: #532
    3.98 +#529 := [quant-inst]: #531
    3.99 +#523 := [mp #529 #375]: #530
   3.100 +#526 := [unit-resolution #523 #605]: #374
   3.101 +#425 := (not #374)
   3.102 +#513 := (or #425 #542)
   3.103 +#11 := (not #10)
   3.104 +#13 := (= f3 f5)
   3.105 +#14 := (not #13)
   3.106 +#15 := (and #11 #14)
   3.107 +#61 := (not #15)
   3.108 +#62 := (or #61 #23)
   3.109 +#65 := (not #62)
   3.110 +#24 := (implies #15 #23)
   3.111 +#25 := (not #24)
   3.112 +#66 := (iff #25 #65)
   3.113 +#63 := (iff #24 #62)
   3.114 +#64 := [rewrite]: #63
   3.115 +#67 := [monotonicity #64]: #66
   3.116 +#60 := [asserted]: #25
   3.117 +#70 := [mp #60 #67]: #65
   3.118 +#68 := [not-or-elim #70]: #15
   3.119 +#69 := [and-elim #68]: #11
   3.120 +#524 := (or #425 #10 #542)
   3.121 +#409 := [def-axiom]: #524
   3.122 +#515 := [unit-resolution #409 #69]: #513
   3.123 +#507 := [unit-resolution #515 #526]: #542
   3.124 +#509 := [symm #507]: #539
   3.125 +#510 := (= #21 #538)
   3.126 +#264 := (f6 #18 f3)
   3.127 +#519 := (= #264 #538)
   3.128 +#518 := (= #538 #264)
   3.129 +#525 := (= #570 #18)
   3.130 +#431 := (= #173 f9)
   3.131 +#260 := (= f9 #173)
   3.132 +#28 := (:var 0 S4)
   3.133 +#27 := (:var 1 S2)
   3.134 +#26 := (:var 2 S3)
   3.135 +#29 := (f7 #26 #27 #28)
   3.136 +#591 := (pattern #29)
   3.137 +#30 := (f6 #29 #27)
   3.138 +#75 := (= #28 #30)
   3.139 +#593 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #591) #75)
   3.140 +#78 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #75)
   3.141 +#592 := (iff #78 #593)
   3.142 +#595 := (iff #593 #593)
   3.143 +#596 := [rewrite]: #595
   3.144 +#594 := [rewrite]: #592
   3.145 +#597 := [trans #594 #596]: #592
   3.146 +#111 := (~ #78 #78)
   3.147 +#109 := (~ #75 #75)
   3.148 +#110 := [refl]: #109
   3.149 +#112 := [nnf-pos #110]: #111
   3.150 +#31 := (= #30 #28)
   3.151 +#32 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #31)
   3.152 +#79 := (iff #32 #78)
   3.153 +#76 := (iff #31 #75)
   3.154 +#77 := [rewrite]: #76
   3.155 +#80 := [quant-intro #77]: #79
   3.156 +#74 := [asserted]: #32
   3.157 +#83 := [mp #74 #80]: #78
   3.158 +#103 := [mp~ #83 #112]: #78
   3.159 +#598 := [mp #103 #597]: #593
   3.160 +#175 := (not #593)
   3.161 +#262 := (or #175 #260)
   3.162 +#253 := [quant-inst]: #262
   3.163 +#430 := [unit-resolution #253 #598]: #260
   3.164 +#432 := [symm #430]: #431
   3.165 +#522 := [monotonicity #432]: #525
   3.166 +#514 := [monotonicity #522]: #518
   3.167 +#508 := [symm #514]: #519
   3.168 +#265 := (= #21 #264)
   3.169 +#263 := (= f10 #21)
   3.170 +#240 := (ite #13 #263 #265)
   3.171 +#252 := (or #251 #240)
   3.172 +#267 := (= f5 f3)
   3.173 +#246 := (ite #267 #263 #265)
   3.174 +#586 := (or #251 #246)
   3.175 +#588 := (iff #586 #252)
   3.176 +#584 := (iff #252 #252)
   3.177 +#590 := [rewrite]: #584
   3.178 +#372 := (iff #246 #240)
   3.179 +#583 := (iff #267 #13)
   3.180 +#585 := [rewrite]: #583
   3.181 +#579 := [monotonicity #585]: #372
   3.182 +#589 := [monotonicity #579]: #588
   3.183 +#580 := [trans #589 #590]: #588
   3.184 +#587 := [quant-inst]: #586
   3.185 +#238 := [mp #587 #580]: #252
   3.186 +#504 := [unit-resolution #238 #605]: #240
   3.187 +#243 := (not #240)
   3.188 +#506 := (or #243 #265)
   3.189 +#71 := [and-elim #68]: #14
   3.190 +#582 := (or #243 #13 #265)
   3.191 +#223 := [def-axiom]: #582
   3.192 +#516 := [unit-resolution #223 #71]: #506
   3.193 +#517 := [unit-resolution #516 #504]: #265
   3.194 +#511 := [trans #517 #508]: #510
   3.195 +#505 := [trans #511 #509]: #23
   3.196 +#72 := (not #23)
   3.197 +#73 := [not-or-elim #70]: #72
   3.198 +[unit-resolution #73 #505]: false
   3.199 +unsat

     4.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 14:58:45 2010 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 16:29:33 2010 +0200
     4.3 @@ -391,7 +391,7 @@
     4.4    fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
     4.5      let val n = fst (Term.dest_Free (Thm.term_of cv))
     4.6      in conv (Symtab.update (free n, 0) tb) cx end)
     4.7 -  val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)}
     4.8 +  val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
     4.9  in
    4.10  fun explicit_application ctxt thms =
    4.11    let
    4.12 @@ -404,12 +404,12 @@
    4.13      and app_conv tb n i ctxt =
    4.14        (case Symtab.lookup tb n of
    4.15          NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
    4.16 -      | SOME j => apply_conv tb ctxt (i - j))
    4.17 -    and apply_conv tb ctxt i ct = (
    4.18 +      | SOME j => fun_app_conv tb ctxt (i - j))
    4.19 +    and fun_app_conv tb ctxt i ct = (
    4.20        if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
    4.21        else
    4.22 -        Conv.rewr_conv apply_rule then_conv
    4.23 -        binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
    4.24 +        Conv.rewr_conv fun_app_rule then_conv
    4.25 +        binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
    4.26  
    4.27      fun needs_exp_app tab = Term.exists_subterm (fn
    4.28          Bound _ $ _ => true

     5.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Thu May 27 14:58:45 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Thu May 27 16:29:33 2010 +0200
     5.3 @@ -192,7 +192,7 @@
     5.4    | mk_distinct (cts as (ct :: _)) =
     5.5        Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
     5.6  
     5.7 -val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
     5.8 +val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_app}
     5.9  fun mk_access array index =
    5.10    let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
    5.11    in Thm.mk_binop (instTs cTs access) array index end

     6.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Thu May 27 14:58:45 2010 +0200
     6.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Thu May 27 16:29:33 2010 +0200
     6.3 @@ -122,7 +122,7 @@
     6.4    | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
     6.5  
     6.6  fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
     6.7 -fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u
     6.8 +fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
     6.9    | mk_eq t (us, u) = mk_eq' t us u
    6.10  
    6.11  fun translate (t, cs) =