author | wenzelm |
Mon, 03 Oct 2016 20:26:32 +0200 | |
changeset 64025 | ff4910ced9ba |
parent 62045 | 75a7db3cae7e |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
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 |
|
60530 | 6 |
section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close> |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
|
62045 | 8 |
theory Comb |
9 |
imports Main |
|
10 |
begin |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
11 |
|
60530 | 12 |
text \<open> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
13 |
Curiously, combinators do not include free variables. |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
14 |
|
58623 | 15 |
Example taken from @{cite camilleri92}. |
62045 | 16 |
\<close> |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
18 |
|
60530 | 19 |
subsection \<open>Definitions\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
20 |
|
61993 | 21 |
text \<open>Datatype definition of combinators \<open>S\<close> and \<open>K\<close>.\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
22 |
|
58310 | 23 |
datatype comb = K |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
24 |
| S |
61993 | 25 |
| Ap comb comb (infixl "\<bullet>" 90) |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
26 |
|
60530 | 27 |
text \<open> |
61993 | 28 |
Inductive definition of contractions, \<open>\<rightarrow>\<^sup>1\<close> and |
29 |
(multi-step) reductions, \<open>\<rightarrow>\<close>. |
|
60530 | 30 |
\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
31 |
|
61993 | 32 |
inductive_set contract :: "(comb*comb) set" |
33 |
and contract_rel1 :: "[comb,comb] \<Rightarrow> bool" (infixl "\<rightarrow>\<^sup>1" 50) |
|
34 |
where |
|
35 |
"x \<rightarrow>\<^sup>1 y == (x,y) \<in> contract" |
|
36 |
| K: "K\<bullet>x\<bullet>y \<rightarrow>\<^sup>1 x" |
|
37 |
| S: "S\<bullet>x\<bullet>y\<bullet>z \<rightarrow>\<^sup>1 (x\<bullet>z)\<bullet>(y\<bullet>z)" |
|
38 |
| Ap1: "x\<rightarrow>\<^sup>1y \<Longrightarrow> x\<bullet>z \<rightarrow>\<^sup>1 y\<bullet>z" |
|
39 |
| Ap2: "x\<rightarrow>\<^sup>1y \<Longrightarrow> z\<bullet>x \<rightarrow>\<^sup>1 z\<bullet>y" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
40 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
41 |
abbreviation |
61993 | 42 |
contract_rel :: "[comb,comb] \<Rightarrow> bool" (infixl "\<rightarrow>" 50) where |
43 |
"x \<rightarrow> y == (x,y) \<in> contract\<^sup>*" |
|
15816 | 44 |
|
60530 | 45 |
text \<open> |
61993 | 46 |
Inductive definition of parallel contractions, \<open>\<Rrightarrow>\<^sup>1\<close> and |
47 |
(multi-step) parallel reductions, \<open>\<Rrightarrow>\<close>. |
|
60530 | 48 |
\<close> |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
|
61993 | 50 |
inductive_set parcontract :: "(comb*comb) set" |
51 |
and parcontract_rel1 :: "[comb,comb] \<Rightarrow> bool" (infixl "\<Rrightarrow>\<^sup>1" 50) |
|
52 |
where |
|
53 |
"x \<Rrightarrow>\<^sup>1 y == (x,y) \<in> parcontract" |
|
54 |
| refl: "x \<Rrightarrow>\<^sup>1 x" |
|
55 |
| K: "K\<bullet>x\<bullet>y \<Rrightarrow>\<^sup>1 x" |
|
56 |
| S: "S\<bullet>x\<bullet>y\<bullet>z \<Rrightarrow>\<^sup>1 (x\<bullet>z)\<bullet>(y\<bullet>z)" |
|
57 |
| Ap: "[| x\<Rrightarrow>\<^sup>1y; z\<Rrightarrow>\<^sup>1w |] ==> x\<bullet>z \<Rrightarrow>\<^sup>1 y\<bullet>w" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
58 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
59 |
abbreviation |
61993 | 60 |
parcontract_rel :: "[comb,comb] \<Rightarrow> bool" (infixl "\<Rrightarrow>" 50) where |
61 |
"x \<Rrightarrow> y == (x,y) \<in> parcontract\<^sup>*" |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
62 |
|
60530 | 63 |
text \<open> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
64 |
Misc definitions. |
60530 | 65 |
\<close> |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
|
19736 | 67 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
68 |
I :: comb where |
61993 | 69 |
"I = S\<bullet>K\<bullet>K" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
70 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
71 |
definition |
61993 | 72 |
diamond :: "('a * 'a)set \<Rightarrow> bool" where |
73 |
\<comment>\<open>confluence; Lambda/Commutation treats this more abstractly\<close> |
|
19736 | 74 |
"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
|
75 |
(\<forall>y'. (x,y') \<in> r --> |
19736 | 76 |
(\<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
|
77 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
78 |
|
60530 | 79 |
subsection \<open>Reflexive/Transitive closure preserves Church-Rosser property\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
80 |
|
60530 | 81 |
text\<open>So does the Transitive closure, with a similar proof\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
82 |
|
60530 | 83 |
text\<open>Strip lemma. |
84 |
The induction hypothesis covers all but the last diamond of the strip.\<close> |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
85 |
lemma diamond_strip_lemmaE [rule_format]: |
61993 | 86 |
"[| diamond(r); (x,y) \<in> r\<^sup>* |] ==> |
87 |
\<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r\<^sup>* & (y,z) \<in> r)" |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
88 |
apply (unfold diamond_def) |
16563 | 89 |
apply (erule rtrancl_induct) |
90 |
apply (meson rtrancl_refl) |
|
91 |
apply (meson rtrancl_trans r_into_rtrancl) |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
92 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
93 |
|
61993 | 94 |
lemma diamond_rtrancl: "diamond(r) \<Longrightarrow> diamond(r\<^sup>*)" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
95 |
apply (simp (no_asm_simp) add: diamond_def) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
96 |
apply (rule impI [THEN allI, THEN allI]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
97 |
apply (erule rtrancl_induct, blast) |
16588 | 98 |
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
|
99 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
100 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
101 |
|
60530 | 102 |
subsection \<open>Non-contraction results\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
103 |
|
60530 | 104 |
text \<open>Derive a case for each combinator constructor.\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
105 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
106 |
inductive_cases |
61993 | 107 |
K_contractE [elim!]: "K \<rightarrow>\<^sup>1 r" |
108 |
and S_contractE [elim!]: "S \<rightarrow>\<^sup>1 r" |
|
109 |
and Ap_contractE [elim!]: "p\<bullet>q \<rightarrow>\<^sup>1 r" |
|
13075
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 |
declare contract.K [intro!] contract.S [intro!] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
112 |
declare contract.Ap1 [intro] contract.Ap2 [intro] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
113 |
|
61993 | 114 |
lemma I_contract_E [elim!]: "I \<rightarrow>\<^sup>1 z \<Longrightarrow> P" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
115 |
by (unfold I_def, blast) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
116 |
|
61993 | 117 |
lemma K1_contractD [elim!]: "K\<bullet>x \<rightarrow>\<^sup>1 z \<Longrightarrow> (\<exists>x'. z = K\<bullet>x' & x \<rightarrow>\<^sup>1 x')" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
118 |
by blast |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
119 |
|
61993 | 120 |
lemma Ap_reduce1 [intro]: "x \<rightarrow> y \<Longrightarrow> x\<bullet>z \<rightarrow> y\<bullet>z" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
121 |
apply (erule rtrancl_induct) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
122 |
apply (blast intro: rtrancl_trans)+ |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
123 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
124 |
|
61993 | 125 |
lemma Ap_reduce2 [intro]: "x \<rightarrow> y \<Longrightarrow> z\<bullet>x \<rightarrow> z\<bullet>y" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
126 |
apply (erule rtrancl_induct) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
127 |
apply (blast intro: rtrancl_trans)+ |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
128 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
129 |
|
61993 | 130 |
text \<open>Counterexample to the diamond property for @{term "x \<rightarrow>\<^sup>1 y"}\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
131 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
132 |
lemma not_diamond_contract: "~ diamond(contract)" |
35621 | 133 |
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
|
134 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
135 |
|
60530 | 136 |
subsection \<open>Results about Parallel Contraction\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
137 |
|
60530 | 138 |
text \<open>Derive a case for each combinator constructor.\<close> |
13075
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 |
inductive_cases |
61993 | 141 |
K_parcontractE [elim!]: "K \<Rrightarrow>\<^sup>1 r" |
142 |
and S_parcontractE [elim!]: "S \<Rrightarrow>\<^sup>1 r" |
|
143 |
and Ap_parcontractE [elim!]: "p\<bullet>q \<Rrightarrow>\<^sup>1 r" |
|
13075
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 |
declare parcontract.intros [intro] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
146 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
147 |
(*** Basic properties of parallel contraction ***) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
148 |
|
60530 | 149 |
subsection \<open>Basic properties of parallel contraction\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
150 |
|
61993 | 151 |
lemma K1_parcontractD [dest!]: "K\<bullet>x \<Rrightarrow>\<^sup>1 z \<Longrightarrow> (\<exists>x'. z = K\<bullet>x' & x \<Rrightarrow>\<^sup>1 x')" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
152 |
by blast |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
153 |
|
61993 | 154 |
lemma S1_parcontractD [dest!]: "S\<bullet>x \<Rrightarrow>\<^sup>1 z \<Longrightarrow> (\<exists>x'. z = S\<bullet>x' & x \<Rrightarrow>\<^sup>1 x')" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
155 |
by blast |
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 S2_parcontractD [dest!]: |
61993 | 158 |
"S\<bullet>x\<bullet>y \<Rrightarrow>\<^sup>1 z \<Longrightarrow> (\<exists>x' y'. z = S\<bullet>x'\<bullet>y' & x \<Rrightarrow>\<^sup>1 x' & y \<Rrightarrow>\<^sup>1 y')" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
159 |
by blast |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
160 |
|
60530 | 161 |
text\<open>The rules above are not essential but make proofs much faster\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
162 |
|
60530 | 163 |
text\<open>Church-Rosser property for parallel contraction\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
164 |
lemma diamond_parcontract: "diamond parcontract" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
165 |
apply (unfold diamond_def) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
166 |
apply (rule impI [THEN allI, THEN allI]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
167 |
apply (erule parcontract.induct, fast+) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
168 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
169 |
|
60530 | 170 |
text \<open> |
61993 | 171 |
\<^medskip> |
172 |
Equivalence of @{prop "p \<rightarrow> q"} and @{prop "p \<Rrightarrow> q"}. |
|
60530 | 173 |
\<close> |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
174 |
|
61993 | 175 |
lemma contract_subset_parcontract: "contract \<subseteq> parcontract" |
35621 | 176 |
by (auto, erule contract.induct, blast+) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
177 |
|
60530 | 178 |
text\<open>Reductions: simply throw together reflexivity, transitivity and |
179 |
the one-step reductions\<close> |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
180 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
181 |
declare r_into_rtrancl [intro] rtrancl_trans [intro] |
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 |
(*Example only: not used*) |
61993 | 184 |
lemma reduce_I: "I\<bullet>x \<rightarrow> x" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
185 |
by (unfold I_def, blast) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
186 |
|
61993 | 187 |
lemma parcontract_subset_reduce: "parcontract \<subseteq> contract\<^sup>*" |
35621 | 188 |
by (auto, erule parcontract.induct, blast+) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
189 |
|
61993 | 190 |
lemma reduce_eq_parreduce: "contract\<^sup>* = parcontract\<^sup>*" |
35621 | 191 |
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
|
192 |
|
61993 | 193 |
theorem diamond_reduce: "diamond(contract\<^sup>*)" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
11359
diff
changeset
|
194 |
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
|
195 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
196 |
end |