84 [when_def, copy_def] @ |
84 [when_def, copy_def] @ |
85 con_defs @ dis_defs @ sel_defs @ |
85 con_defs @ dis_defs @ sel_defs @ |
86 [take_def, finite_def]) |
86 [take_def, finite_def]) |
87 end; (* let *) |
87 end; (* let *) |
88 |
88 |
|
89 val add_axioms_i = PureThy.add_axioms_i o map Attribute.none; |
89 |
90 |
90 in (* local *) |
91 in (* local *) |
91 |
92 |
92 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
93 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
93 val comp_dname = Sign.full_name (sign_of thy') comp_dnam; |
94 val comp_dname = Sign.full_name (sign_of thy') comp_dnam; |
124 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
125 foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
125 ::map one_con cons)))); |
126 ::map one_con cons)))); |
126 in foldr' mk_conj (mapn one_comp 0 eqs)end )); |
127 in foldr' mk_conj (mapn one_comp 0 eqs)end )); |
127 fun add_one (thy,(dnam,axs,dfs)) = thy |
128 fun add_one (thy,(dnam,axs,dfs)) = thy |
128 |> Theory.add_path dnam |
129 |> Theory.add_path dnam |
129 |> PureThy.add_store_axioms_i (infer_types thy' dfs)(*add_store_defs_i*) |
130 |> add_axioms_i (infer_types thy' dfs)(*add_defs_i*) |
130 |> PureThy.add_store_axioms_i (infer_types thy' axs) |
131 |> add_axioms_i (infer_types thy' axs) |
131 |> Theory.add_path ".."; |
132 |> Theory.parent_path; |
132 val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
133 val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
133 in thy |> Theory.add_path comp_dnam |
134 in thy |> Theory.add_path comp_dnam |
134 |> PureThy.add_store_axioms_i (infer_types thy' |
135 |> add_axioms_i (infer_types thy' |
135 (bisim_def::(if length eqs>1 then [copy_def] else []))) |
136 (bisim_def::(if length eqs>1 then [copy_def] else []))) |
136 |> Theory.add_path ".." |
137 |> Theory.parent_path |
137 end; |
138 end; |
138 |
139 |
139 end; (* local *) |
140 end; (* local *) |
140 end; (* struct *) |
141 end; (* struct *) |