added is_norm_hhf (from logic.ML);
authorwenzelm
Thu Jan 17 21:02:52 2002 +0100 (2002-01-17)
changeset 12800abcf9fd6ee65
parent 12799 5472afdd3bd3
child 12801 a94cef8982cc
added is_norm_hhf (from logic.ML);
norm_hhf based on fast Pattern.rewrite_term;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Thu Jan 17 21:02:18 2002 +0100
     1.2 +++ b/src/Pure/drule.ML	Thu Jan 17 21:02:52 2002 +0100
     1.3 @@ -107,6 +107,8 @@
     1.4    val del_rules: thm list -> thm list -> thm list
     1.5    val merge_rules: thm list * thm list -> thm list
     1.6    val norm_hhf_eq: thm
     1.7 +  val is_norm_hhf: term -> bool
     1.8 +  val norm_hhf: Sign.sg -> term -> term
     1.9    val triv_goal: thm
    1.10    val rev_triv_goal: thm
    1.11    val implies_intr_goals: cterm list -> thm -> thm
    1.12 @@ -485,7 +487,7 @@
    1.13  fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
    1.14  
    1.15  (*Useful "distance" function for BEST_FIRST*)
    1.16 -val size_of_thm = size_of_term o #prop o rep_thm;
    1.17 +val size_of_thm = size_of_term o prop_of;
    1.18  
    1.19  (*maintain lists of theorems --- preserving canonical order*)
    1.20  fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
    1.21 @@ -684,6 +686,18 @@
    1.22      |> store_standard_thm_open "norm_hhf_eq"
    1.23    end;
    1.24  
    1.25 +fun is_norm_hhf tm =
    1.26 +  let
    1.27 +    fun is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
    1.28 +      | is_norm (t $ u) = is_norm t andalso is_norm u
    1.29 +      | is_norm (Abs (_, _, t)) = is_norm t
    1.30 +      | is_norm _ = true;
    1.31 +  in is_norm (Pattern.beta_eta_contract tm) end;
    1.32 +
    1.33 +fun norm_hhf sg t =
    1.34 +  if is_norm_hhf t then t
    1.35 +  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] t;
    1.36 +
    1.37  
    1.38  (*** Instantiate theorem th, reading instantiations under signature sg ****)
    1.39  
    1.40 @@ -692,7 +706,7 @@
    1.41  
    1.42  fun read_instantiate_sg sg sinsts th =
    1.43      let val ts = types_sorts th;
    1.44 -        val used = add_term_tvarnames(#prop(rep_thm th),[]);
    1.45 +        val used = add_term_tvarnames (prop_of th, []);
    1.46      in  instantiate (read_insts sg ts ts used sinsts) th  end;
    1.47  
    1.48  (*Instantiate theorem th, reading instantiations under theory of th*)
    1.49 @@ -797,8 +811,8 @@
    1.50  fun tvars_of_terms ts = rev (foldl Term.add_tvars ([], ts));
    1.51  fun vars_of_terms ts = rev (foldl Term.add_vars ([], ts));
    1.52  
    1.53 -fun tvars_of thm = tvars_of_terms [#prop (Thm.rep_thm thm)];
    1.54 -fun vars_of thm = vars_of_terms [#prop (Thm.rep_thm thm)];
    1.55 +fun tvars_of thm = tvars_of_terms [prop_of thm];
    1.56 +fun vars_of thm = vars_of_terms [prop_of thm];
    1.57  
    1.58  
    1.59  (* instantiate by left-to-right occurrence of variables *)