A Collection of Isabelle Programming Hacks
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 

553 lines
24 KiB

  1. (***********************************************************************************
  2. * Copyright (c) 2018-2019 Achim D. Brucker
  3. *
  4. * All rights reserved.
  5. *
  6. * Redistribution and use in source and binary forms, with or without
  7. * modification, are permitted provided that the following conditions are met:
  8. *
  9. * * Redistributions of source code must retain the above copyright notice, this
  10. *
  11. * * Redistributions in binary form must reproduce the above copyright notice,
  12. * this list of conditions and the following disclaimer in the documentation
  13. * and/or other materials provided with the distribution.
  14. *
  15. * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  16. * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  17. * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  18. * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  19. * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  20. * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  21. * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  22. * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  23. * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  24. * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  25. *
  26. * SPDX-License-Identifier: BSD-2-Clause
  27. * Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/
  28. * Dependencies: None (assert.thy is used for testing the theory but it is
  29. * not required for providing the functionality of this hack)
  30. ***********************************************************************************)
  31. (***********************************************************************************
  32. # Changelog
  33. This comment documents all notable changes to this file in a format inspired by
  34. [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres
  35. to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
  36. ## [Unreleased]
  37. ## [1.0.0] - 2017-06-25
  38. - Initial release
  39. ***********************************************************************************)
  40. chapter\<open>Using Print and Parse Translations for Hiding Type Variables\<close>
  41. theory
  42. "Hiding_Type_Variables"
  43. imports
  44. "Assert" (* Can be replaced by Main, after removing all assertions. *)
  45. keywords
  46. "register_default_tvars"
  47. "update_default_tvars_mode"::thy_decl
  48. begin
  49. text\<open>
  50. This theory implements a mechanism for declaring default type variables for
  51. data types. This comes handy for complex data types with many type variables.
  52. The theory sets up both configurable print and parse translations that allows
  53. for replacing @{emph \<open>all\<close>} type variables by \<open>(_)\<close>, e.g., a five-ary
  54. constructor \<open>('a, 'b, 'c, 'd, 'e) hide_tvar_foo\<close> can be shorted to
  55. \<open>(_) hide_tvar_foo\<close>. The use of this shorthand in output (printing) and input
  56. (parsing) is, on a per-type basis, user-configurable using the top-level
  57. commands \<open>register_default_tvars\<close> (for registering the names of the
  58. default type variables and the print/parse mode) and
  59. \<open>update_default_tvars_mode\<close> (for changing the print/parse mode
  60. dynamically).
  61. The input also supports short-hands for declaring default sorts (e.g.,
  62. \<open>(_::linorder)\<close> specifies that all default variables need to be
  63. instances of the sort (type class) @{class \<open>linorder\<close>} and short-hands
  64. of overriding a suffice (or prefix) of the default type variables. For
  65. example, \<open>('state) hide_tvar_foo _.\<close> is a short-hand for
  66. \<open>('a, 'b, 'c, 'd, 'state) hide_tvar_foo\<close>.
  67. \<close>
  68. section\<open>Implementation\<close>
  69. subsection\<open>Theory Managed Data Structure\<close>
  70. ML\<open>
  71. signature HIDE_TVAR = sig
  72. datatype print_mode = print_all | print | noprint
  73. datatype tvar_subst = right | left
  74. datatype parse_mode = parse | noparse
  75. type hide_varT = {
  76. name: string,
  77. tvars: typ list,
  78. typ_syn_tab : (string * typ list*string) Symtab.table,
  79. print_mode: print_mode,
  80. parse_mode: parse_mode
  81. }
  82. val parse_print_mode : string -> print_mode
  83. val parse_parse_mode : string -> parse_mode
  84. val register : string -> print_mode option -> parse_mode option ->
  85. theory -> theory
  86. val update_mode : string -> print_mode option -> parse_mode option ->
  87. theory -> theory
  88. val lookup : theory -> string -> hide_varT option
  89. val hide_tvar_tr' : string -> Proof.context -> term list -> term
  90. val hide_tvar_ast_tr : Proof.context -> Ast.ast list -> Ast.ast
  91. val hide_tvar_subst_ast_tr : tvar_subst -> Proof.context -> Ast.ast list
  92. -> Ast.ast
  93. val hide_tvar_subst_return_ast_tr : tvar_subst -> Proof.context
  94. -> Ast.ast list -> Ast.ast
  95. end
  96. structure Hide_Tvar : HIDE_TVAR = struct
  97. datatype print_mode = print_all | print | noprint
  98. datatype tvar_subst = right | left
  99. datatype parse_mode = parse | noparse
  100. type hide_varT = {
  101. name: string,
  102. tvars: typ list,
  103. typ_syn_tab : (string * typ list*string) Symtab.table,
  104. print_mode: print_mode,
  105. parse_mode: parse_mode
  106. }
  107. type hide_tvar_tab = (hide_varT) Symtab.table
  108. fun hide_tvar_eq (a, a') = (#name a) = (#name a')
  109. fun merge_tvar_tab (tab,tab') = Symtab.merge hide_tvar_eq (tab,tab')
  110. structure Data = Generic_Data
  111. (
  112. type T = hide_tvar_tab
  113. val empty = Symtab.empty:hide_tvar_tab
  114. val extend = I
  115. fun merge(t1,t2) = merge_tvar_tab (t1, t2)
  116. );
  117. fun parse_print_mode "print_all" = print_all
  118. | parse_print_mode "print" = print
  119. | parse_print_mode "noprint" = noprint
  120. | parse_print_mode s = error("Print mode not supported: "^s)
  121. fun parse_parse_mode "parse" = parse
  122. | parse_parse_mode "noparse" = noparse
  123. | parse_parse_mode s = error("Parse mode not supported: "^s)
  124. fun update_mode typ_str print_mode parse_mode thy =
  125. let
  126. val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
  127. val typ = Syntax.parse_typ ctx typ_str (* no type checking *)
  128. val name = case typ of
  129. Type(name,_) => name
  130. | _ => error("Complex type not (yet) supported.")
  131. fun update tab =
  132. let
  133. val old_entry = (case Symtab.lookup tab name of
  134. SOME t => t
  135. | NONE => error ("Type shorthand not registered: "^name))
  136. val print_m = case print_mode of
  137. SOME m => m
  138. | NONE => #print_mode old_entry
  139. val parse_m = case parse_mode of
  140. SOME m => m
  141. | NONE => #parse_mode old_entry
  142. val entry = {
  143. name = name,
  144. tvars = #tvars old_entry,
  145. typ_syn_tab = #typ_syn_tab old_entry,
  146. print_mode = print_m,
  147. parse_mode = parse_m
  148. }
  149. in
  150. Symtab.update (name,entry) tab
  151. end
  152. in
  153. Context.theory_of ( (Data.map update) (Context.Theory thy))
  154. end
  155. fun lookup thy name =
  156. let
  157. val tab = (Data.get o Context.Theory) thy
  158. in
  159. Symtab.lookup tab name
  160. end
  161. fun obtain_normalized_vname lookup_table vname =
  162. case List.find (fn e => fst e = vname) lookup_table of
  163. SOME (_,idx) => (lookup_table, Int.toString idx)
  164. | NONE => let
  165. fun max_idx [] = 0
  166. | max_idx ((_,idx)::lt) = Int.max(idx,max_idx lt)
  167. val idx = (max_idx lookup_table ) + 1
  168. in
  169. ((vname,idx)::lookup_table, Int.toString idx) end
  170. fun normalize_typvar_type lt (Type (a, Ts)) =
  171. let
  172. fun switch (a,b) = (b,a)
  173. val (Ts', lt') = fold_map (fn t => fn lt => switch (normalize_typvar_type lt t)) Ts lt
  174. in
  175. (lt', Type (a, Ts'))
  176. end
  177. | normalize_typvar_type lt (TFree (vname, S)) =
  178. let
  179. val (lt, vname) = obtain_normalized_vname lt (vname)
  180. in
  181. (lt, TFree( vname, S))
  182. end
  183. | normalize_typvar_type lt (TVar (xi, S)) =
  184. let
  185. val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
  186. in
  187. (lt, TFree( vname, S))
  188. end
  189. fun normalize_typvar_type' t = snd ( normalize_typvar_type [] t)
  190. fun mk_p s = s (* "("^s^")" *)
  191. fun key_of_type (Type(a, TS)) = mk_p (a^String.concat(map key_of_type TS))
  192. | key_of_type (TFree (vname, _)) = mk_p vname
  193. | key_of_type (TVar (xi, _ )) = mk_p (Term.string_of_vname xi)
  194. val key_of_type' = key_of_type o normalize_typvar_type'
  195. fun normalize_typvar_term lt (Const (a, t)) = (lt, Const(a, t))
  196. | normalize_typvar_term lt (Free (a, t)) = let
  197. val (lt, vname) = obtain_normalized_vname lt a
  198. in
  199. (lt, Free(vname,t))
  200. end
  201. | normalize_typvar_term lt (Var (xi, t)) =
  202. let
  203. val (lt, vname) = obtain_normalized_vname lt (Term.string_of_vname xi)
  204. in
  205. (lt, Free(vname,t))
  206. end
  207. | normalize_typvar_term lt (Bound (i)) = (lt, Bound(i))
  208. | normalize_typvar_term lt (Abs(s,ty,tr)) =
  209. let
  210. val (lt,tr) = normalize_typvar_term lt tr
  211. in
  212. (lt, Abs(s,ty,tr))
  213. end
  214. | normalize_typvar_term lt (t1$t2) =
  215. let
  216. val (lt,t1) = normalize_typvar_term lt t1
  217. val (lt,t2) = normalize_typvar_term lt t2
  218. in
  219. (lt, t1$t2)
  220. end
  221. fun normalize_typvar_term' t = snd(normalize_typvar_term [] t)
  222. fun key_of_term (Const(s,_)) = if String.isPrefix "\<^type>" s
  223. then Lexicon.unmark_type s
  224. else ""
  225. | key_of_term (Free(s,_)) = s
  226. | key_of_term (Var(xi,_)) = Term.string_of_vname xi
  227. | key_of_term (Bound(_)) = error("Bound() not supported in key_of_term")
  228. | key_of_term (Abs(_,_,_)) = error("Abs() not supported in key_of_term")
  229. | key_of_term (t1$t2) = (key_of_term t1)^(key_of_term t2)
  230. val key_of_term' = key_of_term o normalize_typvar_term'
  231. fun hide_tvar_tr' tname ctx terms =
  232. let
  233. val mtyp = Syntax.parse_typ ctx tname (* no type checking *)
  234. val (fq_name, _) = case mtyp of
  235. Type(s,ts) => (s,ts)
  236. | _ => error("Complex type not (yet) supported.")
  237. val local_name_of = hd o rev o String.fields (fn c => c = #".")
  238. fun hide_type tname = Syntax.const("(_) "^tname)
  239. val reg_type_as_term = Term.list_comb(Const(Lexicon.mark_type tname,dummyT),terms)
  240. val key = key_of_term' reg_type_as_term
  241. val actual_tvars_key = key_of_term reg_type_as_term
  242. in
  243. case lookup (Proof_Context.theory_of ctx) fq_name of
  244. NONE => raise Match
  245. | SOME e => let
  246. val (tname,default_tvars_key) =
  247. case Symtab.lookup (#typ_syn_tab e) key of
  248. NONE => (local_name_of tname, "")
  249. | SOME (s,_,tv) => (local_name_of s,tv)
  250. in
  251. case (#print_mode e) of
  252. print_all => hide_type tname
  253. | print => if default_tvars_key=actual_tvars_key
  254. then hide_type tname
  255. else raise Match
  256. | noprint => raise Match
  257. end
  258. end
  259. fun hide_tvar_ast_tr ctx ast=
  260. let
  261. val thy = Proof_Context.theory_of ctx
  262. fun parse_ast ((Ast.Constant const)::[]) = (const,NONE)
  263. | parse_ast ((Ast.Constant sort)::(Ast.Constant const)::[])
  264. = (const,SOME sort)
  265. | parse_ast _ = error("AST type not supported.")
  266. val (decorated_name, decorated_sort) = parse_ast ast
  267. val name = Lexicon.unmark_type decorated_name
  268. val default_info = case lookup thy name of
  269. NONE => error("No default type vars registered: "^name)
  270. | SOME e => e
  271. val _ = if #parse_mode default_info = noparse
  272. then error("Default type vars disabled (option noparse): "^name)
  273. else ()
  274. fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n
  275. | _ => error("Unsupported type structure.")
  276. val type_vars_ast =
  277. let fun mk_tvar n =
  278. case decorated_sort of
  279. NONE => Ast.Variable(name_of_tvar n)
  280. | SOME sort => Ast.Appl([Ast.Constant("_ofsort"),
  281. Ast.Variable(name_of_tvar n),
  282. Ast.Constant(sort)])
  283. in
  284. map mk_tvar (#tvars default_info)
  285. end
  286. in
  287. Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
  288. end
  289. fun register typ_str print_mode parse_mode thy =
  290. let
  291. val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
  292. val typ = Syntax.parse_typ ctx typ_str
  293. val (name,tvars) = case typ of Type(name,tvars) => (name,tvars)
  294. | _ => error("Unsupported type structure.")
  295. val base_typ = Syntax.read_typ ctx typ_str
  296. val (base_name,base_tvars) = case base_typ of Type(name,tvars) => (name,tvars)
  297. | _ => error("Unsupported type structure.")
  298. val base_key = key_of_type' base_typ
  299. val base_tvar_key = key_of_type base_typ
  300. val print_m = case print_mode of
  301. SOME m => m
  302. | NONE => print_all
  303. val parse_m = case parse_mode of
  304. SOME m => m
  305. | NONE => parse
  306. val entry = {
  307. name = name,
  308. tvars = tvars,
  309. typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
  310. print_mode = print_m,
  311. parse_mode = parse_m
  312. }
  313. val base_entry = if name = base_name
  314. then
  315. {
  316. name = "",
  317. tvars = [],
  318. typ_syn_tab = Symtab.empty:((string * typ list * string) Symtab.table),
  319. print_mode = noprint,
  320. parse_mode = noparse
  321. }
  322. else case lookup thy base_name of
  323. SOME e => e
  324. | NONE => error ("No entry found for "^base_name^
  325. " (via "^name^")")
  326. val base_entry = {
  327. name = #name base_entry,
  328. tvars = #tvars base_entry,
  329. typ_syn_tab = Symtab.update (base_key, (name, base_tvars, base_tvar_key))
  330. (#typ_syn_tab (base_entry)),
  331. print_mode = #print_mode base_entry,
  332. parse_mode = #parse_mode base_entry
  333. }
  334. fun reg tab = let
  335. val tab = Symtab.update_new(name, entry) tab
  336. val tab = if name = base_name
  337. then tab
  338. else Symtab.update(base_name, base_entry) tab
  339. in
  340. tab
  341. end
  342. val thy = Sign.print_translation
  343. [(Lexicon.mark_type name, hide_tvar_tr' name)] thy
  344. in
  345. Context.theory_of ( (Data.map reg) (Context.Theory thy))
  346. handle Symtab.DUP _ => error("Type shorthand already registered: "^name)
  347. end
  348. fun hide_tvar_subst_ast_tr hole ctx (ast::[]) =
  349. let
  350. val thy = Proof_Context.theory_of ctx
  351. val (decorated_name, args) = case ast
  352. of (Ast.Appl ((Ast.Constant s)::args)) => (s, args)
  353. | _ => error "Error in obtaining type constructor."
  354. val name = Lexicon.unmark_type decorated_name
  355. val default_info = case lookup thy name of
  356. NONE => error("No default type vars registered: "^name)
  357. | SOME e => e
  358. val _ = if #parse_mode default_info = noparse
  359. then error("Default type vars disabled (option noparse): "^name)
  360. else ()
  361. fun name_of_tvar tvar = case tvar of (TFree(n,_)) => n
  362. | _ => error("Unsupported type structure.")
  363. val type_vars_ast = map (fn n => Ast.Variable(name_of_tvar n)) (#tvars default_info)
  364. val type_vars_ast = case hole of
  365. right => (List.rev(List.drop(List.rev type_vars_ast, List.length args)))@args
  366. | left => args@List.drop(type_vars_ast, List.length args)
  367. in
  368. Ast.Appl ((Ast.Constant decorated_name)::type_vars_ast)
  369. end
  370. | hide_tvar_subst_ast_tr _ _ _ = error("hide_tvar_subst_ast_tr: empty AST.")
  371. fun hide_tvar_subst_return_ast_tr hole ctx (retval::constructor::[]) =
  372. hide_tvar_subst_ast_tr hole ctx [Ast.Appl (constructor::retval::[])]
  373. | hide_tvar_subst_return_ast_tr _ _ _ =
  374. error("hide_tvar_subst_return_ast_tr: error in parsing AST")
  375. end
  376. \<close>
  377. subsection\<open>Register Parse Translations\<close>
  378. syntax "_tvars_wildcard" :: "type \<Rightarrow> type" ("'('_') _")
  379. syntax "_tvars_wildcard_retval" :: "type \<Rightarrow> type \<Rightarrow> type" ("'('_, _') _")
  380. syntax "_tvars_wildcard_sort" :: "sort \<Rightarrow> type \<Rightarrow> type" ("'('_::_') _")
  381. syntax "_tvars_wildcard_right" :: "type \<Rightarrow> type" ("_ '_..")
  382. syntax "_tvars_wildcard_left" :: "type \<Rightarrow> type" ("_ ..'_")
  383. parse_ast_translation\<open>
  384. [
  385. (@{syntax_const "_tvars_wildcard_sort"}, Hide_Tvar.hide_tvar_ast_tr),
  386. (@{syntax_const "_tvars_wildcard"}, Hide_Tvar.hide_tvar_ast_tr),
  387. (@{syntax_const "_tvars_wildcard_retval"}, Hide_Tvar.hide_tvar_subst_return_ast_tr Hide_Tvar.right),
  388. (@{syntax_const "_tvars_wildcard_right"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.right),
  389. (@{syntax_const "_tvars_wildcard_left"}, Hide_Tvar.hide_tvar_subst_ast_tr Hide_Tvar.left)
  390. ]
  391. \<close>
  392. subsection\<open>Register Top-Level Isar Commands\<close>
  393. ML\<open>
  394. val modeP = (Parse.$$$ "("
  395. |-- (Parse.name --| Parse.$$$ ","
  396. -- Parse.name --|
  397. Parse.$$$ ")"))
  398. val typ_modeP = Parse.typ -- (Scan.optional modeP ("print_all","parse"))
  399. val _ = Outer_Syntax.command @{command_keyword "register_default_tvars"}
  400. "Register default variables (and hiding mechanims) for a type."
  401. (typ_modeP >> (fn (typ,(print_m,parse_m)) =>
  402. (Toplevel.theory
  403. (Hide_Tvar.register typ
  404. (SOME (Hide_Tvar.parse_print_mode print_m))
  405. (SOME (Hide_Tvar.parse_parse_mode parse_m))))));
  406. val _ = Outer_Syntax.command @{command_keyword "update_default_tvars_mode"}
  407. "Update print and/or parse mode or the default type variables for a certain type."
  408. (typ_modeP >> (fn (typ,(print_m,parse_m)) =>
  409. (Toplevel.theory
  410. (Hide_Tvar.update_mode typ
  411. (SOME (Hide_Tvar.parse_print_mode print_m))
  412. (SOME (Hide_Tvar.parse_parse_mode parse_m))))));
  413. \<close>
  414. section\<open>Examples\<close>
  415. subsection\<open>Print Translation\<close>
  416. datatype ('a, 'b) hide_tvar_foobar = hide_tvar_foo 'a | hide_tvar_bar 'b
  417. type_synonym ('a, 'b, 'c, 'd) hide_tvar_baz = "('a+'b, 'a \<times> 'b) hide_tvar_foobar"
  418. definition hide_tvar_f::"('a, 'b) hide_tvar_foobar \<Rightarrow> ('a, 'b) hide_tvar_foobar \<Rightarrow> ('a, 'b) hide_tvar_foobar"
  419. where "hide_tvar_f a b = a"
  420. definition hide_tvar_g::"('a, 'b, 'c, 'd) hide_tvar_baz \<Rightarrow> ('a, 'b, 'c, 'd) hide_tvar_baz \<Rightarrow> ('a, 'b, 'c, 'd) hide_tvar_baz"
  421. where "hide_tvar_g a b = a"
  422. assert[string_of_thm_equal,
  423. thm_def="hide_tvar_f_def",
  424. str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
  425. assert[string_of_thm_equal,
  426. thm_def="hide_tvar_g_def",
  427. str="hide_tvar_g (a::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) (b::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) = a"]
  428. register_default_tvars "('alpha, 'beta) hide_tvar_foobar" (print_all,parse)
  429. register_default_tvars "('alpha, 'beta, 'gamma, 'delta) hide_tvar_baz" (print_all,parse)
  430. update_default_tvars_mode "_ hide_tvar_foobar" (noprint,noparse)
  431. assert[string_of_thm_equal,
  432. thm_def="hide_tvar_f_def",
  433. str="hide_tvar_f (a::('a, 'b) hide_tvar_foobar) (b::('a, 'b) hide_tvar_foobar) = a"]
  434. assert[string_of_thm_equal,
  435. thm_def="hide_tvar_g_def",
  436. str="hide_tvar_g (a::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) (b::('a + 'b, 'a \<times> 'b) hide_tvar_foobar) = a"]
  437. update_default_tvars_mode "_ hide_tvar_foobar" (print_all,noparse)
  438. assert[string_of_thm_equal,
  439. thm_def="hide_tvar_f_def", str="hide_tvar_f (a::(_) hide_tvar_foobar) (b::(_) hide_tvar_foobar) = a"]
  440. assert[string_of_thm_equal,
  441. thm_def="hide_tvar_g_def", str="hide_tvar_g (a::(_) hide_tvar_baz) (b::(_) hide_tvar_baz) = a"]
  442. subsection\<open>Parse Translation\<close>
  443. update_default_tvars_mode "_ hide_tvar_foobar" (print_all,parse)
  444. declare [[show_types]]
  445. definition hide_tvar_A :: "'x \<Rightarrow> (('x::linorder) hide_tvar_foobar) .._"
  446. where "hide_tvar_A x = hide_tvar_foo x"
  447. assert[string_of_thm_equal,
  448. thm_def="hide_tvar_A_def", str="hide_tvar_A (x::'x) = hide_tvar_foo x"]
  449. definition hide_tvar_A' :: "'x \<Rightarrow> (('x,'b) hide_tvar_foobar) .._"
  450. where "hide_tvar_A' x = hide_tvar_foo x"
  451. assert[string_of_thm_equal,
  452. thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]
  453. definition hide_tvar_B' :: "(_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar"
  454. where "hide_tvar_B' x y = x"
  455. assert[string_of_thm_equal,
  456. thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = hide_tvar_foo x"]
  457. definition hide_tvar_B :: "(_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_foobar"
  458. where "hide_tvar_B x y = x"
  459. assert[string_of_thm_equal,
  460. thm_def="hide_tvar_B_def", str="hide_tvar_B (x::(_) hide_tvar_foobar) (y::(_) hide_tvar_foobar) = x"]
  461. definition hide_tvar_C :: "(_) hide_tvar_baz \<Rightarrow> (_) hide_tvar_foobar \<Rightarrow> (_) hide_tvar_baz"
  462. where "hide_tvar_C x y = x"
  463. assert[string_of_thm_equal,
  464. thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]
  465. definition hide_tvar_E :: "(_::linorder) hide_tvar_baz \<Rightarrow> (_::linorder) hide_tvar_foobar \<Rightarrow> (_::linorder) hide_tvar_baz"
  466. where "hide_tvar_E x y = x"
  467. assert[string_of_thm_equal,
  468. thm_def="hide_tvar_C_def", str="hide_tvar_C (x::(_) hide_tvar_baz) (y::(_) hide_tvar_foobar) = x"]
  469. definition hide_tvar_X :: "(_, 'retval::linorder) hide_tvar_baz
  470. \<Rightarrow> (_,'retval) hide_tvar_foobar
  471. \<Rightarrow> (_,'retval) hide_tvar_baz"
  472. where "hide_tvar_X x y = x"
  473. end