tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
authorlcp
Fri Oct 22 11:25:15 1993 +0100 (1993-10-22)
changeset 69e7588b53d6b0
parent 68 d8f380764934
child 70 8a29f8b4aca1
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
right sides of the defs
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Oct 22 10:31:19 1993 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Oct 22 11:25:15 1993 +0100
     1.3 @@ -376,20 +376,41 @@
     1.4  fun asm_rewrite_goal_tac prover_tac mss i =
     1.5        PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i);
     1.6  
     1.7 -(*Rewrite or fold throughout proof state. *)
     1.8 -fun rewrite_tac thms = PRIMITIVE(rewrite_rule thms);
     1.9 -fun fold_tac rths = rewrite_tac (map symmetric rths);
    1.10 +(*Rewrite throughout proof state. *)
    1.11 +fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
    1.12  
    1.13  (*Rewrite subgoals only, not main goal. *)
    1.14 -fun rewrite_goals_tac thms = PRIMITIVE (rewrite_goals_rule thms);
    1.15 -fun fold_goals_tac rths = rewrite_goals_tac (map symmetric rths);
    1.16 +fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.17  
    1.18 -fun rewtac rth = rewrite_goals_tac [rth];
    1.19 +fun rewtac def = rewrite_goals_tac [def];
    1.20  
    1.21  
    1.22 -(** Renaming of parameters in a subgoal
    1.23 -    Names may contain letters, digits or primes and must be
    1.24 -    separated by blanks **)
    1.25 +(*** Tactic for folding definitions, handling critical pairs ***)
    1.26 +
    1.27 +(*The depth of nesting in a term*)
    1.28 +fun term_depth (Abs(a,T,t)) = 1 + term_depth t
    1.29 +  | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
    1.30 +  | term_depth _ = 0;
    1.31 +
    1.32 +val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
    1.33 +
    1.34 +(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
    1.35 +  Returns longest lhs first to avoid folding its subexpressions.*)
    1.36 +fun sort_lhs_depths defs =
    1.37 +  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
    1.38 +      val keys = distinct (sort op> (map #2 keylist))
    1.39 +  in  map (keyfilter keylist) keys  end;
    1.40 +
    1.41 +fun fold_tac defs = EVERY 
    1.42 +    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
    1.43 +
    1.44 +fun fold_goals_tac defs = EVERY 
    1.45 +    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
    1.46 +
    1.47 +
    1.48 +(*** Renaming of parameters in a subgoal
    1.49 +     Names may contain letters, digits or primes and must be
    1.50 +     separated by blanks ***)
    1.51  
    1.52  (*Calling this will generate the warning "Same as previous level" since
    1.53    it affects nothing but the names of bound variables!*)