corrected some long-overseen misperceptions in recdef
authorhaftmann
Thu Aug 19 16:03:01 2010 +0200 (2010-08-19)
changeset 38554f8999e19dd49
parent 38553 56965d8e4e11
child 38555 bd6359ed1636
corrected some long-overseen misperceptions in recdef
src/HOL/Recdef.thy
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/usyntax.ML
     1.1 --- a/src/HOL/Recdef.thy	Thu Aug 19 12:11:57 2010 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Thu Aug 19 16:03:01 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* TFL: recursive function definitions *}
     1.5  
     1.6  theory Recdef
     1.7 -imports FunDef Plain
     1.8 +imports Plain Hilbert_Choice
     1.9  uses
    1.10    ("Tools/TFL/casesplit.ML")
    1.11    ("Tools/TFL/utils.ML")
     2.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 19 12:11:57 2010 +0200
     2.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 19 16:03:01 2010 +0200
     2.3 @@ -24,18 +24,15 @@
     2.4    val dest_exists: cterm -> cterm * cterm
     2.5    val dest_forall: cterm -> cterm * cterm
     2.6    val dest_imp: cterm -> cterm * cterm
     2.7 -  val dest_let: cterm -> cterm * cterm
     2.8    val dest_neg: cterm -> cterm
     2.9    val dest_pair: cterm -> cterm * cterm
    2.10    val dest_var: cterm -> {Name:string, Ty:typ}
    2.11    val is_conj: cterm -> bool
    2.12 -  val is_cons: cterm -> bool
    2.13    val is_disj: cterm -> bool
    2.14    val is_eq: cterm -> bool
    2.15    val is_exists: cterm -> bool
    2.16    val is_forall: cterm -> bool
    2.17    val is_imp: cterm -> bool
    2.18 -  val is_let: cterm -> bool
    2.19    val is_neg: cterm -> bool
    2.20    val is_pair: cterm -> bool
    2.21    val list_mk_disj: cterm list -> cterm
    2.22 @@ -78,15 +75,15 @@
    2.23  
    2.24  fun mk_exists (r as (Bvar, Body)) =
    2.25    let val ty = #T(rep_cterm Bvar)
    2.26 -      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    2.27 +      val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
    2.28    in capply c (uncurry cabs r) end;
    2.29  
    2.30  
    2.31 -local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    2.32 +local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    2.33  in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
    2.34  end;
    2.35  
    2.36 -local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    2.37 +local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    2.38  in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
    2.39  end;
    2.40  
    2.41 @@ -128,17 +125,15 @@
    2.42    handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
    2.43  
    2.44  
    2.45 -val dest_neg    = dest_monop "not"
    2.46 -val dest_pair   = dest_binop @{const_name Pair};
    2.47 -val dest_eq     = dest_binop "op ="
    2.48 -val dest_imp    = dest_binop "op -->"
    2.49 -val dest_conj   = dest_binop "op &"
    2.50 -val dest_disj   = dest_binop "op |"
    2.51 -val dest_cons   = dest_binop "Cons"
    2.52 -val dest_let    = Library.swap o dest_binop "Let";
    2.53 -val dest_select = dest_binder "Hilbert_Choice.Eps"
    2.54 -val dest_exists = dest_binder "Ex"
    2.55 -val dest_forall = dest_binder "All"
    2.56 +val dest_neg    = dest_monop @{const_name Not}
    2.57 +val dest_pair   = dest_binop @{const_name Pair}
    2.58 +val dest_eq     = dest_binop @{const_name "op ="}
    2.59 +val dest_imp    = dest_binop @{const_name "op -->"}
    2.60 +val dest_conj   = dest_binop @{const_name "op &"}
    2.61 +val dest_disj   = dest_binop @{const_name "op |"}
    2.62 +val dest_select = dest_binder @{const_name Eps}
    2.63 +val dest_exists = dest_binder @{const_name Ex}
    2.64 +val dest_forall = dest_binder @{const_name All}
    2.65  
    2.66  (* Query routines *)
    2.67  
    2.68 @@ -151,8 +146,6 @@
    2.69  val is_conj   = can dest_conj
    2.70  val is_disj   = can dest_disj
    2.71  val is_pair   = can dest_pair
    2.72 -val is_let    = can dest_let
    2.73 -val is_cons   = can dest_cons
    2.74  
    2.75  
    2.76  (*---------------------------------------------------------------------------
    2.77 @@ -197,7 +190,7 @@
    2.78    handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
    2.79      | TERM (msg, _) => raise ERR "mk_prop" msg;
    2.80  
    2.81 -fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
    2.82 +fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
    2.83  
    2.84  
    2.85  end;
     3.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 12:11:57 2010 +0200
     3.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 16:03:01 2010 +0200
     3.3 @@ -453,14 +453,14 @@
     3.4  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
     3.5  fun is_cong thm =
     3.6    case (Thm.prop_of thm)
     3.7 -     of (Const("==>",_)$(Const(@{const_name "Trueprop"},_)$ _) $
     3.8 +     of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
     3.9           (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
    3.10        | _ => true;
    3.11  
    3.12  
    3.13  fun dest_equal(Const ("==",_) $
    3.14 -               (Const (@{const_name "Trueprop"},_) $ lhs)
    3.15 -               $ (Const (@{const_name "Trueprop"},_) $ rhs)) = {lhs=lhs, rhs=rhs}
    3.16 +               (Const (@{const_name Trueprop},_) $ lhs)
    3.17 +               $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
    3.18    | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
    3.19    | dest_equal tm = S.dest_eq tm;
    3.20  
    3.21 @@ -759,7 +759,7 @@
    3.22                val cntxt = rev(Simplifier.prems_of_ss ss)
    3.23                val dummy = print_thms "cntxt:" cntxt
    3.24                val thy = Thm.theory_of_thm thm
    3.25 -              val Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ _ = Thm.prop_of thm
    3.26 +              val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
    3.27                fun genl tm = let val vlist = subtract (op aconv) globals
    3.28                                             (OldTerm.add_term_frees(tm,[]))
    3.29                              in fold_rev Forall vlist tm
     4.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 12:11:57 2010 +0200
     4.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 16:03:01 2010 +0200
     4.3 @@ -483,7 +483,7 @@
     4.4       val (case_rewrites,context_congs) = extraction_thms thy
     4.5       val tych = Thry.typecheck thy
     4.6       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
     4.7 -     val Const(@{const_name "All"},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
     4.8 +     val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
     4.9       val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
    4.10                     Rtype)
    4.11       val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
     5.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 12:11:57 2010 +0200
     5.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 16:03:01 2010 +0200
     5.3 @@ -165,19 +165,19 @@
     5.4  
     5.5  fun mk_select (r as {Bvar,Body}) =
     5.6    let val ty = type_of Bvar
     5.7 -      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
     5.8 +      val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
     5.9    in list_comb(c,[mk_abs r])
    5.10    end;
    5.11  
    5.12  fun mk_forall (r as {Bvar,Body}) =
    5.13    let val ty = type_of Bvar
    5.14 -      val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
    5.15 +      val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
    5.16    in list_comb(c,[mk_abs r])
    5.17    end;
    5.18  
    5.19  fun mk_exists (r as {Bvar,Body}) =
    5.20    let val ty = type_of Bvar
    5.21 -      val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
    5.22 +      val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
    5.23    in list_comb(c,[mk_abs r])
    5.24    end;
    5.25  
    5.26 @@ -250,13 +250,13 @@
    5.27  fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
    5.28    | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
    5.29  
    5.30 -fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
    5.31 +fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
    5.32    | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
    5.33  
    5.34 -fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
    5.35 +fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
    5.36    | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
    5.37  
    5.38 -fun dest_neg(Const("not",_) $ M) = M
    5.39 +fun dest_neg(Const(@{const_name Not},_) $ M) = M
    5.40    | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
    5.41  
    5.42  fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
    5.43 @@ -402,6 +402,6 @@
    5.44    | is_WFR _                 = false;
    5.45  
    5.46  fun ARB ty = mk_select{Bvar=Free("v",ty),
    5.47 -                       Body=Const(@{const_name "True"},HOLogic.boolT)};
    5.48 +                       Body=Const(@{const_name True},HOLogic.boolT)};
    5.49  
    5.50  end;