equal
deleted
inserted
replaced
272 using a |
272 using a |
273 apply (induct) |
273 apply (induct) |
274 apply(auto intro: list_eq.intros) |
274 apply(auto intro: list_eq.intros) |
275 done |
275 done |
276 |
276 |
|
277 lemma fun_rel_id: |
|
278 "op = ===> op = \<equiv> op =" |
|
279 apply (rule eq_reflection) |
|
280 apply (rule ext) |
|
281 apply (rule ext) |
|
282 apply (simp) |
|
283 apply (auto) |
|
284 apply (rule ext) |
|
285 apply (simp) |
|
286 done |
|
287 |
277 lemma ho_map_rsp: |
288 lemma ho_map_rsp: |
278 "op = ===> op = ===> op \<approx> ===> op \<approx> map map" |
289 "op = ===> op = ===> op \<approx> ===> op \<approx> map map" |
279 apply (simp add: FUN_REL.simps) |
290 by (simp add: fun_rel_id map_rsp) |
280 apply (rule allI) |
|
281 apply (rule allI) |
|
282 apply (rule impI) |
|
283 apply (rule allI) |
|
284 apply (rule allI) |
|
285 apply (rule impI) |
|
286 sorry (* apply (auto simp add: map_rsp[of "xa" "ya"]) *) |
|
287 |
291 |
288 lemma map_append : |
292 lemma map_append : |
289 "(map f ((a::'a list) @ b)) \<approx> |
293 "(map f ((a::'a list) @ b)) \<approx> |
290 ((map f a) ::'a list) @ (map f b)" |
294 ((map f a) ::'a list) @ (map f b)" |
291 apply simp |
295 by simp (rule list_eq_refl) |
292 apply (rule list_eq_refl) |
|
293 done |
|
294 |
296 |
295 thm list.induct |
297 thm list.induct |
296 lemma list_induct_hol4: |
298 lemma list_induct_hol4: |
297 fixes P :: "'a list \<Rightarrow> bool" |
299 fixes P :: "'a list \<Rightarrow> bool" |
298 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
300 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
529 lthy2 |
531 lthy2 |
530 end; |
532 end; |
531 *} |
533 *} |
532 *) |
534 *) |
533 |
535 |
534 (* These do not work without proper definitions to rewrite back *) |
|
535 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
536 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
536 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
537 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
537 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
538 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
538 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
539 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
539 thm m1_lift |
540 thm m1_lift |
552 val t = Type ("FSet.fset", l) |
553 val t = Type ("FSet.fset", l) |
553 val v = Var (nam, t) |
554 val v = Var (nam, t) |
554 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
555 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
555 *} |
556 *} |
556 |
557 |
557 ML {* |
|
558 Toplevel.program (fn () => |
|
559 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
560 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
|
561 ) |
|
562 ) |
|
563 *} |
|
564 |
|
565 |
|
566 |
|
567 (*prove aaa: {* (Thm.term_of cgoal2) *} |
|
568 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
569 apply (atomize(full)) |
|
570 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
571 done*) |
|
572 |
|
573 (* |
|
574 datatype obj1 = |
|
575 OVAR1 "string" |
|
576 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
|
577 | INVOKE1 "obj1 \<Rightarrow> string" |
|
578 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
|
579 *) |
|
580 |
558 |
581 end |
559 end |