merged

--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 10:30:33 2011 -0700
@@ -60074,3 +60074,483 @@
 #110 := [asserted]: #38
 [mp #110 #120]: false
 unsat
+8021f8e09eb3e47791aed2bed0dafccd5948187d 69 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#16 := f5
+#19 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #19)
+#70 := (not #66)
+#20 := (= #19 f1)
+#21 := (not #20)
+#71 := (iff #21 #70)
+#68 := (iff #20 #66)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#65 := [asserted]: #21
+#75 := [mp #65 #72]: #70
+decl f3 :: (-> S2 S1)
+#17 := (f3 f5)
+#61 := (= f1 #17)
+#18 := (= #17 f1)
+#63 := (iff #18 #61)
+#64 := [rewrite]: #63
+#60 := [asserted]: #18
+#67 := [mp #60 #64]: #61
+#8 := (:var 0 S2)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#12 := (f4 #8)
+#45 := (= f1 #12)
+#42 := (= f1 #9)
+#51 := (not #42)
+#52 := (or #51 #45)
+#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
+#85 := (~ #57 #57)
+#83 := (~ #52 #52)
+#84 := [refl]: #83
+#86 := [nnf-pos #84]: #85
+#13 := (= #12 f1)
+#11 := (= #9 f1)
+#14 := (implies #11 #13)
+#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
+#58 := (iff #15 #57)
+#55 := (iff #14 #52)
+#48 := (implies #42 #45)
+#53 := (iff #48 #52)
+#54 := [rewrite]: #53
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#47 := [rewrite]: #46
+#43 := (iff #11 #42)
+#44 := [rewrite]: #43
+#50 := [monotonicity #44 #47]: #49
+#56 := [trans #50 #54]: #55
+#59 := [quant-intro #56]: #58
+#41 := [asserted]: #15
+#62 := [mp #41 #59]: #57
+#74 := [mp~ #62 #86]: #57
+#137 := (not #61)
+#139 := (not #57)
+#226 := (or #139 #137 #66)
+#224 := (or #137 #66)
+#217 := (or #139 #224)
+#229 := (iff #217 #226)
+#157 := [rewrite]: #229
+#228 := [quant-inst #16]: #217
+#230 := [mp #228 #157]: #226
+[unit-resolution #230 #74 #67 #75]: false
+unsat
+51102b6663906c70b84f1c6e3a1a2e429b49188d 112 0
+#2 := false
+decl f5 :: (-> S2 S1)
+decl f6 :: S2
+#19 := f6
+#24 := (f5 f6)
+decl f1 :: S1
+#4 := f1
+#82 := (= f1 #24)
+#86 := (not #82)
+#25 := (= #24 f1)
+#26 := (not #25)
+#87 := (iff #26 #86)
+#84 := (iff #25 #82)
+#85 := [rewrite]: #84
+#88 := [monotonicity #85]: #87
+#81 := [asserted]: #26
+#91 := [mp #81 #88]: #86
+decl f4 :: (-> S2 S1)
+#22 := (f4 f6)
+#77 := (= f1 #22)
+#23 := (= #22 f1)
+#79 := (iff #23 #77)
+#80 := [rewrite]: #79
+#76 := [asserted]: #23
+#83 := [mp #76 #80]: #77
+decl f3 :: (-> S2 S1)
+#20 := (f3 f6)
+#72 := (= f1 #20)
+#21 := (= #20 f1)
+#74 := (iff #21 #72)
+#75 := [rewrite]: #74
+#71 := [asserted]: #21
+#78 := [mp #71 #75]: #72
+#8 := (:var 0 S2)
+#10 := (f4 #8)
+#9 := (f3 #8)
+#11 := (pattern #9 #10)
+#15 := (f5 #8)
+#56 := (= f1 #15)
+#50 := (= f1 #10)
+#105 := (not #50)
+#47 := (= f1 #9)
+#92 := (not #47)
+#112 := (or #92 #105 #56)
+#117 := (forall (vars (?v0 S2)) (:pat #11) #112)
+#53 := (and #47 #50)
+#62 := (not #53)
+#63 := (or #62 #56)
+#68 := (forall (vars (?v0 S2)) (:pat #11) #63)
+#118 := (iff #68 #117)
+#115 := (iff #63 #112)
+#93 := (or #92 #105)
+#109 := (or #93 #56)
+#113 := (iff #109 #112)
+#114 := [rewrite]: #113
+#110 := (iff #63 #109)
+#107 := (iff #62 #93)
+#94 := (not #93)
+#97 := (not #94)
+#96 := (iff #97 #93)
+#106 := [rewrite]: #96
+#98 := (iff #62 #97)
+#99 := (iff #53 #94)
+#100 := [rewrite]: #99
+#95 := [monotonicity #100]: #98
+#108 := [trans #95 #106]: #107
+#111 := [monotonicity #108]: #110
+#116 := [trans #111 #114]: #115
+#119 := [quant-intro #116]: #118
+#103 := (~ #68 #68)
+#101 := (~ #63 #63)
+#102 := [refl]: #101
+#104 := [nnf-pos #102]: #103
+#16 := (= #15 f1)
+#13 := (= #10 f1)
+#12 := (= #9 f1)
+#14 := (and #12 #13)
+#17 := (implies #14 #16)
+#18 := (forall (vars (?v0 S2)) (:pat #11) #17)
+#69 := (iff #18 #68)
+#66 := (iff #17 #63)
+#59 := (implies #53 #56)
+#64 := (iff #59 #63)
+#65 := [rewrite]: #64
+#60 := (iff #17 #59)
+#57 := (iff #16 #56)
+#58 := [rewrite]: #57
+#54 := (iff #14 #53)
+#51 := (iff #13 #50)
+#52 := [rewrite]: #51
+#48 := (iff #12 #47)
+#49 := [rewrite]: #48
+#55 := [monotonicity #49 #52]: #54
+#61 := [monotonicity #55 #58]: #60
+#67 := [trans #61 #65]: #66
+#70 := [quant-intro #67]: #69
+#46 := [asserted]: #18
+#73 := [mp #46 #70]: #68
+#90 := [mp~ #73 #104]: #68
+#120 := [mp #90 #119]: #117
+#178 := (not #77)
+#265 := (not #72)
+#267 := (not #117)
+#258 := (or #267 #265 #178 #82)
+#179 := (or #265 #178 #82)
+#269 := (or #267 #179)
+#198 := (iff #269 #258)
+#271 := [rewrite]: #198
+#270 := [quant-inst #19]: #269
+#268 := [mp #270 #271]: #258
+[unit-resolution #268 #120 #78 #83 #91]: false
+unsat
+1191e209015c2f2f439f124434700d861e089600 149 0
+#2 := false
+decl f3 :: (-> S2 S1)
+decl f6 :: S2
+#21 := f6
+#22 := (f3 f6)
+decl f1 :: S1
+#4 := f1
+#84 := (= f1 #22)
+#264 := (not #84)
+decl f5 :: (-> S2 S1)
+#27 := (f5 f6)
+#95 := (= f1 #27)
+#178 := (or #264 #95)
+decl f4 :: (-> S2 S1)
+#24 := (f4 f6)
+#88 := (= f1 #24)
+#176 := (not #88)
+#268 := (or #176 #95)
+#266 := (not #268)
+#265 := (not #178)
+#586 := (or #265 #266)
+#375 := (not #586)
+#579 := [hypothesis]: #586
+#8 := (:var 0 S2)
+#11 := (f4 #8)
+#12 := (pattern #11)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#65 := (= f1 #11)
+#71 := (not #65)
+#14 := (f5 #8)
+#53 := (= f1 #14)
+#72 := (or #53 #71)
+#116 := (not #72)
+#50 := (= f1 #9)
+#59 := (not #50)
+#60 := (or #59 #53)
+#105 := (not #60)
+#106 := (or #105 #116)
+#107 := (not #106)
+#108 := (forall (vars (?v0 S2)) (:pat #10 #12) #107)
+#77 := (and #60 #72)
+#80 := (forall (vars (?v0 S2)) (:pat #10 #12) #77)
+#109 := (iff #80 #108)
+#110 := (iff #77 #107)
+#111 := [rewrite]: #110
+#117 := [quant-intro #111]: #109
+#114 := (~ #80 #80)
+#112 := (~ #77 #77)
+#113 := [refl]: #112
+#115 := [nnf-pos #113]: #114
+#15 := (= #14 f1)
+#17 := (= #11 f1)
+#18 := (implies #17 #15)
+#13 := (= #9 f1)
+#16 := (implies #13 #15)
+#19 := (and #16 #18)
+#20 := (forall (vars (?v0 S2)) (:pat #10 #12) #19)
+#81 := (iff #20 #80)
+#78 := (iff #19 #77)
+#75 := (iff #18 #72)
+#68 := (implies #65 #53)
+#73 := (iff #68 #72)
+#74 := [rewrite]: #73
+#69 := (iff #18 #68)
+#54 := (iff #15 #53)
+#55 := [rewrite]: #54
+#66 := (iff #17 #65)
+#67 := [rewrite]: #66
+#70 := [monotonicity #67 #55]: #69
+#76 := [trans #70 #74]: #75
+#63 := (iff #16 #60)
+#56 := (implies #50 #53)
+#61 := (iff #56 #60)
+#62 := [rewrite]: #61
+#57 := (iff #16 #56)
+#51 := (iff #13 #50)
+#52 := [rewrite]: #51
+#58 := [monotonicity #52 #55]: #57
+#64 := [trans #58 #62]: #63
+#79 := [monotonicity #64 #76]: #78
+#82 := [quant-intro #79]: #81
+#49 := [asserted]: #20
+#85 := [mp #49 #82]: #80
+#103 := [mp~ #85 #115]: #80
+#118 := [mp #103 #117]: #108
+#255 := (not #108)
+#589 := (or #255 #375)
+#263 := (or #95 #176)
+#177 := (not #263)
+#256 := (or #265 #177)
+#267 := (not #256)
+#590 := (or #255 #267)
+#592 := (iff #590 #589)
+#593 := (iff #589 #589)
+#583 := [rewrite]: #593
+#582 := (iff #267 #375)
+#588 := (iff #256 #586)
+#270 := (iff #177 #266)
+#196 := (iff #263 #268)
+#269 := [rewrite]: #196
+#249 := [monotonicity #269]: #270
+#243 := [monotonicity #249]: #588
+#254 := [monotonicity #243]: #582
+#587 := [monotonicity #254]: #592
+#241 := [trans #587 #583]: #592
+#591 := [quant-inst #21]: #590
+#246 := [mp #591 #241]: #589
+#217 := [unit-resolution #246 #118 #579]: false
+#218 := [lemma #217]: #375
+#574 := (or #586 #178)
+#575 := [def-axiom]: #574
+#580 := [unit-resolution #575 #218]: #178
+#578 := (or #265 #264)
+#99 := (not #95)
+#28 := (= #27 f1)
+#29 := (not #28)
+#100 := (iff #29 #99)
+#97 := (iff #28 #95)
+#98 := [rewrite]: #97
+#101 := [monotonicity #98]: #100
+#94 := [asserted]: #29
+#104 := [mp #94 #101]: #99
+#569 := (or #265 #264 #95)
+#230 := [def-axiom]: #569
+#581 := [unit-resolution #230 #104]: #578
+#567 := [unit-resolution #581 #580]: #264
+#570 := (or #586 #268)
+#576 := [def-axiom]: #570
+#568 := [unit-resolution #576 #218]: #268
+#274 := (or #266 #176)
+#572 := (or #266 #176 #95)
+#573 := [def-axiom]: #572
+#290 := [unit-resolution #573 #104]: #274
+#291 := [unit-resolution #290 #568]: #176
+#91 := (or #84 #88)
+#25 := (= #24 f1)
+#23 := (= #22 f1)
+#26 := (or #23 #25)
+#92 := (iff #26 #91)
+#89 := (iff #25 #88)
+#90 := [rewrite]: #89
+#86 := (iff #23 #84)
+#87 := [rewrite]: #86
+#93 := [monotonicity #87 #90]: #92
+#83 := [asserted]: #26
+#96 := [mp #83 #93]: #91
+[unit-resolution #96 #291 #567]: false
+unsat
+45f8ffe676ed981a383aaab6faaf520b9ff236c9 69 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#16 := f5
+#19 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #19)
+#70 := (not #66)
+#20 := (= #19 f1)
+#21 := (not #20)
+#71 := (iff #21 #70)
+#68 := (iff #20 #66)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#65 := [asserted]: #21
+#75 := [mp #65 #72]: #70
+decl f3 :: (-> S2 S1)
+#17 := (f3 f5)
+#61 := (= f1 #17)
+#18 := (= #17 f1)
+#63 := (iff #18 #61)
+#64 := [rewrite]: #63
+#60 := [asserted]: #18
+#67 := [mp #60 #64]: #61
+#8 := (:var 0 S2)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#12 := (f4 #8)
+#45 := (= f1 #12)
+#42 := (= f1 #9)
+#51 := (not #42)
+#52 := (or #51 #45)
+#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
+#85 := (~ #57 #57)
+#83 := (~ #52 #52)
+#84 := [refl]: #83
+#86 := [nnf-pos #84]: #85
+#13 := (= #12 f1)
+#11 := (= #9 f1)
+#14 := (implies #11 #13)
+#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
+#58 := (iff #15 #57)
+#55 := (iff #14 #52)
+#48 := (implies #42 #45)
+#53 := (iff #48 #52)
+#54 := [rewrite]: #53
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#47 := [rewrite]: #46
+#43 := (iff #11 #42)
+#44 := [rewrite]: #43
+#50 := [monotonicity #44 #47]: #49
+#56 := [trans #50 #54]: #55
+#59 := [quant-intro #56]: #58
+#41 := [asserted]: #15
+#62 := [mp #41 #59]: #57
+#74 := [mp~ #62 #86]: #57
+#137 := (not #61)
+#139 := (not #57)
+#226 := (or #139 #137 #66)
+#224 := (or #137 #66)
+#217 := (or #139 #224)
+#229 := (iff #217 #226)
+#157 := [rewrite]: #229
+#228 := [quant-inst #16]: #217
+#230 := [mp #228 #157]: #226
+[unit-resolution #230 #74 #67 #75]: false
+unsat
+ceabafba9f0db45264556e8d9525b667725281c7 76 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#15 := f5
+#18 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#65 := (= f1 #18)
+#69 := (not #65)
+#19 := (= #18 f1)
+#20 := (not #19)
+#70 := (iff #20 #69)
+#67 := (iff #19 #65)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#64 := [asserted]: #20
+#74 := [mp #64 #71]: #69
+decl f3 :: (-> S2 S1)
+#16 := (f3 f5)
+#60 := (= f1 #16)
+#17 := (= #16 f1)
+#62 := (iff #17 #60)
+#63 := [rewrite]: #62
+#59 := [asserted]: #17
+#66 := [mp #59 #63]: #60
+#8 := (:var 0 S2)
+#11 := (f4 #8)
+#555 := (pattern #11)
+#9 := (f3 #8)
+#554 := (pattern #9)
+#44 := (= f1 #11)
+#41 := (= f1 #9)
+#50 := (not #41)
+#51 := (or #50 #44)
+#556 := (forall (vars (?v0 S2)) (:pat #554 #555) #51)
+#56 := (forall (vars (?v0 S2)) #51)
+#559 := (iff #56 #556)
+#557 := (iff #51 #51)
+#558 := [refl]: #557
+#560 := [quant-intro #558]: #559
+#84 := (~ #56 #56)
+#82 := (~ #51 #51)
+#83 := [refl]: #82
+#85 := [nnf-pos #83]: #84
+#12 := (= #11 f1)
+#10 := (= #9 f1)
+#13 := (implies #10 #12)
+#14 := (forall (vars (?v0 S2)) #13)
+#57 := (iff #14 #56)
+#54 := (iff #13 #51)
+#47 := (implies #41 #44)
+#52 := (iff #47 #51)
+#53 := [rewrite]: #52
+#48 := (iff #13 #47)
+#45 := (iff #12 #44)
+#46 := [rewrite]: #45
+#42 := (iff #10 #41)
+#43 := [rewrite]: #42
+#49 := [monotonicity #43 #46]: #48
+#55 := [trans #49 #53]: #54
+#58 := [quant-intro #55]: #57
+#40 := [asserted]: #14
+#61 := [mp #40 #58]: #56
+#73 := [mp~ #61 #85]: #56
+#561 := [mp #73 #560]: #556
+#136 := (not #60)
+#138 := (not #556)
+#225 := (or #138 #136 #65)
+#223 := (or #136 #65)
+#216 := (or #138 #223)
+#228 := (iff #216 #225)
+#156 := [rewrite]: #228
+#227 := [quant-inst #15]: #216
+#229 := [mp #227 #156]: #225
+[unit-resolution #229 #561 #66 #74]: false
+unsat

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 10:30:33 2011 -0700
@@ -201,6 +201,9 @@
   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   by smt+
 
+
+section {* Guidance for quantifier heuristics: patterns and weights *}
+
 lemma
   assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
   shows "f 1 = 1"
@@ -211,6 +214,38 @@
   shows "f 1 = g 2"
   using assms by smt
 
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x), SMT.pat (Q x)]]
+    (P x & Q x --> R x)"
+  and "P t" and "Q t"
+  shows "R t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)], [SMT.pat (Q x)]]
+    ((P x --> R x) & (Q x --> R x))"
+  and "P t | Q t"
+  shows "R t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (SMT.weight 2 (P x --> Q x))"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.weight 1 (P x --> Q x)"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
 
 
 section {* Meta logical connectives *}

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 10:30:33 2011 -0700
@@ -22,15 +22,15 @@
     AFun of 'a ho_type * 'a ho_type |
     ATyAbs of 'a list * 'a ho_type
 
-  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
-  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+  datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+  datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
   datatype thf_flavor = THF_Without_Choice | THF_With_Choice
-  datatype format =
+  datatype tptp_format =
     CNF |
     CNF_UEQ |
     FOF |
-    TFF of tff_polymorphism * tff_explicitness |
-    THF0 of thf_flavor
+    TFF of tptp_polymorphism * tptp_explicitness |
+    THF of tptp_polymorphism * tptp_explicitness * thf_flavor
 
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
@@ -92,9 +92,9 @@
     bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
     -> 'd -> 'd
   val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
-  val is_format_thf : format -> bool
-  val is_format_typed : format -> bool
-  val tptp_lines_for_atp_problem : format -> string problem -> string list
+  val is_format_thf : tptp_format -> bool
+  val is_format_typed : tptp_format -> bool
+  val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
   val ensure_cnf_problem :
     (string * string) problem -> (string * string) problem
   val filter_cnf_ueq_problem :
@@ -130,16 +130,16 @@
   AFun of 'a ho_type * 'a ho_type |
   ATyAbs of 'a list * 'a ho_type
 
-datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
-datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
+datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
 
-datatype format =
+datatype tptp_format =
   CNF |
   CNF_UEQ |
   FOF |
-  TFF of tff_polymorphism * tff_explicitness |
-  THF0 of thf_flavor
+  TFF of tptp_polymorphism * tptp_explicitness |
+  THF of tptp_polymorphism * tptp_explicitness * thf_flavor
 
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
@@ -224,10 +224,10 @@
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)
 
-fun is_format_thf (THF0 _) = true
+fun is_format_thf (THF _) = true
   | is_format_thf _ = false
 fun is_format_typed (TFF _) = true
-  | is_format_typed (THF0 _) = true
+  | is_format_typed (THF _) = true
   | is_format_typed _ = false
 
 fun string_for_kind Axiom = "axiom"
@@ -266,7 +266,7 @@
                     ss) ^ "]: " ^ str false ty
   in str true ty end
 
-fun string_for_type (THF0 _) ty = str_for_type ty
+fun string_for_type (THF _) ty = str_for_type ty
   | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
   | string_for_type _ _ = raise Fail "unexpected type in untyped format"
 
@@ -288,6 +288,9 @@
    else
      "")
 
+fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
+  | is_format_with_choice _ = false
+
 fun string_for_term _ (ATerm (s, [])) = s
   | string_for_term format (ATerm (s, ts)) =
     if s = tptp_empty_list then
@@ -298,7 +301,7 @@
       |> is_format_thf format ? enclose "(" ")"
     else
       (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
-             s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
+             s = tptp_choice andalso is_format_with_choice format, ts) of
          (true, _, [AAbs ((s', ty), tm)]) =>
          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
             possible, to work around LEO-II 1.2.8 parser limitation. *)
@@ -306,8 +309,8 @@
              (AQuant (if s = tptp_ho_forall then AForall else AExists,
                       [(s', SOME ty)], AAtom tm))
        | (_, true, [AAbs ((s', ty), tm)]) =>
-         (*There is code in ATP_Translate to ensure that Eps is always applied
-           to an abstraction*)
+         (* There is code in "ATP_Translate" to ensure that "Eps" is always
+            applied to an abstraction. *)
          tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
            string_for_term format tm ^ ""
          |> enclose "(" ")"
@@ -319,7 +322,7 @@
            else
              s ^ "(" ^ commas ss ^ ")"
          end)
-  | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
+  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
     "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
     string_for_term format tm ^ ")"
   | string_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -352,7 +355,7 @@
   | string_for_format CNF_UEQ = tptp_cnf
   | string_for_format FOF = tptp_fof
   | string_for_format (TFF _) = tptp_tff
-  | string_for_format (THF0 _) = tptp_thf
+  | string_for_format (THF _) = tptp_thf
 
 fun string_for_problem_line format (Decl (ident, sym, ty)) =
     string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 10:30:33 2011 -0700
@@ -7,7 +7,7 @@
 
 signature ATP_SYSTEMS =
 sig
-  type format = ATP_Problem.format
+  type tptp_format = ATP_Problem.tptp_format
   type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
@@ -22,7 +22,8 @@
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
-       Proof.context -> (real * (bool * (int * format * string * string))) list}
+       Proof.context
+       -> (real * (bool * (int * tptp_format * string * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
@@ -41,6 +42,7 @@
   val e_tofofN : string
   val leo2N : string
   val pffN : string
+  val phfN : string
   val satallaxN : string
   val snarkN : string
   val spassN : string
@@ -51,7 +53,7 @@
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (failure * string) list -> formula_kind -> formula_kind
-    -> (Proof.context -> int * format * string) -> string * atp_config
+    -> (Proof.context -> int * tptp_format * string) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -79,7 +81,8 @@
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
    best_slices :
-     Proof.context -> (real * (bool * (int * format * string * string))) list}
+     Proof.context
+     -> (real * (bool * (int * tptp_format * string * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" components give the faction of the
@@ -105,6 +108,7 @@
 val e_tofofN = "e_tofof"
 val leo2N = "leo2"
 val pffN = "pff"
+val phfN = "phf"
 val satallaxN = "satallax"
 val snarkN = "snark"
 val spassN = "spass"
@@ -230,6 +234,8 @@
 
 (* LEO-II *)
 
+val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
+
 val leo2_config : atp_config =
   {exec = ("LEO2_HOME", "leo"),
    required_execs = [],
@@ -243,10 +249,8 @@
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, THF0 THF_Without_Choice,
-                       "mono_simple_higher", sosN))),
-      (0.333, (true, (50, THF0 THF_Without_Choice,
-                      "mono_simple_higher", no_sosN)))]
+     [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
+      (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -255,6 +259,8 @@
 
 (* Satallax *)
 
+val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
+
 val satallax_config : atp_config =
   {exec = ("SATALLAX_HOME", "satallax"),
    required_execs = [],
@@ -266,8 +272,8 @@
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
-     K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
-     (* FUDGE *)}
+     (* FUDGE *)
+     K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
 
 val satallax = (satallaxN, satallax_config)
 
@@ -314,7 +320,7 @@
 fun is_old_vampire_version () =
   string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
 
-val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
 
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
@@ -347,9 +353,9 @@
          (0.333, (false, (500, FOF, "mono_tags?", sosN))),
          (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
       else
-        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
-         (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
-         (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
+        [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
+         (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
+         (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -358,7 +364,7 @@
 
 (* Z3 with TPTP syntax *)
 
-val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
+val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
 
 val z3_tptp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
@@ -377,18 +383,17 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
-        (0.25, (false, (125, z3_tff, "mono_simple", ""))),
-        (0.125, (false, (62, z3_tff, "mono_simple", ""))),
-        (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
+     K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
+        (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
+        (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
+        (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
-(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
 
-val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
+(* Not really a prover: Experimental Polymorphic TFF and THF output *)
 
-val pff_config : atp_config =
+fun dummy_config format type_enc : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
    required_execs = [],
    arguments = K (K (K (K (K "")))),
@@ -396,10 +401,16 @@
    known_failures = [(GaveUp, "SZS status Unknown")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
-   best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
+   best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
 
+val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
+val pff_config = dummy_config pff_format "poly_simple"
 val pff = (pffN, pff_config)
 
+val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
+val phf_config = dummy_config phf_format "poly_simple_higher"
+val phf = (phfN, phf_config)
+
 
 (* Remote ATP invocation via SystemOnTPTP *)
 
@@ -475,34 +486,33 @@
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice config)
 
-val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
+val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
                (K (750, FOF, "mono_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-               (K (100, THF0 THF_Without_Choice,
-                   "mono_simple_higher") (* FUDGE *))
+               (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-               (K (100, THF0 THF_With_Choice,
-                   "mono_simple_higher") (* FUDGE *))
+               (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
                (K (250, FOF, "mono_guards?") (* FUDGE *))
 val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
+  remotify_atp z3_tptp "Z3" ["3.0"]
+               (K (250, z3_tff0, "mono_simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             (K (100, dumb_tff, "mono_simple") (* FUDGE *))
+             (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
-             Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
+             Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]
@@ -532,7 +542,7 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+  [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
    remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
    remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 10:30:33 2011 -0700
@@ -11,7 +11,7 @@
   type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
   type connective = ATP_Problem.connective
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
-  type format = ATP_Problem.format
+  type tptp_format = ATP_Problem.tptp_format
   type formula_kind = ATP_Problem.formula_kind
   type 'a problem = 'a ATP_Problem.problem
 
@@ -92,7 +92,7 @@
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_quasi_sound : type_enc -> bool
   val is_type_enc_fairly_sound : type_enc -> bool
-  val adjust_type_enc : format -> type_enc -> type_enc
+  val adjust_type_enc : tptp_format -> type_enc -> type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -100,7 +100,7 @@
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> format -> formula_kind -> formula_kind -> type_enc
+    Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
     -> bool -> string -> bool -> bool -> term list -> term
     -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
@@ -142,7 +142,7 @@
 (* TFF1 is still in development, and it is still unclear whether symbols will be
    allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
    "dummy" type variables. *)
-val exploit_tff1_dummy_type_vars = false
+val avoid_first_order_dummy_type_vars = true
 
 val bound_var_prefix = "B_"
 val all_bound_var_prefix = "BA_"
@@ -325,8 +325,8 @@
   fun default c = const_prefix ^ lookup_const c
 in
   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
-    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
-        if c = choice_const then tptp_choice else default c
+    | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
+      if c = choice_const then tptp_choice else default c
     | make_fixed_const _ c = default c
 end
 
@@ -587,7 +587,9 @@
             | _ => raise Same.SAME)
          | ("simple_higher", (SOME poly, _, Nonuniform)) =>
            (case (poly, level) of
-              (_, Noninf_Nonmono_Types _) => raise Same.SAME
+              (Polymorphic, All_Types) =>
+              Simple_Types (Higher_Order, Polymorphic, All_Types)
+            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
             | (Mangled_Monomorphic, _) =>
               Simple_Types (Higher_Order, Mangled_Monomorphic, level)
             | _ => raise Same.SAME)
@@ -631,12 +633,13 @@
   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   | is_type_level_monotonicity_based _ = false
 
-fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
+fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
+                    (Simple_Types (order, _, level)) =
     Simple_Types (order, Mangled_Monomorphic, level)
-  | adjust_type_enc (THF0 _) type_enc = type_enc
-  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
+  | adjust_type_enc (THF _) type_enc = type_enc
+  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
     Simple_Types (First_Order, Mangled_Monomorphic, level)
-  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
+  | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
     Simple_Types (First_Order, poly, level)
   | adjust_type_enc format (Simple_Types (_, poly, level)) =
     adjust_type_enc format (Guards (poly, level, Uniform))
@@ -746,8 +749,9 @@
 fun type_class_formula type_enc class arg =
   AAtom (ATerm (class, arg ::
       (case type_enc of
-         Simple_Types (_, Polymorphic, _) =>
-         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
+         Simple_Types (First_Order, Polymorphic, _) =>
+         if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
+         else []
        | _ => [])))
 fun formulas_for_types type_enc add_sorts_on_typ Ts =
   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
@@ -1779,18 +1783,19 @@
 
 (** Symbol declarations **)
 
-fun decl_line_for_class s =
+fun decl_line_for_class order s =
   let val name as (s, _) = `make_type_class s in
     Decl (sym_decl_prefix ^ s, name,
-          if exploit_tff1_dummy_type_vars then
-            AFun (atype_of_types, bool_atype)
+          if order = First_Order andalso avoid_first_order_dummy_type_vars then
+            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
           else
-            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
+            AFun (atype_of_types, bool_atype))
   end
 
 fun decl_lines_for_classes type_enc classes =
   case type_enc of
-    Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
+    Simple_Types (order, Polymorphic, _) =>
+    map (decl_line_for_class order) classes
   | _ => []
 
 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
@@ -2232,7 +2237,8 @@
             CNF => ensure_cnf_problem
           | CNF_UEQ => filter_cnf_ueq_problem
           | FOF => I
-          | TFF (_, TFF_Implicit) => I
+          | TFF (_, TPTP_Implicit) => I
+          | THF (_, TPTP_Implicit, _) => I
           | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
                                                         implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names

--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 10:30:33 2011 -0700
@@ -4,7 +4,7 @@
 import Control.Exception;
 import System.IO;
 import System.Exit;
-import Code;
+import Generated_Code;
 
 type Pos = [Int];
 

--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 10:30:33 2011 -0700
@@ -8,7 +8,7 @@
 import System.Exit
 import Maybe
 import List (partition, findIndex)
-import Code
+import Generated_Code
 
 
 type Pos = [Int]

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 10:30:33 2011 -0700
@@ -235,17 +235,17 @@
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
       let
-        val code_file = Path.append in_path (Path.basic "Code.hs")
+        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
         val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
         val main_file = Path.append in_path (Path.basic "Main.hs")
         val main = "module Main where {\n\n" ^
           "import System;\n" ^
           "import Narrowing_Engine;\n" ^
-          "import Code;\n\n" ^
-          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
+          "import Generated_Code;\n\n" ^
+          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
           "}\n"
-        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
-          (unprefix "module Code where {" code)
+        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
+          (unprefix "module Generated_Code where {" code)
         val _ = File.write code_file code'
         val _ = File.write narrowing_engine_file
           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)

--- a/src/Tools/Code/code_target.ML	Tue Sep 06 10:30:00 2011 -0700
+++ b/src/Tools/Code/code_target.ML	Tue Sep 06 10:30:33 2011 -0700
@@ -394,7 +394,7 @@
 
 fun check_code_for thy target strict args naming program names_cs =
   let
-    val module_name = "Code";
+    val module_name = "Generated_Code";
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
     fun ext_check p =
@@ -435,7 +435,7 @@
 fun evaluator thy target naming program consts =
   let
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target NONE "Code" [] naming program consts;
+      target NONE "Generated_Code" [] naming program consts;
   in evaluation mounted_serializer prepared_program consts end;
 
 end; (* local *)