author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5148  74919e8f221c 
child 5223  4cb05273f764 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/comb.ML 
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 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1996 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 
Combinatory Logic example: the ChurchRosser Theorem 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
Curiously, combinators do not include free variables. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 

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

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

10 
J. Camilleri and T. F. Melham. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 
Reasoning with Inductively Defined Relations in the HOL Theorem Prover. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
Report 265, University of Cambridge Computer Laboratory, 1992. 
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 
HOL system proofs may be found in 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
/usr/groups/theory/hvgaftp/contrib/ruleinduction/cl.ml 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

17 

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

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

19 

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

20 
(*** Reflexive/Transitive closure preserves the ChurchRosser property 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
So does the Transitive closure; use r_into_trancl instead of rtrancl_refl 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

23 

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

24 
val [_, spec_mp] = [spec] RL [mp]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

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

26 
(*Strip lemma. The induction hyp is all but the last diamond of the strip.*) 
5069  27 
Goalw [diamond_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

28 
"[ diamond(r); (x,y):r^* ] ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
\ ALL y'. (x,y'):r > (EX z. (y',z): r^* & (y,z): r)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

32 
by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] 
4301  33 
addSDs [spec_mp]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 
val diamond_strip_lemmaE = result() RS spec RS mp RS exE; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 

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

36 
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
by (rewtac diamond_def); (*unfold only in goal, not in premise!*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

41 
by (slow_best_tac (*Seems to be a brittle, undirected search*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
(set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
addEs [major RS diamond_strip_lemmaE]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

45 

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 
(*** Results about Contraction ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 

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

49 
(*Derive a case for each combinator constructor*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
val K_contractE = contract.mk_cases comb.simps "K 1> z"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
val S_contractE = contract.mk_cases comb.simps "S 1> z"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
val Ap_contractE = contract.mk_cases comb.simps "x#y 1> z"; 
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 
AddSIs [contract.K, contract.S]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
AddIs [contract.Ap1, contract.Ap2]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
AddSEs [K_contractE, S_contractE, Ap_contractE]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

58 
Goalw [I_def] "I 1> z ==> P"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

61 
AddSEs [I_contract_E]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

63 
Goal "K#x 1> z ==> (EX x'. z = K#x' & x 1> x')"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

66 
AddSEs [K1_contractD]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

68 
Goal "x > y ==> x#z > y#z"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 
by (etac rtrancl_induct 1); 
4089  70 
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

72 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

73 
Goal "x > y ==> z#x > z#y"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
by (etac rtrancl_induct 1); 
4089  75 
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

77 

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

78 
(** Counterexample to the diamond property for 1> **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 

5069  80 
Goal "K#I#(I#I) 1> I"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (rtac contract.K 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

83 

5069  84 
Goalw [I_def] "K#I#(I#I) 1> K#I#((K#I)#(K#I))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

87 

5069  88 
Goal "K#I#((K#I)#(K#I)) 1> I"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

91 

5069  92 
Goalw [diamond_def] "~ diamond(contract)"; 
4089  93 
by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

95 

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

96 

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

97 

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

98 
(*** Results about Parallel Contraction ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 

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

100 
(*Derive a case for each combinator constructor*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 
val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

103 
val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

104 

4301  105 
AddSIs [parcontract.refl, parcontract.K, parcontract.S]; 
106 
AddIs [parcontract.Ap]; 

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

107 
AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 

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

109 
(*** Basic properties of parallel contraction ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

110 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

111 
Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

114 
AddSDs [K1_parcontractD]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

116 
Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

119 
AddSDs [S1_parcontractD]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

120 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

121 
Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

124 
AddSDs [S2_parcontractD]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

125 

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

126 
(*The rules above are not essential but make proofs much faster*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

127 

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

128 

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

129 
(*ChurchRosser property for parallel contraction*) 
5069  130 
Goalw [diamond_def] "diamond parcontract"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

132 
by (etac parcontract.induct 1 THEN prune_params_tac); 
3724  133 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

134 
by (ALLGOALS Blast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

136 

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

137 

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

138 
(*** Equivalence of x>y and x===>y ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 

5069  140 
Goal "contract <= parcontract"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

144 
by (ALLGOALS Blast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

146 

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

147 
(*Reductions: simply throw together reflexivity, transitivity and 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

148 
the onestep reductions*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

149 

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

150 
AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

151 

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

152 
(*Example only: not used*) 
5069  153 
Goalw [I_def] "I#x > x"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

156 

5069  157 
Goal "parcontract <= contract^*"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

160 
by (etac parcontract.induct 1 THEN prune_params_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

161 
by (ALLGOALS Blast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

163 

5069  164 
Goal "contract^* = parcontract^*"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

166 
(resolve_tac [equalityI, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

167 
contract_subset_parcontract RS rtrancl_mono, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

168 
parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

170 

5069  171 
Goal "diamond(contract^*)"; 
4089  172 
by (simp_tac (simpset() addsimps [reduce_eq_parreduce, diamond_rtrancl, 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

173 
diamond_parcontract]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

175 

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

176 

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

177 
writeln"Reached end of file."; 