81 val newT = Type (full_tname, map TFree lhs_tfrees); |
81 val newT = Type (full_tname, map TFree lhs_tfrees); |
82 |
82 |
83 val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; |
83 val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; |
84 val RepC = Const (full Rep_name, newT --> oldT); |
84 val RepC = Const (full Rep_name, newT --> oldT); |
85 fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT); |
85 fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT); |
86 val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT, |
86 val less_def = Logic.mk_equals (lessC newT, |
87 Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))); |
87 Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); |
88 |
88 |
89 fun make_po tac theory = theory |
89 fun make_po tac thy1 = |
90 |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac |
90 let |
91 ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) |
91 val ((_, {type_definition, set_def, ...}), thy2) = thy1 |
92 (Class.intro_classes_tac []) |
92 |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac; |
93 ||>> PureThy.add_defs true [Thm.no_attributes less_def] |
93 val lthy3 = thy2 |
94 |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => |
94 |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"}); |
95 AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) |
95 val less_def' = Syntax.check_term lthy3 less_def; |
96 (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) |
96 val ((_, (_, less_definition')), lthy4) = lthy3 |
97 #> pair (type_definition, less_definition, set_def)); |
97 |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def')); |
|
98 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); |
|
99 val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition'; |
|
100 val thy5 = lthy4 |
|
101 |> Class.prove_instantiation_instance |
|
102 (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)) |
|
103 |> LocalTheory.exit |
|
104 |> ProofContext.theory_of; |
|
105 in ((type_definition, less_definition, set_def), thy5) end; |
98 |
106 |
99 fun make_cpo admissible (type_def, less_def, set_def) theory = |
107 fun make_cpo admissible (type_def, less_def, set_def) theory = |
100 let |
108 let |
101 val admissible' = fold_rule (the_list set_def) admissible; |
109 val admissible' = fold_rule (the_list set_def) admissible; |
102 val cpo_thms = [type_def, less_def, admissible']; |
110 val cpo_thms = [type_def, less_def, admissible']; |