src/HOL/Tools/Function/termination.ML
changeset 32602 f2b741473860
parent 32149 ef59550a55d3
child 32683 7c1fe854ca6a
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Sep 18 09:07:48 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Sep 18 09:07:49 2009 +0200
     1.3 @@ -79,14 +79,14 @@
     1.4  
     1.5  
     1.6  (* concrete versions for sum types *)
     1.7 -fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
     1.8 -  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
     1.9 +fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
    1.10 +  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
    1.11    | is_inj _ = false
    1.12  
    1.13 -fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
    1.14 +fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
    1.15    | dest_inl _ = NONE
    1.16  
    1.17 -fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
    1.18 +fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
    1.19    | dest_inr _ = NONE
    1.20  
    1.21  
    1.22 @@ -145,8 +145,8 @@
    1.23  
    1.24  fun mk_sum_skel rel =
    1.25    let
    1.26 -    val cs = FundefLib.dest_binop_list @{const_name union} rel
    1.27 -    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
    1.28 +    val cs = FundefLib.dest_binop_list @{const_name Set.union} rel
    1.29 +    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    1.30        let
    1.31          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
    1.32            = Term.strip_qnt_body "Ex" c
    1.33 @@ -179,7 +179,7 @@
    1.34  fun get_descent (_, _, _, _, D) c m1 m2 =
    1.35    Term3tab.lookup D (c, (m1, m2))
    1.36  
    1.37 -fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
    1.38 +fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    1.39    let
    1.40      val n = get_num_points D
    1.41      val (sk, _, _, _, _) = D
    1.42 @@ -233,13 +233,13 @@
    1.43  fun CALLS tac i st =
    1.44    if Thm.no_prems st then all_tac st
    1.45    else case Thm.term_of (Thm.cprem_of st i) of
    1.46 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
    1.47 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Set.union} rel, i) st
    1.48    |_ => no_tac st
    1.49  
    1.50  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
    1.51  
    1.52  fun TERMINATION ctxt tac =
    1.53 -  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
    1.54 +  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
    1.55    let
    1.56      val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
    1.57    in
    1.58 @@ -293,7 +293,7 @@
    1.59            if null ineqs then
    1.60                Const (@{const_name Set.empty}, fastype_of rel)
    1.61            else
    1.62 -              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
    1.63 +              foldr1 (HOLogic.mk_binop @{const_name Set.union}) (map mk_compr ineqs)
    1.64  
    1.65        fun solve_membership_tac i =
    1.66            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)