7 |
7 |
8 signature CPODEF = |
8 signature CPODEF = |
9 sig |
9 sig |
10 type cpo_info = |
10 type cpo_info = |
11 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
11 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
12 is_lub: thm, lub: thm, compact: thm } |
12 lub: thm, compact: thm } |
13 type pcpo_info = |
13 type pcpo_info = |
14 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
14 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
15 Rep_defined: thm, Abs_defined: thm } |
15 Rep_defined: thm, Abs_defined: thm } |
16 |
16 |
17 val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
17 val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
43 |
43 |
44 (** type definitions **) |
44 (** type definitions **) |
45 |
45 |
46 type cpo_info = |
46 type cpo_info = |
47 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
47 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
48 is_lub: thm, lub: thm, compact: thm } |
48 lub: thm, compact: thm } |
49 |
49 |
50 type pcpo_info = |
50 type pcpo_info = |
51 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
51 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
52 Rep_defined: thm, Abs_defined: thm } |
52 Rep_defined: thm, Abs_defined: thm } |
53 |
53 |
92 (* transfer thms so that they will know about the new cpo instance *) |
92 (* transfer thms so that they will know about the new cpo instance *) |
93 val cpo_thms' = map (Thm.transfer thy) cpo_thms |
93 val cpo_thms' = map (Thm.transfer thy) cpo_thms |
94 fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') |
94 fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') |
95 val cont_Rep = make @{thm typedef_cont_Rep} |
95 val cont_Rep = make @{thm typedef_cont_Rep} |
96 val cont_Abs = make @{thm typedef_cont_Abs} |
96 val cont_Abs = make @{thm typedef_cont_Abs} |
97 val is_lub = make @{thm typedef_is_lub} |
|
98 val lub = make @{thm typedef_lub} |
97 val lub = make @{thm typedef_lub} |
99 val compact = make @{thm typedef_compact} |
98 val compact = make @{thm typedef_compact} |
100 val (_, thy) = |
99 val (_, thy) = |
101 thy |
100 thy |
102 |> Sign.add_path (Binding.name_of name) |
101 |> Sign.add_path (Binding.name_of name) |
103 |> Global_Theory.add_thms |
102 |> Global_Theory.add_thms |
104 ([((Binding.prefix_name "adm_" name, admissible'), []), |
103 ([((Binding.prefix_name "adm_" name, admissible'), []), |
105 ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
104 ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
106 ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
105 ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
107 ((Binding.prefix_name "is_lub_" name, is_lub ), []), |
|
108 ((Binding.prefix_name "lub_" name, lub ), []), |
106 ((Binding.prefix_name "lub_" name, lub ), []), |
109 ((Binding.prefix_name "compact_" name, compact ), [])]) |
107 ((Binding.prefix_name "compact_" name, compact ), [])]) |
110 ||> Sign.parent_path |
108 ||> Sign.parent_path |
111 val cpo_info : cpo_info = |
109 val cpo_info : cpo_info = |
112 { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
110 { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
113 cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact } |
111 cont_Abs = cont_Abs, lub = lub, compact = compact } |
114 in |
112 in |
115 (cpo_info, thy) |
113 (cpo_info, thy) |
116 end |
114 end |
117 |
115 |
118 fun prove_pcpo |
116 fun prove_pcpo |