99 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
99 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
100 |
100 |
101 fun mk_atom_fset t = |
101 fun mk_atom_fset t = |
102 let |
102 let |
103 val ty = fastype_of t; |
103 val ty = fastype_of t; |
104 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
104 val atom_ty = dest_fsetT ty |
105 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
105 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
106 val fset = @{term "fset :: atom fset => atom set"} |
106 val fset = @{term "fset :: atom fset => atom set"} |
107 in |
107 in |
108 fset $ (Const (@{const_name map_fset}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
108 fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) |
109 end |
109 end |
110 |
110 |
111 fun mk_atom_list t = |
111 fun mk_atom_list t = |
112 let |
112 let |
113 val ty = fastype_of t; |
113 val ty = fastype_of t |
114 val atom_ty = dest_listT ty --> @{typ atom}; |
114 val atom_ty = dest_listT ty |
115 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
115 val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} |
116 in |
116 in |
117 Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t |
117 Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t |
118 end |
118 end |
119 |
119 |
120 (* functions that coerces singletons, sets and fsets of concrete atoms |
120 (* functions that coerces singletons, sets and fsets of concrete atoms |
121 into sets of general atoms *) |
121 into sets of general atoms *) |
122 fun setify ctxt t = |
122 fun setify ctxt t = |
139 val ty = fastype_of t; |
139 val ty = fastype_of t; |
140 in |
140 in |
141 if is_atom ctxt ty |
141 if is_atom ctxt ty |
142 then HOLogic.mk_list @{typ atom} [mk_atom t] |
142 then HOLogic.mk_list @{typ atom} [mk_atom t] |
143 else if is_atom_list ctxt ty |
143 else if is_atom_list ctxt ty |
144 then mk_atom_set t |
144 then mk_atom_list t |
145 else raise TERM ("listify", [t]) |
145 else raise TERM ("listify", [t]) |
146 end |
146 end |
147 |
147 |
148 (* coerces a list into a set *) |
148 (* coerces a list into a set *) |
149 fun to_set t = |
149 fun to_set t = |
150 if fastype_of t = @{typ "atom list"} |
150 if fastype_of t = @{typ "atom list"} |
151 then @{term "set::atom list => atom set"} $ t |
151 then @{term "set :: atom list => atom set"} $ t |
152 else t |
152 else t |
153 |
153 |
154 |
154 |
155 (** functions that construct the equations for fv and fv_bn **) |
155 (** functions that construct the equations for fv and fv_bn **) |
156 |
156 |
270 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
270 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
271 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
271 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
272 |
272 |
273 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
273 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
274 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
274 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
275 |
275 |
276 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
276 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
277 |
277 |
278 val {fs, simps, inducts, ...} = info; |
278 val {fs, simps, inducts, ...} = info; |
279 |
279 |
280 val morphism = ProofContext.export_morphism lthy'' lthy |
280 val morphism = ProofContext.export_morphism lthy'' lthy |