author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 35621  1c084dda4c3c 
child 58249  180f1b3508ed 
permissions  rwrr 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

1 
(* Title: HOL/Induct/Comb.thy 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

5 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

6 
header {* Combinatory Logic example: the ChurchRosser Theorem *} 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 

16417  8 
theory Comb imports Main begin 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

9 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

10 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

11 
Curiously, combinators do not include free variables. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

12 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

13 
Example taken from \cite{camillerimelham}. 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

15 
HOL system proofs may be found in the HOL distribution at 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

16 
.../contrib/ruleinduction/cl.ml 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

17 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

18 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

19 
subsection {* Definitions *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

20 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

21 
text {* Datatype definition of combinators @{text S} and @{text K}. *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

22 

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

23 
datatype comb = K 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
 S 
19736  25 
 Ap comb comb (infixl "##" 90) 
26 

21210  27 
notation (xsymbols) 
19736  28 
Ap (infixl "\<bullet>" 90) 
29 

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

30 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

31 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

32 
Inductive definition of contractions, @{text "1>"} and 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

33 
(multistep) reductions, @{text ">"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

34 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

35 

23746  36 
inductive_set 
37 
contract :: "(comb*comb) set" 

38 
and contract_rel1 :: "[comb,comb] => bool" (infixl "1>" 50) 

39 
where 

40 
"x 1> y == (x,y) \<in> contract" 

41 
 K: "K##x##y 1> x" 

42 
 S: "S##x##y##z 1> (x##z)##(y##z)" 

43 
 Ap1: "x1>y ==> x##z 1> y##z" 

44 
 Ap2: "x1>y ==> z##x 1> z##y" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

45 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

46 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

47 
contract_rel :: "[comb,comb] => bool" (infixl ">" 50) where 
19736  48 
"x > y == (x,y) \<in> contract^*" 
15816  49 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

50 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

51 
Inductive definition of parallel contractions, @{text "=1=>"} and 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

52 
(multistep) parallel reductions, @{text "===>"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

54 

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

56 
parcontract :: "(comb*comb) set" 
23746  57 
and parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) 
58 
where 

59 
"x =1=> y == (x,y) \<in> parcontract" 

60 
 refl: "x =1=> x" 

61 
 K: "K##x##y =1=> x" 

62 
 S: "S##x##y##z =1=> (x##z)##(y##z)" 

63 
 Ap: "[ x=1=>y; z=1=>w ] ==> x##z =1=> y##w" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

64 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

65 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

66 
parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where 
19736  67 
"x ===> y == (x,y) \<in> parcontract^*" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

69 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

70 
Misc definitions. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

72 

19736  73 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

74 
I :: comb where 
19736  75 
"I = S##K##K" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

77 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

78 
diamond :: "('a * 'a)set => bool" where 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

79 
{*confluence; Lambda/Commutation treats this more abstractly*} 
19736  80 
"diamond(r) = (\<forall>x y. (x,y) \<in> r > 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

81 
(\<forall>y'. (x,y') \<in> r > 
19736  82 
(\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

83 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

84 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

85 
subsection {*Reflexive/Transitive closure preserves ChurchRosser property*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

86 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

87 
text{*So does the Transitive closure, with a similar proof*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

88 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

89 
text{*Strip lemma. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

90 
The induction hypothesis covers all but the last diamond of the strip.*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

91 
lemma diamond_strip_lemmaE [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

92 
"[ diamond(r); (x,y) \<in> r^* ] ==> 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

93 
\<forall>y'. (x,y') \<in> r > (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

94 
apply (unfold diamond_def) 
16563  95 
apply (erule rtrancl_induct) 
96 
apply (meson rtrancl_refl) 

97 
apply (meson rtrancl_trans r_into_rtrancl) 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

98 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

99 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

100 
lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

101 
apply (simp (no_asm_simp) add: diamond_def) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

102 
apply (rule impI [THEN allI, THEN allI]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

103 
apply (erule rtrancl_induct, blast) 
16588  104 
apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

105 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

106 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

107 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

108 
subsection {* Noncontraction results *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

109 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

110 
text {* Derive a case for each combinator constructor. *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

111 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

112 
inductive_cases 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

113 
K_contractE [elim!]: "K 1> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

114 
and S_contractE [elim!]: "S 1> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

115 
and Ap_contractE [elim!]: "p##q 1> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

116 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

117 
declare contract.K [intro!] contract.S [intro!] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

118 
declare contract.Ap1 [intro] contract.Ap2 [intro] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

119 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

120 
lemma I_contract_E [elim!]: "I 1> z ==> P" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

121 
by (unfold I_def, blast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

122 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

123 
lemma K1_contractD [elim!]: "K##x 1> z ==> (\<exists>x'. z = K##x' & x 1> x')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

124 
by blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

125 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

126 
lemma Ap_reduce1 [intro]: "x > y ==> x##z > y##z" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

127 
apply (erule rtrancl_induct) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

128 
apply (blast intro: rtrancl_trans)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

129 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

130 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

131 
lemma Ap_reduce2 [intro]: "x > y ==> z##x > z##y" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

132 
apply (erule rtrancl_induct) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

133 
apply (blast intro: rtrancl_trans)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

134 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

135 

35621  136 
text {*Counterexample to the diamond property for @{term "x 1> y"}*} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

137 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

138 
lemma not_diamond_contract: "~ diamond(contract)" 
35621  139 
by (unfold diamond_def, metis S_contractE contract.K) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

140 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

141 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

142 
subsection {* Results about Parallel Contraction *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

143 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

144 
text {* Derive a case for each combinator constructor. *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

145 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

146 
inductive_cases 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

147 
K_parcontractE [elim!]: "K =1=> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

148 
and S_parcontractE [elim!]: "S =1=> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

149 
and Ap_parcontractE [elim!]: "p##q =1=> r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

150 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

151 
declare parcontract.intros [intro] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

152 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

153 
(*** Basic properties of parallel contraction ***) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

154 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

155 
subsection {* Basic properties of parallel contraction *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

156 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

157 
lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

158 
by blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

159 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

160 
lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

161 
by blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

162 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

163 
lemma S2_parcontractD [dest!]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

164 
"S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

165 
by blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

166 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

167 
text{*The rules above are not essential but make proofs much faster*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

168 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

169 
text{*ChurchRosser property for parallel contraction*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

170 
lemma diamond_parcontract: "diamond parcontract" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

171 
apply (unfold diamond_def) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

172 
apply (rule impI [THEN allI, THEN allI]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

173 
apply (erule parcontract.induct, fast+) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

174 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

175 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

176 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

177 
\medskip Equivalence of @{prop "p > q"} and @{prop "p ===> q"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

178 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

179 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

180 
lemma contract_subset_parcontract: "contract <= parcontract" 
35621  181 
by (auto, erule contract.induct, blast+) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

182 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

183 
text{*Reductions: simply throw together reflexivity, transitivity and 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

184 
the onestep reductions*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

185 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

186 
declare r_into_rtrancl [intro] rtrancl_trans [intro] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

187 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

188 
(*Example only: not used*) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

189 
lemma reduce_I: "I##x > x" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

190 
by (unfold I_def, blast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

191 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

192 
lemma parcontract_subset_reduce: "parcontract <= contract^*" 
35621  193 
by (auto, erule parcontract.induct, blast+) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

194 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

195 
lemma reduce_eq_parreduce: "contract^* = parcontract^*" 
35621  196 
by (metis contract_subset_parcontract parcontract_subset_reduce rtrancl_subset) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

197 

35621  198 
theorem diamond_reduce: "diamond(contract^*)" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

199 
by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

200 

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

201 
end 