91 thm core_haskell.perm_bn_simps |
91 thm core_haskell.perm_bn_simps |
92 thm core_haskell.bn_finite |
92 thm core_haskell.bn_finite |
93 |
93 |
94 thm core_haskell.distinct |
94 thm core_haskell.distinct |
95 thm core_haskell.induct |
95 thm core_haskell.induct |
|
96 thm core_haskell.inducts |
|
97 thm core_haskell.strong_induct |
96 thm core_haskell.exhaust |
98 thm core_haskell.exhaust |
97 thm core_haskell.fv_defs |
99 thm core_haskell.fv_defs |
98 thm core_haskell.bn_defs |
100 thm core_haskell.bn_defs |
99 thm core_haskell.perm_simps |
101 thm core_haskell.perm_simps |
100 thm core_haskell.eq_iff |
102 thm core_haskell.eq_iff |
101 thm core_haskell.fv_bn_eqvt |
103 thm core_haskell.fv_bn_eqvt |
102 thm core_haskell.size_eqvt |
104 thm core_haskell.size_eqvt |
103 thm core_haskell.supp |
105 thm core_haskell.supp |
104 |
106 |
105 lemma strong_induction_principle: |
|
106 fixes c::"'a::fs" |
|
107 assumes a01: "\<And>b. P1 b KStar" |
|
108 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
|
109 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
|
110 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
|
111 and a05: "\<And>string b. P3 b (TC string)" |
|
112 and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)" |
|
113 and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)" |
|
114 and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk> |
|
115 \<Longrightarrow> P3 b (TAll tvar tkind ty)" |
|
116 and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)" |
|
117 and a10: "\<And>b. P4 b TsNil" |
|
118 and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)" |
|
119 and a12: "\<And>string b. P5 b (CVar string)" |
|
120 and a12a:"\<And>str b. P5 b (CConst str)" |
|
121 and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)" |
|
122 and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)" |
|
123 and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk> |
|
124 \<Longrightarrow> P5 b (CAll tvar ckind co)" |
|
125 and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)" |
|
126 and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)" |
|
127 and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)" |
|
128 and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)" |
|
129 and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)" |
|
130 and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)" |
|
131 and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)" |
|
132 and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)" |
|
133 and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)" |
|
134 and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)" |
|
135 and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)" |
|
136 and a25: "\<And>b. P6 b CsNil" |
|
137 and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)" |
|
138 and a27: "\<And>var b. P7 b (Var var)" |
|
139 and a28: "\<And>string b. P7 b (K string)" |
|
140 and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
|
141 \<Longrightarrow> P7 b (LAMT tvar tkind trm)" |
|
142 and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
|
143 \<Longrightarrow> P7 b (LAMC tvar ckind trm)" |
|
144 and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)" |
|
145 and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)" |
|
146 and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)" |
|
147 and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)" |
|
148 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
|
149 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
|
150 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
|
151 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
|
152 and a37: "\<And>b. P8 b ANil" |
|
153 and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk> |
|
154 \<Longrightarrow> P8 b (ACons pt trm assoc_lst)" |
|
155 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
|
156 \<Longrightarrow> P9 b (Kpat string tvars cvars vars)" |
|
157 and a40: "\<And>b. P10 b VsNil" |
|
158 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
|
159 and a42: "\<And>b. P11 b TvsNil" |
|
160 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
|
161 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
|
162 and a44: "\<And>b. P12 b CvsNil" |
|
163 and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk> |
|
164 \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)" |
|
165 shows "P1 c tkind" |
|
166 "P2 c ckind" |
|
167 "P3 c ty" |
|
168 "P4 c ty_lst" |
|
169 "P5 c co" |
|
170 "P6 c co_lst" |
|
171 "P7 c trm" |
|
172 "P8 c assoc_lst" |
|
173 "P9 c pt" |
|
174 "P10 c vars" |
|
175 "P11 c tvars" |
|
176 "P12 c cvars" |
|
177 oops |
|
178 |
107 |
179 end |
108 end |
180 |
109 |