63 val pg = pg' thy; |
63 val pg = pg' thy; |
64 |
64 |
65 |
65 |
66 (* ----- getting the axioms and definitions --------------------------------- *) |
66 (* ----- getting the axioms and definitions --------------------------------- *) |
67 |
67 |
68 local fun ga s dn = get_thm thy (dn^"."^s) in |
68 local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in |
69 val ax_abs_iso = ga "abs_iso" dname; |
69 val ax_abs_iso = ga "abs_iso" dname; |
70 val ax_rep_iso = ga "rep_iso" dname; |
70 val ax_rep_iso = ga "rep_iso" dname; |
71 val ax_when_def = ga "when_def" dname; |
71 val ax_when_def = ga "when_def" dname; |
72 val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons; |
72 val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons; |
73 val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons; |
73 val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons; |
339 val d = writeln("Proving induction properties of domain "^comp_dname^" ..."); |
339 val d = writeln("Proving induction properties of domain "^comp_dname^" ..."); |
340 val pg = pg' thy; |
340 val pg = pg' thy; |
341 |
341 |
342 (* ----- getting the composite axiom and definitions ------------------------ *) |
342 (* ----- getting the composite axiom and definitions ------------------------ *) |
343 |
343 |
344 local fun ga s dn = get_thm thy (dn^"."^s) in |
344 local fun ga s dn = get_thm thy (dn ^ "." ^ s, None) in |
345 val axs_reach = map (ga "reach" ) dnames; |
345 val axs_reach = map (ga "reach" ) dnames; |
346 val axs_take_def = map (ga "take_def" ) dnames; |
346 val axs_take_def = map (ga "take_def" ) dnames; |
347 val axs_finite_def = map (ga "finite_def") dnames; |
347 val axs_finite_def = map (ga "finite_def") dnames; |
348 val ax_copy2_def = ga "copy_def" comp_dnam; |
348 val ax_copy2_def = ga "copy_def" comp_dnam; |
349 val ax_bisim_def = ga "bisim_def" comp_dnam; |
349 val ax_bisim_def = ga "bisim_def" comp_dnam; |
350 end; (* local *) |
350 end; (* local *) |
351 |
351 |
352 local fun gt s dn = get_thm thy (dn^"."^s); |
352 local fun gt s dn = get_thm thy (dn ^ "." ^ s, None); |
353 fun gts s dn = get_thms thy (dn^"."^s) in |
353 fun gts s dn = get_thms thy (dn ^ "." ^ s, None) in |
354 val cases = map (gt "casedist" ) dnames; |
354 val cases = map (gt "casedist" ) dnames; |
355 val con_rews = flat (map (gts "con_rews" ) dnames); |
355 val con_rews = flat (map (gts "con_rews" ) dnames); |
356 val copy_rews = flat (map (gts "copy_rews") dnames); |
356 val copy_rews = flat (map (gts "copy_rews") dnames); |
357 end; (* local *) |
357 end; (* local *) |
358 |
358 |