# HG changeset patch
# User boehmes
# Date 1274970573 -7200
# Node ID 8feed34275ce1498bd9d8202e38c93f1d14e1d40
# Parent  f309fd16a0bdf7098bb7b6ca81da506067b03994
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

diff -r f309fd16a0bd -r 8feed34275ce src/HOL/Boogie/Examples/Boogie_Dijkstra.certs
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Thu May 27 16:29:33 2010 +0200
@@ -1,4 +1,4 @@
-2d5ecda945177c32dc13189db42e7a2391a39390 6889 0
+b3c5003cf9ccaad1080e68445c705767d58e45ae 6889 0
 #2 := false
 decl f11 :: (-> S5 S2 S1)
 decl ?v1!7 :: (-> S2 S2)
diff -r f309fd16a0bd -r 8feed34275ce src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/SMT.thy	Thu May 27 16:29:33 2010 +0200
@@ -59,7 +59,7 @@
 following constant.
 *}
 
-definition "apply" where "apply f x = f x"
+definition fun_app where "fun_app f x = f x"
 
 text {*
 Some solvers support a theory of arrays which can be used to encode
@@ -314,7 +314,7 @@
 
 
 hide_type (open) pattern
-hide_const Pattern "apply" term_eq
-hide_const (open) trigger pat nopat z3div z3mod
+hide_const Pattern term_eq
+hide_const (open) trigger pat nopat fun_app z3div z3mod
 
 end
diff -r f309fd16a0bd -r 8feed34275ce src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Thu May 27 16:29:33 2010 +0200
@@ -16193,3 +16193,196 @@
 #615 := [unit-resolution #638 #1762]: #367
 [unit-resolution #615 #1764]: false
 unsat
+0906dd207f0c510ad6c7f80b2056a8b625974f5b 192 0
+#2 := false
+decl f6 :: (-> S3 S2 S4)
+decl f3 :: S2
+#8 := f3
+decl f8 :: S3
+#16 := f8
+#22 := (f6 f8 f3)
+decl f7 :: (-> S3 S2 S4 S3)
+decl f10 :: S4
+#19 := f10
+decl f5 :: S2
+#12 := f5
+decl f9 :: S4
+#17 := f9
+decl f4 :: S2
+#9 := f4
+#18 := (f7 f8 f4 f9)
+#20 := (f7 #18 f5 f10)
+#21 := (f6 #20 f3)
+#23 := (= #21 #22)
+#173 := (f6 #18 f4)
+#570 := (f7 f8 f4 #173)
+#538 := (f6 #570 f3)
+#539 := (= #538 #22)
+#542 := (= #22 #538)
+#533 := (= #173 #538)
+#10 := (= f3 f4)
+#374 := (ite #10 #533 #542)
+#37 := (:var 0 S2)
+#35 := (:var 1 S4)
+#34 := (:var 2 S2)
+#33 := (:var 3 S3)
+#36 := (f7 #33 #34 #35)
+#38 := (f6 #36 #37)
+#599 := (pattern #38)
+#40 := (f6 #33 #37)
+#100 := (= #38 #40)
+#99 := (= #35 #38)
+#82 := (= #34 #37)
+#107 := (ite #82 #99 #100)
+#600 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) (:pat #599) #107)
+#95 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #107)
+#603 := (iff #95 #600)
+#601 := (iff #107 #107)
+#602 := [refl]: #601
+#604 := [quant-intro #602]: #603
+#86 := (ite #82 #35 #40)
+#89 := (= #38 #86)
+#92 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #89)
+#113 := (iff #92 #95)
+#108 := (iff #89 #107)
+#98 := [rewrite]: #108
+#114 := [quant-intro #98]: #113
+#105 := (~ #92 #92)
+#104 := (~ #89 #89)
+#101 := [refl]: #104
+#106 := [nnf-pos #101]: #105
+#39 := (= #37 #34)
+#41 := (ite #39 #35 #40)
+#42 := (= #38 #41)
+#43 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4) (?v3 S2)) #42)
+#93 := (iff #43 #92)
+#90 := (iff #42 #89)
+#87 := (= #41 #86)
+#84 := (iff #39 #82)
+#85 := [rewrite]: #84
+#88 := [monotonicity #85]: #87
+#91 := [monotonicity #88]: #90
+#94 := [quant-intro #91]: #93
+#81 := [asserted]: #43
+#97 := [mp #81 #94]: #92
+#102 := [mp~ #97 #106]: #92
+#115 := [mp #102 #114]: #95
+#605 := [mp #115 #604]: #600
+#251 := (not #600)
+#530 := (or #251 #374)
+#534 := (= f4 f3)
+#540 := (ite #534 #533 #539)
+#531 := (or #251 #540)
+#532 := (iff #531 #530)
+#415 := (iff #530 #530)
+#416 := [rewrite]: #415
+#527 := (iff #540 #374)
+#371 := (iff #539 #542)
+#373 := [rewrite]: #371
+#541 := (iff #534 #10)
+#535 := [rewrite]: #541
+#528 := [monotonicity #535 #373]: #527
+#414 := [monotonicity #528]: #532
+#375 := [trans #414 #416]: #532
+#529 := [quant-inst]: #531
+#523 := [mp #529 #375]: #530
+#526 := [unit-resolution #523 #605]: #374
+#425 := (not #374)
+#513 := (or #425 #542)
+#11 := (not #10)
+#13 := (= f3 f5)
+#14 := (not #13)
+#15 := (and #11 #14)
+#61 := (not #15)
+#62 := (or #61 #23)
+#65 := (not #62)
+#24 := (implies #15 #23)
+#25 := (not #24)
+#66 := (iff #25 #65)
+#63 := (iff #24 #62)
+#64 := [rewrite]: #63
+#67 := [monotonicity #64]: #66
+#60 := [asserted]: #25
+#70 := [mp #60 #67]: #65
+#68 := [not-or-elim #70]: #15
+#69 := [and-elim #68]: #11
+#524 := (or #425 #10 #542)
+#409 := [def-axiom]: #524
+#515 := [unit-resolution #409 #69]: #513
+#507 := [unit-resolution #515 #526]: #542
+#509 := [symm #507]: #539
+#510 := (= #21 #538)
+#264 := (f6 #18 f3)
+#519 := (= #264 #538)
+#518 := (= #538 #264)
+#525 := (= #570 #18)
+#431 := (= #173 f9)
+#260 := (= f9 #173)
+#28 := (:var 0 S4)
+#27 := (:var 1 S2)
+#26 := (:var 2 S3)
+#29 := (f7 #26 #27 #28)
+#591 := (pattern #29)
+#30 := (f6 #29 #27)
+#75 := (= #28 #30)
+#593 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) (:pat #591) #75)
+#78 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #75)
+#592 := (iff #78 #593)
+#595 := (iff #593 #593)
+#596 := [rewrite]: #595
+#594 := [rewrite]: #592
+#597 := [trans #594 #596]: #592
+#111 := (~ #78 #78)
+#109 := (~ #75 #75)
+#110 := [refl]: #109
+#112 := [nnf-pos #110]: #111
+#31 := (= #30 #28)
+#32 := (forall (vars (?v0 S3) (?v1 S2) (?v2 S4)) #31)
+#79 := (iff #32 #78)
+#76 := (iff #31 #75)
+#77 := [rewrite]: #76
+#80 := [quant-intro #77]: #79
+#74 := [asserted]: #32
+#83 := [mp #74 #80]: #78
+#103 := [mp~ #83 #112]: #78
+#598 := [mp #103 #597]: #593
+#175 := (not #593)
+#262 := (or #175 #260)
+#253 := [quant-inst]: #262
+#430 := [unit-resolution #253 #598]: #260
+#432 := [symm #430]: #431
+#522 := [monotonicity #432]: #525
+#514 := [monotonicity #522]: #518
+#508 := [symm #514]: #519
+#265 := (= #21 #264)
+#263 := (= f10 #21)
+#240 := (ite #13 #263 #265)
+#252 := (or #251 #240)
+#267 := (= f5 f3)
+#246 := (ite #267 #263 #265)
+#586 := (or #251 #246)
+#588 := (iff #586 #252)
+#584 := (iff #252 #252)
+#590 := [rewrite]: #584
+#372 := (iff #246 #240)
+#583 := (iff #267 #13)
+#585 := [rewrite]: #583
+#579 := [monotonicity #585]: #372
+#589 := [monotonicity #579]: #588
+#580 := [trans #589 #590]: #588
+#587 := [quant-inst]: #586
+#238 := [mp #587 #580]: #252
+#504 := [unit-resolution #238 #605]: #240
+#243 := (not #240)
+#506 := (or #243 #265)
+#71 := [and-elim #68]: #14
+#582 := (or #243 #13 #265)
+#223 := [def-axiom]: #582
+#516 := [unit-resolution #223 #71]: #506
+#517 := [unit-resolution #516 #504]: #265
+#511 := [trans #517 #508]: #510
+#505 := [trans #511 #509]: #23
+#72 := (not #23)
+#73 := [not-or-elim #70]: #72
+[unit-resolution #73 #505]: false
+unsat
diff -r f309fd16a0bd -r 8feed34275ce src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu May 27 16:29:33 2010 +0200
@@ -391,7 +391,7 @@
   fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
     let val n = fst (Term.dest_Free (Thm.term_of cv))
     in conv (Symtab.update (free n, 0) tb) cx end)
-  val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)}
+  val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
 in
 fun explicit_application ctxt thms =
   let
@@ -404,12 +404,12 @@
     and app_conv tb n i ctxt =
       (case Symtab.lookup tb n of
         NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
-      | SOME j => apply_conv tb ctxt (i - j))
-    and apply_conv tb ctxt i ct = (
+      | SOME j => fun_app_conv tb ctxt (i - j))
+    and fun_app_conv tb ctxt i ct = (
       if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
       else
-        Conv.rewr_conv apply_rule then_conv
-        binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
+        Conv.rewr_conv fun_app_rule then_conv
+        binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
 
     fun needs_exp_app tab = Term.exists_subterm (fn
         Bound _ $ _ => true
diff -r f309fd16a0bd -r 8feed34275ce src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Thu May 27 16:29:33 2010 +0200
@@ -192,7 +192,7 @@
   | mk_distinct (cts as (ct :: _)) =
       Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
 
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
+val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_app}
 fun mk_access array index =
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
   in Thm.mk_binop (instTs cTs access) array index end
diff -r f309fd16a0bd -r 8feed34275ce src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML	Thu May 27 16:29:33 2010 +0200
@@ -122,7 +122,7 @@
   | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
 
 fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
-fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u
+fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
   | mk_eq t (us, u) = mk_eq' t us u
 
 fun translate (t, cs) =