src/HOL/WF.ML
changeset 1465 5d7a7e439cec
parent 1264 3eb91524b938
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/WF.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/WF.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title: 	HOL/wf.ML
     1.5 +(*  Title:      HOL/WF.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow
     1.8 +    Author:     Tobias Nipkow
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11 -For wf.thy.  Well-founded Recursion
    1.12 +For WF.thy.  Well-founded Recursion
    1.13  *)
    1.14  
    1.15  open WF;
    1.16 @@ -33,8 +33,8 @@
    1.17  (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    1.18  fun wf_ind_tac a prems i = 
    1.19      EVERY [res_inst_tac [("a",a)] wf_induct i,
    1.20 -	   rename_last_tac a ["1"] (i+1),
    1.21 -	   ares_tac prems i];
    1.22 +           rename_last_tac a ["1"] (i+1),
    1.23 +           ares_tac prems i];
    1.24  
    1.25  val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
    1.26  by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
    1.27 @@ -92,14 +92,14 @@
    1.28      ares_tac (TrueI::hyps) ORELSE' 
    1.29      (cut_facts_tac hyps THEN'
    1.30         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
    1.31 -		        eresolve_tac [transD, mp, allE]));
    1.32 +                        eresolve_tac [transD, mp, allE]));
    1.33  
    1.34  (*** NOTE! some simplifications need a different finish_tac!! ***)
    1.35  fun indhyp_tac hyps =
    1.36      resolve_tac (TrueI::refl::hyps) ORELSE' 
    1.37      (cut_facts_tac hyps THEN'
    1.38         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
    1.39 -		        eresolve_tac [transD, mp, allE]));
    1.40 +                        eresolve_tac [transD, mp, allE]));
    1.41  val wf_super_ss = !simpset setsolver indhyp_tac;
    1.42  
    1.43  val prems = goalw WF.thy [is_recfun_def,cut_def]
    1.44 @@ -167,14 +167,14 @@
    1.45      "!!r. [| wf(r);  trans(r) |] ==> \
    1.46  \    wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
    1.47  by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
    1.48 -	    REPEAT o atac, rtac H_cong1]);
    1.49 +            REPEAT o atac, rtac H_cong1]);
    1.50  by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1);
    1.51  qed "wftrec";
    1.52  
    1.53  (*Unused but perhaps interesting*)
    1.54  val prems = goal WF.thy
    1.55      "[| wf(r);  trans(r);  !!f x. H x (cut f r x) = H x f |] ==> \
    1.56 -\		wftrec r a H = H a (%x.wftrec r x H)";
    1.57 +\               wftrec r a H = H a (%x.wftrec r x H)";
    1.58  by (rtac (wftrec RS trans) 1);
    1.59  by (REPEAT (resolve_tac prems 1));
    1.60  qed "wftrec2";