summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Induct/Acc.ML

changeset 5223 | 4cb05273f764 |

parent 5168 | adafef6eb295 |

child 5580 | 354f4914811f |

--- a/src/HOL/Induct/Acc.ML Thu Jul 30 23:14:41 1998 +0200 +++ b/src/HOL/Induct/Acc.ML Fri Jul 31 10:48:42 1998 +0200 @@ -9,8 +9,6 @@ Research Report 92-49, LIP, ENS Lyon. Dec 1992. *) -open Acc; - (*The intended introduction rule*) val prems = goal Acc.thy "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)"; @@ -46,25 +44,25 @@ qed "acc_induct"; -val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)"; -by (rtac (major RS wfI) 1); +Goal "r <= (acc r) Times (acc r) ==> wf(r)"; +by (etac wfI 1); by (etac acc.induct 1); by (rewtac pred_def); by (Fast_tac 1); qed "acc_wfI"; -val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)"; -by (rtac (major RS wf_induct) 1); +Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)"; +by (etac wf_induct 1); by (rtac (impI RS allI) 1); by (rtac accI 1); by (Fast_tac 1); qed "acc_wfD_lemma"; -val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)"; +Goal "wf(r) ==> r <= (acc r) Times (acc r)"; by (rtac subsetI 1); by (res_inst_tac [("p", "x")] PairE 1); by (fast_tac (claset() addSIs [SigmaI, - major RS acc_wfD_lemma RS spec RS mp]) 1); + acc_wfD_lemma RS spec RS mp]) 1); qed "acc_wfD"; Goal "wf(r) = (r <= (acc r) Times (acc r))";