57 (*lhs*) |
57 (*lhs*) |
58 val lhs_tfrees = |
58 val lhs_tfrees = |
59 map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; |
59 map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; |
60 |
60 |
61 val tname = Syntax.type_name t mx; |
61 val tname = Syntax.type_name t mx; |
62 val tlen = length vs; |
|
63 val newT = Type (full_name tname, map TFree lhs_tfrees); |
62 val newT = Type (full_name tname, map TFree lhs_tfrees); |
64 |
63 |
65 val Rep_name = "Rep_" ^ name; |
64 val Rep_name = "Rep_" ^ name; |
66 val Abs_name = "Abs_" ^ name; |
65 val Abs_name = "Abs_" ^ name; |
67 val setC = Const (full_name name, setT); |
66 val setC = Const (full_name name, setT); |
104 |
103 |
105 writeln("Proving nonemptiness of " ^ quote name ^ " ..."); |
104 writeln("Proving nonemptiness of " ^ quote name ^ " ..."); |
106 prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac; |
105 prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac; |
107 |
106 |
108 thy |
107 thy |
109 |> Theory.add_types [(t, tlen, mx)] |
108 |> PureThy.add_typedecls [(t, vs, mx)] |
110 |> Theory.add_arities_i |
109 |> Theory.add_arities_i |
111 [(full_name tname, replicate tlen logicS, logicS), |
110 [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)] |
112 (full_name tname, replicate tlen HOLogic.termS, HOLogic.termS)] |
|
113 |> Theory.add_consts_i |
111 |> Theory.add_consts_i |
114 [(name, setT, NoSyn), |
112 [(name, setT, NoSyn), |
115 (Rep_name, newT --> oldT, NoSyn), |
113 (Rep_name, newT --> oldT, NoSyn), |
116 (Abs_name, oldT --> newT, NoSyn)] |
114 (Abs_name, oldT --> newT, NoSyn)] |
117 |> (PureThy.add_defs_i o map Attribute.none) |
115 |> (PureThy.add_defs_i o map Attribute.none) |