src/Provers/hypsubst.ML
 changeset 3537 79ac9b475621 parent 2750 fe3799355b5e child 4179 cc4b6791d5dc
equal inserted replaced
`   114   it is easy to handle several consecutive equality assumptions in a row.`
`   114   it is easy to handle several consecutive equality assumptions in a row.`
`   115   Note that we have to inspect the proof state after doing the rewriting,`
`   115   Note that we have to inspect the proof state after doing the rewriting,`
`   116   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality`
`   116   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality`
`   117   must NOT be deleted.  Tactic must rotate or delete m assumptions.`
`   117   must NOT be deleted.  Tactic must rotate or delete m assumptions.`
`   118 *)`
`   118 *)`
`   119 fun thin_leading_eqs_tac bnd m i = STATE(fn state =>`
`   119 fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>`
`   120     let fun count []      = 0`
`   120     let fun count []      = 0`
`   121 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  `
`   121 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  `
`   122 			      1 + count Bs)`
`   122 			      1 + count Bs)`
`   123                              handle Match => 0)`
`   123                              handle Match => 0)`
`   125         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))`
`   124         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))`
`   126     in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i`
`   125     in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i`
`   127     end);`
`   126     end);`
`   128 `
`   127 `
`   129 (*For the simpset.  Adds ALL suitable equalities, even if not first!`
`   128 (*For the simpset.  Adds ALL suitable equalities, even if not first!`
`   139 `
`   138 `
`   140   val hyp_subst_ss = empty_ss setmksimps mk_eqs`
`   139   val hyp_subst_ss = empty_ss setmksimps mk_eqs`
`   141 `
`   140 `
`   142   (*Select a suitable equality assumption and substitute throughout the subgoal`
`   141   (*Select a suitable equality assumption and substitute throughout the subgoal`
`   143     Replaces only Bound variables if bnd is true*)`
`   142     Replaces only Bound variables if bnd is true*)`
`   144   fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>`
`   143   fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>`
`   145 	let val (_,_,Bi,_) = dest_state(state,i)`
`   144 	let val n = length(Logic.strip_assums_hyp Bi) - 1`
`   146 	    val n = length(Logic.strip_assums_hyp Bi) - 1`
`       `
`   147 	    val (k,_) = eq_var bnd true Bi`
`   145 	    val (k,_) = eq_var bnd true Bi`
`   148 	in `
`   146 	in `
`   149 	   EVERY [rotate_tac k i,`
`   147 	   DETERM (EVERY [rotate_tac k i,`
`   150 		  asm_full_simp_tac hyp_subst_ss i,`
`   148 			  asm_full_simp_tac hyp_subst_ss i,`
`   151 		  etac thin_rl i,`
`   149 			  etac thin_rl i,`
`   152 		  thin_leading_eqs_tac bnd (n-k) i]`
`   150 			  thin_leading_eqs_tac bnd (n-k) i])`
`   153 	end`
`   151 	end`
`   154 	handle THM _ => no_tac | EQ_VAR => no_tac));`
`   152 	handle THM _ => no_tac | EQ_VAR => no_tac);`
`   155 `
`   153 `
`   156 end;`
`   154 end;`
`   157 `
`   155 `
`   158 val ssubst = standard (sym RS subst);`
`   156 val ssubst = standard (sym RS subst);`
`   159 `
`   157 `
`   160 (*Old version of the tactic above -- slower but the only way`
`   158 (*Old version of the tactic above -- slower but the only way`
`   161   to handle equalities containing Vars.*)`
`   159   to handle equalities containing Vars.*)`
`   162 fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>`
`   160 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>`
`   163       let val (_,_,Bi,_) = dest_state(state,i)`
`   161       let val n = length(Logic.strip_assums_hyp Bi) - 1`
`   164 	  val n = length(Logic.strip_assums_hyp Bi) - 1`
`       `
`   165 	  val (k,symopt) = eq_var bnd false Bi`
`   162 	  val (k,symopt) = eq_var bnd false Bi`
`   166       in `
`   163       in `
`   167 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),`
`   164 	 DETERM`
`   168 		etac revcut_rl i,`
`   165            (EVERY [REPEAT_DETERM_N k (etac rev_mp i),`
`   169 		REPEAT_DETERM_N (n-k) (etac rev_mp i),`
`   166 		   etac revcut_rl i,`
`   170 		etac (if symopt then ssubst else subst) i,`
`   167 		   REPEAT_DETERM_N (n-k) (etac rev_mp i),`
`   171 		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]`
`   168 		   etac (if symopt then ssubst else subst) i,`
`       `
`   169 		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])`
`   172       end`
`   170       end`
`   173       handle THM _ => no_tac | EQ_VAR => no_tac));`
`   171       handle THM _ => no_tac | EQ_VAR => no_tac);`
`   174 `
`   172 `
`   175 (*Substitutes for Free or Bound variables*)`
`   173 (*Substitutes for Free or Bound variables*)`
`   176 val hyp_subst_tac = `
`   174 val hyp_subst_tac = `
`   177     gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;`
`   175     gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;`
`   178 `
`   176 `