277 |
277 |
278 fun get_fun_fun s fs_tys = |
278 fun get_fun_fun s fs_tys = |
279 let |
279 let |
280 val (fs, tys) = split_list fs_tys |
280 val (fs, tys) = split_list fs_tys |
281 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
281 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
282 val oty = Type (s, [oty2, nty1]) |
282 val oty = Type (s, [nty1, oty2]) |
283 val nty = Type (s, [oty1, nty2]) |
283 val nty = Type (s, [oty1, nty2]) |
|
284 val _ = tracing (Syntax.string_of_typ @{context} oty) |
284 val ftys = map (op -->) tys |
285 val ftys = map (op -->) tys |
285 in |
286 in |
286 (case (lookup (ProofContext.theory_of lthy) s) of |
287 (case (lookup (ProofContext.theory_of lthy) s) of |
287 SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) |
288 SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) |
288 | NONE => raise ERROR ("no map association for type " ^ s)) |
289 | NONE => raise ERROR ("no map association for type " ^ s)) |
343 It currently doesn't do it, the following code generates a wrong |
346 It currently doesn't do it, the following code generates a wrong |
344 function and the second ML block fails to typecheck for this reason: |
347 function and the second ML block fails to typecheck for this reason: |
345 |
348 |
346 *} |
349 *} |
347 |
350 |
348 (*ML {* |
351 ML {* |
349 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
352 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt"} |
350 |> fst |
|
351 |> type_of |
|
352 *} |
|
353 |
|
354 |
|
355 ML {* |
|
356 get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
|
357 |> fst |
353 |> fst |
358 |> cterm_of @{theory} |
354 |> cterm_of @{theory} |
359 *} |
355 *} |
360 *) |
|
361 |
|
362 ML {* |
|
363 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
364 |> fst |
|
365 |> type_of |
|
366 *} |
|
367 |
|
368 ML {* |
|
369 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
370 |> fst |
|
371 |> cterm_of @{theory} |
|
372 *} |
|
373 |
|
374 (* The followng also fails due to incorrect types... *) |
|
375 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
|
376 local_setup {* |
|
377 fn lthy => (Toplevel.program (fn () => |
|
378 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
|
379 )) |> snd |
|
380 *} |
|
381 |
|
382 |
|
383 |
356 |
384 text {* produces the definition for a lifted constant *} |
357 text {* produces the definition for a lifted constant *} |
385 |
358 |
386 ML {* |
359 ML {* |
387 fun get_const_def nconst oconst rty qty lthy = |
360 fun get_const_def nconst oconst rty qty lthy = |
424 val def_trm = get_const_def nconst oconst rty qty lthy |
397 val def_trm = get_const_def nconst oconst rty qty lthy |
425 in |
398 in |
426 define (nconst_bname, mx, def_trm) lthy |
399 define (nconst_bname, mx, def_trm) lthy |
427 end |
400 end |
428 *} |
401 *} |
|
402 |
|
403 (* A test whether get_fun works properly |
|
404 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
|
405 local_setup {* |
|
406 fn lthy => (Toplevel.program (fn () => |
|
407 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
|
408 )) |> snd |
|
409 *} |
|
410 *) |
429 |
411 |
430 local_setup {* |
412 local_setup {* |
431 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
413 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
432 make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
414 make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
433 make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
415 make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
732 fun mk_rep x = @{term REP_fset} $ x; |
714 fun mk_rep x = @{term REP_fset} $ x; |
733 fun mk_abs x = @{term ABS_fset} $ x; |
715 fun mk_abs x = @{term ABS_fset} $ x; |
734 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
716 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
735 @{const_name "membship"}, @{const_name "card1"}, |
717 @{const_name "membship"}, @{const_name "card1"}, |
736 @{const_name "append"}, @{const_name "fold1"}]; |
718 @{const_name "append"}, @{const_name "fold1"}]; |
737 |
|
738 *} |
719 *} |
739 |
720 |
740 ML {* val tm = @{term "x :: 'a list"} *} |
721 ML {* val tm = @{term "x :: 'a list"} *} |
741 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *} |
722 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *} |
742 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *} |
723 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *} |
1201 apply (metis) |
1182 apply (metis) |
1202 done |
1183 done |
1203 |
1184 |
1204 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1185 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1205 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1186 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1206 ML {* Syntax.string_of_term @{context} trm |> writeln *} |
1187 prove trm |
1207 term fun_map |
1188 sorry |
1208 ML {* Toplevel.program (fn () => cterm_of @{theory} trm) *} |
|
1209 |
1189 |
1210 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1190 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1211 |
1191 |
1212 prove card1_suc_r: {* |
1192 prove card1_suc_r: {* |
1213 Logic.mk_implies |
1193 Logic.mk_implies |
1227 done |
1207 done |
1228 |
1208 |
1229 ML {* @{thm fold1_def_2_r} OF [li] *} |
1209 ML {* @{thm fold1_def_2_r} OF [li] *} |
1230 |
1210 |
1231 ML {* |
1211 ML {* |
1232 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
|
1233 *} |
|
1234 |
|
1235 ML {* |
|
1236 val goal = |
|
1237 Toplevel.program (fn () => |
|
1238 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
1239 ) |
|
1240 *} |
|
1241 ML {* |
|
1242 val cgoal = |
|
1243 Toplevel.program (fn () => |
|
1244 cterm_of @{theory} goal |
|
1245 ) |
|
1246 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
|
1247 *} |
|
1248 |
|
1249 prove {* (Thm.term_of cgoal2) *} |
|
1250 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
1251 sorry |
|
1252 |
|
1253 ML {* |
|
1254 fun lift_theorem_fset_aux thm lthy = |
1212 fun lift_theorem_fset_aux thm lthy = |
1255 let |
1213 let |
1256 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1214 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1257 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1215 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
1258 val cgoal = cterm_of @{theory} goal; |
1216 val cgoal = cterm_of @{theory} goal; |
1259 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1217 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1260 val tac = transconv_fset_tac' @{context}; |
1218 val tac = transconv_fset_tac' @{context}; |
1261 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1219 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1262 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1220 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1340 |
1298 |
1341 = Ball (Respects ((op \<approx>) ===> (op =))) |
1299 = Ball (Respects ((op \<approx>) ===> (op =))) |
1342 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1300 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1343 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1301 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1344 thm APPLY_RSP |
1302 thm APPLY_RSP |
1345 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"] |
1303 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] |
1346 . |
1304 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]) |
1347 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1305 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1348 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1306 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1349 thm LAMBDA_PRS1[symmetric] |
1307 thm LAMBDA_PRS1[symmetric] |
1350 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1308 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1351 apply (unfold Ball_def) |
1309 apply (unfold Ball_def) |