9 imports Term |
9 imports Term |
10 begin |
10 begin |
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 Subtype :: "['a set, 'a => o] => 'a set" |
14 Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set" |
15 Bool :: "i set" |
15 Bool :: "i set" |
16 Unit :: "i set" |
16 Unit :: "i set" |
17 Plus :: "[i set, i set] => i set" (infixr "+" 55) |
17 Plus :: "[i set, i set] \<Rightarrow> i set" (infixr "+" 55) |
18 Pi :: "[i set, i => i set] => i set" |
18 Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set" |
19 Sigma :: "[i set, i => i set] => i set" |
19 Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set" |
20 Nat :: "i set" |
20 Nat :: "i set" |
21 List :: "i set => i set" |
21 List :: "i set \<Rightarrow> i set" |
22 Lists :: "i set => i set" |
22 Lists :: "i set \<Rightarrow> i set" |
23 ILists :: "i set => i set" |
23 ILists :: "i set \<Rightarrow> i set" |
24 TAll :: "(i set => i set) => i set" (binder "TALL " 55) |
24 TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TALL " 55) |
25 TEx :: "(i set => i set) => i set" (binder "TEX " 55) |
25 TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TEX " 55) |
26 Lift :: "i set => i set" ("(3[_])") |
26 Lift :: "i set \<Rightarrow> i set" ("(3[_])") |
27 |
27 |
28 SPLIT :: "[i, [i, i] => i set] => i set" |
28 SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set" |
29 |
29 |
30 syntax |
30 syntax |
31 "_Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" |
31 "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3PROD _:_./ _)" |
32 [0,0,60] 60) |
32 [0,0,60] 60) |
33 |
33 |
34 "_Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" |
34 "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3SUM _:_./ _)" |
35 [0,0,60] 60) |
35 [0,0,60] 60) |
36 |
36 |
37 "_arrow" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) |
37 "_arrow" :: "[i set, i set] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53) |
38 "_star" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
38 "_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55) |
39 "_Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
39 "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})") |
40 |
40 |
41 translations |
41 translations |
42 "PROD x:A. B" => "CONST Pi(A, %x. B)" |
42 "PROD x:A. B" => "CONST Pi(A, \<lambda>x. B)" |
43 "A -> B" => "CONST Pi(A, %_. B)" |
43 "A -> B" => "CONST Pi(A, \<lambda>_. B)" |
44 "SUM x:A. B" => "CONST Sigma(A, %x. B)" |
44 "SUM x:A. B" => "CONST Sigma(A, \<lambda>x. B)" |
45 "A * B" => "CONST Sigma(A, %_. B)" |
45 "A * B" => "CONST Sigma(A, \<lambda>_. B)" |
46 "{x: A. B}" == "CONST Subtype(A, %x. B)" |
46 "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)" |
47 |
47 |
48 print_translation {* |
48 print_translation {* |
49 [(@{const_syntax Pi}, |
49 [(@{const_syntax Pi}, |
50 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
50 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
51 (@{const_syntax Sigma}, |
51 (@{const_syntax Sigma}, |
52 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
52 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
53 *} |
53 *} |
54 |
54 |
55 defs |
55 defs |
56 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
56 Subtype_def: "{x:A. P(x)} == {x. x:A \<and> P(x)}" |
57 Unit_def: "Unit == {x. x=one}" |
57 Unit_def: "Unit == {x. x=one}" |
58 Bool_def: "Bool == {x. x=true | x=false}" |
58 Bool_def: "Bool == {x. x=true | x=false}" |
59 Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
59 Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
60 Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |
60 Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}" |
61 Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
61 Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
62 Nat_def: "Nat == lfp(% X. Unit + X)" |
62 Nat_def: "Nat == lfp(\<lambda>X. Unit + X)" |
63 List_def: "List(A) == lfp(% X. Unit + A*X)" |
63 List_def: "List(A) == lfp(\<lambda>X. Unit + A*X)" |
64 |
64 |
65 Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" |
65 Lists_def: "Lists(A) == gfp(\<lambda>X. Unit + A*X)" |
66 ILists_def: "ILists(A) == gfp(% X.{} + A*X)" |
66 ILists_def: "ILists(A) == gfp(\<lambda>X.{} + A*X)" |
67 |
67 |
68 Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
68 Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
69 Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
69 Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
70 Lift_def: "[A] == A Un {bot}" |
70 Lift_def: "[A] == A Un {bot}" |
71 |
71 |
72 SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" |
72 SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})" |
73 |
73 |
74 |
74 |
75 lemmas simp_type_defs = |
75 lemmas simp_type_defs = |
76 Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def |
76 Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def |
77 and ind_type_defs = Nat_def List_def |
77 and ind_type_defs = Nat_def List_def |
78 and simp_data_defs = one_def inl_def inr_def |
78 and simp_data_defs = one_def inl_def inr_def |
79 and ind_data_defs = zero_def succ_def nil_def cons_def |
79 and ind_data_defs = zero_def succ_def nil_def cons_def |
80 |
80 |
81 lemma subsetXH: "A <= B <-> (ALL x. x:A --> x:B)" |
81 lemma subsetXH: "A <= B \<longleftrightarrow> (ALL x. x:A \<longrightarrow> x:B)" |
82 by blast |
82 by blast |
83 |
83 |
84 |
84 |
85 subsection {* Exhaustion Rules *} |
85 subsection {* Exhaustion Rules *} |
86 |
86 |
87 lemma EmptyXH: "!!a. a : {} <-> False" |
87 lemma EmptyXH: "\<And>a. a : {} \<longleftrightarrow> False" |
88 and SubtypeXH: "!!a A P. a : {x:A. P(x)} <-> (a:A & P(a))" |
88 and SubtypeXH: "\<And>a A P. a : {x:A. P(x)} \<longleftrightarrow> (a:A \<and> P(a))" |
89 and UnitXH: "!!a. a : Unit <-> a=one" |
89 and UnitXH: "\<And>a. a : Unit \<longleftrightarrow> a=one" |
90 and BoolXH: "!!a. a : Bool <-> a=true | a=false" |
90 and BoolXH: "\<And>a. a : Bool \<longleftrightarrow> a=true | a=false" |
91 and PlusXH: "!!a A B. a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" |
91 and PlusXH: "\<And>a A B. a : A+B \<longleftrightarrow> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" |
92 and PiXH: "!!a A B. a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))" |
92 and PiXH: "\<And>a A B. a : PROD x:A. B(x) \<longleftrightarrow> (EX b. a=lam x. b(x) \<and> (ALL x:A. b(x):B(x)))" |
93 and SgXH: "!!a A B. a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=<x,y>)" |
93 and SgXH: "\<And>a A B. a : SUM x:A. B(x) \<longleftrightarrow> (EX x:A. EX y:B(x).a=<x,y>)" |
94 unfolding simp_type_defs by blast+ |
94 unfolding simp_type_defs by blast+ |
95 |
95 |
96 lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH |
96 lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH |
97 |
97 |
98 lemma LiftXH: "a : [A] <-> (a=bot | a:A)" |
98 lemma LiftXH: "a : [A] \<longleftrightarrow> (a=bot | a:A)" |
99 and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))" |
99 and TallXH: "a : TALL X. B(X) \<longleftrightarrow> (ALL X. a:B(X))" |
100 and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" |
100 and TexXH: "a : TEX X. B(X) \<longleftrightarrow> (EX X. a:B(X))" |
101 unfolding simp_type_defs by blast+ |
101 unfolding simp_type_defs by blast+ |
102 |
102 |
103 ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *} |
103 ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *} |
104 |
104 |
105 |
105 |
106 subsection {* Canonical Type Rules *} |
106 subsection {* Canonical Type Rules *} |
107 |
107 |
108 lemma oneT: "one : Unit" |
108 lemma oneT: "one : Unit" |
109 and trueT: "true : Bool" |
109 and trueT: "true : Bool" |
110 and falseT: "false : Bool" |
110 and falseT: "false : Bool" |
111 and lamT: "!!b B. [| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)" |
111 and lamT: "\<And>b B. (\<And>x. x:A \<Longrightarrow> b(x):B(x)) \<Longrightarrow> lam x. b(x) : Pi(A,B)" |
112 and pairT: "!!b B. [| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)" |
112 and pairT: "\<And>b B. \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> <a,b>:Sigma(A,B)" |
113 and inlT: "a:A ==> inl(a) : A+B" |
113 and inlT: "a:A \<Longrightarrow> inl(a) : A+B" |
114 and inrT: "b:B ==> inr(b) : A+B" |
114 and inrT: "b:B \<Longrightarrow> inr(b) : A+B" |
115 by (blast intro: XHs [THEN iffD2])+ |
115 by (blast intro: XHs [THEN iffD2])+ |
116 |
116 |
117 lemmas canTs = oneT trueT falseT pairT lamT inlT inrT |
117 lemmas canTs = oneT trueT falseT pairT lamT inlT inrT |
118 |
118 |
119 |
119 |
120 subsection {* Non-Canonical Type Rules *} |
120 subsection {* Non-Canonical Type Rules *} |
121 |
121 |
122 lemma lem: "[| a:B(u); u=v |] ==> a : B(v)" |
122 lemma lem: "\<lbrakk>a:B(u); u = v\<rbrakk> \<Longrightarrow> a : B(v)" |
123 by blast |
123 by blast |
124 |
124 |
125 |
125 |
126 ML {* |
126 ML {* |
127 fun mk_ncanT_tac top_crls crls = |
127 fun mk_ncanT_tac top_crls crls = |
135 |
135 |
136 method_setup ncanT = {* |
136 method_setup ncanT = {* |
137 Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) |
137 Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) |
138 *} |
138 *} |
139 |
139 |
140 lemma ifT: |
140 lemma ifT: "\<lbrakk>b:Bool; b=true \<Longrightarrow> t:A(true); b=false \<Longrightarrow> u:A(false)\<rbrakk> \<Longrightarrow> if b then t else u : A(b)" |
141 "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> |
|
142 if b then t else u : A(b)" |
|
143 by ncanT |
141 by ncanT |
144 |
142 |
145 lemma applyT: "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)" |
143 lemma applyT: "\<lbrakk>f : Pi(A,B); a:A\<rbrakk> \<Longrightarrow> f ` a : B(a)" |
146 by ncanT |
144 by ncanT |
147 |
145 |
148 lemma splitT: |
146 lemma splitT: "\<lbrakk>p:Sigma(A,B); \<And>x y. \<lbrakk>x:A; y:B(x); p=<x,y>\<rbrakk> \<Longrightarrow> c(x,y):C(<x,y>)\<rbrakk> \<Longrightarrow> split(p,c):C(p)" |
149 "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |] |
|
150 ==> split(p,c):C(p)" |
|
151 by ncanT |
147 by ncanT |
152 |
148 |
153 lemma whenT: |
149 lemma whenT: |
154 "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B; p=inr(y) |] |
150 "\<lbrakk>p:A+B; |
155 ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)" |
151 \<And>x. \<lbrakk>x:A; p=inl(x)\<rbrakk> \<Longrightarrow> a(x):C(inl(x)); |
|
152 \<And>y. \<lbrakk>y:B; p=inr(y)\<rbrakk> \<Longrightarrow> b(y):C(inr(y))\<rbrakk> \<Longrightarrow> when(p,a,b) : C(p)" |
156 by ncanT |
153 by ncanT |
157 |
154 |
158 lemmas ncanTs = ifT applyT splitT whenT |
155 lemmas ncanTs = ifT applyT splitT whenT |
159 |
156 |
160 |
157 |
161 subsection {* Subtypes *} |
158 subsection {* Subtypes *} |
162 |
159 |
163 lemma SubtypeD1: "a : Subtype(A, P) ==> a : A" |
160 lemma SubtypeD1: "a : Subtype(A, P) \<Longrightarrow> a : A" |
164 and SubtypeD2: "a : Subtype(A, P) ==> P(a)" |
161 and SubtypeD2: "a : Subtype(A, P) \<Longrightarrow> P(a)" |
165 by (simp_all add: SubtypeXH) |
162 by (simp_all add: SubtypeXH) |
166 |
163 |
167 lemma SubtypeI: "[| a:A; P(a) |] ==> a : {x:A. P(x)}" |
164 lemma SubtypeI: "\<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}" |
168 by (simp add: SubtypeXH) |
165 by (simp add: SubtypeXH) |
169 |
166 |
170 lemma SubtypeE: "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q" |
167 lemma SubtypeE: "\<lbrakk>a : {x:A. P(x)}; \<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
171 by (simp add: SubtypeXH) |
168 by (simp add: SubtypeXH) |
172 |
169 |
173 |
170 |
174 subsection {* Monotonicity *} |
171 subsection {* Monotonicity *} |
175 |
172 |
176 lemma idM: "mono (%X. X)" |
173 lemma idM: "mono (\<lambda>X. X)" |
177 apply (rule monoI) |
174 apply (rule monoI) |
178 apply assumption |
175 apply assumption |
179 done |
176 done |
180 |
177 |
181 lemma constM: "mono(%X. A)" |
178 lemma constM: "mono(\<lambda>X. A)" |
182 apply (rule monoI) |
179 apply (rule monoI) |
183 apply (rule subset_refl) |
180 apply (rule subset_refl) |
184 done |
181 done |
185 |
182 |
186 lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])" |
183 lemma "mono(\<lambda>X. A(X)) \<Longrightarrow> mono(\<lambda>X.[A(X)])" |
187 apply (rule subsetI [THEN monoI]) |
184 apply (rule subsetI [THEN monoI]) |
188 apply (drule LiftXH [THEN iffD1]) |
185 apply (drule LiftXH [THEN iffD1]) |
189 apply (erule disjE) |
186 apply (erule disjE) |
190 apply (erule disjI1 [THEN LiftXH [THEN iffD2]]) |
187 apply (erule disjI1 [THEN LiftXH [THEN iffD2]]) |
191 apply (rule disjI2 [THEN LiftXH [THEN iffD2]]) |
188 apply (rule disjI2 [THEN LiftXH [THEN iffD2]]) |
192 apply (drule (1) monoD) |
189 apply (drule (1) monoD) |
193 apply blast |
190 apply blast |
194 done |
191 done |
195 |
192 |
196 lemma SgM: |
193 lemma SgM: |
197 "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> |
194 "\<lbrakk>mono(\<lambda>X. A(X)); \<And>x X. x:A(X) \<Longrightarrow> mono(\<lambda>X. B(X,x))\<rbrakk> \<Longrightarrow> |
198 mono(%X. Sigma(A(X),B(X)))" |
195 mono(\<lambda>X. Sigma(A(X),B(X)))" |
199 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
196 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
200 dest!: monoD [THEN subsetD]) |
197 dest!: monoD [THEN subsetD]) |
201 |
198 |
202 lemma PiM: |
199 lemma PiM: "(\<And>x. x:A \<Longrightarrow> mono(\<lambda>X. B(X,x))) \<Longrightarrow> mono(\<lambda>X. Pi(A,B(X)))" |
203 "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))" |
|
204 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
200 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
205 dest!: monoD [THEN subsetD]) |
201 dest!: monoD [THEN subsetD]) |
206 |
202 |
207 lemma PlusM: |
203 lemma PlusM: "\<lbrakk>mono(\<lambda>X. A(X)); mono(\<lambda>X. B(X))\<rbrakk> \<Longrightarrow> mono(\<lambda>X. A(X)+B(X))" |
208 "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))" |
|
209 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
204 by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
210 dest!: monoD [THEN subsetD]) |
205 dest!: monoD [THEN subsetD]) |
211 |
206 |
212 |
207 |
213 subsection {* Recursive types *} |
208 subsection {* Recursive types *} |
214 |
209 |
215 subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} |
210 subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} |
216 |
211 |
217 lemma NatM: "mono(%X. Unit+X)" |
212 lemma NatM: "mono(\<lambda>X. Unit+X)" |
218 apply (rule PlusM constM idM)+ |
213 apply (rule PlusM constM idM)+ |
219 done |
214 done |
220 |
215 |
221 lemma def_NatB: "Nat = Unit + Nat" |
216 lemma def_NatB: "Nat = Unit + Nat" |
222 apply (rule def_lfp_Tarski [OF Nat_def]) |
217 apply (rule def_lfp_Tarski [OF Nat_def]) |
223 apply (rule NatM) |
218 apply (rule NatM) |
224 done |
219 done |
225 |
220 |
226 lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))" |
221 lemma ListM: "mono(\<lambda>X.(Unit+Sigma(A,\<lambda>y. X)))" |
227 apply (rule PlusM SgM constM idM)+ |
222 apply (rule PlusM SgM constM idM)+ |
228 done |
223 done |
229 |
224 |
230 lemma def_ListB: "List(A) = Unit + A * List(A)" |
225 lemma def_ListB: "List(A) = Unit + A * List(A)" |
231 apply (rule def_lfp_Tarski [OF List_def]) |
226 apply (rule def_lfp_Tarski [OF List_def]) |
264 |
259 |
265 |
260 |
266 subsection {* Type Rules *} |
261 subsection {* Type Rules *} |
267 |
262 |
268 lemma zeroT: "zero : Nat" |
263 lemma zeroT: "zero : Nat" |
269 and succT: "n:Nat ==> succ(n) : Nat" |
264 and succT: "n:Nat \<Longrightarrow> succ(n) : Nat" |
270 and nilT: "[] : List(A)" |
265 and nilT: "[] : List(A)" |
271 and consT: "[| h:A; t:List(A) |] ==> h$t : List(A)" |
266 and consT: "\<lbrakk>h:A; t:List(A)\<rbrakk> \<Longrightarrow> h$t : List(A)" |
272 by (blast intro: iXHs [THEN iffD2])+ |
267 by (blast intro: iXHs [THEN iffD2])+ |
273 |
268 |
274 lemmas icanTs = zeroT succT nilT consT |
269 lemmas icanTs = zeroT succT nilT consT |
275 |
270 |
276 |
271 |
277 method_setup incanT = {* |
272 method_setup incanT = {* |
278 Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) |
273 Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) |
279 *} |
274 *} |
280 |
275 |
281 lemma ncaseT: |
276 lemma ncaseT: "\<lbrakk>n:Nat; n=zero \<Longrightarrow> b:C(zero); \<And>x. \<lbrakk>x:Nat; n=succ(x)\<rbrakk> \<Longrightarrow> c(x):C(succ(x))\<rbrakk> |
282 "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] |
277 \<Longrightarrow> ncase(n,b,c) : C(n)" |
283 ==> ncase(n,b,c) : C(n)" |
|
284 by incanT |
278 by incanT |
285 |
279 |
286 lemma lcaseT: |
280 lemma lcaseT: "\<lbrakk>l:List(A); l = [] \<Longrightarrow> b:C([]); \<And>h t. \<lbrakk>h:A; t:List(A); l=h$t\<rbrakk> \<Longrightarrow> c(h,t):C(h$t)\<rbrakk> |
287 "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A; t:List(A); l=h$t |] ==> |
281 \<Longrightarrow> lcase(l,b,c) : C(l)" |
288 c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)" |
|
289 by incanT |
282 by incanT |
290 |
283 |
291 lemmas incanTs = ncaseT lcaseT |
284 lemmas incanTs = ncaseT lcaseT |
292 |
285 |
293 |
286 |
294 subsection {* Induction Rules *} |
287 subsection {* Induction Rules *} |
295 |
288 |
296 lemmas ind_Ms = NatM ListM |
289 lemmas ind_Ms = NatM ListM |
297 |
290 |
298 lemma Nat_ind: "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" |
291 lemma Nat_ind: "\<lbrakk>n:Nat; P(zero); \<And>x. \<lbrakk>x:Nat; P(x)\<rbrakk> \<Longrightarrow> P(succ(x))\<rbrakk> \<Longrightarrow> P(n)" |
299 apply (unfold ind_data_defs) |
292 apply (unfold ind_data_defs) |
300 apply (erule def_induct [OF Nat_def _ NatM]) |
293 apply (erule def_induct [OF Nat_def _ NatM]) |
301 apply (blast intro: canTs elim!: case_rls) |
294 apply (blast intro: canTs elim!: case_rls) |
302 done |
295 done |
303 |
296 |
304 lemma List_ind: |
297 lemma List_ind: "\<lbrakk>l:List(A); P([]); \<And>x xs. \<lbrakk>x:A; xs:List(A); P(xs)\<rbrakk> \<Longrightarrow> P(x$xs)\<rbrakk> \<Longrightarrow> P(l)" |
305 "[| l:List(A); P([]); !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> P(l)" |
|
306 apply (unfold ind_data_defs) |
298 apply (unfold ind_data_defs) |
307 apply (erule def_induct [OF List_def _ ListM]) |
299 apply (erule def_induct [OF List_def _ ListM]) |
308 apply (blast intro: canTs elim!: case_rls) |
300 apply (blast intro: canTs elim!: case_rls) |
309 done |
301 done |
310 |
302 |
311 lemmas inds = Nat_ind List_ind |
303 lemmas inds = Nat_ind List_ind |
312 |
304 |
313 |
305 |
314 subsection {* Primitive Recursive Rules *} |
306 subsection {* Primitive Recursive Rules *} |
315 |
307 |
316 lemma nrecT: |
308 lemma nrecT: "\<lbrakk>n:Nat; b:C(zero); \<And>x g. \<lbrakk>x:Nat; g:C(x)\<rbrakk> \<Longrightarrow> c(x,g):C(succ(x))\<rbrakk> |
317 "[| n:Nat; b:C(zero); |
309 \<Longrightarrow> nrec(n,b,c) : C(n)" |
318 !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==> |
|
319 nrec(n,b,c) : C(n)" |
|
320 by (erule Nat_ind) auto |
310 by (erule Nat_ind) auto |
321 |
311 |
322 lemma lrecT: |
312 lemma lrecT: "\<lbrakk>l:List(A); b:C([]); \<And>x xs g. \<lbrakk>x:A; xs:List(A); g:C(xs)\<rbrakk> \<Longrightarrow> c(x,xs,g):C(x$xs) \<rbrakk> |
323 "[| l:List(A); b:C([]); |
313 \<Longrightarrow> lrec(l,b,c) : C(l)" |
324 !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> |
|
325 lrec(l,b,c) : C(l)" |
|
326 by (erule List_ind) auto |
314 by (erule List_ind) auto |
327 |
315 |
328 lemmas precTs = nrecT lrecT |
316 lemmas precTs = nrecT lrecT |
329 |
317 |
330 |
318 |
331 subsection {* Theorem proving *} |
319 subsection {* Theorem proving *} |
332 |
320 |
333 lemma SgE2: |
321 lemma SgE2: "\<lbrakk><a,b> : Sigma(A,B); \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
334 "[| <a,b> : Sigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" |
|
335 unfolding SgXH by blast |
322 unfolding SgXH by blast |
336 |
323 |
337 (* General theorem proving ignores non-canonical term-formers, *) |
324 (* General theorem proving ignores non-canonical term-formers, *) |
338 (* - intro rules are type rules for canonical terms *) |
325 (* - intro rules are type rules for canonical terms *) |
339 (* - elim rules are case rules (no non-canonical terms appear) *) |
326 (* - elim rules are case rules (no non-canonical terms appear) *) |
430 by (rule po_refl [THEN PO_iff [THEN iffD1]]) |
415 by (rule po_refl [THEN PO_iff [THEN iffD1]]) |
431 |
416 |
432 lemma POgenIs: |
417 lemma POgenIs: |
433 "<true,true> : POgen(R)" |
418 "<true,true> : POgen(R)" |
434 "<false,false> : POgen(R)" |
419 "<false,false> : POgen(R)" |
435 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)" |
420 "\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : POgen(R)" |
436 "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)" |
421 "\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : POgen(R)" |
437 "<one,one> : POgen(R)" |
422 "<one,one> : POgen(R)" |
438 "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> |
423 "<a,a'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
439 <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
424 <inl(a),inl(a')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
440 "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> |
425 "<b,b'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
441 <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
426 <inr(b),inr(b')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
442 "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
427 "<zero,zero> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
443 "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> |
428 "<n,n'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
444 <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
429 <succ(n),succ(n')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
445 "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
430 "<[],[]> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
446 "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] |
431 "\<lbrakk><h,h'> : lfp(\<lambda>x. POgen(x) Un R Un PO); <t,t'> : lfp(\<lambda>x. POgen(x) Un R Un PO)\<rbrakk> |
447 ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
432 \<Longrightarrow> <h$t,h'$t'> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
448 unfolding data_defs by (genIs POgenXH POgen_mono)+ |
433 unfolding data_defs by (genIs POgenXH POgen_mono)+ |
449 |
434 |
450 ML {* |
435 ML {* |
451 fun POgen_tac ctxt (rla, rlb) i = |
436 fun POgen_tac ctxt (rla, rlb) i = |
452 SELECT_GOAL (safe_tac ctxt) i THEN |
437 SELECT_GOAL (safe_tac ctxt) i THEN |
464 by (rule refl [THEN EQ_iff [THEN iffD1]]) |
449 by (rule refl [THEN EQ_iff [THEN iffD1]]) |
465 |
450 |
466 lemma EQgenIs: |
451 lemma EQgenIs: |
467 "<true,true> : EQgen(R)" |
452 "<true,true> : EQgen(R)" |
468 "<false,false> : EQgen(R)" |
453 "<false,false> : EQgen(R)" |
469 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)" |
454 "\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : EQgen(R)" |
470 "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)" |
455 "\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : EQgen(R)" |
471 "<one,one> : EQgen(R)" |
456 "<one,one> : EQgen(R)" |
472 "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
457 "<a,a'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
473 <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
458 <inl(a),inl(a')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
474 "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
459 "<b,b'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
475 <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
460 <inr(b),inr(b')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
476 "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
461 "<zero,zero> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
477 "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
462 "<n,n'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
478 <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
463 <succ(n),succ(n')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
479 "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
464 "<[],[]> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
480 "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] |
465 "\<lbrakk><h,h'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ); <t,t'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ)\<rbrakk> |
481 ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
466 \<Longrightarrow> <h$t,h'$t'> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
482 unfolding data_defs by (genIs EQgenXH EQgen_mono)+ |
467 unfolding data_defs by (genIs EQgenXH EQgen_mono)+ |
483 |
468 |
484 ML {* |
469 ML {* |
485 fun EQgen_raw_tac i = |
470 fun EQgen_raw_tac i = |
486 (REPEAT (resolve_tac (@{thms EQgenIs} @ |
471 (REPEAT (resolve_tac (@{thms EQgenIs} @ |