equal
deleted
inserted
replaced
345 print_theorems |
345 print_theorems |
346 |
346 |
347 thm Rep_qtrm |
347 thm Rep_qtrm |
348 |
348 |
349 text {* another test *} |
349 text {* another test *} |
350 datatype 'a my = Foo |
|
351 consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool" |
|
352 axioms rmy_eq: "EQUIV Rmy" |
|
353 |
|
354 term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x" |
|
355 |
|
356 datatype 'a trm' = |
350 datatype 'a trm' = |
357 var' "'a" |
351 var' "'a" |
358 | app' "'a trm'" "'a trm'" |
352 | app' "'a trm'" "'a trm'" |
359 | lam' "'a" "'a trm'" |
353 | lam' "'a" "'a trm'" |
360 |
354 |
407 *} |
401 *} |
408 |
402 |
409 (* mapfuns for some standard types *) |
403 (* mapfuns for some standard types *) |
410 setup {* |
404 setup {* |
411 Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}}) |
405 Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}}) |
412 #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}}) |
406 #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}}) |
413 #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}}) |
407 #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}}) |
414 *} |
408 *} |
415 |
|
416 |
409 |
417 ML {* lookup (Context.Proof @{context}) @{type_name list} *} |
410 ML {* lookup (Context.Proof @{context}) @{type_name list} *} |
418 |
411 |
419 ML {* |
412 ML {* |
420 datatype abs_or_rep = abs | rep |
413 datatype abs_or_rep = abs | rep |
614 term UNION |
607 term UNION |
615 thm UNION_def |
608 thm UNION_def |
616 |
609 |
617 (* Maybe the infrastructure should not allow this kind of definition, without showing that |
610 (* Maybe the infrastructure should not allow this kind of definition, without showing that |
618 the relation respects lenght... *) |
611 the relation respects lenght... *) |
|
612 (* cu: what does this mean? *) |
619 local_setup {* |
613 local_setup {* |
620 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
614 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
621 *} |
615 *} |
622 |
616 |
623 term length |
617 term length |
646 fixes z |
640 fixes z |
647 assumes a: "xs \<approx> ys" |
641 assumes a: "xs \<approx> ys" |
648 shows "(z # xs) \<approx> (z # ys)" |
642 shows "(z # xs) \<approx> (z # ys)" |
649 using a by (rule QuotMain.list_eq.intros(5)) |
643 using a by (rule QuotMain.list_eq.intros(5)) |
650 |
644 |
|
645 (* cu: what does unlam do? *) |
651 ML {* |
646 ML {* |
652 fun unlam_def orig_ctxt ctxt t = |
647 fun unlam_def orig_ctxt ctxt t = |
653 let val rhs = Thm.rhs_of t in |
648 let val rhs = Thm.rhs_of t in |
654 (case try (Thm.dest_abs NONE) rhs of |
649 (case try (Thm.dest_abs NONE) rhs of |
655 SOME (v, vt) => |
650 SOME (v, vt) => |