--- a/NEWS Fri Aug 27 09:43:52 2010 +0200
+++ b/NEWS Fri Aug 27 10:57:32 2010 +0200
@@ -104,6 +104,8 @@
Trueprop ~> HOL.Trueprop
True ~> HOL.True
False ~> HOL.False
+ op & ~> HOL.conj
+ op | ~> HOL.disj
op --> ~> HOL.implies
Not ~> HOL.Not
The ~> HOL.The
--- a/src/HOL/Auth/Yahalom.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Aug 27 10:57:32 2010 +0200
@@ -197,6 +197,7 @@
apply (erule yahalom.induct,
drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
done
lemma analz_insert_freshK:
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 10:57:32 2010 +0200
@@ -50,11 +50,11 @@
local
- fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
+ fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u
| explode_conj t = [t]
fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
- | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
+ | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u)
| splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
| splt (_, @{term True}) = []
| splt tp = [tp]
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 10:57:32 2010 +0200
@@ -62,9 +62,9 @@
| vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
| vc_of (@{term HOL.implies} $ t $ u) =
vc_of u |> Option.map (assume t)
- | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
+ | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
SOME (vc_of u |> the_default True |> assert (n, t))
- | vc_of (@{term "op &"} $ t $ u) =
+ | vc_of (@{term HOL.conj} $ t $ u) =
(case (vc_of t, vc_of u) of
(NONE, r) => r
| (l, NONE) => l
@@ -74,7 +74,7 @@
val prop_of_vc =
let
- fun mk_conj t u = @{term "op &"} $ t $ u
+ fun mk_conj t u = @{term HOL.conj} $ t $ u
fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
| term_of (Assert ((n, t), v)) =
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 10:57:32 2010 +0200
@@ -1952,9 +1952,9 @@
| NONE => error "num_of_term: unsupported dvd")
| fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -2016,7 +2016,7 @@
fun term_bools acc t =
let
- val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
+ val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "op = :: int => _"}, @{term "op < :: int => _"},
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 10:57:32 2010 +0200
@@ -1996,8 +1996,8 @@
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
| fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 10:57:32 2010 +0200
@@ -5837,9 +5837,9 @@
@{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
| fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
@{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
@{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 10:57:32 2010 +0200
@@ -2954,8 +2954,8 @@
fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
val brT = [bT, bT] ---> bT;
val nott = @{term "Not"};
-val conjt = @{term "op &"};
-val disjt = @{term "op |"};
+val conjt = @{term HOL.conj};
+val disjt = @{term HOL.disj};
val impt = @{term HOL.implies};
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3018,8 +3018,8 @@
Const(@{const_name True},_) => @{code T}
| Const(@{const_name False},_) => @{code F}
| Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
- | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op ="},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 10:57:32 2010 +0200
@@ -33,12 +33,12 @@
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
let
fun uset (vars as (x::vs)) p = case term_of p of
- Const(@{const_name "op &"}, _)$ _ $ _ =>
+ Const(@{const_name HOL.conj}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
in (lS@rS, Drule.binop_cong_rule b lth rth) end
- | Const(@{const_name "op |"}, _)$ _ $ _ =>
+ | Const(@{const_name HOL.disj}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
@@ -122,12 +122,12 @@
fun decomp_mpinf fm =
case term_of fm of
- Const(@{const_name "op &"},_)$_$_ =>
+ Const(@{const_name HOL.conj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
(Thm.cabs x p) (Thm.cabs x q))
end
- | Const(@{const_name "op |"},_)$_$_ =>
+ | Const(@{const_name HOL.disj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
(Thm.cabs x p) (Thm.cabs x q))
@@ -181,8 +181,8 @@
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
--- a/src/HOL/Decision_Procs/langford.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Aug 27 10:57:32 2010 +0200
@@ -69,28 +69,28 @@
val all_conjuncts =
let fun h acc ct =
case term_of ct of
- @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
| _ => ct::acc
in h [] end;
fun conjuncts ct =
case term_of ct of
- @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
| _ => [ct];
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
case prop_of th of
- @{term "Trueprop"}$(@{term "op &"}$p$q) =>
+ @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
| @{term "Trueprop"}$p => (p,th)::acc
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -183,8 +183,8 @@
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
--- a/src/HOL/HOL.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/HOL.thy Fri Aug 27 10:57:32 2010 +0200
@@ -56,14 +56,14 @@
True :: bool
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
+
+ conj :: "[bool, bool] => bool" (infixr "&" 35)
+ disj :: "[bool, bool] => bool" (infixr "|" 30)
implies :: "[bool, bool] => bool" (infixr "-->" 25)
setup Sign.root_path
consts
- "op &" :: "[bool, bool] => bool" (infixr "&" 35)
- "op |" :: "[bool, bool] => bool" (infixr "|" 30)
-
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
setup Sign.local_path
@@ -89,15 +89,15 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
HOL.implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
not_equal (infix "\<noteq>" 50)
abbreviation (iff)
@@ -1578,7 +1578,7 @@
val atomize_conjL = @{thm atomize_conjL}
val atomize_disjL = @{thm atomize_disjL}
val operator_names =
- [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
+ [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
);
*}
@@ -1737,8 +1737,8 @@
"True" ("true")
"False" ("false")
"Not" ("Bool.not")
- "op |" ("(_ orelse/ _)")
- "op &" ("(_ andalso/ _)")
+ HOL.disj ("(_ orelse/ _)")
+ HOL.conj ("(_ andalso/ _)")
"If" ("(if _/ then _/ else _)")
setup {*
@@ -1914,7 +1914,7 @@
(Haskell "Bool")
(Scala "Boolean")
-code_const True and False and Not and "op &" and "op |" and If
+code_const True and False and Not and HOL.conj and HOL.disj and If
(SML "true" and "false" and "not"
and infixl 1 "andalso" and infixl 0 "orelse"
and "!(if (_)/ then (_)/ else (_))")
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 10:57:32 2010 +0200
@@ -17,8 +17,8 @@
T > True
F > False
"!" > All
- "/\\" > "op &"
- "\\/" > "op |"
+ "/\\" > HOL.conj
+ "\\/" > HOL.disj
"?" > Ex
"?!" > Ex1
"~" > Not
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 10:57:32 2010 +0200
@@ -55,8 +55,8 @@
ONTO > Fun.surj
"=" > "op ="
"==>" > HOL.implies
- "/\\" > "op &"
- "\\/" > "op |"
+ "/\\" > HOL.conj
+ "\\/" > HOL.disj
"!" > All
"?" > Ex
"?!" > Ex1
--- a/src/HOL/Import/HOL/bool.imp Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp Fri Aug 27 10:57:32 2010 +0200
@@ -14,7 +14,7 @@
const_maps
"~" > "HOL.Not"
"bool_case" > "Datatype.bool.bool_case"
- "\\/" > "op |"
+ "\\/" > HOL.disj
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
"T" > "HOL.True"
"RES_SELECT" > "HOL4Base.bool.RES_SELECT"
@@ -30,7 +30,7 @@
"ARB" > "HOL4Base.bool.ARB"
"?!" > "HOL.Ex1"
"?" > "HOL.Ex"
- "/\\" > "op &"
+ "/\\" > HOL.conj
"!" > "HOL.All"
thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 10:57:32 2010 +0200
@@ -115,7 +115,7 @@
"_10303" > "HOLLight.hollight._10303"
"_10302" > "HOLLight.hollight._10302"
"_0" > "0" :: "nat"
- "\\/" > "op |"
+ "\\/" > HOL.disj
"ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
"ZIP" > "HOLLight.hollight.ZIP"
"ZCONSTR" > "HOLLight.hollight.ZCONSTR"
@@ -237,7 +237,7 @@
"=" > "op ="
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
- "/\\" > "op &"
+ "/\\" > HOL.conj
"-" > "Groups.minus" :: "nat => nat => nat"
"," > "Product_Type.Pair"
"+" > "Groups.plus" :: "nat => nat => nat"
--- a/src/HOL/Import/proof_kernel.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Aug 27 10:57:32 2010 +0200
@@ -1205,7 +1205,7 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
if c = @{const_name Trueprop} orelse c = @{const_name All}
- orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+ orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
then I else insert (op =) c
| _ => I) t [];
@@ -1217,7 +1217,7 @@
| @{const_name HOL.implies} => insert (op =) "==>" cs
| @{const_name All} => cs
| "all" => cs
- | @{const_name "op &"} => cs
+ | @{const_name HOL.conj} => cs
| @{const_name Trueprop} => cs
| _ => insert (op =) c cs)
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
@@ -1521,7 +1521,7 @@
val th1 = norm_hyps th1
val th2 = norm_hyps th2
val (l,r) = case concl_of th of
- _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
+ _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
| _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 10:57:32 2010 +0200
@@ -1356,7 +1356,7 @@
val known_sos_constants =
[@{term "op ==>"}, @{term "Trueprop"},
- @{term HOL.implies}, @{term "op &"}, @{term "op |"},
+ @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
@{term "Not"}, @{term "op = :: bool => _"},
@{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
@{term "op = :: real => _"}, @{term "op < :: real => _"},
--- a/src/HOL/Library/positivstellensatz.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Fri Aug 27 10:57:32 2010 +0200
@@ -439,8 +439,8 @@
val is_req = is_binop @{cterm "op =:: real => _"}
val is_ge = is_binop @{cterm "op <=:: real => _"}
val is_gt = is_binop @{cterm "op <:: real => _"}
- val is_conj = is_binop @{cterm "op &"}
- val is_disj = is_binop @{cterm "op |"}
+ val is_conj = is_binop @{cterm HOL.conj}
+ val is_disj = is_binop @{cterm HOL.disj}
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
fun disj_cases th th1 th2 =
let val (p,q) = Thm.dest_binop (concl th)
@@ -484,7 +484,7 @@
val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
- val th' = Drule.binop_cong_rule @{cterm "op |"}
+ val th' = Drule.binop_cong_rule @{cterm HOL.disj}
(Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
(Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
in Thm.transitive th th'
@@ -542,12 +542,12 @@
let
val nnf_norm_conv' =
nnf_conv then_conv
- literals_conv [@{term "op &"}, @{term "op |"}] []
+ literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
(Conv.cache_conv
(first_conv [real_lt_conv, real_le_conv,
real_eq_conv, real_not_lt_conv,
real_not_le_conv, real_not_eq_conv, all_conv]))
- fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] []
+ fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
--- a/src/HOL/Multivariate_Analysis/Gauge_Measure.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Gauge_Measure.thy Fri Aug 27 10:57:32 2010 +0200
@@ -311,7 +311,7 @@
shows "(\<Union> f) has_gmeasure (setsum m f)" using assms
proof induct case (insert x s)
have *:"(x \<inter> \<Union>s) = \<Union>{x \<inter> y| y. y\<in>s}"by auto
- show ?case unfolding Union_insert ring_class.setsum.insert[OF insert(1-2)]
+ show ?case unfolding Union_insert setsum.insert [OF insert(1-2)]
apply(rule has_gmeasure_negligible_union) unfolding *
apply(rule insert) defer apply(rule insert) apply(rule insert) defer
apply(rule insert) prefer 4 apply(rule negligible_unions)
--- a/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 10:57:32 2010 +0200
@@ -4,7 +4,7 @@
begin
ML {*
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
val forbidden =
[(@{const_name Power.power}, "'a"),
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 10:57:32 2010 +0200
@@ -187,7 +187,7 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Aug 27 10:57:32 2010 +0200
@@ -1200,7 +1200,7 @@
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
val tnames = Datatype_Prop.make_tnames recTs;
val zs = Name.variant_list tnames (replicate (length descr'') "z");
- val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
(descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1215,7 +1215,7 @@
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
- val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
(descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1225,7 +1225,7 @@
(Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
map mk_permT dt_atomTs) @ [("z", fsT')];
val aux_ind_Ts = rev (map snd aux_ind_vars);
- val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn (((i, _), T), tname) =>
HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Aug 27 10:57:32 2010 +0200
@@ -71,7 +71,7 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
@@ -89,7 +89,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 27 10:57:32 2010 +0200
@@ -76,7 +76,7 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
@@ -94,7 +94,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Orderings.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Orderings.thy Fri Aug 27 10:57:32 2010 +0200
@@ -641,7 +641,7 @@
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
val impl = @{const_syntax HOL.implies};
- val conj = @{const_syntax "op &"};
+ val conj = @{const_syntax HOL.conj};
val less = @{const_syntax less};
val less_eq = @{const_syntax less_eq};
--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 10:57:32 2010 +0200
@@ -11,12 +11,12 @@
fun isD t = case t of
Const(@{const_name Trueprop},_)$t => isD t
- | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isD l andalso isD r
| Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
| Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
- | Const(@{const_name "op |"},_)$_$_ => false
+ | Const(@{const_name HOL.disj},_)$_$_ => false
| Const(@{const_name Ex} ,_)$_ => false
| Const(@{const_name Not},_)$_ => false
| Const(@{const_name True},_) => false
@@ -30,8 +30,8 @@
and
isG t = case t of
Const(@{const_name Trueprop},_)$t => isG t
- | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
- | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.disj} ,_)$l$r => isG l andalso isG r
| Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
| Const(@{const_name All},_)$Abs(_,_,t) => isG t
@@ -53,7 +53,7 @@
fun at thm = case concl_of thm of
_$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
- | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
--- a/src/HOL/Set.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Set.thy Fri Aug 27 10:57:32 2010 +0200
@@ -220,7 +220,7 @@
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
val impl = @{const_syntax HOL.implies};
- val conj = @{const_syntax "op &"};
+ val conj = @{const_syntax HOL.conj};
val sbset = @{const_syntax subset};
val sbset_eq = @{const_syntax subset_eq};
@@ -269,7 +269,7 @@
fun setcompr_tr [e, idts, b] =
let
val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
- val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
+ val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
val exP = ex_tr [idts, P];
in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
@@ -288,7 +288,7 @@
fun setcompr_tr' [Abs (abs as (_, _, P))] =
let
fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
- | check (Const (@{const_syntax "op &"}, _) $
+ | check (Const (@{const_syntax HOL.conj}, _) $
(Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
@@ -305,7 +305,7 @@
val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
in
case t of
- Const (@{const_syntax "op &"}, _) $
+ Const (@{const_syntax HOL.conj}, _) $
(Const (@{const_syntax Set.member}, _) $
(Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
--- a/src/HOL/Statespace/state_fun.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Aug 27 10:57:32 2010 +0200
@@ -53,7 +53,7 @@
val lazy_conj_simproc =
Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
- (case t of (Const (@{const_name "op &"},_)$P$Q) =>
+ (case t of (Const (@{const_name HOL.conj},_)$P$Q) =>
let
val P_P' = Simplifier.rewrite ss (cterm_of thy P);
val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Aug 27 10:57:32 2010 +0200
@@ -120,8 +120,8 @@
fun split_conj_thm th =
((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
+val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
+val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Aug 27 10:57:32 2010 +0200
@@ -70,7 +70,7 @@
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
@@ -149,7 +149,7 @@
val prems = maps (fn ((i, (_, _, constrs)), T) =>
map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)))
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Aug 27 10:57:32 2010 +0200
@@ -99,7 +99,7 @@
if member (op =) is i then SOME
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
--- a/src/HOL/Tools/Function/termination.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri Aug 27 10:57:32 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 10:57:32 2010 +0200
@@ -130,8 +130,8 @@
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
$ t1 $ t2 =>
Subset (to_R_rep Ts t1, to_R_rep Ts t2)
- | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
- | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
| @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
| t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
| Free _ => raise SAME ()
@@ -173,10 +173,10 @@
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name ord_class.less_eq}, _) =>
to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
| @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
| @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name bot_class.bot},
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 10:57:32 2010 +0200
@@ -386,13 +386,13 @@
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
| strip_connective _ t = [t]
fun strip_any_connective (t as (t0 $ _ $ _)) =
- if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
+ if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
(strip_connective t0 t, t0)
else
([t], @{const Not})
| strip_any_connective t = ([t], @{const Not})
-val conjuncts_of = strip_connective @{const "op &"}
-val disjuncts_of = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const HOL.conj}
+val disjuncts_of = strip_connective @{const HOL.disj}
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -409,8 +409,8 @@
(@{const_name All}, 1),
(@{const_name Ex}, 1),
(@{const_name "op ="}, 1),
- (@{const_name "op &"}, 2),
- (@{const_name "op |"}, 2),
+ (@{const_name HOL.conj}, 2),
+ (@{const_name HOL.disj}, 2),
(@{const_name HOL.implies}, 2),
(@{const_name If}, 3),
(@{const_name Let}, 2),
@@ -2148,8 +2148,8 @@
fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
Const (@{const_name Ex}, T1)
$ Abs (s2, T2, repair_rec (j + 1) t2')
- | repair_rec j (@{const "op &"} $ t1 $ t2) =
- @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
+ | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
| repair_rec j t =
let val (head, args) = strip_comb t in
if head = Bound j then
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 10:57:32 2010 +0200
@@ -777,7 +777,7 @@
$ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| (t0 as Const (@{const_name Ex}, _))
- $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+ $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_term (betapply (t2, t1)) accum
@@ -883,8 +883,8 @@
| (t0 as Const (s0, _)) $ t1 $ t2 =>
if s0 = @{const_name "==>"} orelse
s0 = @{const_name Pure.conjunction} orelse
- s0 = @{const_name "op &"} orelse
- s0 = @{const_name "op |"} orelse
+ s0 = @{const_name HOL.conj} orelse
+ s0 = @{const_name HOL.disj} orelse
s0 = @{const_name HOL.implies} then
let
val impl = (s0 = @{const_name "==>"} orelse
@@ -975,7 +975,7 @@
do_all t0 s0 T1 t1 accum
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
- | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
| (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 10:57:32 2010 +0200
@@ -518,9 +518,9 @@
| (Const (@{const_name "op ="}, T), [t1]) =>
Op1 (SingletonSet, range_type T, Any, sub t1)
| (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
- | (Const (@{const_name "op &"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
Op2 (And, bool_T, Any, sub' t1, sub' t2)
- | (Const (@{const_name "op |"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, sub t1, sub t2)
| (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 10:57:32 2010 +0200
@@ -211,11 +211,11 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ do_term new_Ts old_Ts polar t1
+ | @{const HOL.conj} $ t1 $ t2 =>
+ @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
$ do_term new_Ts old_Ts polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ do_term new_Ts old_Ts polar t1
+ | @{const HOL.disj} $ t1 $ t2 =>
+ @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
$ do_term new_Ts old_Ts polar t2
| @{const HOL.implies} $ t1 $ t2 =>
@{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
@@ -449,7 +449,7 @@
(** Destruction of universal and existential equalities **)
fun curry_assms (@{const "==>"} $ (@{const Trueprop}
- $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+ $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
| curry_assms (@{const "==>"} $ t1 $ t2) =
@{const "==>"} $ curry_assms t1 $ curry_assms t2
@@ -604,9 +604,9 @@
do_quantifier s0 T0 s1 T1 t1
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | @{const "op &"} $ t1 $ t2 =>
+ | @{const HOL.conj} $ t1 $ t2 =>
s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
- | @{const "op |"} $ t1 $ t2 =>
+ | @{const HOL.disj} $ t1 $ t2 =>
s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
| @{const HOL.implies} $ t1 $ t2 =>
@{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
@@ -620,8 +620,8 @@
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
val (pref, connective) =
- if gfp then (lbfp_prefix, @{const "op |"})
- else (ubfp_prefix, @{const "op &"})
+ if gfp then (lbfp_prefix, @{const HOL.disj})
+ else (ubfp_prefix, @{const HOL.conj})
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js skolemizable polar
fun neg () = Const (pref ^ s, T)
@@ -1105,7 +1105,7 @@
case t of
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
(case t1 of
- (t10 as @{const "op &"}) $ t11 $ t12 =>
+ (t10 as @{const HOL.conj}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
| (t10 as @{const Not}) $ t11 =>
@@ -1118,7 +1118,7 @@
t0 $ Abs (s, T1, distribute_quantifiers t1))
| (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
(case distribute_quantifiers t1 of
- (t10 as @{const "op |"}) $ t11 $ t12 =>
+ (t10 as @{const HOL.disj}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
| (t10 as @{const HOL.implies}) $ t11 $ t12 =>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 10:57:32 2010 +0200
@@ -405,7 +405,7 @@
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 10:57:32 2010 +0200
@@ -524,7 +524,7 @@
fun dest_conjunct_prem th =
case HOLogic.dest_Trueprop (prop_of th) of
- (Const (@{const_name "op &"}, _) $ t $ t') =>
+ (Const (@{const_name HOL.conj}, _) $ t $ t') =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
| _ => [th]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 10:57:32 2010 +0200
@@ -221,8 +221,8 @@
@{const_name HOL.implies},
@{const_name All},
@{const_name Ex},
- @{const_name "op &"},
- @{const_name "op |"}]
+ @{const_name HOL.conj},
+ @{const_name HOL.disj}]
fun special_cases (c, T) = member (op =) [
@{const_name Product_Type.Unity},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 27 10:57:32 2010 +0200
@@ -89,8 +89,8 @@
fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true
- | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
+ | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
+ | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
@@ -250,7 +250,7 @@
fun split_conjs thy t =
let
- fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+ fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
(split_conjunctions t1) @ (split_conjunctions t2)
| split_conjunctions t = [t]
in
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 10:57:32 2010 +0200
@@ -28,7 +28,7 @@
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
- @{term "op &"}, @{term "op |"}, @{term HOL.implies},
+ @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -120,8 +120,8 @@
fun whatis x ct =
( case (term_of ct) of
- Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
-| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+ Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
@@ -353,8 +353,8 @@
then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
- | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
- | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
end
fun unit_conv t =
case (term_of t) of
- Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
- | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
+ Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
+ | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
@@ -569,7 +569,7 @@
fun add_bools t =
let
val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
- @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
+ @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
val is_op = member (op =) ops;
@@ -612,9 +612,9 @@
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
| fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
- | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 10:57:32 2010 +0200
@@ -25,7 +25,7 @@
case (term_of p) of
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
- andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
+ andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
@{const_name HOL.implies}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 27 10:57:32 2010 +0200
@@ -485,7 +485,7 @@
end
| (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
- (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+ (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
(Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
Const (@{const_name Ex1}, ty') $ t') =>
let
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 10:57:32 2010 +0200
@@ -159,8 +159,8 @@
fun conn @{const_name True} = SOME "true"
| conn @{const_name False} = SOME "false"
| conn @{const_name Not} = SOME "not"
- | conn @{const_name "op &"} = SOME "and"
- | conn @{const_name "op |"} = SOME "or"
+ | conn @{const_name HOL.conj} = SOME "and"
+ | conn @{const_name HOL.disj} = SOME "or"
| conn @{const_name HOL.implies} = SOME "implies"
| conn @{const_name "op ="} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 10:57:32 2010 +0200
@@ -216,8 +216,8 @@
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Fri Aug 27 10:57:32 2010 +0200
@@ -62,14 +62,14 @@
val is_neg = (fn @{term Not} $ _ => true | _ => false)
fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
fun dest_disj_term' f = (fn
- @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
+ @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
| _ => NONE)
-val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
val dest_disj_term =
dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
@@ -202,11 +202,11 @@
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
- fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
+ fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
| dest_conj t = raise TERM ("dest_conj", [t])
val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
+ fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 27 10:57:32 2010 +0200
@@ -298,13 +298,13 @@
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
in
(case Thm.term_of ct1 of
- @{term Not} $ (@{term "op &"} $ _ $ _) =>
+ @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term "op &"} $ _ $ _ =>
+ | @{term HOL.conj} $ _ $ _ =>
prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term "op |"} $ _ $ _) =>
+ | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term "op |"} $ _ $ _ =>
+ | @{term HOL.disj} $ _ $ _ =>
prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
| Const (@{const_name distinct}, _) $ _ =>
let
@@ -477,8 +477,8 @@
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
- | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
+ @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
| Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 10:57:32 2010 +0200
@@ -196,8 +196,8 @@
| @{term True} => pair ct
| @{term False} => pair ct
| @{term Not} $ _ => abstr1 cvs ct
- | @{term "op &"} $ _ $ _ => abstr2 cvs ct
- | @{term "op |"} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
| @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 10:57:32 2010 +0200
@@ -68,8 +68,8 @@
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
- | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
| dec_sko _ rhss = rhss
in dec_sko (prop_of th) [] end;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 10:57:32 2010 +0200
@@ -95,8 +95,8 @@
Symtab.make [(@{type_name Product_Type.prod}, "prod"),
(@{type_name Sum_Type.sum}, "sum"),
(@{const_name "op ="}, "equal"),
- (@{const_name "op &"}, "and"),
- (@{const_name "op |"}, "or"),
+ (@{const_name HOL.conj}, "and"),
+ (@{const_name HOL.disj}, "or"),
(@{const_name HOL.implies}, "implies"),
(@{const_name Set.member}, "member"),
(@{const_name fequal}, "fequal"),
@@ -430,7 +430,7 @@
fun literals_of_term1 args thy (@{const Trueprop} $ P) =
literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+ | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
literals_of_term1 (literals_of_term1 args thy P) thy Q
| literals_of_term1 (lits, ts) thy P =
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 10:57:32 2010 +0200
@@ -159,8 +159,8 @@
do_quantifier (pos = SOME false) body_t
| Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
do_quantifier (pos = SOME true) body_t
- | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const HOL.implies} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
@@ -545,8 +545,8 @@
do_formula (not pos) t1 andalso
(t2 = @{const False} orelse do_formula pos t2)
| (_, @{const Not} $ t1) => do_formula (not pos) t1
- | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
| _ => false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 10:57:32 2010 +0200
@@ -70,11 +70,11 @@
| negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
| negate_term (@{const HOL.implies} $ t1 $ t2) =
- @{const "op &"} $ t1 $ negate_term t2
- | negate_term (@{const "op &"} $ t1 $ t2) =
- @{const "op |"} $ negate_term t1 $ negate_term t2
- | negate_term (@{const "op |"} $ t1 $ t2) =
- @{const "op &"} $ negate_term t1 $ negate_term t2
+ @{const HOL.conj} $ t1 $ negate_term t2
+ | negate_term (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.disj} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const HOL.disj} $ t1 $ t2) =
+ @{const HOL.conj} $ negate_term t1 $ negate_term t2
| negate_term (@{const Not} $ t) = t
| negate_term t = @{const Not} $ t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 10:57:32 2010 +0200
@@ -70,8 +70,8 @@
do_quant bs AForall s T t'
| Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
do_quant bs AExists s T t'
- | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
| @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
| Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
@@ -125,8 +125,8 @@
t0 $ Abs (s, T, aux (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
--- a/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 10:57:32 2010 +0200
@@ -79,11 +79,11 @@
in capply c (uncurry cabs r) end;
-local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;
-local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;
@@ -129,8 +129,8 @@
val dest_pair = dest_binop @{const_name Pair}
val dest_eq = dest_binop @{const_name "op ="}
val dest_imp = dest_binop @{const_name HOL.implies}
-val dest_conj = dest_binop @{const_name "op &"}
-val dest_disj = dest_binop @{const_name "op |"}
+val dest_conj = dest_binop @{const_name HOL.conj}
+val dest_disj = dest_binop @{const_name HOL.disj}
val dest_select = dest_binder @{const_name Eps}
val dest_exists = dest_binder @{const_name Ex}
val dest_forall = dest_binder @{const_name All}
--- a/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 10:57:32 2010 +0200
@@ -183,12 +183,12 @@
fun mk_conj{conj1,conj2} =
- let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[conj1,conj2])
end;
fun mk_disj{disj1,disj2} =
- let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[disj1,disj2])
end;
@@ -259,10 +259,10 @@
fun dest_neg(Const(@{const_name Not},_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
| dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
-fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
| dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
fun mk_pair{fst,snd} =
--- a/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 10:57:32 2010 +0200
@@ -95,8 +95,8 @@
fun is_atom (Const (@{const_name False}, _)) = false
| is_atom (Const (@{const_name True}, _)) = false
- | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
| is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
@@ -105,7 +105,7 @@
fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
| is_literal x = is_atom x;
-fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
(* ------------------------------------------------------------------------- *)
@@ -184,14 +184,14 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
conj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
@@ -218,14 +218,14 @@
make_nnf_not_false
| make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
@@ -276,7 +276,7 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
end
end
- | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+ | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
fun make_cnf_thm thy t =
let
(* Term.term -> Thm.thm *)
- fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
+ fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
val thm2 = make_cnf_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+ fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnf_disj_thm x1 y'
val thm2 = make_cnf_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+ | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
let
val thm1 = make_cnf_disj_thm x' y1
val thm2 = make_cnf_disj_thm x' y2
@@ -403,27 +403,27 @@
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
+ fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
if is_clause x andalso is_clause y then
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
else if is_literal y orelse is_literal x then let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
(* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+ fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnfx_disj_thm x1 y'
val thm2 = make_cnfx_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+ | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
let
val thm1 = make_cnfx_disj_thm x' y1
val thm2 = make_cnfx_disj_thm x' y2
--- a/src/HOL/Tools/groebner.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Aug 27 10:57:32 2010 +0200
@@ -395,7 +395,7 @@
fun refute_disj rfn tm =
case term_of tm of
- Const(@{const_name "op |"},_)$l$r =>
+ Const(@{const_name HOL.disj},_)$l$r =>
compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
| _ => rfn tm ;
@@ -454,7 +454,7 @@
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
val cTrp = @{cterm "Trueprop"};
-val cConj = @{cterm "op &"};
+val cConj = @{cterm HOL.conj};
val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
val assume_Trueprop = mk_comb cTrp #> assume;
val list_mk_conj = list_mk_binop cConj;
@@ -479,22 +479,22 @@
(* FIXME : copied from cqe.ML -- complex QE*)
fun conjuncts ct =
case term_of ct of
- @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
| _ => [ct];
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
case prop_of th of
- @{term "Trueprop"}$(@{term "op &"}$p$q) =>
+ @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
| @{term "Trueprop"}$p => (p,th)::acc
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -852,14 +852,14 @@
fun unwind_polys_conv tm =
let
val (vars,bod) = strip_exists tm
- val cjs = striplist (dest_binary @{cterm "op &"}) bod
+ val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
val th1 = (the (get_first (try (isolate_variable vars)) cjs)
handle Option => raise CTERM ("unwind_polys_conv",[tm]))
val eq = Thm.lhs_of th1
- val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
+ val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
val th2 = conj_ac_rule (mk_eq bod bod')
val th3 = transitive th2
- (Drule.binop_cong_rule @{cterm "op &"} th1
+ (Drule.binop_cong_rule @{cterm HOL.conj} th1
(reflexive (Thm.dest_arg (Thm.rhs_of th2))))
val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
val vars' = (remove op aconvc v vars) @ [v]
@@ -929,8 +929,8 @@
| Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
| Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| @{term "op ==>"} $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm
--- a/src/HOL/Tools/hologic.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Aug 27 10:57:32 2010 +0200
@@ -208,8 +208,8 @@
let val (th1, th2) = conj_elim th
in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
-val conj = @{term "op &"}
-and disj = @{term "op |"}
+val conj = @{term HOL.conj}
+and disj = @{term HOL.disj}
and imp = @{term implies}
and Not = @{term Not};
@@ -218,14 +218,14 @@
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_not t = Not $ t;
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
| dest_disj t = [t];
(*Like dest_disj, but flattens disjunctions however nested*)
-fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
| disjuncts_aux t disjs = t::disjs;
fun disjuncts t = disjuncts_aux t [];
--- a/src/HOL/Tools/inductive_set.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Aug 27 10:57:32 2010 +0200
@@ -74,9 +74,9 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop @{const_name "op &"} T x =
+ fun mkop @{const_name HOL.conj} T x =
SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
- | mkop @{const_name "op |"} T x =
+ | mkop @{const_name HOL.disj} T x =
SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
--- a/src/HOL/Tools/lin_arith.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 27 10:57:32 2010 +0200
@@ -46,7 +46,7 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
--- a/src/HOL/Tools/meson.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 27 10:57:32 2010 +0200
@@ -151,8 +151,8 @@
let fun has (Const(a,_)) = false
| has (Const(@{const_name Trueprop},_) $ p) = has p
| has (Const(@{const_name Not},_) $ p) = has p
- | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
- | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+ | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
+ | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
| has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
| has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
| has _ = false
@@ -162,7 +162,7 @@
(**** Clause handling ****)
fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
- | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+ | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
| literals (Const(@{const_name Not},_) $ P) = [(false,P)]
| literals P = [(true,P)];
@@ -172,7 +172,7 @@
(*** Tautology Checking ***)
-fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
| signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
| signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
@@ -208,16 +208,16 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (concl_of th) of
- (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
+ (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+ | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
- | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+ | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
| _ => (*not a disjunction*) th;
-fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
| notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
@@ -268,10 +268,10 @@
(*Estimate the number of clauses in order to detect infeasible theorems*)
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
| signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
- | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
if b then sum (signed_nclauses b t) (signed_nclauses b u)
else prod (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
if b then prod (signed_nclauses b t) (signed_nclauses b u)
else sum (signed_nclauses b t) (signed_nclauses b u)
| signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
@@ -330,10 +330,10 @@
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
- else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
+ else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
then nodups ctxt th :: ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
- Const (@{const_name "op &"}, _) => (*conjunction*)
+ Const (@{const_name HOL.conj}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
| Const (@{const_name All}, _) => (*universal quantifier*)
let val (th',ctxt') = freeze_spec th (!ctxtr)
@@ -341,7 +341,7 @@
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
- | Const (@{const_name "op |"}, _) =>
+ | Const (@{const_name HOL.disj}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
let val tac =
@@ -365,7 +365,7 @@
(**** Generation of contrapositives ****)
fun is_left (Const (@{const_name Trueprop}, _) $
- (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
+ (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -400,7 +400,7 @@
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
- [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
+ [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
@{const_name HOL.implies}, @{const_name Not},
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
@@ -429,7 +429,7 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
| ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
| ok4horn _ = false;
--- a/src/HOL/Tools/prop_logic.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Fri Aug 27 10:57:32 2010 +0200
@@ -397,14 +397,14 @@
(False, table)
| aux (Const (@{const_name Not}, _) $ x) table =
apfst Not (aux x table)
- | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
+ | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
- | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
+ | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
--- a/src/HOL/Tools/refute.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Aug 27 10:57:32 2010 +0200
@@ -648,8 +648,8 @@
| Const (@{const_name All}, _) => t
| Const (@{const_name Ex}, _) => t
| Const (@{const_name "op ="}, _) => t
- | Const (@{const_name "op &"}, _) => t
- | Const (@{const_name "op |"}, _) => t
+ | Const (@{const_name HOL.conj}, _) => t
+ | Const (@{const_name HOL.disj}, _) => t
| Const (@{const_name HOL.implies}, _) => t
(* sets *)
| Const (@{const_name Collect}, _) => t
@@ -824,8 +824,8 @@
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
| Const (@{const_name "op ="}, T) => collect_type_axioms T axs
- | Const (@{const_name "op &"}, _) => axs
- | Const (@{const_name "op |"}, _) => axs
+ | Const (@{const_name HOL.conj}, _) => axs
+ | Const (@{const_name HOL.disj}, _) => axs
| Const (@{const_name HOL.implies}, _) => axs
(* sets *)
| Const (@{const_name Collect}, T) => collect_type_axioms T axs
@@ -1861,7 +1861,7 @@
SOME (interpret thy model args (eta_expand t 1))
| Const (@{const_name "op ="}, _) =>
SOME (interpret thy model args (eta_expand t 2))
- | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1871,14 +1871,14 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op &"}, _) $ t1 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op &"}, _) =>
+ | Const (@{const_name HOL.conj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "False & undef": *)
(* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
- | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1888,9 +1888,9 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op |"}, _) $ t1 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op |"}, _) =>
+ | Const (@{const_name HOL.disj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "True | undef": *)
--- a/src/HOL/Tools/simpdata.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Aug 27 10:57:32 2010 +0200
@@ -12,7 +12,7 @@
(*abstract syntax*)
fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
| dest_eq _ = NONE;
- fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
| dest_imp _ = NONE;
@@ -160,7 +160,7 @@
val mksimps_pairs =
[(@{const_name HOL.implies}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, []),
--- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 10:57:32 2010 +0200
@@ -88,8 +88,8 @@
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*abstraction of a formula*)
- and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
--- a/src/HOL/ex/svc_funcs.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Aug 27 10:57:32 2010 +0200
@@ -89,8 +89,8 @@
let fun tag t =
let val (c,ts) = strip_comb t
in case c of
- Const(@{const_name "op &"}, _) => apply c (map tag ts)
- | Const(@{const_name "op |"}, _) => apply c (map tag ts)
+ Const(@{const_name HOL.conj}, _) => apply c (map tag ts)
+ | Const(@{const_name HOL.disj}, _) => apply c (map tag ts)
| Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
| Const(@{const_name Not}, _) => apply c (map tag ts)
| Const(@{const_name True}, _) => (c, false)
@@ -183,9 +183,9 @@
| tm t = Int (lit t)
handle Match => var (t,[])
(*translation of a formula*)
- and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
+ and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
Buildin("AND", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
+ | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
Buildin("OR", [fm pos p, fm pos q])
| fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
--- a/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 27 10:57:32 2010 +0200
@@ -121,7 +121,7 @@
val r_inst = read_instantiate ctxt;
fun at thm =
case concl_of thm of
- _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
| _ => [thm];
in map zero_var_indexes (at thm) end;
--- a/src/Tools/Code/code_thingol.ML Fri Aug 27 09:43:52 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Aug 27 10:57:32 2010 +0200
@@ -271,9 +271,6 @@
of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
| NONE => Codegen.thyname_of_const thy c);
fun purify_base "==>" = "follows"
- | purify_base "op &" = "and"
- | purify_base "op |" = "or"
- | purify_base "op -->" = "implies"
| purify_base "op =" = "eq"
| purify_base s = Name.desymbolize false s;
fun namify thy get_basename get_thyname name =