--- a/IntEx.thy Sun Dec 06 23:35:02 2009 +0100
+++ b/IntEx.thy Mon Dec 07 00:07:23 2009 +0100
@@ -149,37 +149,6 @@
apply(rule refl)
done
-
-(*
-lemma yy:
- "(REP_my_int ---> id)
- (\<lambda>x. Ball (Respects op \<approx>)
- ((ABS_my_int ---> id)
- ((REP_my_int ---> id)
- (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
- ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
- (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx>
- (ABS_my_int ---> ABS_my_int ---> REP_my_int)
- ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
- (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) =
-(\<lambda>x. Ball (Respects op \<approx>)
- ((ABS_my_int ---> id)
- ((REP_my_int ---> id)
- (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
- ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
- (REP_my_int (ABS_my_int b)) \<approx>
- (ABS_my_int ---> ABS_my_int ---> REP_my_int)
- ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
- (REP_my_int (ABS_my_int b))))))"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*})
-
-apply(rule lambda_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(simp add: id_simps)
-apply(tactic {* quotient_tac @{context} 1 *})
-done
-*)
-
lemma "PLUS a b = PLUS a b"
apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
apply(tactic {* regularize_tac @{context} 1 *})
--- a/IntEx2.thy Sun Dec 06 23:35:02 2009 +0100
+++ b/IntEx2.thy Mon Dec 07 00:07:23 2009 +0100
@@ -175,41 +175,41 @@
fix i j k :: int
show "(i + j) + k = i + (j + k)"
unfolding add_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
done
show "i + j = j + i"
unfolding add_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
done
show "0 + i = (i::int)"
unfolding add_int_def Zero_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *})
done
show "- i + i = 0"
unfolding add_int_def minus_int_def Zero_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *})
done
show "i - j = i + - j"
by (simp add: diff_int_def)
show "(i * j) * k = i * (j * k)"
unfolding mult_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *})
done
show "i * j = j * i"
unfolding mult_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *})
done
show "1 * i = i"
unfolding mult_int_def One_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *})
done
show "(i + j) * k = i * k + j * k"
unfolding mult_int_def add_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *})
done
show "0 \<noteq> (1::int)"
unfolding Zero_int_def One_int_def
- apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *})
done
qed
@@ -246,21 +246,21 @@
fix i j k :: int
show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
done
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
by (auto simp add: less_int_def dest: antisym)
show "i \<le> i"
unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
done
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
done
show "i \<le> j \<or> j \<le> i"
unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
done
qed
@@ -289,7 +289,7 @@
fix i j k :: int
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
unfolding le_int_def add_int_def
- apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
done
qed
@@ -307,7 +307,7 @@
fix i j k :: int
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
unfolding mult_int_def le_int_def less_int_def Zero_int_def
- apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
+ apply(tactic {* lift_tac @{context} @{thm test} 1 *})
done
show "\<bar>i\<bar> = (if i < 0 then -i else i)"
by (simp only: zabs_def)
--- a/LFex.thy Sun Dec 06 23:35:02 2009 +0100
+++ b/LFex.thy Mon Dec 07 00:07:23 2009 +0100
@@ -296,7 +296,7 @@
\<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
\<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
\<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
done
print_quotients
--- a/QuotMain.thy Sun Dec 06 23:35:02 2009 +0100
+++ b/QuotMain.thy Mon Dec 07 00:07:23 2009 +0100
@@ -1083,7 +1083,7 @@
ML {*
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+ ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
let
val thy = ProofContext.theory_of ctxt
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -1096,9 +1096,14 @@
val tl = Thm.lhs_of ts
val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
- (*val _ = tracing "lambda_prs"
- val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
- val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+ val _ = if not (s = @{const_name "id"}) then
+ (tracing "lambda_prs";
+ tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+ tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+ tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+ else ()
in
Conv.rewr_conv ti ctrm
end