equal
deleted
inserted
replaced
1598 fun tag tm = ATerm (type_tag, [var "A", tm]) |
1598 fun tag tm = ATerm (type_tag, [var "A", tm]) |
1599 val tagged_var = tag (var "X") |
1599 val tagged_var = tag (var "X") |
1600 in |
1600 in |
1601 Formula (type_tag_idempotence_helper_name, Axiom, |
1601 Formula (type_tag_idempotence_helper_name, Axiom, |
1602 eq_formula type_enc [] false (tag tagged_var) tagged_var, |
1602 eq_formula type_enc [] false (tag tagged_var) tagged_var, |
1603 isabelle_info format simpN, NONE) |
1603 isabelle_info format eqN, NONE) |
1604 end |
1604 end |
1605 |
1605 |
1606 fun should_specialize_helper type_enc t = |
1606 fun should_specialize_helper type_enc t = |
1607 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1607 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1608 level_of_type_enc type_enc <> No_Types andalso |
1608 level_of_type_enc type_enc <> No_Types andalso |
1919 NONE, |
1919 NONE, |
1920 case snd stature of |
1920 case snd stature of |
1921 Intro => isabelle_info format introN |
1921 Intro => isabelle_info format introN |
1922 | Elim => isabelle_info format elimN |
1922 | Elim => isabelle_info format elimN |
1923 | Simp => isabelle_info format simpN |
1923 | Simp => isabelle_info format simpN |
1924 | Eq => isabelle_info format simpN |
1924 | Eq => isabelle_info format eqN |
1925 | _ => NONE) |
1925 | _ => NONE) |
1926 |> Formula |
1926 |> Formula |
1927 |
1927 |
1928 fun formula_line_for_class_rel_clause format type_enc |
1928 fun formula_line_for_class_rel_clause format type_enc |
1929 ({name, subclass, superclass, ...} : class_rel_clause) = |
1929 ({name, subclass, superclass, ...} : class_rel_clause) = |
2162 Formula (tags_sym_formula_prefix ^ |
2162 Formula (tags_sym_formula_prefix ^ |
2163 ascii_of (mangled_type format type_enc T), |
2163 ascii_of (mangled_type format type_enc T), |
2164 Axiom, |
2164 Axiom, |
2165 eq_formula type_enc (atomic_types_of T) false |
2165 eq_formula type_enc (atomic_types_of T) false |
2166 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, |
2166 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, |
2167 isabelle_info format simpN, NONE) |
2167 isabelle_info format eqN, NONE) |
2168 end |
2168 end |
2169 |
2169 |
2170 fun problem_lines_for_mono_types ctxt format mono type_enc Ts = |
2170 fun problem_lines_for_mono_types ctxt format mono type_enc Ts = |
2171 case type_enc of |
2171 case type_enc of |
2172 Simple_Types _ => [] |
2172 Simple_Types _ => [] |
2267 else |
2267 else |
2268 bounds |
2268 bounds |
2269 in |
2269 in |
2270 cons (Formula (ident_base ^ "_res", kind, |
2270 cons (Formula (ident_base ^ "_res", kind, |
2271 eq (tag_with res_T (cst bounds)) (cst tagged_bounds), |
2271 eq (tag_with res_T (cst bounds)) (cst tagged_bounds), |
2272 isabelle_info format simpN, NONE)) |
2272 isabelle_info format eqN, NONE)) |
2273 end |
2273 end |
2274 else |
2274 else |
2275 I |
2275 I |
2276 fun add_formula_for_arg k = |
2276 fun add_formula_for_arg k = |
2277 let val arg_T = nth arg_Ts k in |
2277 let val arg_T = nth arg_Ts k in |
2279 case chop k bounds of |
2279 case chop k bounds of |
2280 (bounds1, bound :: bounds2) => |
2280 (bounds1, bound :: bounds2) => |
2281 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, |
2281 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, |
2282 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) |
2282 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) |
2283 (cst bounds), |
2283 (cst bounds), |
2284 isabelle_info format simpN, NONE)) |
2284 isabelle_info format eqN, NONE)) |
2285 | _ => raise Fail "expected nonempty tail" |
2285 | _ => raise Fail "expected nonempty tail" |
2286 else |
2286 else |
2287 I |
2287 I |
2288 end |
2288 end |
2289 in |
2289 in |