src/HOL/Import/shuffler.ML
changeset 21078 101aefd61aac
parent 20951 868120282837
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:25 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Fri Oct 20 17:07:26 2006 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  val copy = I
     1.5  val extend = I
     1.6  fun merge _ = Library.gen_union Thm.eq_thm
     1.7 -fun print sg thms =
     1.8 +fun print _ thms =
     1.9      Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    1.10  				    (map Display.pretty_thm thms))
    1.11  end
    1.12 @@ -92,7 +92,7 @@
    1.13  
    1.14  val weaken =
    1.15      let
    1.16 -	val cert = cterm_of (sign_of ProtoPure.thy)
    1.17 +	val cert = cterm_of ProtoPure.thy
    1.18  	val P = Free("P",propT)
    1.19  	val Q = Free("Q",propT)
    1.20  	val PQ = Logic.mk_implies(P,Q)
    1.21 @@ -111,7 +111,7 @@
    1.22  
    1.23  val imp_comm =
    1.24      let
    1.25 -	val cert = cterm_of (sign_of ProtoPure.thy)
    1.26 +	val cert = cterm_of ProtoPure.thy
    1.27  	val P = Free("P",propT)
    1.28  	val Q = Free("Q",propT)
    1.29  	val R = Free("R",propT)
    1.30 @@ -131,7 +131,7 @@
    1.31  
    1.32  val def_norm =
    1.33      let
    1.34 -	val cert = cterm_of (sign_of ProtoPure.thy)
    1.35 +	val cert = cterm_of ProtoPure.thy
    1.36  	val aT = TFree("'a",[])
    1.37  	val bT = TFree("'b",[])
    1.38  	val v = Free("v",aT)
    1.39 @@ -158,7 +158,7 @@
    1.40  
    1.41  val all_comm =
    1.42      let
    1.43 -	val cert = cterm_of (sign_of ProtoPure.thy)
    1.44 +	val cert = cterm_of ProtoPure.thy
    1.45  	val xT = TFree("'a",[])
    1.46  	val yT = TFree("'b",[])
    1.47  	val P = Free("P",xT-->yT-->propT)
    1.48 @@ -182,7 +182,7 @@
    1.49  
    1.50  val equiv_comm =
    1.51      let
    1.52 -	val cert = cterm_of (sign_of ProtoPure.thy)
    1.53 +	val cert = cterm_of ProtoPure.thy
    1.54  	val T    = TFree("'a",[])
    1.55  	val t    = Free("t",T)
    1.56  	val u    = Free("u",T)
    1.57 @@ -216,28 +216,28 @@
    1.58    | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
    1.59    | swap_bound n t = t
    1.60  
    1.61 -fun rew_th sg (xv as (x,xT)) (yv as (y,yT)) t =
    1.62 +fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
    1.63      let
    1.64  	val lhs = list_all ([xv,yv],t)
    1.65  	val rhs = list_all ([yv,xv],swap_bound 0 t)
    1.66  	val rew = Logic.mk_equals (lhs,rhs)
    1.67 -	val init = trivial (cterm_of sg rew)
    1.68 +	val init = trivial (cterm_of thy rew)
    1.69      in
    1.70  	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
    1.71      end
    1.72  
    1.73 -fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    1.74 +fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    1.75      let
    1.76  	val res = (find_bound 0 body;2) handle RESULT i => i
    1.77      in
    1.78  	case res of
    1.79 -	    0 => SOME (rew_th sg (x,xT) (y,yT) body)
    1.80 +	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
    1.81  	  | 1 => if string_ord(y,x) = LESS
    1.82  		 then
    1.83  		     let
    1.84  			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
    1.85 -			 val t_th    = reflexive (cterm_of sg t)
    1.86 -			 val newt_th = reflexive (cterm_of sg newt)
    1.87 +			 val t_th    = reflexive (cterm_of thy t)
    1.88 +			 val newt_th = reflexive (cterm_of thy newt)
    1.89  		     in
    1.90  			 SOME (transitive t_th newt_th)
    1.91  		     end
    1.92 @@ -264,10 +264,10 @@
    1.93  		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
    1.94      end
    1.95  
    1.96 -fun inst_tfrees sg [] thm = thm
    1.97 -  | inst_tfrees sg ((name,U)::rest) thm = 
    1.98 +fun inst_tfrees thy [] thm = thm
    1.99 +  | inst_tfrees thy ((name,U)::rest) thm = 
   1.100      let
   1.101 -	val cU = ctyp_of sg U
   1.102 +	val cU = ctyp_of thy U
   1.103  	val tfrees = add_term_tfrees (prop_of thm,[])
   1.104  	val (rens, thm') = Thm.varifyT'
   1.105      (remove (op = o apsnd fst) name tfrees) thm
   1.106 @@ -275,10 +275,10 @@
   1.107  	    case rens of
   1.108  		[] => thm'
   1.109  	      | [((_, S), idx)] => instantiate
   1.110 -            ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
   1.111 +            ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
   1.112  	      | _ => error "Shuffler.inst_tfrees internal error"
   1.113      in
   1.114 -	inst_tfrees sg rest mid
   1.115 +	inst_tfrees thy rest mid
   1.116      end
   1.117  
   1.118  fun is_Abs (Abs _) = true
   1.119 @@ -295,11 +295,11 @@
   1.120      end
   1.121    | eta_redex _ = false
   1.122  
   1.123 -fun eta_contract sg assumes origt =
   1.124 +fun eta_contract thy assumes origt =
   1.125      let
   1.126  	val (typet,Tinst) = freeze_thaw_term origt
   1.127 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
   1.128 -	val final = inst_tfrees sg Tinst o thaw
   1.129 +	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.130 +	val final = inst_tfrees thy Tinst o thaw
   1.131  	val t = #1 (Logic.dest_equals (prop_of init))
   1.132  	val _ =
   1.133  	    let
   1.134 @@ -307,11 +307,11 @@
   1.135  	    in
   1.136  		if not (lhs aconv origt)
   1.137  		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.138 -		      writeln (string_of_cterm (cterm_of sg origt));
   1.139 -		      writeln (string_of_cterm (cterm_of sg lhs));
   1.140 -		      writeln (string_of_cterm (cterm_of sg typet));
   1.141 -		      writeln (string_of_cterm (cterm_of sg t));
   1.142 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
   1.143 +		      writeln (string_of_cterm (cterm_of thy origt));
   1.144 +		      writeln (string_of_cterm (cterm_of thy lhs));
   1.145 +		      writeln (string_of_cterm (cterm_of thy typet));
   1.146 +		      writeln (string_of_cterm (cterm_of thy t));
   1.147 +		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.148  		      writeln "done")
   1.149  		else ()
   1.150  	    end
   1.151 @@ -321,7 +321,7 @@
   1.152  	    ((if eta_redex P andalso eta_redex Q
   1.153  	      then
   1.154  		  let
   1.155 -		      val cert = cterm_of sg
   1.156 +		      val cert = cterm_of thy
   1.157  		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
   1.158  		      val cv = cert v
   1.159  		      val ct = cert t
   1.160 @@ -347,21 +347,21 @@
   1.161  	  | _ => NONE
   1.162         end
   1.163  
   1.164 -fun beta_fun sg assume t =
   1.165 -    SOME (beta_conversion true (cterm_of sg t))
   1.166 +fun beta_fun thy assume t =
   1.167 +    SOME (beta_conversion true (cterm_of thy t))
   1.168  
   1.169  val meta_sym_rew = thm "refl"
   1.170  
   1.171 -fun equals_fun sg assume t =
   1.172 +fun equals_fun thy assume t =
   1.173      case t of
   1.174  	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
   1.175        | _ => NONE
   1.176  
   1.177 -fun eta_expand sg assumes origt =
   1.178 +fun eta_expand thy assumes origt =
   1.179      let
   1.180  	val (typet,Tinst) = freeze_thaw_term origt
   1.181 -	val (init,thaw) = freeze_thaw (reflexive (cterm_of sg typet))
   1.182 -	val final = inst_tfrees sg Tinst o thaw
   1.183 +	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
   1.184 +	val final = inst_tfrees thy Tinst o thaw
   1.185  	val t = #1 (Logic.dest_equals (prop_of init))
   1.186  	val _ =
   1.187  	    let
   1.188 @@ -369,11 +369,11 @@
   1.189  	    in
   1.190  		if not (lhs aconv origt)
   1.191  		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
   1.192 -		      writeln (string_of_cterm (cterm_of sg origt));
   1.193 -		      writeln (string_of_cterm (cterm_of sg lhs));
   1.194 -		      writeln (string_of_cterm (cterm_of sg typet));
   1.195 -		      writeln (string_of_cterm (cterm_of sg t));
   1.196 -		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of sg T)))) Tinst;
   1.197 +		      writeln (string_of_cterm (cterm_of thy origt));
   1.198 +		      writeln (string_of_cterm (cterm_of thy lhs));
   1.199 +		      writeln (string_of_cterm (cterm_of thy typet));
   1.200 +		      writeln (string_of_cterm (cterm_of thy t));
   1.201 +		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
   1.202  		      writeln "done")
   1.203  		else ()
   1.204  	    end
   1.205 @@ -384,7 +384,7 @@
   1.206  	    then (case domain_type T of
   1.207  		      Type("fun",[aT,bT]) =>
   1.208  		      let
   1.209 -			  val cert = cterm_of sg
   1.210 +			  val cert = cterm_of thy
   1.211  			  val vname = Name.variant (add_term_free_names(t,[])) "v"
   1.212  			  val v = Free(vname,aT)
   1.213  			  val cv = cert v
   1.214 @@ -409,7 +409,7 @@
   1.215  		      end
   1.216  		    | _ => NONE)
   1.217  	    else NONE
   1.218 -	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
   1.219 +	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
   1.220      end
   1.221      handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
   1.222  
   1.223 @@ -423,30 +423,30 @@
   1.224  val S  = mk_free "S" xT
   1.225  val S'  = mk_free "S'" xT
   1.226  in
   1.227 -fun beta_simproc sg = Simplifier.simproc_i
   1.228 -		      sg
   1.229 +fun beta_simproc thy = Simplifier.simproc_i
   1.230 +		      thy
   1.231  		      "Beta-contraction"
   1.232  		      [Abs("x",xT,Q) $ S]
   1.233  		      beta_fun
   1.234  
   1.235 -fun equals_simproc sg = Simplifier.simproc_i
   1.236 -		      sg
   1.237 +fun equals_simproc thy = Simplifier.simproc_i
   1.238 +		      thy
   1.239  		      "Ordered rewriting of meta equalities"
   1.240  		      [Const("op ==",xT) $ S $ S']
   1.241  		      equals_fun
   1.242  
   1.243 -fun quant_simproc sg = Simplifier.simproc_i
   1.244 -			   sg
   1.245 +fun quant_simproc thy = Simplifier.simproc_i
   1.246 +			   thy
   1.247  			   "Ordered rewriting of nested quantifiers"
   1.248  			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
   1.249  			   quant_rewrite
   1.250 -fun eta_expand_simproc sg = Simplifier.simproc_i
   1.251 -			 sg
   1.252 +fun eta_expand_simproc thy = Simplifier.simproc_i
   1.253 +			 thy
   1.254  			 "Smart eta-expansion by equivalences"
   1.255  			 [Logic.mk_equals(Q,R)]
   1.256  			 eta_expand
   1.257 -fun eta_contract_simproc sg = Simplifier.simproc_i
   1.258 -			 sg
   1.259 +fun eta_contract_simproc thy = Simplifier.simproc_i
   1.260 +			 thy
   1.261  			 "Smart handling of eta-contractions"
   1.262  			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
   1.263  			 eta_contract
   1.264 @@ -455,7 +455,7 @@
   1.265  (* Disambiguates the names of bound variables in a term, returning t
   1.266  == t' where all the names of bound variables in t' are unique *)
   1.267  
   1.268 -fun disamb_bound sg t =
   1.269 +fun disamb_bound thy t =
   1.270      let
   1.271  	
   1.272  	fun F (t $ u,idx) =
   1.273 @@ -474,8 +474,8 @@
   1.274  	    end
   1.275  	  | F arg = arg
   1.276  	val (t',_) = F (t,0)
   1.277 -	val ct = cterm_of sg t
   1.278 -	val ct' = cterm_of sg t'
   1.279 +	val ct = cterm_of thy t
   1.280 +	val ct' = cterm_of thy t'
   1.281  	val res = transitive (reflexive ct) (reflexive ct')
   1.282  	val _ = message ("disamb_term: " ^ (string_of_thm res))
   1.283      in
   1.284 @@ -488,12 +488,11 @@
   1.285  
   1.286  fun norm_term thy t =
   1.287      let
   1.288 -	val sg = sign_of thy
   1.289  	val norms = ShuffleData.get thy
   1.290  	val ss = Simplifier.theory_context thy empty_ss
   1.291            setmksimps single
   1.292 -	  addsimps (map (Thm.transfer sg) norms)
   1.293 -          addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
   1.294 +	  addsimps (map (Thm.transfer thy) norms)
   1.295 +          addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
   1.296  	fun chain f th =
   1.297  	    let
   1.298                  val rhs = snd (dest_equals (cprop_of th))
   1.299 @@ -501,7 +500,7 @@
   1.300  		transitive th (f rhs)
   1.301  	    end
   1.302  	val th =
   1.303 -            t |> disamb_bound sg
   1.304 +            t |> disamb_bound thy
   1.305  	      |> chain (Simplifier.full_rewrite ss)
   1.306                |> chain eta_conversion
   1.307  	      |> strip_shyps
   1.308 @@ -509,7 +508,7 @@
   1.309      in
   1.310  	th
   1.311      end
   1.312 -    handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
   1.313 +    handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
   1.314  
   1.315  
   1.316  (* Closes a theorem with respect to free and schematic variables (does
   1.317 @@ -517,11 +516,11 @@
   1.318  
   1.319  fun close_thm th =
   1.320      let
   1.321 -	val sg = sign_of_thm th
   1.322 +	val thy = sign_of_thm th
   1.323  	val c = prop_of th
   1.324  	val vars = add_term_frees (c,add_term_vars(c,[]))
   1.325      in
   1.326 -	Drule.forall_intr_list (map (cterm_of sg) vars) th
   1.327 +	Drule.forall_intr_list (map (cterm_of thy) vars) th
   1.328      end
   1.329      handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
   1.330  
   1.331 @@ -534,14 +533,14 @@
   1.332  	equal_elim (norm_term thy c) th
   1.333      end
   1.334  
   1.335 -(* make_equal sg t u tries to construct the theorem t == u under the
   1.336 -signature sg.  If it succeeds, SOME (t == u) is returned, otherwise
   1.337 +(* make_equal thy t u tries to construct the theorem t == u under the
   1.338 +signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
   1.339  NONE is returned. *)
   1.340  
   1.341 -fun make_equal sg t u =
   1.342 +fun make_equal thy t u =
   1.343      let
   1.344 -	val t_is_t' = norm_term sg t
   1.345 -	val u_is_u' = norm_term sg u
   1.346 +	val t_is_t' = norm_term thy t
   1.347 +	val u_is_u' = norm_term thy u
   1.348  	val th = transitive t_is_t' (symmetric u_is_u')
   1.349  	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
   1.350      in
   1.351 @@ -569,7 +568,7 @@
   1.352      end
   1.353      
   1.354  val collect_ignored =
   1.355 -    foldr (fn (thm,cs) =>
   1.356 +    fold_rev (fn thm => fn cs =>
   1.357  	      let
   1.358  		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
   1.359  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
   1.360 @@ -584,10 +583,9 @@
   1.361  
   1.362  fun set_prop thy t =
   1.363      let
   1.364 -	val sg = sign_of thy
   1.365  	val vars = add_term_frees (t,add_term_vars (t,[]))
   1.366 -	val closed_t = foldr (fn (v,body) => let val vT = type_of v
   1.367 -					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
   1.368 +	val closed_t = Library.foldr (fn (v, body) =>
   1.369 +      let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
   1.370  	val rew_th = norm_term thy closed_t
   1.371  	val rhs = snd (dest_equals (cprop_of rew_th))
   1.372  
   1.373 @@ -595,7 +593,7 @@
   1.374  	fun process [] = NONE
   1.375  	  | process ((name,th)::thms) =
   1.376  	    let
   1.377 -		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
   1.378 +		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
   1.379  		val triv_th = trivial rhs
   1.380  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
   1.381  		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
   1.382 @@ -608,7 +606,7 @@
   1.383  			val closed_th = equal_elim (symmetric rew_th) mod_th
   1.384  		    in
   1.385  			message ("Shuffler.set_prop succeeded by " ^ name);
   1.386 -			SOME (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
   1.387 +			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
   1.388  		    end
   1.389  		  | NONE => process thms
   1.390  	    end
   1.391 @@ -626,7 +624,7 @@
   1.392  fun find_potential thy t =
   1.393      let
   1.394  	val shuffles = ShuffleData.get thy
   1.395 -	val ignored = collect_ignored [] shuffles
   1.396 +	val ignored = collect_ignored shuffles []
   1.397  	val rel_consts = term_consts t \\ ignored
   1.398  	val pot_thms = PureThy.thms_containing_consts thy rel_consts
   1.399      in