src/HOL/Tools/Function/pat_completeness.ML
changeset 36945 9bec62c10714
parent 33099 b8cdd3d73022
child 37744 3daaf23b9ab4
     1.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
     1.5  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
     1.6  
     1.7 -fun inst_free var inst = forall_elim inst o forall_intr var
     1.8 +fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
     1.9  
    1.10  fun inst_case_thm thy x P thm =
    1.11    let val [Pv, xv] = Term.add_vars (prop_of thm) []
    1.12 @@ -69,10 +69,10 @@
    1.13    let
    1.14      val (_, subps) = strip_comb pat
    1.15      val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
    1.16 -    val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
    1.17 +    val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum
    1.18    in
    1.19      (subps @ pats,
    1.20 -     fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
    1.21 +     fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
    1.22    end
    1.23  
    1.24  
    1.25 @@ -82,12 +82,12 @@
    1.26    let
    1.27      val (avars, pvars, newidx) = invent_vars cons idx
    1.28      val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
    1.29 -    val c_assum = assume c_hyp
    1.30 +    val c_assum = Thm.assume c_hyp
    1.31      val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
    1.32    in
    1.33      o_alg thy P newidx (avars @ vs) newpats
    1.34 -    |> implies_intr c_hyp
    1.35 -    |> fold_rev (forall_intr o cterm_of thy) avars
    1.36 +    |> Thm.implies_intr c_hyp
    1.37 +    |> fold_rev (Thm.forall_intr o cterm_of thy) avars
    1.38    end
    1.39    | constr_case _ _ _ _ _ _ = raise Match
    1.40  and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
    1.41 @@ -119,11 +119,11 @@
    1.42        |> cterm_of thy
    1.43  
    1.44      val hyps = map2 mk_assum qss patss
    1.45 -    fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
    1.46 +    fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
    1.47      val assums = map2 inst_hyps hyps qss
    1.48      in
    1.49        o_alg thy P 2 xs (patss ~~ assums)
    1.50 -      |> fold_rev implies_intr hyps
    1.51 +      |> fold_rev Thm.implies_intr hyps
    1.52      end
    1.53  
    1.54  fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
    1.55 @@ -147,7 +147,7 @@
    1.56  
    1.57      val patss = map (map snd) x_pats
    1.58      val complete_thm = prove_completeness thy xs thesis qss patss
    1.59 -      |> fold_rev (forall_intr o cterm_of thy) vs
    1.60 +      |> fold_rev (Thm.forall_intr o cterm_of thy) vs
    1.61      in
    1.62        PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
    1.63    end