1(* Title: HOL/HOLCF/Tools/Domain/domain_axioms.ML 2 Author: David von Oheimb 3 Author: Brian Huffman 4 5Syntax generator for domain command. 6*) 7 8signature DOMAIN_AXIOMS = 9sig 10 val axiomatize_isomorphism : 11 binding * (typ * typ) -> 12 theory -> Domain_Take_Proofs.iso_info * theory 13 14 val axiomatize_lub_take : 15 binding * term -> theory -> thm * theory 16 17 val add_axioms : 18 (binding * mixfix * (typ * typ)) list -> theory -> 19 (Domain_Take_Proofs.iso_info list 20 * Domain_Take_Proofs.take_induct_info) * theory 21end 22 23 24structure Domain_Axioms : DOMAIN_AXIOMS = 25struct 26 27open HOLCF_Library 28 29infixr 6 ->> 30infix -->> 31infix 9 ` 32 33fun axiomatize_isomorphism 34 (dbind : binding, (lhsT, rhsT)) 35 (thy : theory) 36 : Domain_Take_Proofs.iso_info * theory = 37 let 38 val abs_bind = Binding.suffix_name "_abs" dbind 39 val rep_bind = Binding.suffix_name "_rep" dbind 40 41 val (abs_const, thy) = 42 Sign.declare_const_global ((abs_bind, rhsT ->> lhsT), NoSyn) thy 43 val (rep_const, thy) = 44 Sign.declare_const_global ((rep_bind, lhsT ->> rhsT), NoSyn) thy 45 46 val x = Free ("x", lhsT) 47 val y = Free ("y", rhsT) 48 49 val abs_iso_eqn = 50 Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y))) 51 val rep_iso_eqn = 52 Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x))) 53 54 val abs_iso_bind = Binding.qualify_name true dbind "abs_iso" 55 val rep_iso_bind = Binding.qualify_name true dbind "rep_iso" 56 57 val (abs_iso_thm, thy) = Specification.axiom ((abs_iso_bind, []), abs_iso_eqn) thy 58 val (rep_iso_thm, thy) = Specification.axiom ((rep_iso_bind, []), rep_iso_eqn) thy 59 60 val result = 61 { 62 absT = lhsT, 63 repT = rhsT, 64 abs_const = abs_const, 65 rep_const = rep_const, 66 abs_inverse = Drule.export_without_context abs_iso_thm, 67 rep_inverse = Drule.export_without_context rep_iso_thm 68 } 69 in 70 (result, thy) 71 end 72 73fun axiomatize_lub_take 74 (dbind : binding, take_const : term) 75 (thy : theory) 76 : thm * theory = 77 let 78 val i = Free ("i", natT) 79 val T = (fst o dest_cfunT o range_type o fastype_of) take_const 80 81 val lub_take_eqn = 82 mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) 83 84 val lub_take_bind = Binding.qualify_name true dbind "lub_take" 85 86 val (lub_take_thm, thy) = Specification.axiom ((lub_take_bind, []), lub_take_eqn) thy 87 in 88 (lub_take_thm, thy) 89 end 90 91fun add_axioms 92 (dom_eqns : (binding * mixfix * (typ * typ)) list) 93 (thy : theory) = 94 let 95 96 val dbinds = map #1 dom_eqns 97 98 (* declare new types *) 99 fun thy_type (dbind, mx, (lhsT, _)) = 100 (dbind, (length o snd o dest_Type) lhsT, mx) 101 val thy = Sign.add_types_global (map thy_type dom_eqns) thy 102 103 (* axiomatize type constructor arities *) 104 fun thy_arity (_, _, (lhsT, _)) = 105 let val (dname, tvars) = dest_Type lhsT 106 in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end 107 val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy 108 109 (* declare and axiomatize abs/rep *) 110 val (iso_infos, thy) = 111 fold_map axiomatize_isomorphism 112 (map (fn (dbind, _, eqn) => (dbind, eqn)) dom_eqns) thy 113 114 (* define take functions *) 115 val (take_info, thy) = 116 Domain_Take_Proofs.define_take_functions 117 (dbinds ~~ iso_infos) thy 118 119 (* declare lub_take axioms *) 120 val (lub_take_thms, thy) = 121 fold_map axiomatize_lub_take 122 (dbinds ~~ #take_consts take_info) thy 123 124 (* prove additional take theorems *) 125 val (take_info2, thy) = 126 Domain_Take_Proofs.add_lub_take_theorems 127 (dbinds ~~ iso_infos) take_info lub_take_thms thy 128 129 (* define map functions *) 130 val (_, thy) = 131 Domain_Isomorphism.define_map_functions 132 (dbinds ~~ iso_infos) thy 133 134 in 135 ((iso_infos, take_info2), thy) 136 end 137 138end (* struct *) 139