# HG changeset patch # User Christian Urban # Date 1263509311 -3600 # Node ID fe7d27e197e5fdb78a1d3d3abd3e8b0c5e72531c # Parent e49c6b6f37f4c45a27f087824f24cd770c5151f9 tuned quotient_typ.ML diff -r e49c6b6f37f4 -r fe7d27e197e5 Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Thu Jan 14 23:17:21 2010 +0100 +++ b/Quot/quotient_typ.ML Thu Jan 14 23:48:31 2010 +0100 @@ -74,9 +74,9 @@ (* tactic to prove the Quot_Type theorem for the new type *) fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let - val rep_thm = (#Rep typedef_info) RS mem_def1 + val rep_thm = #Rep typedef_info RS mem_def1 val rep_inv = #Rep_inverse typedef_info - val abs_inv = mem_def2 RS (#Abs_inverse typedef_info) + val abs_inv = mem_def2 RS #Abs_inverse typedef_info val rep_inj = #Rep_inject typedef_info in (rtac @{thm Quot_Type.intro} THEN' @@ -88,7 +88,7 @@ end -(* proves the Quot_Type theorem *) +(* proves the Quot_Type theorem for the new type *) fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) @@ -99,7 +99,7 @@ (K (typedef_quot_type_tac equiv_thm typedef_info)) end -(* proves the quotient theorem *) +(* proves the quotient theorem for the new type *) fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = let val quotient_const = Const (@{const_name "Quotient"}, dummyT) @@ -117,7 +117,7 @@ (* main function for constructing a quotient type *) -fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = +fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = let (* generates the typedef *) val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy @@ -141,7 +141,7 @@ val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 - (* quot_type theorem - needed below *) + (* quot_type theorem *) val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 (* quotient theorem *) @@ -173,7 +173,7 @@ val rel_frees = map fst (Term.add_frees rel []) val rel_vars = Term.add_vars rel [] val rel_tvars = Term.add_tvars rel [] - val qty_str = (Binding.str_of qty_name) ^ ": " + val qty_str = Binding.str_of qty_name ^ ": " val illegal_rel_vars = if null rel_vars andalso null rel_tvars then [] @@ -212,7 +212,7 @@ fun map_check_aux rty warns = case rty of Type (_, []) => warns - | Type (s, _) => if (maps_defined thy s) then warns else s::warns + | Type (s, _) => if maps_defined thy s then warns else s::warns | _ => warns val warns = map_check_aux rty [] @@ -255,7 +255,7 @@ val goals = map (mk_goal o snd) quot_list fun after_qed thms lthy = - fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd + fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd in theorem after_qed goals lthy end