# HG changeset patch # User Cezary Kaliszyk # Date 1265727358 -3600 # Node ID 5eb84b817855c420060ccd95835af3813bb3e4ab # Parent 2fb07e01c57b1f0648cab3331ee2741b3aebbc81 More indentation cleaning. diff -r 2fb07e01c57b -r 5eb84b817855 Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Tue Feb 09 15:43:39 2010 +0100 +++ b/Quot/quotient_typ.ML Tue Feb 09 15:55:58 2010 +0100 @@ -55,9 +55,10 @@ (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) fun typedef_term rel rty lthy = let - val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] - |> Variable.variant_frees lthy [rel] - |> map Free + val [x, c] = + [("x", rty), ("c", HOLogic.mk_setT rty)] + |> Variable.variant_frees lthy [rel] + |> map Free in lambda c (HOLogic.exists_const rty $ lambda x (HOLogic.mk_eq (c, (rel $ x)))) @@ -86,12 +87,12 @@ val abs_inv = mem_def2 RS #Abs_inverse typedef_info val rep_inj = #Rep_inject typedef_info in - (rtac @{thm Quot_Type.intro} THEN' - RANGE [rtac equiv_thm, - rtac rep_thm, - rtac rep_inv, - EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), - rtac rep_inj]) 1 + (rtac @{thm Quot_Type.intro} THEN' RANGE [ + rtac equiv_thm, + rtac rep_thm, + rtac rep_inv, + EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), + rtac rep_inj]) 1 end @@ -99,8 +100,9 @@ fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) - val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) - |> Syntax.check_term lthy + val goal = + HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) + |> Syntax.check_term lthy in Goal.prove lthy [] [] goal (K (typedef_quot_type_tac equiv_thm typedef_info)) @@ -110,13 +112,15 @@ fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = let val quotient_const = Const (@{const_name "Quotient"}, dummyT) - val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) - |> Syntax.check_term lthy + val goal = + HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) + |> Syntax.check_term lthy val typedef_quotient_thm_tac = - EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), - rtac @{thm Quot_Type.Quotient}, - rtac quot_type_thm] + EVERY1 [ + K (rewrite_goals_tac [abs_def, rep_def]), + rtac @{thm Quot_Type.Quotient}, + rtac quot_type_thm] in Goal.prove lthy [] [] goal (K typedef_quotient_thm_tac) @@ -161,10 +165,10 @@ (* storing the quot-info *) (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) fun qinfo phi = transform_quotdata phi - {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, - equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} + {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, + equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} val lthy4 = Local_Theory.declaration true - (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 + (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 in lthy4 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) @@ -224,9 +228,9 @@ val warns = map_check_aux rty [] in - if null warns then () + if null warns then () else warning ("No map function defined for " ^ commas warns ^ - ". This will cause problems later on.") + ". This will cause problems later on.") end