53 in |
51 in |
54 proc_exprop cos (thy',thm') |
52 proc_exprop cos (thy',thm') |
55 end |
53 end |
56 | _ => raise THM ("Internal error: Bad specification theorem",0,[thm]) |
54 | _ => raise THM ("Internal error: Bad specification theorem",0,[thm]) |
57 |
55 |
58 fun add_specification_i cos (name,atts) arg = |
56 fun add_specification_i cos arg = |
59 let |
57 arg |> apsnd freezeT |
60 fun apply_attributes arg = Thm.apply_attributes(arg,atts) |
58 |> proc_exprop cos |
61 fun add_final (arg as (thy,thm)) = |
59 |> apsnd standard |
62 if name = "" |
|
63 then arg |
|
64 else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm)); |
|
65 PureThy.store_thm((name,thm),[]) thy) |
|
66 in |
|
67 arg |> apsnd freezeT |
|
68 |> proc_exprop cos |
|
69 |> apsnd standard |
|
70 |> apply_attributes |
|
71 |> add_final |
|
72 end |
|
73 |
|
74 fun add_specification cos (name,atts) arg = |
|
75 add_specification_i cos (name,map (Attrib.global_attribute thy) atts) arg |
|
76 |
60 |
77 (* Collect all intances of constants in term *) |
61 (* Collect all intances of constants in term *) |
78 |
62 |
79 fun collect_consts ( t $ u,tms) = collect_consts (u,collect_consts (t,tms)) |
63 fun collect_consts ( t $ u,tms) = collect_consts (u,collect_consts (t,tms)) |
80 | collect_consts ( Abs(_,_,t),tms) = collect_consts (t,tms) |
64 | collect_consts ( Abs(_,_,t),tms) = collect_consts (t,tms) |
124 end) thawed_prop_consts of |
108 end) thawed_prop_consts of |
125 [] => error ("Constant \"" ^ (Sign.string_of_term sg c) ^ "\" not found in specification") |
109 [] => error ("Constant \"" ^ (Sign.string_of_term sg c) ^ "\" not found in specification") |
126 | [cf] => unvarify cf vmap |
110 | [cf] => unvarify cf vmap |
127 | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification") |
111 | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification") |
128 end |
112 end |
|
113 val frees = Term.term_frees prop |
|
114 val tsig = Sign.tsig_of (sign_of thy) |
|
115 val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees) |
|
116 "Only free variables of sort 'type' allowed in specifications" |
|
117 val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop) |
129 val proc_consts = map proc_const consts |
118 val proc_consts = map proc_const consts |
130 fun mk_exist (c,prop) = |
119 fun mk_exist (c,prop) = |
131 let |
120 let |
132 val T = type_of c |
121 val T = type_of c |
133 in |
122 in |
134 HOLogic.exists_const T $ Abs("x",T,Term.abstract_over (c,prop)) |
123 HOLogic.exists_const T $ Abs("x",T,Term.abstract_over (c,prop)) |
135 end |
124 end |
136 val ex_prop = foldr mk_exist (proc_consts,prop) |
125 val ex_prop = foldr mk_exist (proc_consts,prop_closed) |
137 val cnames = map (fst o dest_Const) proc_consts |
126 val cnames = map (fst o dest_Const) proc_consts |
138 fun zip3 [] [] [] = [] |
127 fun zip3 [] [] [] = [] |
139 | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs |
128 | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs |
140 | zip3 _ _ _ = error "Internal error: Bad specification syntax" |
129 | zip3 _ _ _ = error "Internal error: Bad specification syntax" |
|
130 val (name,atts) = alt_name |
|
131 fun add_final (arg as (thy,thm)) = |
|
132 if name = "" |
|
133 then arg |
|
134 else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm)); |
|
135 PureThy.store_thm((name,thm),[]) thy) |
|
136 fun post_process (arg as (thy,thm)) = |
|
137 let |
|
138 fun inst_all sg (thm,v) = |
|
139 let |
|
140 val cv = cterm_of sg v |
|
141 val cT = ctyp_of_term cv |
|
142 val spec' = instantiate' [Some cT] [None,Some cv] spec |
|
143 in |
|
144 thm RS spec' |
|
145 end |
|
146 fun remove_alls frees thm = foldl (inst_all (sign_of_thm thm)) (thm,frees) |
|
147 fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts) |
|
148 in |
|
149 arg |> apsnd (remove_alls frees) |
|
150 |> apsnd standard |
|
151 |> apply_atts |
|
152 |> add_final |
|
153 end |
141 in |
154 in |
142 IsarThy.theorem_i Drule.internalK |
155 IsarThy.theorem_i Drule.internalK |
143 (("",[add_specification (zip3 (names:string list) (cnames:string list) (overloaded:bool list)) alt_name]), |
156 (("",[add_specification_i (zip3 (names:string list) (cnames:string list) (overloaded:bool list)),post_process]), |
144 (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy |
157 (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy |
145 end |
158 end |
146 |
159 |
147 (* outer syntax *) |
160 (* outer syntax *) |
148 |
161 |