author  wenzelm 
Mon, 03 Nov 1997 12:13:18 +0100  
changeset 4089  96fba19bcbe2 
parent 3120  c58423c20740 
child 5069  3ea049f7979d 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/Acc 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
Inductive definition of acc(r) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 
See Ch. PaulinMohring, Inductive Definitions in the System Coq. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
Research Report 9249, LIP, ENS Lyon. Dec 1992. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
open Acc; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
(*The intended introduction rule*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
val prems = goal Acc.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
"[ !!b. (b,a):r ==> b: acc(r) ] ==> a: acc(r)"; 
4089  17 
by (fast_tac (claset() addIs (prems @ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
map (rewrite_rule [pred_def]) acc.intrs)) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
qed "accI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
goal Acc.thy "!!a b r. [ b: acc(r); (a,b): r ] ==> a: acc(r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
by (etac acc.elim 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
by (rewtac pred_def); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
qed "acc_downward"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
val [major,indhyp] = goal Acc.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
"[ a : acc(r); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
\ !!x. [ x: acc(r); ALL y. (y,x):r > P(y) ] ==> P(x) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 
\ ] ==> P(a)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
by (rtac (major RS acc.induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
by (rtac indhyp 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
by (resolve_tac acc.intrs 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 
by (rewtac pred_def); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
by (Fast_tac 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
qed "acc_induct"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 
val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
by (rtac (major RS wfI) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
by (etac acc.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
by (rewtac pred_def); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
qed "acc_wfI"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r  (y,x):r > y: acc(r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
by (rtac (major RS wf_induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
by (rtac (impI RS allI) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
by (rtac accI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
qed "acc_wfD_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
by (rtac subsetI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
by (res_inst_tac [("p", "x")] PairE 1); 
4089  57 
by (fast_tac (claset() addSIs [SigmaI, 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 
major RS acc_wfD_lemma RS spec RS mp]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 
qed "acc_wfD"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 
goal Acc.thy "wf(r) = (r <= (acc r) Times (acc r))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

63 
qed "wf_acc_iff"; 