author  wenzelm 
Tue, 07 Nov 2006 11:47:57 +0100  
changeset 21210  c17fd2df4e9e 
parent 19736  d8d0f8f51d69 
child 21404  eb85850d3eb7 
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 
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 

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

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

8 

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

10 

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

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

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

13 

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

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

15 

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

16 
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

17 
.../contrib/ruleinduction/cl.ml 
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 

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

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

21 

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

22 
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

23 

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

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

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

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

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

31 

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

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

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

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

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

36 

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

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

38 
contract :: "(comb*comb) set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

19736  40 
abbreviation 
41 
contract_rel1 :: "[comb,comb] => bool" (infixl "1>" 50) 

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

43 
contract_rel :: "[comb,comb] => bool" (infixl ">" 50) 

44 
"x > y == (x,y) \<in> contract^*" 

15816  45 

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

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

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

48 
K: "K##x##y 1> x" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

49 
S: "S##x##y##z 1> (x##z)##(y##z)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

50 
Ap1: "x1>y ==> x##z 1> y##z" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

51 
Ap2: "x1>y ==> z##x 1> z##y" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 

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

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

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

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

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

57 

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

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

59 
parcontract :: "(comb*comb) set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

19736  61 
abbreviation 
62 
parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) 

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

64 
parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) 

65 
"x ===> y == (x,y) \<in> parcontract^*" 

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

66 

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

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

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

69 
refl: "x =1=> x" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

70 
K: "K##x##y =1=> x" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

71 
S: "S##x##y##z =1=> (x##z)##(y##z)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

72 
Ap: "[ x=1=>y; z=1=>w ] ==> x##z =1=> y##w" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 

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

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

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

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

77 

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

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

81 

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

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

83 
{*confluence; Lambda/Commutation treats this more abstractly*} 
19736  84 
"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

85 
(\<forall>y'. (x,y') \<in> r > 
19736  86 
(\<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

87 

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 
subsection {*Reflexive/Transitive closure preserves ChurchRosser property*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

90 

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

91 
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

92 

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

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

94 
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

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

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

97 
\<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

98 
apply (unfold diamond_def) 
16563  99 
apply (erule rtrancl_induct) 
100 
apply (meson rtrancl_refl) 

101 
apply (meson rtrancl_trans r_into_rtrancl) 

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

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

103 

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

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

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

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

107 
apply (erule rtrancl_induct, blast) 
16588  108 
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

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

110 

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 
subsection {* Noncontraction results *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

113 

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

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

115 

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

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

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

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

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

120 

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

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

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

123 

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

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

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

126 

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

127 
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

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

129 

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

130 
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

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

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

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

134 

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

135 
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

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

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

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

139 

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

140 
(** Counterexample to the diamond property for 1> **) 
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 
lemma KIII_contract1: "K##I##(I##I) 1> I" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

143 
by (rule contract.K) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

144 

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

145 
lemma KIII_contract2: "K##I##(I##I) 1> K##I##((K##I)##(K##I))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

147 

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

148 
lemma KIII_contract3: "K##I##((K##I)##(K##I)) 1> I" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

149 
by blast 
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 
lemma not_diamond_contract: "~ diamond(contract)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

153 
apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

155 

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 
subsection {* Results about Parallel Contraction *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

158 

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

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

160 

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

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

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

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

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

165 

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

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

167 

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

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

169 

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

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

171 

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

172 
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

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

174 

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

175 
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

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

177 

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

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

179 
"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

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

181 

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

182 
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

183 

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

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

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

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

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

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

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

190 

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

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

192 
\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

193 
*} 
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 contract_subset_parcontract: "contract <= parcontract" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

196 
apply (rule subsetI) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

197 
apply (simp only: split_tupled_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

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

200 

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

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

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

203 

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

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

205 

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

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

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

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

209 

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

210 
lemma parcontract_subset_reduce: "parcontract <= contract^*" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

211 
apply (rule subsetI) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

212 
apply (simp only: split_tupled_all) 
16563  213 
apply (erule parcontract.induct, blast+) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

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

215 

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

216 
lemma reduce_eq_parreduce: "contract^* = parcontract^*" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

217 
by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

218 
parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset

219 

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

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

221 
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

222 

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

223 
end 