equal
deleted
inserted
replaced
96 val dummy_thm: thm |
96 val dummy_thm: thm |
97 val free_dummy_thm: thm |
97 val free_dummy_thm: thm |
98 val is_sort_constraint: term -> bool |
98 val is_sort_constraint: term -> bool |
99 val sort_constraintI: thm |
99 val sort_constraintI: thm |
100 val sort_constraint_eq: thm |
100 val sort_constraint_eq: thm |
101 val sort_constraint_intr: indexname * sort -> thm -> thm |
|
102 val sort_constraint_intr_shyps: thm -> thm |
|
103 val with_subgoal: int -> (thm -> thm) -> thm -> thm |
101 val with_subgoal: int -> (thm -> thm) -> thm -> thm |
104 val comp_no_flatten: thm * int -> int -> thm -> thm |
102 val comp_no_flatten: thm * int -> int -> thm -> thm |
105 val rename_bvars: (string * string) list -> thm -> thm |
103 val rename_bvars: (string * string) list -> thm -> thm |
106 val rename_bvars': string option list -> thm -> thm |
104 val rename_bvars': string option list -> thm -> thm |
107 val incr_indexes: thm -> thm -> thm |
105 val incr_indexes: thm -> thm -> thm |
646 store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>))) |
644 store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>))) |
647 (Thm.equal_intr |
645 (Thm.equal_intr |
648 (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) |
646 (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) |
649 (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) |
647 (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) |
650 (implies_intr_list [A, C] (Thm.assume A))); |
648 (implies_intr_list [A, C] (Thm.assume A))); |
651 |
|
652 val sort_constraint_eq' = Thm.symmetric sort_constraint_eq; |
|
653 |
|
654 fun sort_constraint_intr tvar thm = |
|
655 Thm.equal_elim |
|
656 (Thm.instantiate |
|
657 ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))], |
|
658 [((("A", 0), propT), Thm.cprop_of thm)]) |
|
659 sort_constraint_eq') thm; |
|
660 |
|
661 fun sort_constraint_intr_shyps raw_thm = |
|
662 let val thm = Thm.strip_shyps raw_thm in |
|
663 (case Thm.extra_shyps thm of |
|
664 [] => thm |
|
665 | shyps => |
|
666 let |
|
667 val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm [])); |
|
668 val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps; |
|
669 in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end) |
|
670 end; |
|
671 |
649 |
672 end; |
650 end; |
673 |
651 |
674 |
652 |
675 (* HHF normalization *) |
653 (* HHF normalization *) |