src/Pure/tactic.ML
changeset 12801 a94cef8982cc
parent 12782 a4183c50ae5f
child 12847 afa356dbcb15
     1.1 --- a/src/Pure/tactic.ML	Thu Jan 17 21:02:52 2002 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Jan 17 21:03:29 2002 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4    val net_biresolve_tac : (bool*thm) list -> int -> tactic
     1.5    val net_match_tac     : thm list -> int -> tactic
     1.6    val net_resolve_tac   : thm list -> int -> tactic
     1.7 -  val norm_hhf          : thm -> thm
     1.8 +  val norm_hhf_rule     : thm -> thm
     1.9    val norm_hhf_tac      : int -> tactic
    1.10    val PRIMITIVE         : (thm -> thm) -> tactic
    1.11    val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
    1.12 @@ -110,7 +110,6 @@
    1.13    val untaglist: (int * 'a) list -> 'a list
    1.14    val orderlist: (int * 'a) list -> 'a list
    1.15    val rewrite: bool -> thm list -> cterm -> thm
    1.16 -  val rewrite_cterm: bool -> thm list -> cterm -> cterm
    1.17    val simplify: bool -> thm list -> thm -> thm
    1.18    val conjunction_tac: tactic
    1.19    val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.20 @@ -242,7 +241,7 @@
    1.21      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    1.22        | types'(ixn) = types ixn;
    1.23      val used = add_term_tvarnames
    1.24 -                  (#prop(rep_thm st) $ #prop(rep_thm rule),[])
    1.25 +                  (prop_of st $ prop_of rule,[])
    1.26      val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
    1.27  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.28                       (lift_rule (st,i) rule)
    1.29 @@ -502,7 +501,6 @@
    1.30    result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    1.31  
    1.32  val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    1.33 -val rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) ooo rewrite;
    1.34  val simplify = MetaSimplifier.simplify_aux simple_prover;
    1.35  val rewrite_rule = simplify true;
    1.36  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.37 @@ -522,14 +520,14 @@
    1.38  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.39  fun rewtac def = rewrite_goals_tac [def];
    1.40  
    1.41 -fun norm_hhf th =
    1.42 -  (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th)
    1.43 -  |> Drule.gen_all;
    1.44 +fun norm_hhf_rule th =
    1.45 + (if Drule.is_norm_hhf (prop_of th) then th
    1.46 +  else rewrite_rule [Drule.norm_hhf_eq] th) |> Drule.gen_all;
    1.47  
    1.48  val norm_hhf_tac =
    1.49    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.50    THEN' SUBGOAL (fn (t, i) =>
    1.51 -    if Logic.is_norm_hhf (Pattern.beta_eta_contract t) then all_tac
    1.52 +    if Drule.is_norm_hhf t then all_tac
    1.53      else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.54  
    1.55  
    1.56 @@ -540,7 +538,7 @@
    1.57    | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
    1.58    | term_depth _ = 0;
    1.59  
    1.60 -val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
    1.61 +val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
    1.62  
    1.63  (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
    1.64    Returns longest lhs first to avoid folding its subexpressions.*)
    1.65 @@ -645,14 +643,14 @@
    1.66  
    1.67      val cparams = map (cert_safe o Free) params;
    1.68      val casms = map cert_safe asms;
    1.69 -    val prems = map (norm_hhf o Thm.assume) casms;
    1.70 +    val prems = map (norm_hhf_rule o Thm.assume) casms;
    1.71      val goal = Drule.mk_triv_goal (cert_safe prop);
    1.72  
    1.73      val goal' =
    1.74        (case Seq.pull (tac prems goal) of Some (goal', _) => goal' | _ => err "Tactic failed.");
    1.75      val ngoals = Thm.nprems_of goal';
    1.76      val raw_result = goal' RS Drule.rev_triv_goal;
    1.77 -    val prop' = #prop (Thm.rep_thm raw_result);
    1.78 +    val prop' = prop_of raw_result;
    1.79    in
    1.80      if ngoals <> 0 then
    1.81        err ("Proof failed.\n" ^ Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal'))
    1.82 @@ -663,7 +661,7 @@
    1.83        raw_result
    1.84        |> Drule.implies_intr_list casms
    1.85        |> Drule.forall_intr_list cparams
    1.86 -      |> norm_hhf
    1.87 +      |> norm_hhf_rule
    1.88        |> (#1 o Thm.varifyT' fixed_tfrees)
    1.89        |> Drule.zero_var_indexes
    1.90    end;