ex/Acc.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Acc.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -0,0 +1,63 @@
+(*  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 (set_cs addIs (prems @ 
+			    map (rewrite_rule [pred_def]) acc.intrs)) 1);
+val accI = result();
+
+goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
+by (etac acc.elim 1);
+by (rewtac pred_def);
+by (fast_tac set_cs 1);
+val acc_downward = result();
+
+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 set_cs 2);
+be (Int_lower1 RS Pow_mono RS subsetD) 1;
+val acc_induct = result();
+
+
+val [major] = goal Acc.thy "r <= Sigma(acc(r), %u. acc(r)) ==> wf(r)";
+by (rtac (major RS wfI) 1);
+by (etac acc.induct 1);
+by (rewtac pred_def);
+by (fast_tac set_cs 1);
+val acc_wfI = result();
+
+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);
+br (impI RS allI) 1;
+br accI 1;
+by (fast_tac set_cs 1);
+val acc_wfD_lemma = result();
+
+val [major] = goal Acc.thy "wf(r) ==> r <= Sigma(acc(r), %u. acc(r))";
+by (rtac subsetI 1);
+by (res_inst_tac [("p", "x")] PairE 1);
+by (fast_tac (set_cs addSIs [SigmaI,
+			     major RS acc_wfD_lemma RS spec RS mp]) 1);
+val acc_wfD = result();
+
+goal Acc.thy "wf(r)  =  (r <= Sigma(acc(r), %u. acc(r)))";
+by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
+val wf_acc_iff = result();