(* Title: HOL/wf.ML ID: $Id$ Author: Tobias Nipkow, with minor changes by Konrad Slind Copyright 1992 University of Cambridge/1995 TU Munich Wellfoundedness, induction, and recursion *) open WF; val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); val H_cong1 = refl RS H_cong; (*Restriction to domain A. If r is well-founded over A then wf(r)*) val [prem1,prem2] = Goalw [wf_def] "[| r <= A Times A; \ \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ \ ==> wf(r)"; by (Clarify_tac 1); by (rtac allE 1); by (assume_tac 1); by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); qed "wfI"; val major::prems = Goalw [wf_def] "[| wf(r); \ \ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ \ |] ==> P(a)"; by (rtac (major RS spec RS mp RS spec) 1); by (blast_tac (claset() addIs prems) 1); qed "wf_induct"; (*Perform induction on i, then prove the wf(r) subgoal using prems. *) fun wf_ind_tac a prems i = EVERY [res_inst_tac [("a",a)] wf_induct i, rename_last_tac a ["1"] (i+1), ares_tac prems i]; Goal "[| wf(r); (a,x):r; (x,a):r |] ==> P"; by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); by (Blast_tac 1); by (wf_ind_tac "a" [] 1); by (Blast_tac 1); qed "wf_asym"; Goal "[| wf(r); (a,a): r |] ==> P"; by (blast_tac (claset() addEs [wf_asym]) 1); qed "wf_irrefl"; (*transitive closure of a wf relation is wf! *) Goal "wf(r) ==> wf(r^+)"; by (stac wf_def 1); by (Clarify_tac 1); (*must retain the universal formula for later use!*) by (rtac allE 1 THEN assume_tac 1); by (etac mp 1); by (eres_inst_tac [("a","x")] wf_induct 1); by (rtac (impI RS allI) 1); by (etac tranclE 1); by (Blast_tac 1); by (Blast_tac 1); qed "wf_trancl"; val wf_converse_trancl = prove_goal thy "!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [ stac (trancl_converse RS sym) 1, etac wf_trancl 1]); (*---------------------------------------------------------------------------- * Minimal-element characterization of well-foundedness *---------------------------------------------------------------------------*) Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)"; by (dtac spec 1); by (etac (mp RS spec) 1); by (Blast_tac 1); val lemma1 = result(); Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r"; by (Clarify_tac 1); by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1); by (Blast_tac 1); val lemma2 = result(); Goal "wf r = (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q))"; by (blast_tac (claset() addSIs [lemma1, lemma2]) 1); qed "wf_eq_minimal"; (*--------------------------------------------------------------------------- * Wellfoundedness of subsets *---------------------------------------------------------------------------*) Goal "[| wf(r); p<=r |] ==> wf(p)"; by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); by (Fast_tac 1); qed "wf_subset"; (*--------------------------------------------------------------------------- * Wellfoundedness of the empty relation. *---------------------------------------------------------------------------*) Goal "wf({})"; by (simp_tac (simpset() addsimps [wf_def]) 1); qed "wf_empty"; AddIffs [wf_empty]; (*--------------------------------------------------------------------------- * Wellfoundedness of `insert' *---------------------------------------------------------------------------*) Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; by (rtac iffI 1); by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); by Safe_tac; by (EVERY1[rtac allE, atac, etac impE, Blast_tac]); by (etac bexE 1); by (rename_tac "a" 1); by (case_tac "a = x" 1); by (res_inst_tac [("x","a")]bexI 2); by (assume_tac 3); by (Blast_tac 2); by (case_tac "y:Q" 1); by (Blast_tac 2); by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1); by (assume_tac 1); by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1); (*essential for speed*) (*Blast_tac with new substOccur fails*) by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); qed "wf_insert"; AddIffs [wf_insert]; (*--------------------------------------------------------------------------- * Wellfoundedness of `disjoint union' *---------------------------------------------------------------------------*) (*Intuition behind this proof for the case of binary union: Goal: find an (R u S)-min element of a nonempty subset A. by case distinction: 1. There is a step a -R-> b with a,b : A. Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot have an S-successor and is thus S-min in A as well. 2. There is no such step. Pick an S-min element of A. In this case it must be an R-min element of A as well. *) Goal "[| !i:I. wf(r i); \ \ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \ \ Domain(r j) Int Range(r i) = {} \ \ |] ==> wf(UN i:I. r i)"; by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); by (Clarify_tac 1); by (rename_tac "A a" 1); by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1); by (Clarify_tac 1); by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]); by (EVERY1[etac allE,etac impE]); by (Blast_tac 1); by (Clarify_tac 1); by (rename_tac "z'" 1); by (res_inst_tac [("x","z'")] bexI 1); by (assume_tac 2); by (Clarify_tac 1); by (rename_tac "j" 1); by (case_tac "r j = r i" 1); by (EVERY1[etac allE,etac impE,atac]); by (Asm_full_simp_tac 1); by (Blast_tac 1); by (blast_tac (claset() addEs [equalityE]) 1); by (Asm_full_simp_tac 1); by (case_tac "? i. i:I" 1); by (Clarify_tac 1); by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]); by (Blast_tac 1); by (Blast_tac 1); qed "wf_UN"; Goalw [Union_def] "[| !r:R. wf r; \ \ !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \ \ Domain s Int Range r = {} \ \ |] ==> wf(Union R)"; by (rtac wf_UN 1); by (Blast_tac 1); by (Blast_tac 1); qed "wf_Union"; Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \ \ |] ==> wf(r Un s)"; by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1); by (Blast_tac 1); by (Blast_tac 1); qed "wf_Un"; (*--------------------------------------------------------------------------- * Wellfoundedness of `image' *---------------------------------------------------------------------------*) Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)"; by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); by (Clarify_tac 1); by (case_tac "? p. f p : Q" 1); by (eres_inst_tac [("x","{p. f p : Q}")]allE 1); by (fast_tac (claset() addDs [injD]) 1); by (Blast_tac 1); qed "wf_prod_fun_image"; (*** acyclic ***) val acyclicI = prove_goalw WF.thy [acyclic_def] "!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]); Goalw [acyclic_def] "wf r ==> acyclic r"; by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); qed "wf_acyclic"; Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; by (simp_tac (simpset() addsimps [trancl_insert]) 1); by (blast_tac (claset() addEs [make_elim rtrancl_trans]) 1); qed "acyclic_insert"; AddIffs [acyclic_insert]; Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; by (simp_tac (simpset() addsimps [trancl_converse]) 1); qed "acyclic_converse"; (** cut **) (*This rewrite rule works upon formulae; thus it requires explicit use of H_cong to expose the equality*) Goalw [cut_def] "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1); qed "cuts_eq"; Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)"; by (asm_simp_tac HOL_ss 1); qed "cut_apply"; (*** is_recfun ***) Goalw [is_recfun_def,cut_def] "[| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary"; by (etac ssubst 1); by (asm_simp_tac HOL_ss 1); qed "is_recfun_undef"; (*** NOTE! some simplifications need a different finish_tac!! ***) fun indhyp_tac hyps = (cut_facts_tac hyps THEN' DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' eresolve_tac [transD, mp, allE])); val wf_super_ss = HOL_ss addSolver indhyp_tac; Goalw [is_recfun_def,cut_def] "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ \ (x,a):r --> (x,b):r --> f(x)=g(x)"; by (etac wf_induct 1); by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); qed_spec_mp "is_recfun_equal"; val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] "[| wf(r); trans(r); \ \ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \ \ cut f r b = g"; val gundef = recgb RS is_recfun_undef and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); by (cut_facts_tac prems 1); by (rtac ext 1); by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1); qed "is_recfun_cut"; (*** Main Existence Lemma -- Basic Properties of the_recfun ***) Goalw [the_recfun_def] "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1); qed "is_the_recfun"; Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; by (wf_ind_tac "a" [] 1); by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] is_the_recfun 1); by (rewtac is_recfun_def); by (stac cuts_eq 1); by (Clarify_tac 1); by (rtac (refl RSN (2,H_cong)) 1); by (subgoal_tac "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); by (etac allE 2); by (dtac impE 2); by (atac 2); by (atac 3); by (atac 2); by (etac ssubst 1); by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); by (Clarify_tac 1); by (stac cut_apply 1); by (fast_tac (claset() addDs [transD]) 1); by (rtac (refl RSN (2,H_cong)) 1); by (fold_tac [is_recfun_def]); by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1); qed "unfold_the_recfun"; val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun; (*--------------Old proof----------------------------------------------------- val prems = Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; by (cut_facts_tac prems 1); by (wf_ind_tac "a" prems 1); by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); by (rewrite_goals_tac [is_recfun_def, wftrec_def]); by (stac cuts_eq 1); (*Applying the substitution: must keep the quantified assumption!!*) by (EVERY1 [Clarify_tac, rtac H_cong1, rtac allE, atac, etac (mp RS ssubst), atac]); by (fold_tac [is_recfun_def]); by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); qed "unfold_the_recfun"; ---------------------------------------------------------------------------*) (** Removal of the premise trans(r) **) val th = rewrite_rule[is_recfun_def] (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); Goalw [wfrec_def] "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; by (rtac H_cong 1); by (rtac refl 2); by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); by (rtac allI 1); by (rtac impI 1); by (simp_tac(HOL_ss addsimps [wfrec_def]) 1); by (res_inst_tac [("a1","a")] (th RS ssubst) 1); by (atac 1); by (forward_tac[wf_trancl] 1); by (forward_tac[r_into_trancl] 1); by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); by (rtac H_cong 1); (*expose the equality of cuts*) by (rtac refl 2); by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); by (Clarify_tac 1); by (res_inst_tac [("r","r^+")] is_recfun_equal 1); by (atac 1); by (rtac trans_trancl 1); by (rtac unfold_the_recfun 1); by (atac 1); by (rtac trans_trancl 1); by (rtac unfold_the_recfun 1); by (atac 1); by (rtac trans_trancl 1); by (rtac transD 1); by (rtac trans_trancl 1); by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); by (atac 1); by (atac 1); by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); by (atac 1); qed "wfrec"; (*--------------Old proof----------------------------------------------------- Goalw [wfrec_def] "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; by (etac (wf_trancl RS wftrec RS ssubst) 1); by (rtac trans_trancl 1); by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); qed "wfrec"; ---------------------------------------------------------------------------*) (*--------------------------------------------------------------------------- * This form avoids giant explosions in proofs. NOTE USE OF == *---------------------------------------------------------------------------*) val rew::prems = goal thy "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"; by (rewtac rew); by (REPEAT (resolve_tac (prems@[wfrec]) 1)); qed "def_wfrec"; (**** TFL variants ****) Goal "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))"; by (Clarify_tac 1); by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); by (assume_tac 1); by (Blast_tac 1); qed"tfl_wf_induct"; Goal "!f R. (x,a):R --> (cut f R a)(x) = f(x)"; by (Clarify_tac 1); by (rtac cut_apply 1); by (assume_tac 1); qed"tfl_cut_apply"; Goal "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; by (Clarify_tac 1); by (etac wfrec 1); qed "tfl_wfrec";