avoid low-level tsig;
authorwenzelm
Sat Aug 05 14:55:09 2006 +0200 (2006-08-05)
changeset 20344d02b43ea722e
parent 20343 e093a54bf25e
child 20345 32ed5f5fee84
avoid low-level tsig;
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/specification_package.ML
src/Provers/ind.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Aug 05 14:52:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Aug 05 14:55:09 2006 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4      ID:         $Id$
     1.5      Author:     Alexander Krauss, TU Muenchen
     1.6  
     1.7 -A package for general recursive function definitions. 
     1.8 +A package for general recursive function definitions.
     1.9  A tactic to prove completeness of datatype patterns.
    1.10  *)
    1.11  
    1.12 -signature FUNDEF_DATATYPE = 
    1.13 +signature FUNDEF_DATATYPE =
    1.14  sig
    1.15      val pat_complete_tac: int -> tactic
    1.16  
    1.17 @@ -28,52 +28,52 @@
    1.18  
    1.19  fun inst_case_thm thy x P thm =
    1.20      let
    1.21 -	val [Pv, xv] = term_vars (prop_of thm)
    1.22 +        val [Pv, xv] = term_vars (prop_of thm)
    1.23      in
    1.24 -	cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
    1.25 +        cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
    1.26      end
    1.27  
    1.28  
    1.29  fun invent_vars constr i =
    1.30      let
    1.31 -	val Ts = binder_types (fastype_of constr)
    1.32 -	val j = i + length Ts
    1.33 -	val is = i upto (j - 1)
    1.34 -	val avs = map2 mk_argvar is Ts
    1.35 -	val pvs = map2 mk_patvar is Ts
    1.36 +        val Ts = binder_types (fastype_of constr)
    1.37 +        val j = i + length Ts
    1.38 +        val is = i upto (j - 1)
    1.39 +        val avs = map2 mk_argvar is Ts
    1.40 +        val pvs = map2 mk_patvar is Ts
    1.41      in
    1.42 -	(avs, pvs, j)
    1.43 +        (avs, pvs, j)
    1.44      end
    1.45  
    1.46  
    1.47  fun filter_pats thy cons pvars [] = []
    1.48    | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
    1.49 -  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = 
    1.50 +  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
    1.51      case pat of
    1.52 -	Free _ => let val inst = list_comb (cons, pvars)
    1.53 -		 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
    1.54 -		    :: (filter_pats thy cons pvars pts) end
    1.55 +        Free _ => let val inst = list_comb (cons, pvars)
    1.56 +                 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
    1.57 +                    :: (filter_pats thy cons pvars pts) end
    1.58        | _ => if fst (strip_comb pat) = cons
    1.59 -	     then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
    1.60 -	     else filter_pats thy cons pvars pts
    1.61 +             then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
    1.62 +             else filter_pats thy cons pvars pts
    1.63  
    1.64  
    1.65  fun inst_constrs_of thy (T as Type (name, _)) =
    1.66 -	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    1.67 -	    (the (DatatypePackage.get_datatype_constrs thy name))
    1.68 +        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    1.69 +            (the (DatatypePackage.get_datatype_constrs thy name))
    1.70    | inst_constrs_of thy _ = raise Match
    1.71  
    1.72  
    1.73  fun transform_pat thy avars c_assum ([] , thm) = raise Match
    1.74    | transform_pat thy avars c_assum (pat :: pats, thm) =
    1.75      let
    1.76 -	val (_, subps) = strip_comb pat
    1.77 -	val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
    1.78 -	val a_eqs = map assume eqs
    1.79 -	val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
    1.80 +        val (_, subps) = strip_comb pat
    1.81 +        val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
    1.82 +        val a_eqs = map assume eqs
    1.83 +        val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
    1.84      in
    1.85 -	(subps @ pats, fold_rev implies_intr eqs
    1.86 -				(implies_elim thm c_eq_pat))
    1.87 +        (subps @ pats, fold_rev implies_intr eqs
    1.88 +                                (implies_elim thm c_eq_pat))
    1.89      end
    1.90  
    1.91  
    1.92 @@ -81,14 +81,14 @@
    1.93  
    1.94  fun constr_case thy P idx (v :: vs) pats cons =
    1.95      let
    1.96 -	val (avars, pvars, newidx) = invent_vars cons idx
    1.97 -	val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
    1.98 -	val c_assum = assume c_hyp
    1.99 -	val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
   1.100 +        val (avars, pvars, newidx) = invent_vars cons idx
   1.101 +        val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
   1.102 +        val c_assum = assume c_hyp
   1.103 +        val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
   1.104      in
   1.105 -	o_alg thy P newidx (avars @ vs) newpats
   1.106 -	      |> implies_intr c_hyp
   1.107 -	      |> fold_rev (forall_intr o cterm_of thy) avars
   1.108 +        o_alg thy P newidx (avars @ vs) newpats
   1.109 +              |> implies_intr c_hyp
   1.110 +              |> fold_rev (forall_intr o cterm_of thy) avars
   1.111      end
   1.112    | constr_case _ _ _ _ _ _ = raise Match
   1.113  and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
   1.114 @@ -96,72 +96,72 @@
   1.115    | o_alg thy P idx (v :: vs) pts =
   1.116      if forall (is_Free o hd o fst) pts (* Var case *)
   1.117      then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
   1.118 -			       (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
   1.119 +                               (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
   1.120      else (* Cons case *)
   1.121 -	 let  
   1.122 -	     val T = fastype_of v
   1.123 -	     val (tname, _) = dest_Type T
   1.124 -	     val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
   1.125 -	     val constrs = inst_constrs_of thy T
   1.126 -	     val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
   1.127 -	 in 
   1.128 -	     inst_case_thm thy v P case_thm
   1.129 -			   |> fold (curry op COMP) c_cases
   1.130 -	 end
   1.131 +         let
   1.132 +             val T = fastype_of v
   1.133 +             val (tname, _) = dest_Type T
   1.134 +             val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
   1.135 +             val constrs = inst_constrs_of thy T
   1.136 +             val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
   1.137 +         in
   1.138 +             inst_case_thm thy v P case_thm
   1.139 +                           |> fold (curry op COMP) c_cases
   1.140 +         end
   1.141    | o_alg _ _ _ _ _ = raise Match
   1.142  
   1.143 -			   
   1.144 +
   1.145  fun prove_completeness thy x P qss pats =
   1.146      let
   1.147 -	fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
   1.148 -						HOLogic.mk_Trueprop P)
   1.149 -					       |> fold_rev mk_forall qs
   1.150 -					       |> cterm_of thy
   1.151 +        fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
   1.152 +                                                HOLogic.mk_Trueprop P)
   1.153 +                                               |> fold_rev mk_forall qs
   1.154 +                                               |> cterm_of thy
   1.155  
   1.156 -	val hyps = map2 mk_assum qss pats
   1.157 +        val hyps = map2 mk_assum qss pats
   1.158  
   1.159 -	fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
   1.160 +        fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
   1.161  
   1.162 -	val assums = map2 inst_hyps hyps qss
   1.163 +        val assums = map2 inst_hyps hyps qss
   1.164      in
   1.165 -	o_alg thy P 2 [x] (map2 (pair o single) pats assums)
   1.166 -	      |> fold_rev implies_intr hyps
   1.167 +        o_alg thy P 2 [x] (map2 (pair o single) pats assums)
   1.168 +              |> fold_rev implies_intr hyps
   1.169      end
   1.170  
   1.171  
   1.172  
   1.173  fun pat_complete_tac i thm =
   1.174 -    let 
   1.175 +    let
   1.176        val thy = theory_of_thm thm
   1.177  
   1.178 -	val subgoal = nth (prems_of thm) (i - 1)
   1.179 +        val subgoal = nth (prems_of thm) (i - 1)   (* FIXME SUBGOAL tactical *)
   1.180  
   1.181          val ([P, x], subgf) = dest_all_all subgoal
   1.182  
   1.183 -	val assums = Logic.strip_imp_prems subgf
   1.184 -		    
   1.185 -	fun pat_of assum = 
   1.186 -	    let
   1.187 -		val (qs, imp) = dest_all_all assum
   1.188 -	    in
   1.189 -		case Logic.dest_implies imp of 
   1.190 -		    (_ $ (_ $ _ $ pat), _) => (qs, pat)
   1.191 -		  | _ => raise COMPLETENESS
   1.192 -	    end
   1.193 +        val assums = Logic.strip_imp_prems subgf
   1.194  
   1.195 -	val (qss, pats) = split_list (map pat_of assums)
   1.196 +        fun pat_of assum =
   1.197 +            let
   1.198 +                val (qs, imp) = dest_all_all assum
   1.199 +            in
   1.200 +                case Logic.dest_implies imp of
   1.201 +                    (_ $ (_ $ _ $ pat), _) => (qs, pat)
   1.202 +                  | _ => raise COMPLETENESS
   1.203 +            end
   1.204  
   1.205 -	val complete_thm = prove_completeness thy x P qss pats
   1.206 +        val (qss, pats) = split_list (map pat_of assums)
   1.207 +
   1.208 +        val complete_thm = prove_completeness thy x P qss pats
   1.209                                                |> forall_intr (cterm_of thy x)
   1.210                                                |> forall_intr (cterm_of thy P)
   1.211      in
   1.212 -	Seq.single (Drule.compose_single(complete_thm, i, thm))
   1.213 +        Seq.single (Drule.compose_single(complete_thm, i, thm))
   1.214      end
   1.215      handle COMPLETENESS => Seq.empty
   1.216  
   1.217  
   1.218  
   1.219 -val setup = 
   1.220 +val setup =
   1.221      Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
   1.222  
   1.223 -end
   1.224 \ No newline at end of file
   1.225 +end
     2.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Sat Aug 05 14:52:58 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Sat Aug 05 14:55:09 2006 +0200
     2.3 @@ -2,29 +2,29 @@
     2.4      ID:         $Id$
     2.5      Author:     Alexander Krauss, TU Muenchen
     2.6  
     2.7 -A package for general recursive function definitions. 
     2.8 +A package for general recursive function definitions.
     2.9  
    2.10 -Automatic splitting of overlapping constructor patterns. This is a preprocessing step which 
    2.11 +Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
    2.12  turns a specification with overlaps into an overlap-free specification.
    2.13  
    2.14  *)
    2.15  
    2.16 -signature FUNDEF_SPLIT = 
    2.17 +signature FUNDEF_SPLIT =
    2.18  sig
    2.19    val split_some_equations :
    2.20      Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
    2.21  
    2.22  end
    2.23  
    2.24 -structure FundefSplit : FUNDEF_SPLIT = 
    2.25 +structure FundefSplit : FUNDEF_SPLIT =
    2.26  struct
    2.27  
    2.28  
    2.29  (* We use proof context for the variable management *)
    2.30  (* FIXME: no __ *)
    2.31  
    2.32 -fun new_var ctx vs T = 
    2.33 -    let 
    2.34 +fun new_var ctx vs T =
    2.35 +    let
    2.36        val [v] = Variable.variant_frees ctx vs [("v", T)]
    2.37      in
    2.38        (Free v :: vs, Free v)
    2.39 @@ -37,17 +37,17 @@
    2.40  
    2.41  (* This is copied from "fundef_datatype.ML" *)
    2.42  fun inst_constrs_of thy (T as Type (name, _)) =
    2.43 -	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    2.44 -	    (the (DatatypePackage.get_datatype_constrs thy name))
    2.45 +        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    2.46 +            (the (DatatypePackage.get_datatype_constrs thy name))
    2.47    | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
    2.48  
    2.49  
    2.50  
    2.51  fun pattern_subtract_subst ctx vs _ (Free v2) = []
    2.52    | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
    2.53 -    let 
    2.54 -      fun foo constr = 
    2.55 -          let 
    2.56 +    let
    2.57 +      fun foo constr =
    2.58 +          let
    2.59              val (vs', t) = saturate ctx vs constr
    2.60              val substs = pattern_subtract_subst ctx vs' t t'
    2.61            in
    2.62 @@ -95,7 +95,7 @@
    2.63  
    2.64  
    2.65  fun split_all_equations ctx eqns =
    2.66 -    let 
    2.67 +    let
    2.68        fun split_aux prev [] = []
    2.69          | split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es
    2.70      in
    2.71 @@ -108,8 +108,8 @@
    2.72        fun split_aux prev [] = []
    2.73          | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
    2.74                                                            :: split_aux (eq :: prev) es
    2.75 -        | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
    2.76 -                                                           :: split_aux (eq :: prev) es
    2.77 +        | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq])
    2.78 +                                                                :: split_aux (eq :: prev) es
    2.79      in
    2.80        split_aux [] eqns
    2.81      end
     3.1 --- a/src/HOL/Tools/specification_package.ML	Sat Aug 05 14:52:58 2006 +0200
     3.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Aug 05 14:55:09 2006 +0200
     3.3 @@ -131,8 +131,7 @@
     3.4          fun proc_single prop =
     3.5              let
     3.6                  val frees = Term.term_frees prop
     3.7 -                val tsig = Sign.tsig_of (sign_of thy)
     3.8 -                val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
     3.9 +                val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
    3.10                                 "Specificaton: Only free variables of sort 'type' allowed"
    3.11                  val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    3.12              in
     4.1 --- a/src/Provers/ind.ML	Sat Aug 05 14:52:58 2006 +0200
     4.2 +++ b/src/Provers/ind.ML	Sat Aug 05 14:55:09 2006 +0200
     4.3 @@ -26,9 +26,9 @@
     4.4  
     4.5  val _$(_$Var(a_ixname,aT)) = concl_of spec;
     4.6  
     4.7 -fun add_term_frees tsig =
     4.8 +fun add_term_frees thy =
     4.9  let fun add(tm, vars) = case tm of
    4.10 -	Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
    4.11 +	Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
    4.12  		     else vars
    4.13        | Abs (_,_,body) => add(body,vars)
    4.14        | rator$rand => add(rator, add(rand, vars))
    4.15 @@ -40,8 +40,7 @@
    4.16  
    4.17  (*Generalizes over all free variables, with the named var outermost.*)
    4.18  fun all_frees_tac (var:string) i thm = 
    4.19 -    let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
    4.20 -        val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
    4.21 +    let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
    4.22          val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
    4.23      in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    4.24