src/HOL/WF.ML
changeset 923 ff1574a81019
child 950 323f8ca4587a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/WF.ML	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,198 @@
     1.4 +(*  Title: 	HOL/wf.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For wf.thy.  Well-founded Recursion
    1.10 +*)
    1.11 +
    1.12 +open WF;
    1.13 +
    1.14 +val H_cong = read_instantiate [("f","H::[?'a, ?'a=>?'b]=>?'b")]
    1.15 +               (standard(refl RS cong RS cong));
    1.16 +val H_cong1 = refl RS H_cong;
    1.17 +
    1.18 +(*Restriction to domain A.  If r is well-founded over A then wf(r)*)
    1.19 +val [prem1,prem2] = goalw WF.thy [wf_def]
    1.20 + "[| r <= Sigma A (%u.A);  \
    1.21 +\    !!x P. [| ! x. (! y. <y,x> : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
    1.22 +\ ==>  wf(r)";
    1.23 +by (strip_tac 1);
    1.24 +by (rtac allE 1);
    1.25 +by (assume_tac 1);
    1.26 +by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
    1.27 +qed "wfI";
    1.28 +
    1.29 +val major::prems = goalw WF.thy [wf_def]
    1.30 +    "[| wf(r);          \
    1.31 +\       !!x.[| ! y. <y,x>: r --> P(y) |] ==> P(x) \
    1.32 +\    |]  ==>  P(a)";
    1.33 +by (rtac (major RS spec RS mp RS spec) 1);
    1.34 +by (fast_tac (HOL_cs addEs prems) 1);
    1.35 +qed "wf_induct";
    1.36 +
    1.37 +(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
    1.38 +fun wf_ind_tac a prems i = 
    1.39 +    EVERY [res_inst_tac [("a",a)] wf_induct i,
    1.40 +	   rename_last_tac a ["1"] (i+1),
    1.41 +	   ares_tac prems i];
    1.42 +
    1.43 +val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
    1.44 +by (subgoal_tac "! x. <a,x>:r --> <x,a>:r --> P" 1);
    1.45 +by (fast_tac (HOL_cs addIs prems) 1);
    1.46 +by (wf_ind_tac "a" prems 1);
    1.47 +by (fast_tac set_cs 1);
    1.48 +qed "wf_asym";
    1.49 +
    1.50 +val prems = goal WF.thy "[| wf(r);  <a,a>: r |] ==> P";
    1.51 +by (rtac wf_asym 1);
    1.52 +by (REPEAT (resolve_tac prems 1));
    1.53 +qed "wf_anti_refl";
    1.54 +
    1.55 +(*transitive closure of a WF relation is WF!*)
    1.56 +val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
    1.57 +by (rewtac wf_def);
    1.58 +by (strip_tac 1);
    1.59 +(*must retain the universal formula for later use!*)
    1.60 +by (rtac allE 1 THEN assume_tac 1);
    1.61 +by (etac mp 1);
    1.62 +by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
    1.63 +by (rtac (impI RS allI) 1);
    1.64 +by (etac tranclE 1);
    1.65 +by (fast_tac HOL_cs 1);
    1.66 +by (fast_tac HOL_cs 1);
    1.67 +qed "wf_trancl";
    1.68 +
    1.69 +
    1.70 +(** cut **)
    1.71 +
    1.72 +(*This rewrite rule works upon formulae; thus it requires explicit use of
    1.73 +  H_cong to expose the equality*)
    1.74 +goalw WF.thy [cut_def]
    1.75 +    "(cut f r x = cut g r x) = (!y. <y,x>:r --> f(y)=g(y))";
    1.76 +by(simp_tac (HOL_ss addsimps [expand_fun_eq]
    1.77 +                    setloop (split_tac [expand_if])) 1);
    1.78 +qed "cut_cut_eq";
    1.79 +
    1.80 +goalw WF.thy [cut_def] "!!x. <x,a>:r ==> (cut f r a)(x) = f(x)";
    1.81 +by(asm_simp_tac HOL_ss 1);
    1.82 +qed "cut_apply";
    1.83 +
    1.84 +
    1.85 +(*** is_recfun ***)
    1.86 +
    1.87 +goalw WF.thy [is_recfun_def,cut_def]
    1.88 +    "!!f. [| is_recfun r a H f;  ~<b,a>:r |] ==> f(b) = (@z.True)";
    1.89 +by (etac ssubst 1);
    1.90 +by(asm_simp_tac HOL_ss 1);
    1.91 +qed "is_recfun_undef";
    1.92 +
    1.93 +(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
    1.94 +  mp amd allE  instantiate induction hypotheses*)
    1.95 +fun indhyp_tac hyps =
    1.96 +    ares_tac (TrueI::hyps) ORELSE' 
    1.97 +    (cut_facts_tac hyps THEN'
    1.98 +       DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
    1.99 +		        eresolve_tac [transD, mp, allE]));
   1.100 +
   1.101 +(*** NOTE! some simplifications need a different finish_tac!! ***)
   1.102 +fun indhyp_tac hyps =
   1.103 +    resolve_tac (TrueI::refl::hyps) ORELSE' 
   1.104 +    (cut_facts_tac hyps THEN'
   1.105 +       DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
   1.106 +		        eresolve_tac [transD, mp, allE]));
   1.107 +val wf_super_ss = HOL_ss setsolver indhyp_tac;
   1.108 +
   1.109 +val prems = goalw WF.thy [is_recfun_def,cut_def]
   1.110 +    "[| wf(r);  trans(r);  is_recfun r a H f;  is_recfun r b H g |] ==> \
   1.111 +    \ <x,a>:r --> <x,b>:r --> f(x)=g(x)";
   1.112 +by (cut_facts_tac prems 1);
   1.113 +by (etac wf_induct 1);
   1.114 +by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   1.115 +by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
   1.116 +qed "is_recfun_equal_lemma";
   1.117 +bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
   1.118 +
   1.119 +
   1.120 +val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
   1.121 +    "[| wf(r);  trans(r); \
   1.122 +\       is_recfun r a H f;  is_recfun r b H g;  <b,a>:r |] ==> \
   1.123 +\    cut f r b = g";
   1.124 +val gundef = recgb RS is_recfun_undef
   1.125 +and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
   1.126 +by (cut_facts_tac prems 1);
   1.127 +by (rtac ext 1);
   1.128 +by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
   1.129 +                              setloop (split_tac [expand_if])) 1);
   1.130 +qed "is_recfun_cut";
   1.131 +
   1.132 +(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
   1.133 +
   1.134 +val prems = goalw WF.thy [the_recfun_def]
   1.135 +    "is_recfun r a H f ==> is_recfun r a H (the_recfun r a H)";
   1.136 +by (res_inst_tac [("P", "is_recfun r a H")] selectI 1);
   1.137 +by (resolve_tac prems 1);
   1.138 +qed "is_the_recfun";
   1.139 +
   1.140 +val prems = goal WF.thy
   1.141 +    "[| wf(r);  trans(r) |] ==> is_recfun r a H (the_recfun r a H)";
   1.142 +by (cut_facts_tac prems 1);
   1.143 +by (wf_ind_tac "a" prems 1);
   1.144 +by (res_inst_tac [("f", "cut (%y. wftrec r y H) r a1")] is_the_recfun 1);
   1.145 +by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
   1.146 +by (rtac (cut_cut_eq RS ssubst) 1);
   1.147 +(*Applying the substitution: must keep the quantified assumption!!*)
   1.148 +by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
   1.149 +            etac (mp RS ssubst), atac]);
   1.150 +by (fold_tac [is_recfun_def]);
   1.151 +by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1);
   1.152 +qed "unfold_the_recfun";
   1.153 +
   1.154 +
   1.155 +(*Beware incompleteness of unification!*)
   1.156 +val prems = goal WF.thy
   1.157 +    "[| wf(r);  trans(r);  <c,a>:r;  <c,b>:r |] \
   1.158 +\    ==> the_recfun r a H c = the_recfun r b H c";
   1.159 +by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
   1.160 +qed "the_recfun_equal";
   1.161 +
   1.162 +val prems = goal WF.thy
   1.163 +    "[| wf(r); trans(r); <b,a>:r |] \
   1.164 +\    ==> cut (the_recfun r a H) r b = the_recfun r b H";
   1.165 +by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
   1.166 +qed "the_recfun_cut";
   1.167 +
   1.168 +(*** Unfolding wftrec ***)
   1.169 +
   1.170 +goalw WF.thy [wftrec_def]
   1.171 +    "!!r. [| wf(r);  trans(r) |] ==> \
   1.172 +\    wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
   1.173 +by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
   1.174 +	    REPEAT o atac, rtac H_cong1]);
   1.175 +by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1);
   1.176 +qed "wftrec";
   1.177 +
   1.178 +(*Unused but perhaps interesting*)
   1.179 +val prems = goal WF.thy
   1.180 +    "[| wf(r);  trans(r);  !!f x. H x (cut f r x) = H x f |] ==> \
   1.181 +\		wftrec r a H = H a (%x.wftrec r x H)";
   1.182 +by (rtac (wftrec RS trans) 1);
   1.183 +by (REPEAT (resolve_tac prems 1));
   1.184 +qed "wftrec2";
   1.185 +
   1.186 +(** Removal of the premise trans(r) **)
   1.187 +
   1.188 +goalw WF.thy [wfrec_def]
   1.189 +    "!!r. wf(r) ==> wfrec r a H = H a (cut (%x.wfrec r x H) r a)";
   1.190 +by (etac (wf_trancl RS wftrec RS ssubst) 1);
   1.191 +by (rtac trans_trancl 1);
   1.192 +by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)
   1.193 +by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
   1.194 +qed "wfrec";
   1.195 +
   1.196 +(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   1.197 +val rew::prems = goal WF.thy
   1.198 +    "[| !!x. f(x)==wfrec r x H;  wf(r) |] ==> f(a) = H a (cut (%x.f(x)) r a)";
   1.199 +by (rewtac rew);
   1.200 +by (REPEAT (resolve_tac (prems@[wfrec]) 1));
   1.201 +qed "def_wfrec";