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

src/HOL/Induct/Acc.ML

author | berghofe |

Fri, 24 Jul 1998 13:39:47 +0200 | |

changeset 5191 | 8ceaa19f7717 |

parent 5168 | adafef6eb295 |

child 5223 | 4cb05273f764 |

permissions | -rw-r--r-- |

Renamed '$' to 'Scons' because of clashes with constants of the same
name in theories using datatypes.

(* Title: HOL/ex/Acc ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Inductive definition of acc(r) See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. 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)"; by (fast_tac (claset() addIs (prems @ map (rewrite_rule [pred_def]) acc.intrs)) 1); qed "accI"; Goal "[| b: acc(r); (a,b): r |] ==> a: acc(r)"; by (etac acc.elim 1); by (rewtac pred_def); by (Fast_tac 1); qed "acc_downward"; Goal "(b,a) : r^* ==> a : acc r --> b : acc r"; by (etac rtrancl_induct 1); by (Blast_tac 1); by (blast_tac (claset() addDs [acc_downward]) 1); val lemma = result(); Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; by (blast_tac (claset() addDs [lemma]) 1); qed "acc_downwards"; val [major,indhyp] = goal Acc.thy "[| a : acc(r); \ \ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ \ |] ==> P(a)"; by (rtac (major RS acc.induct) 1); by (rtac indhyp 1); by (resolve_tac acc.intrs 1); by (rewtac pred_def); by (Fast_tac 2); by (etac (Int_lower1 RS Pow_mono RS subsetD) 1); qed "acc_induct"; val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)"; by (rtac (major RS 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); 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)"; 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); qed "acc_wfD"; Goal "wf(r) = (r <= (acc r) Times (acc r))"; by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); qed "wf_acc_iff";