src/HOL/WF.ML
 author paulson Thu Sep 10 17:23:51 1998 +0200 (1998-09-10) changeset 5452 b38332431a8c parent 5337 2f7d09a927c4 child 5521 7970832271cc permissions -rw-r--r--
New theorem wf_not_sym and well-formed wf_asym
 clasohm@1475 ` 1` ```(* Title: HOL/wf.ML ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1475 ` 3` ``` Author: Tobias Nipkow, with minor changes by Konrad Slind ``` clasohm@1475 ` 4` ``` Copyright 1992 University of Cambridge/1995 TU Munich ``` clasohm@923 ` 5` paulson@3198 ` 6` ```Wellfoundedness, induction, and recursion ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` clasohm@923 ` 9` ```open WF; ``` clasohm@923 ` 10` nipkow@950 ` 11` ```val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); ``` clasohm@923 ` 12` ```val H_cong1 = refl RS H_cong; ``` clasohm@923 ` 13` clasohm@923 ` 14` ```(*Restriction to domain A. If r is well-founded over A then wf(r)*) ``` paulson@5316 ` 15` ```val [prem1,prem2] = Goalw [wf_def] ``` paulson@1642 ` 16` ``` "[| r <= A Times A; \ ``` clasohm@972 ` 17` ```\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ ``` clasohm@923 ` 18` ```\ ==> wf(r)"; ``` paulson@3708 ` 19` ```by (Clarify_tac 1); ``` clasohm@923 ` 20` ```by (rtac allE 1); ``` clasohm@923 ` 21` ```by (assume_tac 1); ``` wenzelm@4089 ` 22` ```by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); ``` clasohm@923 ` 23` ```qed "wfI"; ``` clasohm@923 ` 24` paulson@5316 ` 25` ```val major::prems = Goalw [wf_def] ``` clasohm@923 ` 26` ``` "[| wf(r); \ ``` clasohm@972 ` 27` ```\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ ``` clasohm@923 ` 28` ```\ |] ==> P(a)"; ``` clasohm@923 ` 29` ```by (rtac (major RS spec RS mp RS spec) 1); ``` wenzelm@4089 ` 30` ```by (blast_tac (claset() addIs prems) 1); ``` clasohm@923 ` 31` ```qed "wf_induct"; ``` clasohm@923 ` 32` clasohm@923 ` 33` ```(*Perform induction on i, then prove the wf(r) subgoal using prems. *) ``` clasohm@923 ` 34` ```fun wf_ind_tac a prems i = ``` clasohm@923 ` 35` ``` EVERY [res_inst_tac [("a",a)] wf_induct i, ``` clasohm@1465 ` 36` ``` rename_last_tac a ["1"] (i+1), ``` clasohm@1465 ` 37` ``` ares_tac prems i]; ``` clasohm@923 ` 38` paulson@5452 ` 39` ```Goal "wf(r) ==> ! x. (a,x):r --> (x,a)~:r"; ``` paulson@5316 ` 40` ```by (wf_ind_tac "a" [] 1); ``` paulson@2935 ` 41` ```by (Blast_tac 1); ``` paulson@5452 ` 42` ```qed_spec_mp "wf_not_sym"; ``` paulson@5452 ` 43` paulson@5452 ` 44` ```(* [| wf(r); (a,x):r; ~P ==> (x,a):r |] ==> P *) ``` paulson@5452 ` 45` ```bind_thm ("wf_asym", wf_not_sym RS swap); ``` clasohm@923 ` 46` paulson@5316 ` 47` ```Goal "[| wf(r); (a,a): r |] ==> P"; ``` paulson@5316 ` 48` ```by (blast_tac (claset() addEs [wf_asym]) 1); ``` paulson@1618 ` 49` ```qed "wf_irrefl"; ``` clasohm@923 ` 50` clasohm@1475 ` 51` ```(*transitive closure of a wf relation is wf! *) ``` paulson@5316 ` 52` ```Goal "wf(r) ==> wf(r^+)"; ``` paulson@5316 ` 53` ```by (stac wf_def 1); ``` paulson@3708 ` 54` ```by (Clarify_tac 1); ``` clasohm@923 ` 55` ```(*must retain the universal formula for later use!*) ``` clasohm@923 ` 56` ```by (rtac allE 1 THEN assume_tac 1); ``` clasohm@923 ` 57` ```by (etac mp 1); ``` paulson@5316 ` 58` ```by (eres_inst_tac [("a","x")] wf_induct 1); ``` clasohm@923 ` 59` ```by (rtac (impI RS allI) 1); ``` clasohm@923 ` 60` ```by (etac tranclE 1); ``` paulson@2935 ` 61` ```by (Blast_tac 1); ``` paulson@2935 ` 62` ```by (Blast_tac 1); ``` clasohm@923 ` 63` ```qed "wf_trancl"; ``` clasohm@923 ` 64` clasohm@923 ` 65` oheimb@4762 ` 66` ```val wf_converse_trancl = prove_goal thy ``` oheimb@4762 ` 67` ```"!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [ ``` oheimb@4762 ` 68` ``` stac (trancl_converse RS sym) 1, ``` oheimb@4762 ` 69` ``` etac wf_trancl 1]); ``` oheimb@4762 ` 70` paulson@3198 ` 71` ```(*---------------------------------------------------------------------------- ``` paulson@3198 ` 72` ``` * Minimal-element characterization of well-foundedness ``` paulson@3198 ` 73` ``` *---------------------------------------------------------------------------*) ``` paulson@3198 ` 74` paulson@5316 ` 75` ```Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)"; ``` paulson@5318 ` 76` ```by (dtac spec 1); ``` paulson@5316 ` 77` ```by (etac (mp RS spec) 1); ``` paulson@3198 ` 78` ```by (Blast_tac 1); ``` paulson@3198 ` 79` ```val lemma1 = result(); ``` paulson@3198 ` 80` paulson@5316 ` 81` ```Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r"; ``` paulson@3708 ` 82` ```by (Clarify_tac 1); ``` paulson@3198 ` 83` ```by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1); ``` paulson@3198 ` 84` ```by (Blast_tac 1); ``` paulson@3198 ` 85` ```val lemma2 = result(); ``` paulson@3198 ` 86` wenzelm@5069 ` 87` ```Goal "wf r = (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q))"; ``` wenzelm@4089 ` 88` ```by (blast_tac (claset() addSIs [lemma1, lemma2]) 1); ``` paulson@3198 ` 89` ```qed "wf_eq_minimal"; ``` paulson@3198 ` 90` nipkow@3413 ` 91` ```(*--------------------------------------------------------------------------- ``` nipkow@3413 ` 92` ``` * Wellfoundedness of subsets ``` nipkow@3413 ` 93` ``` *---------------------------------------------------------------------------*) ``` nipkow@3413 ` 94` paulson@5143 ` 95` ```Goal "[| wf(r); p<=r |] ==> wf(p)"; ``` wenzelm@4089 ` 96` ```by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); ``` nipkow@3413 ` 97` ```by (Fast_tac 1); ``` nipkow@3413 ` 98` ```qed "wf_subset"; ``` nipkow@3413 ` 99` nipkow@3413 ` 100` ```(*--------------------------------------------------------------------------- ``` nipkow@3413 ` 101` ``` * Wellfoundedness of the empty relation. ``` nipkow@3413 ` 102` ``` *---------------------------------------------------------------------------*) ``` nipkow@3413 ` 103` wenzelm@5069 ` 104` ```Goal "wf({})"; ``` wenzelm@4089 ` 105` ```by (simp_tac (simpset() addsimps [wf_def]) 1); ``` nipkow@3413 ` 106` ```qed "wf_empty"; ``` nipkow@5281 ` 107` ```AddIffs [wf_empty]; ``` nipkow@3413 ` 108` nipkow@3413 ` 109` ```(*--------------------------------------------------------------------------- ``` nipkow@3413 ` 110` ``` * Wellfoundedness of `insert' ``` nipkow@3413 ` 111` ``` *---------------------------------------------------------------------------*) ``` nipkow@3413 ` 112` wenzelm@5069 ` 113` ```Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; ``` paulson@3457 ` 114` ```by (rtac iffI 1); ``` paulson@4350 ` 115` ``` by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] ``` paulson@4350 ` 116` ``` addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); ``` wenzelm@4089 ` 117` ```by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); ``` paulson@4153 ` 118` ```by Safe_tac; ``` paulson@3457 ` 119` ```by (EVERY1[rtac allE, atac, etac impE, Blast_tac]); ``` paulson@3457 ` 120` ```by (etac bexE 1); ``` paulson@3457 ` 121` ```by (rename_tac "a" 1); ``` paulson@3457 ` 122` ```by (case_tac "a = x" 1); ``` paulson@3457 ` 123` ``` by (res_inst_tac [("x","a")]bexI 2); ``` paulson@3457 ` 124` ``` by (assume_tac 3); ``` paulson@3457 ` 125` ``` by (Blast_tac 2); ``` paulson@3457 ` 126` ```by (case_tac "y:Q" 1); ``` paulson@3457 ` 127` ``` by (Blast_tac 2); ``` paulson@4059 ` 128` ```by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1); ``` paulson@3457 ` 129` ``` by (assume_tac 1); ``` paulson@4059 ` 130` ```by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1); (*essential for speed*) ``` paulson@4350 ` 131` ```(*Blast_tac with new substOccur fails*) ``` paulson@4350 ` 132` ```by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); ``` nipkow@3413 ` 133` ```qed "wf_insert"; ``` nipkow@3413 ` 134` ```AddIffs [wf_insert]; ``` nipkow@3413 ` 135` nipkow@5281 ` 136` ```(*--------------------------------------------------------------------------- ``` nipkow@5281 ` 137` ``` * Wellfoundedness of `disjoint union' ``` nipkow@5281 ` 138` ``` *---------------------------------------------------------------------------*) ``` nipkow@5281 ` 139` paulson@5330 ` 140` ```(*Intuition behind this proof for the case of binary union: ``` paulson@5330 ` 141` paulson@5330 ` 142` ``` Goal: find an (R u S)-min element of a nonempty subset A. ``` paulson@5330 ` 143` ``` by case distinction: ``` paulson@5330 ` 144` ``` 1. There is a step a -R-> b with a,b : A. ``` paulson@5330 ` 145` ``` Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. ``` paulson@5330 ` 146` ``` By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the ``` paulson@5330 ` 147` ``` subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot ``` paulson@5330 ` 148` ``` have an S-successor and is thus S-min in A as well. ``` paulson@5330 ` 149` ``` 2. There is no such step. ``` paulson@5330 ` 150` ``` Pick an S-min element of A. In this case it must be an R-min ``` paulson@5330 ` 151` ``` element of A as well. ``` paulson@5330 ` 152` paulson@5330 ` 153` ```*) ``` paulson@5330 ` 154` paulson@5316 ` 155` ```Goal "[| !i:I. wf(r i); \ ``` paulson@5316 ` 156` ```\ !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \ ``` paulson@5316 ` 157` ```\ Domain(r j) Int Range(r i) = {} \ ``` paulson@5316 ` 158` ```\ |] ==> wf(UN i:I. r i)"; ``` paulson@5318 ` 159` ```by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); ``` paulson@5318 ` 160` ```by (Clarify_tac 1); ``` paulson@5318 ` 161` ```by (rename_tac "A a" 1); ``` paulson@5318 ` 162` ```by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1); ``` paulson@5318 ` 163` ``` by (Clarify_tac 1); ``` paulson@5318 ` 164` ``` by (EVERY1[dtac bspec, atac, ``` nipkow@5281 ` 165` ``` eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]); ``` paulson@5318 ` 166` ``` by (EVERY1[etac allE,etac impE]); ``` paulson@5318 ` 167` ``` by (Blast_tac 1); ``` paulson@5318 ` 168` ``` by (Clarify_tac 1); ``` paulson@5318 ` 169` ``` by (rename_tac "z'" 1); ``` paulson@5318 ` 170` ``` by (res_inst_tac [("x","z'")] bexI 1); ``` paulson@5318 ` 171` ``` by (assume_tac 2); ``` paulson@5318 ` 172` ``` by (Clarify_tac 1); ``` paulson@5318 ` 173` ``` by (rename_tac "j" 1); ``` paulson@5318 ` 174` ``` by (case_tac "r j = r i" 1); ``` paulson@5318 ` 175` ``` by (EVERY1[etac allE,etac impE,atac]); ``` paulson@5318 ` 176` ``` by (Asm_full_simp_tac 1); ``` paulson@5318 ` 177` ``` by (Blast_tac 1); ``` paulson@5318 ` 178` ``` by (blast_tac (claset() addEs [equalityE]) 1); ``` paulson@5318 ` 179` ```by (Asm_full_simp_tac 1); ``` paulson@5337 ` 180` ```by (Fast_tac 1); (*faster than Blast_tac*) ``` nipkow@5281 ` 181` ```qed "wf_UN"; ``` nipkow@5281 ` 182` nipkow@5281 ` 183` ```Goalw [Union_def] ``` nipkow@5281 ` 184` ``` "[| !r:R. wf r; \ ``` nipkow@5281 ` 185` ```\ !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \ ``` nipkow@5281 ` 186` ```\ Domain s Int Range r = {} \ ``` nipkow@5281 ` 187` ```\ |] ==> wf(Union R)"; ``` paulson@5318 ` 188` ```by (rtac wf_UN 1); ``` paulson@5318 ` 189` ```by (Blast_tac 1); ``` paulson@5318 ` 190` ```by (Blast_tac 1); ``` nipkow@5281 ` 191` ```qed "wf_Union"; ``` nipkow@5281 ` 192` paulson@5316 ` 193` ```Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \ ``` paulson@5316 ` 194` ```\ |] ==> wf(r Un s)"; ``` paulson@5318 ` 195` ```by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1); ``` paulson@5318 ` 196` ```by (Blast_tac 1); ``` paulson@5318 ` 197` ```by (Blast_tac 1); ``` nipkow@5281 ` 198` ```qed "wf_Un"; ``` nipkow@5281 ` 199` nipkow@5281 ` 200` ```(*--------------------------------------------------------------------------- ``` nipkow@5281 ` 201` ``` * Wellfoundedness of `image' ``` nipkow@5281 ` 202` ``` *---------------------------------------------------------------------------*) ``` nipkow@5281 ` 203` nipkow@5281 ` 204` ```Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)"; ``` paulson@5318 ` 205` ```by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); ``` paulson@5318 ` 206` ```by (Clarify_tac 1); ``` paulson@5318 ` 207` ```by (case_tac "? p. f p : Q" 1); ``` paulson@5318 ` 208` ```by (eres_inst_tac [("x","{p. f p : Q}")]allE 1); ``` paulson@5318 ` 209` ```by (fast_tac (claset() addDs [injD]) 1); ``` paulson@5318 ` 210` ```by (Blast_tac 1); ``` nipkow@5281 ` 211` ```qed "wf_prod_fun_image"; ``` nipkow@5281 ` 212` nipkow@3413 ` 213` ```(*** acyclic ***) ``` nipkow@3413 ` 214` oheimb@4750 ` 215` ```val acyclicI = prove_goalw WF.thy [acyclic_def] ``` oheimb@4750 ` 216` ```"!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]); ``` oheimb@4750 ` 217` wenzelm@5069 ` 218` ```Goalw [acyclic_def] ``` paulson@5148 ` 219` ``` "wf r ==> acyclic r"; ``` wenzelm@4089 ` 220` ```by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); ``` nipkow@3413 ` 221` ```qed "wf_acyclic"; ``` nipkow@3413 ` 222` paulson@5452 ` 223` ```Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; ``` wenzelm@4089 ` 224` ```by (simp_tac (simpset() addsimps [trancl_insert]) 1); ``` paulson@5452 ` 225` ```by (blast_tac (claset() addIs [rtrancl_trans]) 1); ``` nipkow@3413 ` 226` ```qed "acyclic_insert"; ``` nipkow@3413 ` 227` ```AddIffs [acyclic_insert]; ``` nipkow@3413 ` 228` wenzelm@5069 ` 229` ```Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; ``` paulson@4746 ` 230` ```by (simp_tac (simpset() addsimps [trancl_converse]) 1); ``` paulson@4746 ` 231` ```qed "acyclic_converse"; ``` paulson@3198 ` 232` clasohm@923 ` 233` ```(** cut **) ``` clasohm@923 ` 234` clasohm@923 ` 235` ```(*This rewrite rule works upon formulae; thus it requires explicit use of ``` clasohm@923 ` 236` ``` H_cong to expose the equality*) ``` wenzelm@5069 ` 237` ```Goalw [cut_def] ``` clasohm@972 ` 238` ``` "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; ``` nipkow@4686 ` 239` ```by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1); ``` clasohm@1475 ` 240` ```qed "cuts_eq"; ``` clasohm@923 ` 241` paulson@5143 ` 242` ```Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)"; ``` paulson@1552 ` 243` ```by (asm_simp_tac HOL_ss 1); ``` clasohm@923 ` 244` ```qed "cut_apply"; ``` clasohm@923 ` 245` clasohm@923 ` 246` ```(*** is_recfun ***) ``` clasohm@923 ` 247` wenzelm@5069 ` 248` ```Goalw [is_recfun_def,cut_def] ``` paulson@5148 ` 249` ``` "[| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary"; ``` clasohm@923 ` 250` ```by (etac ssubst 1); ``` paulson@1552 ` 251` ```by (asm_simp_tac HOL_ss 1); ``` clasohm@923 ` 252` ```qed "is_recfun_undef"; ``` clasohm@923 ` 253` clasohm@923 ` 254` ```(*** NOTE! some simplifications need a different finish_tac!! ***) ``` clasohm@923 ` 255` ```fun indhyp_tac hyps = ``` clasohm@923 ` 256` ``` (cut_facts_tac hyps THEN' ``` clasohm@923 ` 257` ``` DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' ``` clasohm@1465 ` 258` ``` eresolve_tac [transD, mp, allE])); ``` oheimb@2637 ` 259` ```val wf_super_ss = HOL_ss addSolver indhyp_tac; ``` clasohm@923 ` 260` paulson@5316 ` 261` ```Goalw [is_recfun_def,cut_def] ``` clasohm@1475 ` 262` ``` "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ ``` clasohm@972 ` 263` ``` \ (x,a):r --> (x,b):r --> f(x)=g(x)"; ``` clasohm@923 ` 264` ```by (etac wf_induct 1); ``` clasohm@923 ` 265` ```by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); ``` clasohm@923 ` 266` ```by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); ``` nipkow@1485 ` 267` ```qed_spec_mp "is_recfun_equal"; ``` clasohm@923 ` 268` clasohm@923 ` 269` clasohm@923 ` 270` ```val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] ``` clasohm@923 ` 271` ``` "[| wf(r); trans(r); \ ``` clasohm@1475 ` 272` ```\ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \ ``` clasohm@923 ` 273` ```\ cut f r b = g"; ``` clasohm@923 ` 274` ```val gundef = recgb RS is_recfun_undef ``` clasohm@923 ` 275` ```and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); ``` clasohm@923 ` 276` ```by (cut_facts_tac prems 1); ``` clasohm@923 ` 277` ```by (rtac ext 1); ``` nipkow@4686 ` 278` ```by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1); ``` clasohm@923 ` 279` ```qed "is_recfun_cut"; ``` clasohm@923 ` 280` clasohm@923 ` 281` ```(*** Main Existence Lemma -- Basic Properties of the_recfun ***) ``` clasohm@923 ` 282` paulson@5316 ` 283` ```Goalw [the_recfun_def] ``` clasohm@1475 ` 284` ``` "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; ``` paulson@5316 ` 285` ```by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1); ``` clasohm@923 ` 286` ```qed "is_the_recfun"; ``` clasohm@923 ` 287` paulson@5316 ` 288` ```Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; ``` paulson@5316 ` 289` ```by (wf_ind_tac "a" [] 1); ``` nipkow@4821 ` 290` ```by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] ``` nipkow@4821 ` 291` ``` is_the_recfun 1); ``` nipkow@4821 ` 292` ```by (rewtac is_recfun_def); ``` nipkow@4821 ` 293` ```by (stac cuts_eq 1); ``` nipkow@4821 ` 294` ```by (Clarify_tac 1); ``` nipkow@4821 ` 295` ```by (rtac (refl RSN (2,H_cong)) 1); ``` nipkow@4821 ` 296` ```by (subgoal_tac ``` clasohm@1475 ` 297` ``` "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); ``` nipkow@4821 ` 298` ``` by (etac allE 2); ``` nipkow@4821 ` 299` ``` by (dtac impE 2); ``` nipkow@4821 ` 300` ``` by (atac 2); ``` clasohm@1475 ` 301` ``` by (atac 3); ``` nipkow@4821 ` 302` ``` by (atac 2); ``` nipkow@4821 ` 303` ```by (etac ssubst 1); ``` nipkow@4821 ` 304` ```by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); ``` nipkow@4821 ` 305` ```by (Clarify_tac 1); ``` nipkow@4821 ` 306` ```by (stac cut_apply 1); ``` wenzelm@5132 ` 307` ``` by (fast_tac (claset() addDs [transD]) 1); ``` nipkow@4821 ` 308` ```by (rtac (refl RSN (2,H_cong)) 1); ``` nipkow@4821 ` 309` ```by (fold_tac [is_recfun_def]); ``` nipkow@4821 ` 310` ```by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1); ``` clasohm@923 ` 311` ```qed "unfold_the_recfun"; ``` clasohm@923 ` 312` clasohm@1475 ` 313` ```val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun; ``` clasohm@923 ` 314` clasohm@1475 ` 315` ```(*--------------Old proof----------------------------------------------------- ``` paulson@5316 ` 316` ```val prems = Goal ``` clasohm@1475 ` 317` ``` "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; ``` clasohm@1475 ` 318` ```by (cut_facts_tac prems 1); ``` clasohm@1475 ` 319` ```by (wf_ind_tac "a" prems 1); ``` clasohm@1475 ` 320` ```by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); ``` clasohm@1475 ` 321` ```by (rewrite_goals_tac [is_recfun_def, wftrec_def]); ``` paulson@2031 ` 322` ```by (stac cuts_eq 1); ``` clasohm@1475 ` 323` ```(*Applying the substitution: must keep the quantified assumption!!*) ``` paulson@3708 ` 324` ```by (EVERY1 [Clarify_tac, rtac H_cong1, rtac allE, atac, ``` clasohm@1475 ` 325` ``` etac (mp RS ssubst), atac]); ``` clasohm@1475 ` 326` ```by (fold_tac [is_recfun_def]); ``` clasohm@1475 ` 327` ```by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); ``` clasohm@1475 ` 328` ```qed "unfold_the_recfun"; ``` clasohm@1475 ` 329` ```---------------------------------------------------------------------------*) ``` clasohm@923 ` 330` clasohm@923 ` 331` ```(** Removal of the premise trans(r) **) ``` clasohm@1475 ` 332` ```val th = rewrite_rule[is_recfun_def] ``` clasohm@1475 ` 333` ``` (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); ``` clasohm@923 ` 334` wenzelm@5069 ` 335` ```Goalw [wfrec_def] ``` paulson@5148 ` 336` ``` "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; ``` clasohm@1475 ` 337` ```by (rtac H_cong 1); ``` clasohm@1475 ` 338` ```by (rtac refl 2); ``` clasohm@1475 ` 339` ```by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); ``` clasohm@1475 ` 340` ```by (rtac allI 1); ``` clasohm@1475 ` 341` ```by (rtac impI 1); ``` clasohm@1475 ` 342` ```by (simp_tac(HOL_ss addsimps [wfrec_def]) 1); ``` clasohm@1475 ` 343` ```by (res_inst_tac [("a1","a")] (th RS ssubst) 1); ``` clasohm@1475 ` 344` ```by (atac 1); ``` clasohm@1475 ` 345` ```by (forward_tac[wf_trancl] 1); ``` clasohm@1475 ` 346` ```by (forward_tac[r_into_trancl] 1); ``` clasohm@1475 ` 347` ```by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); ``` clasohm@1475 ` 348` ```by (rtac H_cong 1); (*expose the equality of cuts*) ``` clasohm@1475 ` 349` ```by (rtac refl 2); ``` clasohm@1475 ` 350` ```by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); ``` paulson@3708 ` 351` ```by (Clarify_tac 1); ``` nipkow@1485 ` 352` ```by (res_inst_tac [("r","r^+")] is_recfun_equal 1); ``` clasohm@1475 ` 353` ```by (atac 1); ``` clasohm@1475 ` 354` ```by (rtac trans_trancl 1); ``` clasohm@1475 ` 355` ```by (rtac unfold_the_recfun 1); ``` clasohm@1475 ` 356` ```by (atac 1); ``` clasohm@1475 ` 357` ```by (rtac trans_trancl 1); ``` clasohm@1475 ` 358` ```by (rtac unfold_the_recfun 1); ``` clasohm@1475 ` 359` ```by (atac 1); ``` clasohm@1475 ` 360` ```by (rtac trans_trancl 1); ``` clasohm@1475 ` 361` ```by (rtac transD 1); ``` clasohm@1475 ` 362` ```by (rtac trans_trancl 1); ``` oheimb@4762 ` 363` ```by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); ``` clasohm@1475 ` 364` ```by (atac 1); ``` clasohm@1475 ` 365` ```by (atac 1); ``` oheimb@4762 ` 366` ```by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1); ``` clasohm@1475 ` 367` ```by (atac 1); ``` clasohm@1475 ` 368` ```qed "wfrec"; ``` clasohm@1475 ` 369` clasohm@1475 ` 370` ```(*--------------Old proof----------------------------------------------------- ``` wenzelm@5069 ` 371` ```Goalw [wfrec_def] ``` paulson@5148 ` 372` ``` "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; ``` clasohm@923 ` 373` ```by (etac (wf_trancl RS wftrec RS ssubst) 1); ``` clasohm@923 ` 374` ```by (rtac trans_trancl 1); ``` clasohm@923 ` 375` ```by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) ``` clasohm@1475 ` 376` ```by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); ``` clasohm@923 ` 377` ```qed "wfrec"; ``` clasohm@1475 ` 378` ```---------------------------------------------------------------------------*) ``` clasohm@923 ` 379` clasohm@1475 ` 380` ```(*--------------------------------------------------------------------------- ``` clasohm@1475 ` 381` ``` * This form avoids giant explosions in proofs. NOTE USE OF == ``` clasohm@1475 ` 382` ``` *---------------------------------------------------------------------------*) ``` paulson@5316 ` 383` ```val rew::prems = goal thy ``` clasohm@1475 ` 384` ``` "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"; ``` clasohm@923 ` 385` ```by (rewtac rew); ``` clasohm@923 ` 386` ```by (REPEAT (resolve_tac (prems@[wfrec]) 1)); ``` clasohm@923 ` 387` ```qed "def_wfrec"; ``` clasohm@1475 ` 388` paulson@3198 ` 389` paulson@3198 ` 390` ```(**** TFL variants ****) ``` paulson@3198 ` 391` paulson@5278 ` 392` ```Goal "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))"; ``` paulson@3708 ` 393` ```by (Clarify_tac 1); ``` paulson@3198 ` 394` ```by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); ``` paulson@3198 ` 395` ```by (assume_tac 1); ``` paulson@3198 ` 396` ```by (Blast_tac 1); ``` paulson@3198 ` 397` ```qed"tfl_wf_induct"; ``` paulson@3198 ` 398` wenzelm@5069 ` 399` ```Goal "!f R. (x,a):R --> (cut f R a)(x) = f(x)"; ``` paulson@3708 ` 400` ```by (Clarify_tac 1); ``` paulson@3198 ` 401` ```by (rtac cut_apply 1); ``` paulson@3198 ` 402` ```by (assume_tac 1); ``` paulson@3198 ` 403` ```qed"tfl_cut_apply"; ``` paulson@3198 ` 404` wenzelm@5069 ` 405` ```Goal "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; ``` paulson@3708 ` 406` ```by (Clarify_tac 1); ``` paulson@4153 ` 407` ```by (etac wfrec 1); ``` paulson@3198 ` 408` ```qed "tfl_wfrec"; ```