52 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
52 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
53 |
53 |
54 fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = |
54 fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = |
55 let |
55 let |
56 val ctxt = ProofContext.init thy; |
56 val ctxt = ProofContext.init thy; |
57 val full = Sign.full_name thy; |
57 val full = Sign.full_bname thy; |
58 |
58 |
59 (*rhs*) |
59 (*rhs*) |
60 val full_name = full name; |
60 val full_name = full name; |
61 val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
61 val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
62 val setT = Term.fastype_of set; |
62 val setT = Term.fastype_of set; |
92 |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; |
92 |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; |
93 val lthy3 = thy2 |
93 val lthy3 = thy2 |
94 |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"}); |
94 |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"}); |
95 val less_def' = Syntax.check_term lthy3 less_def; |
95 val less_def' = Syntax.check_term lthy3 less_def; |
96 val ((_, (_, less_definition')), lthy4) = lthy3 |
96 val ((_, (_, less_definition')), lthy4) = lthy3 |
97 |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def')); |
97 |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def')); |
98 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); |
98 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); |
99 val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition'; |
99 val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition'; |
100 val thy5 = lthy4 |
100 val thy5 = lthy4 |
101 |> Class.prove_instantiation_instance |
101 |> Class.prove_instantiation_instance |
102 (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)) |
102 (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)) |