equal
deleted
inserted
replaced
1165 apply (assumption) |
1165 apply (assumption) |
1166 apply (metis) |
1166 apply (metis) |
1167 done |
1167 done |
1168 |
1168 |
1169 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1169 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1170 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1170 ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1171 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1171 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1172 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1172 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1173 |
1173 |
1174 prove trm |
1174 ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
1175 |
|
1176 prove list_induct_tr: trm_r |
1175 apply (atomize(full)) |
1177 apply (atomize(full)) |
1176 apply (simp only: id_def[symmetric]) |
1178 apply (simp only: id_def[symmetric]) |
1177 |
1179 |
1178 (* APPLY_RSP_TAC *) |
1180 (* APPLY_RSP_TAC *) |
1179 ML_prf {* |
1181 ML_prf {* |
1298 apply (assumption) |
1300 apply (assumption) |
1299 prefer 2 |
1301 prefer 2 |
1300 apply (simp) |
1302 apply (simp) |
1301 sorry |
1303 sorry |
1302 |
1304 |
|
1305 prove list_induct_t: trm |
|
1306 apply (simp only: list_induct_tr[symmetric]) |
|
1307 apply (tactic {* rtac thm 1 *}) |
|
1308 done |
|
1309 |
|
1310 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
|
1311 |
1303 thm list.recs(2) |
1312 thm list.recs(2) |
1304 |
1313 |
1305 |
1314 |
1306 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1315 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1307 |
1316 |