--- a/IntEx.thy Sun Dec 06 06:39:32 2009 +0100
+++ b/IntEx.thy Sun Dec 06 06:41:52 2009 +0100
@@ -147,12 +147,37 @@
apply(rule refl)
done
-abbreviation
- "Abs \<equiv> ABS_my_int"
-abbreviation
- "Rep \<equiv> REP_my_int"
-abbreviation
- "Resp \<equiv> Respects"
+
+(*
+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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IntEx2.thy Sun Dec 06 06:41:52 2009 +0100
@@ -0,0 +1,460 @@
+theory IntEx2
+imports QuotMain
+uses
+ ("Tools/numeral.ML")
+ ("Tools/numeral_syntax.ML")
+ ("Tools/int_arith.ML")
+begin
+
+fun
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient int = "nat \<times> nat" / intrel
+ apply(unfold equivp_def)
+ apply(auto simp add: mem_def expand_fun_eq)
+ done
+
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+begin
+
+quotient_def
+ zero_qnt::"int"
+where
+ "zero_qnt \<equiv> (0::nat, 0::nat)"
+
+definition Zero_int_def[code del]:
+ "0 = zero_qnt"
+
+quotient_def
+ one_qnt::"int"
+where
+ "one_qnt \<equiv> (1::nat, 0::nat)"
+
+definition One_int_def[code del]:
+ "1 = one_qnt"
+
+fun
+ plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "plus_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_def
+ plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+ "plus_qnt \<equiv> plus_raw"
+
+definition add_int_def[code del]:
+ "z + w = plus_qnt z w"
+
+fun
+ minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "minus_raw (x, y) = (y, x)"
+
+quotient_def
+ minus_qnt::"int \<Rightarrow> int"
+where
+ "minus_qnt \<equiv> minus_raw"
+
+definition minus_int_def [code del]:
+ "- z = minus_qnt z"
+
+definition
+ diff_int_def [code del]: "z - w = z + (-w::int)"
+
+fun
+ mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_def
+ mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+ "mult_qnt \<equiv> mult_raw"
+
+definition
+ mult_int_def [code del]: "z * w = mult_qnt z w"
+
+fun
+ le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_def
+ le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
+where
+ "le_qnt \<equiv> le_raw"
+
+definition
+ le_int_def [code del]:
+ "z \<le> w = le_qnt z w"
+
+definition
+ less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
+
+thm add_assoc
+
+lemma plus_raw_rsp[quotient_rsp]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
+by auto
+
+lemma mult_raw_rsp[quotient_rsp]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
+apply(auto)
+apply(simp add: mult algebra_simps)
+sorry
+
+lemma le_raw_rsp[quotient_rsp]:
+ shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
+by auto
+
+lemma plus_assoc_raw:
+ shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
+by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+ shows "plus_raw i j \<approx> plus_raw j i"
+by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+ shows "plus_raw (0, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+ shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
+by (cases i) (simp)
+
+lemma mult_assoc_raw:
+ shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
+by (cases i, cases j, cases k)
+ (simp add: mult algebra_simps)
+
+lemma mult_sym_raw:
+ shows "mult_raw i j \<approx> mult_raw j i"
+by (cases i, cases j) (simp)
+
+lemma mult_one_raw:
+ shows "mult_raw (1, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma mult_plus_comm_raw:
+ shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
+by (cases i, cases j, cases k)
+ (simp add: mult algebra_simps)
+
+lemma one_zero_distinct:
+ shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
+ by simp
+
+text{*The integers form a @{text comm_ring_1}*}
+
+
+ML {* val qty = @{typ "int"} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
+
+instance int :: comm_ring_1
+proof
+ 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 *})
+ done
+ show "i + j = j + i"
+ unfolding add_int_def
+ apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+ done
+ show "0 + i = (i::int)"
+ unfolding add_int_def Zero_int_def
+ apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "- i + i = 0"
+ unfolding add_int_def minus_int_def Zero_int_def
+ apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "i - j = i + - j"
+ by (simp add: diff_int_def)
+ show "(i * j) * k = i * (j * k)"
+ unfolding mult_int_def
+ apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "i * j = j * i"
+ unfolding mult_int_def
+ apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "1 * i = i"
+ unfolding mult_int_def One_int_def
+ apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "(i + j) * k = i * k + j * k"
+ unfolding mult_int_def add_int_def
+ apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
+ apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "0 \<noteq> (1::int)"
+ unfolding Zero_int_def One_int_def
+ apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
+ defer
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+qed
+
+term of_nat
+thm of_nat_def
+
+lemma int_def: "of_nat m = ABS_int (m, 0)"
+apply(induct m)
+apply(simp add: Zero_int_def zero_qnt_def)
+apply(simp)
+apply(simp add: add_int_def One_int_def)
+apply(simp add: plus_qnt_def one_qnt_def)
+oops
+
+lemma le_antisym_raw:
+ shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
+by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+ shows "le_raw i i"
+by (cases i) (simp)
+
+lemma le_trans_raw:
+ shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
+by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+ shows "le_raw i j \<or> le_raw j i"
+by (cases i, cases j)
+ (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+ 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 *})
+ 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 *})
+ 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 *})
+ 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 *})
+ done
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+ by intro_classes
+ (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_raw:
+ shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
+by (cases i, cases j, cases k) (simp)
+
+
+instance int :: pordered_cancel_ab_semigroup_add
+proof
+ 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 *})
+ done
+qed
+
+lemma test:
+ "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
+ \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
+apply(cases i, cases j, cases k)
+apply(auto simp add: mult algebra_simps)
+sorry
+
+
+text{*The integers form an ordered integral domain*}
+instance int :: ordered_idom
+proof
+ 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 {* procedure_tac @{context} @{thm test} 1 *})
+ defer
+ apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+ defer
+ apply(tactic {* clean_tac @{context} 1*})
+ sorry
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+ by (simp only: zabs_def)
+ show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
+qed
+
+instance int :: lordered_ring
+proof
+ fix k :: int
+ show "abs k = sup k (- k)"
+ by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+qed
+
+lemmas int_distrib =
+ left_distrib [of "z1::int" "z2" "w", standard]
+ right_distrib [of "w::int" "z1" "z2", standard]
+ left_diff_distrib [of "z1::int" "z2" "w", standard]
+ right_diff_distrib [of "w::int" "z1" "z2", standard]
+
+
+subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
+
+(*
+context ring_1
+begin
+
+
+definition
+ of_int :: "int \<Rightarrow> 'a"
+where
+ "of_int
+*)
+
+
+subsection {* Binary representation *}
+
+text {*
+ This formalization defines binary arithmetic in terms of the integers
+ rather than using a datatype. This avoids multiple representations (leading
+ zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
+ int_of_binary}, for the numerical interpretation.
+
+ The representation expects that @{text "(m mod 2)"} is 0 or 1,
+ even if m is negative;
+ For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+ @{text "-5 = (-3)*2 + 1"}.
+
+ This two's complement binary representation derives from the paper
+ "An Efficient Representation of Arithmetic for Term Rewriting" by
+ Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
+ Springer LNCS 488 (240-251), 1991.
+*}
+
+subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
+
+definition
+ Pls :: int where
+ [code del]: "Pls = 0"
+
+definition
+ Min :: int where
+ [code del]: "Min = - 1"
+
+definition
+ Bit0 :: "int \<Rightarrow> int" where
+ [code del]: "Bit0 k = k + k"
+
+definition
+ Bit1 :: "int \<Rightarrow> int" where
+ [code del]: "Bit1 k = 1 + k + k"
+
+class number = -- {* for numeric types: nat, int, real, \dots *}
+ fixes number_of :: "int \<Rightarrow> 'a"
+
+use "~~/src/HOL/Tools/numeral.ML"
+
+syntax
+ "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
+
+use "~~/src/HOL/Tools/numeral_syntax.ML"
+setup NumeralSyntax.setup
+
+abbreviation
+ "Numeral0 \<equiv> number_of Pls"
+
+abbreviation
+ "Numeral1 \<equiv> number_of (Bit1 Pls)"
+
+lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
+ -- {* Unfold all @{text let}s involving constants *}
+ unfolding Let_def ..
+
+definition
+ succ :: "int \<Rightarrow> int" where
+ [code del]: "succ k = k + 1"
+
+definition
+ pred :: "int \<Rightarrow> int" where
+ [code del]: "pred k = k - 1"
+
+lemmas
+ max_number_of [simp] = max_def
+ [of "number_of u" "number_of v", standard, simp]
+and
+ min_number_of [simp] = min_def
+ [of "number_of u" "number_of v", standard, simp]
+ -- {* unfolding @{text minx} and @{text max} on numerals *}
+
+lemmas numeral_simps =
+ succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
+
+text {* Removal of leading zeroes *}
+
+lemma Bit0_Pls [simp, code_post]:
+ "Bit0 Pls = Pls"
+ unfolding numeral_simps by simp
+
+lemma Bit1_Min [simp, code_post]:
+ "Bit1 Min = Min"
+ unfolding numeral_simps by simp
+
+lemmas normalize_bin_simps =
+ Bit0_Pls Bit1_Min
--- a/LamEx.thy Sun Dec 06 06:39:32 2009 +0100
+++ b/LamEx.thy Sun Dec 06 06:41:52 2009 +0100
@@ -80,6 +80,35 @@
where
"fv \<equiv> rfv"
+ML {*
+local
+ fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
+ fun pp_list xs = Pretty.list "[" "]" xs
+ fun pp_str s = Pretty.str s
+ fun pp_qstr s = Pretty.quote (pp_str s)
+ fun pp_int i = pp_str (string_of_int i)
+ fun pp_sort S = pp_list (map pp_qstr S)
+ fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
+in
+fun raw_pp_typ (TVar ((a, i), S)) =
+ pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
+ | raw_pp_typ (TFree (a, S)) =
+ pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
+ | raw_pp_typ (Type (a, tys)) =
+ pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
+end *}
+
+ML {*
+PolyML.addPrettyPrinter
+ (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)
+
+*}
+
+typ "name set"
+typ "name => bool"
+
+ML {* @{typ "name set"} *}
+
thm fv_def
(* definition of overloaded permutation function *)
--- a/QuotMain.thy Sun Dec 06 06:39:32 2009 +0100
+++ b/QuotMain.thy Sun Dec 06 06:41:52 2009 +0100
@@ -740,12 +740,17 @@
then rtrm
else mk_repabs lthy (T, T') rtrm
- | (Const (_, T), Const (_, T')) =>
- if T = T'
+ | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+ (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+ | (_, Const (_, T')) =>
+ let
+ val rty = fastype_of rtrm
+ in
+ if rty = T'
then rtrm
- else mk_repabs lthy (T, T') rtrm
-
- | (_, Const (@{const_name "op ="}, _)) => rtrm
+ else mk_repabs lthy (rty, T') rtrm
+ end
| _ => raise (LIFT_MATCH "injection")
*}
@@ -773,6 +778,12 @@
resolve_tac (quotient_rules_get ctxt)])
*}
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
definition
"QUOT_TRUE x \<equiv> True"
@@ -1041,92 +1052,77 @@
*}
ML {*
-fun lambda_allex_prs_simple_conv ctxt ctrm =
+fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
- let
- val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
- val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
- val thy = ProofContext.theory_of ctxt;
- val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
- val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
- val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
- val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
- val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
- 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;
- in
- Conv.rewr_conv ti ctrm
- end
+ ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
+ val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
+ val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+ 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)))*)
+ in
+ Conv.rewr_conv ti ctrm
+ end
| _ => Conv.all_conv ctrm
*}
ML {*
-val lambda_allex_prs_conv =
- More_Conv.top_conv lambda_allex_prs_simple_conv
+val lambda_prs_conv =
+ More_Conv.top_conv lambda_prs_simple_conv
-fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
*}
(*
- Cleaning the theorem consists of 6 kinds of rewrites.
+ Cleaning the theorem consists of three rewriting steps.
The first two need to be done before fun_map is unfolded
- - lambda_prs:
+ 1) lambda_prs:
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
- - all_prs (and the same for exists: ex_prs)
- \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f
-
- - Rewriting with definitions from the argument defs
- NewConst ----> (rep ---> abs) oldConst
+ Implemented as conversion since it is not a pattern.
- - Quotient_rel_rep:
- Rel (Rep x) (Rep y) ----> x = y
+ 2) all_prs (the same for exists):
+ Ball (Respects R) ((abs ---> id) f) ----> All f
- - ABS_REP
- Abs (Rep x) ----> x
+ Rewriting with definitions from the argument defs
+ (rep ---> abs) oldConst ----> newconst
- - id_simps; fun_map.simps
+ 3) Quotient_rel_rep:
+ Rel (Rep x) (Rep y) ----> x = y
- The first one is implemented as a conversion (fast).
- The second one is an EqSubst (slow).
- The rest are a simp_tac and are fast.
+ Quotient_abs_rep:
+ Abs (Rep x) ----> x
+
+ id_simps; fun_map.simps
*)
ML {*
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
fun clean_tac lthy =
let
val thy = ProofContext.theory_of lthy;
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ (* FIXME: shouldn't the definitions already be varified? *)
val thms1 = @{thms all_prs ex_prs} @ defs
val thms2 = @{thms eq_reflection[OF fun_map.simps]}
@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
- fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
- (* FIXME: use of someting smaller than HOL_basic_ss *)
+ fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
+ (* FIXME: use of someting smaller than HOL_basic_ss *)
in
- EVERY' [
- (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *)
- NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
-
- (* Ball (Respects R) ((abs ---> id) f) ----> All f *)
- NDT lthy "b" (simp_tac (simp_ctxt thms1)),
-
- (* NewConst -----> (rep ---> abs) oldConst *)
- (* abs (rep x) -----> x *)
- (* R (Rep x) (Rep y) -----> x = y *)
- (* id_simps; fun_map.simps *)
- NDT lthy "c" (simp_tac (simp_ctxt thms2)),
-
- (* final step *)
- NDT lthy "d" (TRY o rtac refl)
- ]
+ EVERY' [lambda_prs_tac lthy,
+ simp_tac (simps thms1),
+ simp_tac (simps thms2),
+ TRY o rtac refl]
end
*}