1(* Title: HOL/Types_To_Sets/unoverload_def.ML 2 Author: Fabian Immler, CMU 3 4Define unoverloaded constants from overloaded definitions. 5*) 6 7structure Unoverload_Def = struct 8 9fun unoverload_def name_opt thm thy = 10 let 11 val ctxt = Proof_Context.init_global thy 12 val thm_abs = Local_Defs.abs_def_rule ctxt thm 13 |> Conv.fconv_rule (Conv.top_conv 14 (K (Conv.try_conv (Conv.rewrs_conv 15 (Named_Theorems.get ctxt @{named_theorems unoverload_def})))) ctxt) 16 val (lhs, rhs) = thm_abs 17 |> Thm.cprop_of 18 |> Thm.dest_equals 19 val c = lhs |> Thm.term_of |> Term.dest_Const 20 val binding_with = 21 case name_opt of NONE => 22 Binding.qualify_name true 23 (Binding.name (Binding.name_of (Binding.qualified_name (#1 c)))) 24 "with" 25 | SOME name => name 26 27 val tvars = Term.add_tvars (Thm.term_of rhs) [] |> map fst 28 29 val thm_with = Thm.reflexive rhs 30 |> Unoverload_Type.unoverload_type (Context.Proof ctxt) (tvars) 31 32 val rhs_with' = thm_with |> Thm.cconcl_of |> Thm.dest_equals |> #2 |> Thm.term_of 33 val vars = Term.add_vars rhs_with' [] 34 val rhs_abs = fold (Var #> Term.lambda) vars rhs_with' 35 36 val ([rhs_abs'], ctxt') = Variable.importT_terms [rhs_abs] ctxt 37 val (with_const, thy') = Sign.declare_const_global 38 ((binding_with, Term.fastype_of rhs_abs'), NoSyn) 39 thy 40 val ([with_def], thy'') = Global_Theory.add_defs false 41 [((Binding.suffix_name "_def" binding_with, 42 Logic.mk_equals (with_const, rhs_abs')), [])] thy' 43 44 val with_var_def = 45 fold_rev 46 (fn (x, _) => fn thm => 47 let 48 val ty = Thm.concl_of thm |> Logic.dest_equals |> #2 |> 49 fastype_of |> dest_funT |> #1 50 in 51 Thm.combination thm 52 (Thm.reflexive (Thm.var (x, Thm.ctyp_of (Proof_Context.init_global thy'') ty))) 53 end) 54 (vars) 55 (with_def) 56 57 val thm_with = ([thm_abs, Thm.symmetric with_var_def] MRS @{thm Pure.transitive}) 58 val thy''' = 59 Global_Theory.add_thm 60 ((binding_with, thm_with), [Named_Theorems.add @{named_theorems "unoverload_def"}]) thy'' 61 |> #2 62 in thy''' end 63 64fun unoverload_def1_cmd (name_opt, facts) thy = 65 let 66 val [thm] = Attrib.eval_thms (Proof_Context.init_global thy) [facts] 67 in unoverload_def name_opt thm thy end 68 69val _ = 70 Outer_Syntax.local_theory \<^command_keyword>\<open>unoverload_definition\<close> 71 "definition of unoverloaded constants" 72 (Parse.and_list (Scan.option (Parse.binding --| \<^keyword>\<open>:\<close>) -- Parse.thm) >> 73 (fn things => Local_Theory.raw_theory (fold unoverload_def1_cmd things)) 74 ) 75 76end