minor cleanup
authorkrauss
Mon Nov 06 12:04:44 2006 +0100 (2006-11-06)
changeset 211882aa15b663cd4
parent 21187 16fb5afbf228
child 21189 5435ccdb4ea1
minor cleanup
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_prep.ML
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Sun Nov 05 21:44:42 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Nov 06 12:04:44 2006 +0100
     1.3 @@ -55,8 +55,11 @@
     1.4  (*** Dependency analysis for congruence rules ***)
     1.5  
     1.6  fun branch_vars t = 
     1.7 -    let	val (assumes, term) = dest_implies_list (snd (dest_all_all t))
     1.8 -    in (fold (curry add_term_vars) assumes [], term_vars term)
     1.9 +    let	
    1.10 +      val t' = snd (dest_all_all t)
    1.11 +      val assumes = Logic.strip_imp_prems t'
    1.12 +      val concl = Logic.strip_imp_concl t'
    1.13 +    in (fold (curry add_term_vars) assumes [], term_vars concl)
    1.14      end
    1.15  
    1.16  fun cong_deps crule =
    1.17 @@ -78,9 +81,8 @@
    1.18  fun mk_branch ctx t = 
    1.19      let
    1.20  	val (ctx', fixes, impl) = dest_all_all_ctx ctx t
    1.21 -	val (assumes, term) = dest_implies_list impl
    1.22      in
    1.23 -      (ctx', fixes, assumes, rhs_of term)
    1.24 +      (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
    1.25      end
    1.26  
    1.27  fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
     2.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Sun Nov 05 21:44:42 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 06 12:04:44 2006 +0100
     2.3 @@ -12,29 +12,26 @@
     2.4  
     2.5  fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
     2.6  
     2.7 -fun mk_forall (var as Free (v,T)) t =
     2.8 -    all T $ Abs (v,T, abstract_over (var,t))
     2.9 -  | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
    2.10 -
    2.11 +fun mk_forall v t = all (fastype_of v) $ lambda v t
    2.12  
    2.13  (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
    2.14  fun tupled_lambda vars t =
    2.15      case vars of
    2.16 -	(Free v) => lambda (Free v) t
    2.17 -      | (Var v) => lambda (Var v) t
    2.18 -      | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
    2.19 -	(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    2.20 -      | _ => raise Match
    2.21 -
    2.22 -
    2.23 +	    (Free v) => lambda (Free v) t
    2.24 +    | (Var v) => lambda (Var v) t
    2.25 +    | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
    2.26 +	    (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    2.27 +    | _ => raise Match
    2.28 +                 
    2.29 +                 
    2.30  fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
    2.31      let
    2.32 -	val (n, body) = Term.dest_abs a
    2.33 +	    val (n, body) = Term.dest_abs a
    2.34      in
    2.35 -	(Free (n, T), body)
    2.36 +	    (Free (n, T), body)
    2.37      end
    2.38    | dest_all _ = raise Match
    2.39 -
    2.40 +                         
    2.41  
    2.42  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    2.43  fun dest_all_all (t as (Const ("all",_) $ _)) = 
    2.44 @@ -63,13 +60,6 @@
    2.45      (ctx, [], t)
    2.46  
    2.47  
    2.48 -
    2.49 -(* unfold *)
    2.50 -fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
    2.51 -
    2.52 -val dest_implies_list = 
    2.53 -    split_last o (unfold (can Logic.dest_implies) (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
    2.54 -
    2.55  fun implies_elim_swp a b = implies_elim b a
    2.56  
    2.57  fun map3 _ [] [] [] = []
     3.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Sun Nov 05 21:44:42 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 06 12:04:44 2006 +0100
     3.3 @@ -48,33 +48,31 @@
     3.4      end
     3.5  
     3.6  
     3.7 -
     3.8 -(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
     3.9 -(* Takes bound form of qglrs tuples *)
    3.10 -fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
    3.11 +fun mk_compat_proof_obligations domT ranT fvar f glrs =
    3.12      let
    3.13 -      val shift = incr_boundvars (length qs')
    3.14 +      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
    3.15 +          let
    3.16 +            val shift = incr_boundvars (length qs')
    3.17 +          in
    3.18 +            (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
    3.19 +                     $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
    3.20 +              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
    3.21 +              |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
    3.22 +              |> curry abstract_over fvar
    3.23 +              |> curry subst_bound f
    3.24 +          end
    3.25      in
    3.26 -      (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
    3.27 -               $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
    3.28 -        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
    3.29 -        |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
    3.30 -        |> curry abstract_over fvar
    3.31 -        |> curry subst_bound f
    3.32 +      map mk_impl (unordered_pairs glrs)
    3.33      end
    3.34  
    3.35 -fun mk_compat_proof_obligations domT ranT fvar f glrs =
    3.36 -    map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs)
    3.37  
    3.38 -
    3.39 -fun mk_completeness globals clauses qglrs =
    3.40 +fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
    3.41      let
    3.42 -        val Globals {x, Pbool, ...} = globals
    3.43 -
    3.44 -        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool
    3.45 -                                                |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
    3.46 -                                                |> fold_rev (curry Logic.mk_implies) gs
    3.47 -                                                |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
    3.48 +        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
    3.49 +            Trueprop Pbool
    3.50 +                     |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
    3.51 +                     |> fold_rev (curry Logic.mk_implies) gs
    3.52 +                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
    3.53      in
    3.54          Trueprop Pbool
    3.55                   |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
    3.56 @@ -244,15 +242,6 @@
    3.57      end
    3.58  
    3.59  
    3.60 -
    3.61 -
    3.62 -fun pr (s:string) x =
    3.63 -    let val _ = print s
    3.64 -    in
    3.65 -      x
    3.66 -    end
    3.67 -
    3.68 -
    3.69  fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
    3.70      let
    3.71          val Globals {h, y, x, fvar, ...} = globals