adhoc_freeze_vars;
authorwenzelm
Thu Aug 08 23:49:44 2002 +0200 (2002-08-08)
changeset 13484d8f5d3391766
parent 13483 0e6adce08fb0
child 13485 acf39e924091
adhoc_freeze_vars;
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/extract_common_term.ML
src/Pure/term.ML
     1.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Thu Aug 08 23:48:31 2002 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Thu Aug 08 23:49:44 2002 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4                               as with < and <= but not = and div*)
     1.5    (*proof tools*)
     1.6    val prove_conv: tactic list -> Sign.sg -> 
     1.7 -                  thm list -> term * term -> thm option
     1.8 +                  thm list -> string list -> term * term -> thm option
     1.9    val trans_tac: thm option -> tactic (*applies the initial lemma*)
    1.10    val norm_tac: tactic                (*proves the initial lemma*)
    1.11    val numeral_simp_tac: tactic        (*proves the final theorem*)
    1.12 @@ -53,10 +53,7 @@
    1.13  (*the simplification procedure*)
    1.14  fun proc sg hyps t =
    1.15    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.16 -      val rand_s = gensym"_"
    1.17 -      fun mk_inst (var as Var((a,i),T))  = 
    1.18 -	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    1.19 -      val t' = subst_atomic (map mk_inst (term_vars t)) t
    1.20 +      val (t', xs) = Term.adhoc_freeze_vars t;
    1.21        val (t1,t2) = Data.dest_bal t' 
    1.22        val (m1, t1') = Data.dest_coeff t1
    1.23        and (m2, t2') = Data.dest_coeff t2
    1.24 @@ -73,13 +70,13 @@
    1.25                  else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
    1.26        val reshape =  (*Move d to the front and put the rest into standard form
    1.27  		       i * #m * j == #d * (#n * (j * k)) *)
    1.28 -	    Data.prove_conv [Data.norm_tac] sg hyps 
    1.29 +	    Data.prove_conv [Data.norm_tac] sg hyps xs
    1.30  	      (t',   Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
    1.31    in
    1.32        apsome Data.simplify_meta_eq
    1.33         (Data.prove_conv 
    1.34  	       [Data.trans_tac reshape, rtac Data.cancel 1,
    1.35 -		Data.numeral_simp_tac] sg hyps (t', rhs))
    1.36 +		Data.numeral_simp_tac] sg hyps xs (t', rhs))
    1.37    end
    1.38    handle TERM _ => None
    1.39         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
     2.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Aug 08 23:48:31 2002 +0200
     2.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Aug 08 23:49:44 2002 +0200
     2.3 @@ -37,7 +37,7 @@
     2.4    val bal_add2: thm
     2.5    (*proof tools*)
     2.6    val prove_conv: tactic list -> Sign.sg -> 
     2.7 -                  thm list -> term * term -> thm option
     2.8 +                  thm list -> string list -> term * term -> thm option
     2.9    val trans_tac: thm option -> tactic (*applies the initial lemma*)
    2.10    val norm_tac: tactic                (*proves the initial lemma*)
    2.11    val numeral_simp_tac: tactic        (*proves the final theorem*)
    2.12 @@ -71,10 +71,7 @@
    2.13  (*the simplification procedure*)
    2.14  fun proc sg hyps t =
    2.15    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    2.16 -      val rand_s = gensym"_"
    2.17 -      fun mk_inst (var as Var((a,i),T))  = 
    2.18 -	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    2.19 -      val t' = subst_atomic (map mk_inst (term_vars t)) t
    2.20 +      val (t', xs) = Term.adhoc_freeze_vars t;
    2.21        val (t1,t2) = Data.dest_bal t' 
    2.22        val terms1 = Data.dest_sum t1
    2.23        and terms2 = Data.dest_sum t2
    2.24 @@ -86,7 +83,7 @@
    2.25  		       i + #m + j + k == #m + i + (j + k) *)
    2.26  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    2.27  		raise TERM("cancel_numerals", []) 
    2.28 -	    else Data.prove_conv [Data.norm_tac] sg hyps
    2.29 +	    else Data.prove_conv [Data.norm_tac] sg hyps xs
    2.30  			(t', 
    2.31  			 Data.mk_bal (newshape(n1,terms1'), 
    2.32  				      newshape(n2,terms2')))
    2.33 @@ -95,13 +92,13 @@
    2.34         (if n2<=n1 then 
    2.35  	    Data.prove_conv 
    2.36  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    2.37 -		Data.numeral_simp_tac] sg hyps
    2.38 +		Data.numeral_simp_tac] sg hyps xs
    2.39  	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    2.40  				 Data.mk_sum terms2'))
    2.41  	else
    2.42  	    Data.prove_conv 
    2.43  	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    2.44 -		Data.numeral_simp_tac] sg hyps
    2.45 +		Data.numeral_simp_tac] sg hyps xs
    2.46  	       (t', Data.mk_bal (Data.mk_sum terms1', 
    2.47  				 newshape(n2-n1,terms2'))))
    2.48    end
     3.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Aug 08 23:48:31 2002 +0200
     3.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Aug 08 23:49:44 2002 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4    (*rules*)
     3.5    val left_distrib: thm
     3.6    (*proof tools*)
     3.7 -  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
     3.8 +  val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
     3.9    val trans_tac: thm option -> tactic (*applies the initial lemma*)
    3.10    val norm_tac: tactic                (*proves the initial lemma*)
    3.11    val numeral_simp_tac: tactic        (*proves the final theorem*)
    3.12 @@ -66,16 +66,13 @@
    3.13  (*the simplification procedure*)
    3.14  fun proc sg _ t =
    3.15    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    3.16 -      val rand_s = gensym"_"
    3.17 -      fun mk_inst (var as Var((a,i),T))  = 
    3.18 -	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    3.19 -      val t' = subst_atomic (map mk_inst (term_vars t)) t
    3.20 +      val (t', xs) = Term.adhoc_freeze_vars t;
    3.21        val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    3.22        val reshape =  (*Move i*u to the front and put j*u into standard form
    3.23  		       i + #m + j + k == #m + i + (j + k) *)
    3.24  	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    3.25  		raise TERM("combine_numerals", []) 
    3.26 -	    else Data.prove_conv [Data.norm_tac] sg 
    3.27 +	    else Data.prove_conv [Data.norm_tac] sg xs
    3.28  			(t', 
    3.29  			 Data.mk_sum ([Data.mk_coeff(m,u),
    3.30  				       Data.mk_coeff(n,u)] @ terms))
    3.31 @@ -83,7 +80,7 @@
    3.32        apsome Data.simplify_meta_eq
    3.33  	 (Data.prove_conv 
    3.34  	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    3.35 -	     Data.numeral_simp_tac] sg
    3.36 +	     Data.numeral_simp_tac] sg xs
    3.37  	    (t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    3.38    end
    3.39    handle TERM _ => None
     4.1 --- a/src/Provers/Arith/extract_common_term.ML	Thu Aug 08 23:48:31 2002 +0200
     4.2 +++ b/src/Provers/Arith/extract_common_term.ML	Thu Aug 08 23:49:44 2002 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4    val find_first: term -> term list -> term list
     4.5    (*proof tools*)
     4.6    val prove_conv: tactic list -> Sign.sg -> 
     4.7 -                  thm list -> term * term -> thm option
     4.8 +                  thm list -> string list -> term * term -> thm option
     4.9    val norm_tac: tactic                (*proves the result*)
    4.10    val simplify_meta_eq: thm -> thm    (*simplifies the result*)
    4.11  end;
    4.12 @@ -52,10 +52,7 @@
    4.13  (*the simplification procedure*)
    4.14  fun proc sg hyps t =
    4.15    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    4.16 -      val rand_s = gensym"_"
    4.17 -      fun mk_inst (var as Var((a,i),T))  = 
    4.18 -	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
    4.19 -      val t' = subst_atomic (map mk_inst (term_vars t)) t
    4.20 +      val (t', xs) = Term.adhoc_freeze_vars t;
    4.21        val (t1,t2) = Data.dest_bal t' 
    4.22        val terms1 = Data.dest_sum t1
    4.23        and terms2 = Data.dest_sum t2
    4.24 @@ -63,7 +60,7 @@
    4.25        val terms1' = Data.find_first u terms1
    4.26        and terms2' = Data.find_first u terms2
    4.27        val reshape = 
    4.28 -	    Data.prove_conv [Data.norm_tac] sg hyps
    4.29 +	    Data.prove_conv [Data.norm_tac] sg hyps xs
    4.30  	        (t', 
    4.31  		 Data.mk_bal (Data.mk_sum (u::terms1'), 
    4.32  		              Data.mk_sum (u::terms2')))
     5.1 --- a/src/Pure/term.ML	Thu Aug 08 23:48:31 2002 +0200
     5.2 +++ b/src/Pure/term.ML	Thu Aug 08 23:49:44 2002 +0200
     5.3 @@ -195,6 +195,7 @@
     5.4    val no_dummy_patterns: term -> term
     5.5    val replace_dummy_patterns: int * term -> int * term
     5.6    val is_replaced_dummy_pattern: indexname -> bool
     5.7 +  val adhoc_freeze_vars: term -> term * string list
     5.8  end;
     5.9  
    5.10  structure Term: TERM =
    5.11 @@ -1100,6 +1101,18 @@
    5.12  fun is_replaced_dummy_pattern ("_dummy_", _) = true
    5.13    | is_replaced_dummy_pattern _ = false;
    5.14  
    5.15 +
    5.16 +(* adhoc freezing *)
    5.17 +
    5.18 +fun adhoc_freeze_vars tm =
    5.19 +  let
    5.20 +    fun mk_inst (var as Var ((a, i), T)) =
    5.21 +      let val x = a ^ Library.gensym "_" ^ string_of_int i
    5.22 +      in ((var,  Free(x, T)), x) end;
    5.23 +    val (insts, xs) = split_list (map mk_inst (term_vars tm));
    5.24 +  in (subst_atomic insts tm, xs) end;
    5.25 +
    5.26 +
    5.27  end;
    5.28  
    5.29