src/HOL/HOLCF/Tools/fixrec.ML
changeset 44080 53d95b52954c
parent 43324 2b47822868e4
child 45592 8baa0b7f3f66
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 16:57:37 2011 -0700
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Aug 08 18:36:32 2011 -0700
     1.3 @@ -28,8 +28,6 @@
     1.4  val def_cont_fix_ind = @{thm def_cont_fix_ind}
     1.5  
     1.6  fun fixrec_err s = error ("fixrec definition error:\n" ^ s)
     1.7 -fun fixrec_eq_err thy s eq =
     1.8 -  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq))
     1.9  
    1.10  (*************************************************************************)
    1.11  (***************************** building types ****************************)
    1.12 @@ -41,13 +39,10 @@
    1.13    | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
    1.14    | binder_cfun _   =  []
    1.15  
    1.16 -fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
    1.17 -  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
    1.18 +fun body_cfun (Type(@{type_name cfun},[_, U])) = body_cfun U
    1.19 +  | body_cfun (Type(@{type_name "fun"},[_, U])) = body_cfun U
    1.20    | body_cfun T   =  T
    1.21  
    1.22 -fun strip_cfun T : typ list * typ =
    1.23 -  (binder_cfun T, body_cfun T)
    1.24 -
    1.25  in
    1.26  
    1.27  fun matcherT (T, U) =
    1.28 @@ -65,10 +60,9 @@
    1.29  fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
    1.30  
    1.31  (* similar to Thm.head_of, but for continuous application *)
    1.32 -fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
    1.33 +fun chead_of (Const(@{const_name Rep_cfun},_)$f$_) = chead_of f
    1.34    | chead_of u = u
    1.35  
    1.36 -infix 0 ==  val (op ==) = Logic.mk_equals
    1.37  infix 1 === val (op ===) = HOLogic.mk_eq
    1.38  
    1.39  fun mk_mplus (t, u) =
    1.40 @@ -102,8 +96,8 @@
    1.41  
    1.42  local
    1.43  
    1.44 -fun name_of (Const (n, T)) = n
    1.45 -  | name_of (Free (n, T)) = n
    1.46 +fun name_of (Const (n, _)) = n
    1.47 +  | name_of (Free (n, _)) = n
    1.48    | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t])
    1.49  
    1.50  val lhs_name =
    1.51 @@ -145,7 +139,7 @@
    1.52          Goal.prove lthy [] [] prop (K tac)
    1.53        end
    1.54  
    1.55 -    fun one_def (l as Free(n,_)) r =
    1.56 +    fun one_def (Free(n,_)) r =
    1.57            let val b = Long_Name.base_name n
    1.58            in ((Binding.name (b^"_def"), []), r) end
    1.59        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
    1.60 @@ -164,7 +158,7 @@
    1.61        |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
    1.62      val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
    1.63        |> Local_Defs.unfold lthy @{thms split_conv}
    1.64 -    fun unfolds [] thm = []
    1.65 +    fun unfolds [] _ = []
    1.66        | unfolds (n::[]) thm = [(n, thm)]
    1.67        | unfolds (n::ns) thm = let
    1.68            val thmL = thm RS @{thm Pair_eqD1}
    1.69 @@ -184,7 +178,7 @@
    1.70        in
    1.71          ((thm_name, [src]), [thm])
    1.72        end
    1.73 -    val (thmss, lthy) = lthy
    1.74 +    val (_, lthy) = lthy
    1.75        |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms)
    1.76    in
    1.77      (lthy, names, fixdef_thms, map snd unfold_thms)
    1.78 @@ -303,7 +297,7 @@
    1.79        else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
    1.80      fun tac (t, i) =
    1.81        let
    1.82 -        val (c, T) =
    1.83 +        val (c, _) =
    1.84              (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
    1.85          val unfold_thm = the (Symtab.lookup tab c)
    1.86          val rule = unfold_thm RS @{thm ssubst_lhs}
    1.87 @@ -346,7 +340,7 @@
    1.88      val chead_of_spec =
    1.89        chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
    1.90      fun name_of (Free (n, _)) = n
    1.91 -      | name_of t = fixrec_err ("unknown term")
    1.92 +      | name_of _ = fixrec_err ("unknown term")
    1.93      val all_names = map (name_of o chead_of_spec) spec
    1.94      val names = distinct (op =) all_names
    1.95      fun block_of_name n =
    1.96 @@ -362,7 +356,7 @@
    1.97  
    1.98      val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
    1.99      val spec' = map (pair Attrib.empty_binding) matches
   1.100 -    val (lthy, cnames, fixdef_thms, unfold_thms) =
   1.101 +    val (lthy, _, _, unfold_thms) =
   1.102        add_fixdefs fixes spec' lthy
   1.103  
   1.104      val blocks' = map (map fst o filter_out snd) blocks