--- a/src/HOL/Recdef.thy Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Recdef.thy Thu Aug 19 16:03:01 2010 +0200
@@ -5,7 +5,7 @@
header {* TFL: recursive function definitions *}
theory Recdef
-imports FunDef Plain
+imports Plain Hilbert_Choice
uses
("Tools/TFL/casesplit.ML")
("Tools/TFL/utils.ML")
--- a/src/HOL/Tools/TFL/dcterm.ML Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Thu Aug 19 16:03:01 2010 +0200
@@ -24,18 +24,15 @@
val dest_exists: cterm -> cterm * cterm
val dest_forall: cterm -> cterm * cterm
val dest_imp: cterm -> cterm * cterm
- val dest_let: cterm -> cterm * cterm
val dest_neg: cterm -> cterm
val dest_pair: cterm -> cterm * cterm
val dest_var: cterm -> {Name:string, Ty:typ}
val is_conj: cterm -> bool
- val is_cons: cterm -> bool
val is_disj: cterm -> bool
val is_eq: cterm -> bool
val is_exists: cterm -> bool
val is_forall: cterm -> bool
val is_imp: cterm -> bool
- val is_let: cterm -> bool
val is_neg: cterm -> bool
val is_pair: cterm -> bool
val list_mk_disj: cterm list -> cterm
@@ -78,15 +75,15 @@
fun mk_exists (r as (Bvar, Body)) =
let val ty = #T(rep_cterm Bvar)
- val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
in capply c (uncurry cabs r) end;
-local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;
-local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;
@@ -128,17 +125,15 @@
handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
-val dest_neg = dest_monop "not"
-val dest_pair = dest_binop @{const_name Pair};
-val dest_eq = dest_binop "op ="
-val dest_imp = dest_binop "op -->"
-val dest_conj = dest_binop "op &"
-val dest_disj = dest_binop "op |"
-val dest_cons = dest_binop "Cons"
-val dest_let = Library.swap o dest_binop "Let";
-val dest_select = dest_binder "Hilbert_Choice.Eps"
-val dest_exists = dest_binder "Ex"
-val dest_forall = dest_binder "All"
+val dest_neg = dest_monop @{const_name Not}
+val dest_pair = dest_binop @{const_name Pair}
+val dest_eq = dest_binop @{const_name "op ="}
+val dest_imp = dest_binop @{const_name "op -->"}
+val dest_conj = dest_binop @{const_name "op &"}
+val dest_disj = dest_binop @{const_name "op |"}
+val dest_select = dest_binder @{const_name Eps}
+val dest_exists = dest_binder @{const_name Ex}
+val dest_forall = dest_binder @{const_name All}
(* Query routines *)
@@ -151,8 +146,6 @@
val is_conj = can dest_conj
val is_disj = can dest_disj
val is_pair = can dest_pair
-val is_let = can dest_let
-val is_cons = can dest_cons
(*---------------------------------------------------------------------------
@@ -197,7 +190,7 @@
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
| TERM (msg, _) => raise ERR "mk_prop" msg;
-fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
+fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
end;
--- a/src/HOL/Tools/TFL/rules.ML Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Aug 19 16:03:01 2010 +0200
@@ -453,14 +453,14 @@
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
case (Thm.prop_of thm)
- of (Const("==>",_)$(Const(@{const_name "Trueprop"},_)$ _) $
+ of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
(Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
fun dest_equal(Const ("==",_) $
- (Const (@{const_name "Trueprop"},_) $ lhs)
- $ (Const (@{const_name "Trueprop"},_) $ rhs)) = {lhs=lhs, rhs=rhs}
+ (Const (@{const_name Trueprop},_) $ lhs)
+ $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = S.dest_eq tm;
@@ -759,7 +759,7 @@
val cntxt = rev(Simplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
- val Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ _ = Thm.prop_of thm
+ val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
(OldTerm.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
--- a/src/HOL/Tools/TFL/tfl.ML Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Aug 19 16:03:01 2010 +0200
@@ -483,7 +483,7 @@
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val Const(@{const_name "All"},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
+ val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
Rtype)
val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Aug 19 16:03:01 2010 +0200
@@ -165,19 +165,19 @@
fun mk_select (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
+ val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
in list_comb(c,[mk_abs r])
end;
fun mk_forall (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_exists (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
@@ -250,13 +250,13 @@
fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
-fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
-fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
-fun dest_neg(Const("not",_) $ M) = M
+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}
@@ -402,6 +402,6 @@
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
- Body=Const(@{const_name "True"},HOLogic.boolT)};
+ Body=Const(@{const_name True},HOLogic.boolT)};
end;