1.1 --- a/src/HOL/Import/proof_kernel.ML Thu Aug 19 16:08:53 2010 +0200
1.2 +++ b/src/HOL/Import/proof_kernel.ML Thu Aug 19 16:08:54 2010 +0200
1.3 @@ -1006,7 +1006,7 @@
1.4 local
1.5 val th = thm "not_def"
1.6 val thy = theory_of_thm th
1.7 - val pp = Thm.reflexive (cterm_of thy (Const(@{const_name "Trueprop"},HOLogic.boolT-->propT)))
1.8 + val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
1.9 in
1.10 val not_elim_thm = Thm.combination pp th
1.11 end
1.12 @@ -1052,9 +1052,9 @@
1.13 val c = prop_of th3
1.14 val vname = fst(dest_Free v)
1.15 val (cold,cnew) = case c of
1.16 - tpc $ (Const(@{const_name "All"},allT) $ Abs(oldname,ty,body)) =>
1.17 + tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
1.18 (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
1.19 - | tpc $ (Const(@{const_name "All"},allT) $ rest) => (tpc,tpc)
1.20 + | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
1.21 | _ => raise ERR "mk_GEN" "Unknown conclusion"
1.22 val th4 = Thm.rename_boundvars cold cnew th3
1.23 val res = implies_intr_hyps th4
1.24 @@ -1204,7 +1204,8 @@
1.25
1.26 fun non_trivial_term_consts t = fold_aterms
1.27 (fn Const (c, _) =>
1.28 - if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
1.29 + if c = @{const_name Trueprop} orelse c = @{const_name All}
1.30 + orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
1.31 then I else insert (op =) c
1.32 | _ => I) t [];
1.33
1.34 @@ -1212,12 +1213,12 @@
1.35 let
1.36 fun add_consts (Const (c, _), cs) =
1.37 (case c of
1.38 - "op =" => insert (op =) "==" cs
1.39 - | "op -->" => insert (op =) "==>" cs
1.40 - | "All" => cs
1.41 + @{const_name "op ="} => insert (op =) "==" cs
1.42 + | @{const_name "op -->"} => insert (op =) "==>" cs
1.43 + | @{const_name All} => cs
1.44 | "all" => cs
1.45 - | "op &" => cs
1.46 - | "Trueprop" => cs
1.47 + | @{const_name "op &"} => cs
1.48 + | @{const_name Trueprop} => cs
1.49 | _ => insert (op =) c cs)
1.50 | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
1.51 | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
1.52 @@ -1653,7 +1654,7 @@
1.53 val cwit = cterm_of thy wit'
1.54 val cty = ctyp_of_term cwit
1.55 val a = case ex' of
1.56 - (Const(@{const_name "Ex"},_) $ a) => a
1.57 + (Const(@{const_name Ex},_) $ a) => a
1.58 | _ => raise ERR "EXISTS" "Argument not existential"
1.59 val ca = cterm_of thy a
1.60 val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
1.61 @@ -1686,7 +1687,7 @@
1.62 val c = HOLogic.dest_Trueprop (concl_of th2)
1.63 val cc = cterm_of thy c
1.64 val a = case concl_of th1 of
1.65 - _ $ (Const(@{const_name "Ex"},_) $ a) => a
1.66 + _ $ (Const(@{const_name Ex},_) $ a) => a
1.67 | _ => raise ERR "CHOOSE" "Conclusion not existential"
1.68 val ca = cterm_of (theory_of_thm th1) a
1.69 val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
1.70 @@ -1772,7 +1773,7 @@
1.71 val (info',tm') = disamb_term_from info tm
1.72 val th = norm_hyps th
1.73 val ct = cterm_of thy tm'
1.74 - val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name "Not"},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
1.75 + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
1.76 val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
1.77 val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
1.78 val res = HOLThm(rens_of info',res1)
1.79 @@ -1859,7 +1860,7 @@
1.80 val _ = if_debug pth hth
1.81 val th1 = implies_elim_all (beta_eta_thm th)
1.82 val a = case concl_of th1 of
1.83 - _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name "False"},_)) => a
1.84 + _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
1.85 | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
1.86 val ca = cterm_of thy a
1.87 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
1.88 @@ -1876,7 +1877,7 @@
1.89 val _ = if_debug pth hth
1.90 val th1 = implies_elim_all (beta_eta_thm th)
1.91 val a = case concl_of th1 of
1.92 - _ $ (Const(@{const_name "Not"},_) $ a) => a
1.93 + _ $ (Const(@{const_name Not},_) $ a) => a
1.94 | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
1.95 val ca = cterm_of thy a
1.96 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
1.97 @@ -1995,7 +1996,7 @@
1.98 ("x",dT,body $ Bound 0)
1.99 end
1.100 handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
1.101 - fun dest_exists (Const(@{const_name "Ex"},_) $ abody) =
1.102 + fun dest_exists (Const(@{const_name Ex},_) $ abody) =
1.103 dest_eta_abs abody
1.104 | dest_exists tm =
1.105 raise ERR "new_specification" "Bad existential formula"
1.106 @@ -2081,7 +2082,7 @@
1.107 val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.108 val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
1.109 val c = case concl_of th2 of
1.110 - _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.111 + _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.112 | _ => raise ERR "new_type_definition" "Bad type definition theorem"
1.113 val tfrees = OldTerm.term_tfrees c
1.114 val tnames = map fst tfrees
1.115 @@ -2107,7 +2108,7 @@
1.116 val rew = rewrite_hol4_term (concl_of td_th) thy4
1.117 val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
1.118 val c = case HOLogic.dest_Trueprop (prop_of th) of
1.119 - Const(@{const_name "Ex"},exT) $ P =>
1.120 + Const(@{const_name Ex},exT) $ P =>
1.121 let
1.122 val PT = domain_type exT
1.123 in
1.124 @@ -2156,7 +2157,7 @@
1.125 SOME (cterm_of thy t)] light_nonempty
1.126 val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
1.127 val c = case concl_of th2 of
1.128 - _ $ (Const(@{const_name "Ex"},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.129 + _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
1.130 | _ => raise ERR "type_introduction" "Bad type definition theorem"
1.131 val tfrees = OldTerm.term_tfrees c
1.132 val tnames = sort_strings (map fst tfrees)
2.1 --- a/src/HOL/Prolog/prolog.ML Thu Aug 19 16:08:53 2010 +0200
2.2 +++ b/src/HOL/Prolog/prolog.ML Thu Aug 19 16:08:54 2010 +0200
2.3 @@ -10,17 +10,17 @@
2.4 exception not_HOHH;
2.5
2.6 fun isD t = case t of
2.7 - Const(@{const_name "Trueprop"},_)$t => isD t
2.8 + Const(@{const_name Trueprop},_)$t => isD t
2.9 | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
2.10 | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
2.11 | Const( "==>",_)$l$r => isG l andalso isD r
2.12 - | Const(@{const_name "All"},_)$Abs(s,_,t) => isD t
2.13 + | Const(@{const_name All},_)$Abs(s,_,t) => isD t
2.14 | Const("all",_)$Abs(s,_,t) => isD t
2.15 | Const(@{const_name "op |"},_)$_$_ => false
2.16 - | Const(@{const_name "Ex"} ,_)$_ => false
2.17 - | Const("not",_)$_ => false
2.18 - | Const(@{const_name "True"},_) => false
2.19 - | Const(@{const_name "False"},_) => false
2.20 + | Const(@{const_name Ex} ,_)$_ => false
2.21 + | Const(@{const_name Not},_)$_ => false
2.22 + | Const(@{const_name True},_) => false
2.23 + | Const(@{const_name False},_) => false
2.24 | l $ r => isD l
2.25 | Const _ (* rigid atom *) => true
2.26 | Bound _ (* rigid atom *) => true
2.27 @@ -29,17 +29,17 @@
2.28 anything else *) => false
2.29 and
2.30 isG t = case t of
2.31 - Const(@{const_name "Trueprop"},_)$t => isG t
2.32 + Const(@{const_name Trueprop},_)$t => isG t
2.33 | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
2.34 | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
2.35 | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
2.36 | Const( "==>",_)$l$r => isD l andalso isG r
2.37 - | Const(@{const_name "All"},_)$Abs(_,_,t) => isG t
2.38 + | Const(@{const_name All},_)$Abs(_,_,t) => isG t
2.39 | Const("all",_)$Abs(_,_,t) => isG t
2.40 - | Const(@{const_name "Ex"} ,_)$Abs(_,_,t) => isG t
2.41 - | Const(@{const_name "True"},_) => true
2.42 - | Const("not",_)$_ => false
2.43 - | Const(@{const_name "False"},_) => false
2.44 + | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
2.45 + | Const(@{const_name True},_) => true
2.46 + | Const(@{const_name Not},_)$_ => false
2.47 + | Const(@{const_name False},_) => false
2.48 | _ (* atom *) => true;
2.49
2.50 val check_HOHH_tac1 = PRIMITIVE (fn thm =>
2.51 @@ -51,7 +51,7 @@
2.52
2.53 fun atomizeD ctxt thm = let
2.54 fun at thm = case concl_of thm of
2.55 - _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS
2.56 + _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
2.57 (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
2.58 | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
2.59 | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
2.60 @@ -71,7 +71,7 @@
2.61 resolve_tac (maps atomizeD prems) 1);
2.62 -- is nice, but cannot instantiate unknowns in the assumptions *)
2.63 fun hyp_resolve_tac i st = let
2.64 - fun ap (Const(@{const_name "All"},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
2.65 + fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
2.66 | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
2.67 | ap t = (0,false,t);
2.68 (*
2.69 @@ -79,7 +79,7 @@
2.70 | rep_goal (Const ("==>",_)$s$t) =
2.71 (case rep_goal t of (l,t) => (s::l,t))
2.72 | rep_goal t = ([] ,t);
2.73 - val (prems, Const(@{const_name "Trueprop"}, _)$concl) = rep_goal
2.74 + val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
2.75 (#3(dest_state (st,i)));
2.76 *)
2.77 val subgoal = #3(Thm.dest_state (st,i));
3.1 --- a/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:53 2010 +0200
3.2 +++ b/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:54 2010 +0200
3.3 @@ -149,7 +149,7 @@
3.4 fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
3.5 let
3.6 val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
3.7 - = Term.strip_qnt_body "Ex" c
3.8 + = Term.strip_qnt_body @{const_name Ex} c
3.9 in cons r o cons l end
3.10 in
3.11 mk_skel (fold collect_pats cs [])
3.12 @@ -182,11 +182,11 @@
3.13 fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
3.14 let
3.15 val (sk, _, _, _, _) = D
3.16 - val vs = Term.strip_qnt_vars "Ex" c
3.17 + val vs = Term.strip_qnt_vars @{const_name Ex} c
3.18
3.19 (* FIXME: throw error "dest_call" for malformed terms *)
3.20 val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
3.21 - = Term.strip_qnt_body "Ex" c
3.22 + = Term.strip_qnt_body @{const_name Ex} c
3.23 val (p, l') = dest_inj sk l
3.24 val (q, r') = dest_inj sk r
3.25 in
4.1 --- a/src/HOL/Tools/meson.ML Thu Aug 19 16:08:53 2010 +0200
4.2 +++ b/src/HOL/Tools/meson.ML Thu Aug 19 16:08:54 2010 +0200
4.3 @@ -149,21 +149,21 @@
4.4 (*Are any of the logical connectives in "bs" present in the term?*)
4.5 fun has_conns bs =
4.6 let fun has (Const(a,_)) = false
4.7 - | has (Const(@{const_name "Trueprop"},_) $ p) = has p
4.8 - | has (Const(@{const_name "Not"},_) $ p) = has p
4.9 - | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
4.10 - | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
4.11 - | has (Const(@{const_name "All"},_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
4.12 - | has (Const(@{const_name "Ex"},_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
4.13 + | has (Const(@{const_name Trueprop},_) $ p) = has p
4.14 + | has (Const(@{const_name Not},_) $ p) = has p
4.15 + | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
4.16 + | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
4.17 + | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
4.18 + | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
4.19 | has _ = false
4.20 in has end;
4.21
4.22
4.23 (**** Clause handling ****)
4.24
4.25 -fun literals (Const(@{const_name "Trueprop"},_) $ P) = literals P
4.26 +fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
4.27 | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
4.28 - | literals (Const(@{const_name "Not"},_) $ P) = [(false,P)]
4.29 + | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
4.30 | literals P = [(true,P)];
4.31
4.32 (*number of literals in a term*)
4.33 @@ -174,14 +174,14 @@
4.34
4.35 fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
4.36 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
4.37 - | signed_lits_aux (Const(@{const_name "Not"},_) $ P) (poslits, neglits) = (poslits, P::neglits)
4.38 + | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
4.39 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
4.40
4.41 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
4.42
4.43 (*Literals like X=X are tautologous*)
4.44 fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
4.45 - | taut_poslit (Const(@{const_name "True"},_)) = true
4.46 + | taut_poslit (Const(@{const_name True},_)) = true
4.47 | taut_poslit _ = false;
4.48
4.49 fun is_taut th =
4.50 @@ -210,7 +210,7 @@
4.51 case HOLogic.dest_Trueprop (concl_of th) of
4.52 (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
4.53 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
4.54 - | (Const (@{const_name "op |"}, _) $ (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
4.55 + | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
4.56 if eliminable(t,u)
4.57 then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
4.58 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
4.59 @@ -219,7 +219,7 @@
4.60
4.61 fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
4.62 notequal_lits_count P + notequal_lits_count Q
4.63 - | notequal_lits_count (Const(@{const_name "Not"},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
4.64 + | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
4.65 | notequal_lits_count _ = 0;
4.66
4.67 (*Simplify a clause by applying reflexivity to its negated equality literals*)
4.68 @@ -266,8 +266,8 @@
4.69 fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
4.70
4.71 (*Estimate the number of clauses in order to detect infeasible theorems*)
4.72 - fun signed_nclauses b (Const(@{const_name "Trueprop"},_) $ t) = signed_nclauses b t
4.73 - | signed_nclauses b (Const(@{const_name "Not"},_) $ t) = signed_nclauses (not b) t
4.74 + fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
4.75 + | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
4.76 | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
4.77 if b then sum (signed_nclauses b t) (signed_nclauses b u)
4.78 else prod (signed_nclauses b t) (signed_nclauses b u)
4.79 @@ -284,8 +284,8 @@
4.80 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
4.81 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
4.82 else 1
4.83 - | signed_nclauses b (Const(@{const_name "Ex"}, _) $ Abs (_,_,t)) = signed_nclauses b t
4.84 - | signed_nclauses b (Const(@{const_name "All"},_) $ Abs (_,_,t)) = signed_nclauses b t
4.85 + | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
4.86 + | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
4.87 | signed_nclauses _ _ = 1; (* literal *)
4.88 in
4.89 signed_nclauses true t >= max_cl
4.90 @@ -296,7 +296,7 @@
4.91 local
4.92 val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
4.93 val spec_varT = #T (Thm.rep_cterm spec_var);
4.94 - fun name_of (Const (@{const_name "All"}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
4.95 + fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
4.96 in
4.97 fun freeze_spec th ctxt =
4.98 let
4.99 @@ -314,8 +314,7 @@
4.100
4.101 (*Any need to extend this list with
4.102 "HOL.type_class","HOL.eq_class","Pure.term"?*)
4.103 -val has_meta_conn =
4.104 - exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
4.105 +val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
4.106
4.107 fun apply_skolem_theorem (th, rls) =
4.108 let
4.109 @@ -331,15 +330,15 @@
4.110 let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
4.111 fun cnf_aux (th,ths) =
4.112 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
4.113 - else if not (has_conns ["All","Ex","op &"] (prop_of th))
4.114 + else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
4.115 then nodups ctxt th :: ths (*no work to do, terminate*)
4.116 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
4.117 Const (@{const_name "op &"}, _) => (*conjunction*)
4.118 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
4.119 - | Const (@{const_name "All"}, _) => (*universal quantifier*)
4.120 + | Const (@{const_name All}, _) => (*universal quantifier*)
4.121 let val (th',ctxt') = freeze_spec th (!ctxtr)
4.122 in ctxtr := ctxt'; cnf_aux (th', ths) end
4.123 - | Const (@{const_name "Ex"}, _) =>
4.124 + | Const (@{const_name Ex}, _) =>
4.125 (*existential quantifier: Insert Skolem functions*)
4.126 cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
4.127 | Const (@{const_name "op |"}, _) =>
4.128 @@ -365,7 +364,7 @@
4.129
4.130 (**** Generation of contrapositives ****)
4.131
4.132 -fun is_left (Const (@{const_name "Trueprop"}, _) $
4.133 +fun is_left (Const (@{const_name Trueprop}, _) $
4.134 (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
4.135 | is_left _ = false;
4.136
4.137 @@ -401,8 +400,9 @@
4.138 (*Is the string the name of a connective? Really only | and Not can remain,
4.139 since this code expects to be called on a clause form.*)
4.140 val is_conn = member (op =)
4.141 - ["Trueprop", "op &", "op |", "op -->", "Not",
4.142 - "All", "Ex", @{const_name Ball}, @{const_name Bex}];
4.143 + [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
4.144 + @{const_name "op -->"}, @{const_name Not},
4.145 + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
4.146
4.147 (*True if the term contains a function--not a logical connective--where the type
4.148 of any argument contains bool.*)
4.149 @@ -420,7 +420,7 @@
4.150 (*Returns false if any Vars in the theorem mention type bool.
4.151 Also rejects functions whose arguments are Booleans or other functions.*)
4.152 fun is_fol_term thy t =
4.153 - Term.is_first_order ["all","All","Ex"] t andalso
4.154 + Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
4.155 not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
4.156 | _ => false) t orelse
4.157 has_bool_arg_const t orelse
4.158 @@ -429,8 +429,8 @@
4.159
4.160 fun rigid t = not (is_Var (head_of t));
4.161
4.162 -fun ok4horn (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
4.163 - | ok4horn (Const (@{const_name "Trueprop"},_) $ t) = rigid t
4.164 +fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
4.165 + | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
4.166 | ok4horn _ = false;
4.167
4.168 (*Create a meta-level Horn clause*)
4.169 @@ -464,7 +464,7 @@
4.170
4.171 (***** MESON PROOF PROCEDURE *****)
4.172
4.173 -fun rhyps (Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ phi,
4.174 +fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
4.175 As) = rhyps(phi, A::As)
4.176 | rhyps (_, As) = As;
4.177
4.178 @@ -509,8 +509,8 @@
4.179 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
4.180 not_impD, not_iffD, not_allD, not_exD, not_notD];
4.181
4.182 -fun ok4nnf (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ t)) = rigid t
4.183 - | ok4nnf (Const (@{const_name "Trueprop"},_) $ t) = rigid t
4.184 +fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
4.185 + | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
4.186 | ok4nnf _ = false;
4.187
4.188 fun make_nnf1 ctxt th =
4.189 @@ -546,7 +546,7 @@
4.190 (*Pull existential quantifiers to front. This accomplishes Skolemization for
4.191 clauses that arise from a subgoal.*)
4.192 fun skolemize1 ctxt th =
4.193 - if not (has_conns ["Ex"] (prop_of th)) then th
4.194 + if not (has_conns [@{const_name Ex}] (prop_of th)) then th
4.195 else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
4.196 disj_exD, disj_exD1, disj_exD2])))
4.197 handle THM ("tryres", _, _) =>
5.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 16:08:53 2010 +0200
5.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Aug 19 16:08:54 2010 +0200
5.3 @@ -122,7 +122,7 @@
5.4 fun at thm =
5.5 case concl_of thm of
5.6 _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
5.7 - | _$(Const(@{const_name "All"} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
5.8 + | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
5.9 | _ => [thm];
5.10 in map zero_var_indexes (at thm) end;
5.11
5.12 @@ -185,7 +185,7 @@
5.13 fun mk_lam (x,T) = Abs(x,dummyT,T);
5.14 fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
5.15 fun mk_ex (x,P) = mk_exists (x,dummyT,P);
5.16 -fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
5.17 +fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
5.18 end
5.19
5.20 fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)