- Added new "undefined" constant
authorberghofe
Fri Jul 21 11:34:01 2006 +0200 (2006-07-21)
changeset 20172b65eb8145f5e
parent 20171 424739228123
child 20173 c8f791af9a60
- Added new "undefined" constant
- normalization_conv no longer expects term to
have form "Trueprop ..."
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Thu Jul 20 14:35:37 2006 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Jul 21 11:34:01 2006 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    True          :: bool
     1.5    False         :: bool
     1.6    arbitrary     :: 'a
     1.7 +  undefined     :: 'a
     1.8  
     1.9    The           :: "('a => bool) => 'a"
    1.10    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.11 @@ -185,6 +186,7 @@
    1.12    "op -->"
    1.13    The
    1.14    arbitrary
    1.15 +  undefined
    1.16  
    1.17  
    1.18  subsubsection {* Generic algebraic operations *}
    1.19 @@ -1281,15 +1283,21 @@
    1.20  
    1.21  exception Normalization of term;
    1.22  
    1.23 -fun normalization_oracle (thy, Normalization t) = Logic.mk_equals
    1.24 -  (t, HOLogic.mk_Trueprop (NBE.norm_term thy (HOLogic.dest_Trueprop t)));
    1.25 +fun normalization_oracle (thy, Normalization t) =
    1.26 +  Logic.mk_equals (t, NBE.norm_term thy t);
    1.27  
    1.28  fun normalization_conv ct =
    1.29    let val {sign, t, ...} = rep_cterm ct
    1.30    in Thm.invoke_oracle_i sign "HOL.Normalization" (sign, Normalization t) end;
    1.31  
    1.32 +fun Trueprop_conv conv ct = (case term_of ct of
    1.33 +    Const ("Trueprop", _) $ _ =>
    1.34 +      let val (ct1, ct2) = Thm.dest_comb ct
    1.35 +      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
    1.36 +  | _ => raise TERM ("Trueprop_conv", []));
    1.37 +
    1.38  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.39 -  (Drule.goals_conv (equal i) normalization_conv));
    1.40 +  (Drule.goals_conv (equal i) (Trueprop_conv normalization_conv)));
    1.41  
    1.42  val normalization_meth =
    1.43    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI,refl] 1));