118 fun proc_single prop = |
118 fun proc_single prop = |
119 let |
119 let |
120 val frees = OldTerm.term_frees prop |
120 val frees = OldTerm.term_frees prop |
121 val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees |
121 val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees |
122 orelse error "Specificaton: Only free variables of sort 'type' allowed" |
122 orelse error "Specificaton: Only free variables of sort 'type' allowed" |
123 val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees) |
123 val prop_closed = fold_rev (fn (vname, T) => fn prop => |
|
124 HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop |
124 in |
125 in |
125 (prop_closed,frees) |
126 (prop_closed,frees) |
126 end |
127 end |
127 |
128 |
128 val props'' = map proc_single props' |
129 val props'' = map proc_single props' |
149 [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") |
150 [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") |
150 | [cf] => unvarify cf vmap |
151 | [cf] => unvarify cf vmap |
151 | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)") |
152 | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)") |
152 end |
153 end |
153 val proc_consts = map proc_const consts |
154 val proc_consts = map proc_const consts |
154 fun mk_exist (c,prop) = |
155 fun mk_exist c prop = |
155 let |
156 let |
156 val T = type_of c |
157 val T = type_of c |
157 val cname = Long_Name.base_name (fst (dest_Const c)) |
158 val cname = Long_Name.base_name (fst (dest_Const c)) |
158 val vname = if Syntax.is_identifier cname |
159 val vname = if Syntax.is_identifier cname |
159 then cname |
160 then cname |
160 else "x" |
161 else "x" |
161 in |
162 in |
162 HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) |
163 HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) |
163 end |
164 end |
164 val ex_prop = List.foldr mk_exist prop proc_consts |
165 val ex_prop = fold_rev mk_exist proc_consts prop |
165 val cnames = map (fst o dest_Const) proc_consts |
166 val cnames = map (fst o dest_Const) proc_consts |
166 fun post_process (arg as (thy,thm)) = |
167 fun post_process (arg as (thy,thm)) = |
167 let |
168 let |
168 fun inst_all thy v thm = |
169 fun inst_all thy v thm = |
169 let |
170 let |