--- a/QuotMain.thy Tue Sep 15 10:00:34 2009 +0200
+++ b/QuotMain.thy Tue Sep 15 11:31:35 2009 +0200
@@ -2,12 +2,6 @@
imports QuotScript QuotList Prove
begin
-(*
-prove {* @{prop "True"} *}
-apply(rule TrueI)
-done
-*)
-
locale QUOT_TYPE =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -90,11 +84,6 @@
section {* type definition for the quotient type *}
ML {*
-Variable.variant_frees
-*}
-
-
-ML {*
(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
fun typedef_term rel ty lthy =
let
@@ -200,19 +189,12 @@
end
*}
-(*
-locale foo = fixes x :: nat
-begin
-
-ML {* make_def (@{binding foo}, NoSyn, @{term "x + x"}) @{context} *}
-*)
-
ML {*
fun reg_thm (name, thm) lthy =
let
val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
in
- (thm',lthy')
+ (thm', lthy')
end
*}
@@ -224,28 +206,11 @@
in th' end);
*}
-ML ProofContext.theory_of
-
-ML Expression.interpretation
-
-ML {*
-fun my_print_tac ctxt thm =
-let
- val _ = tracing (Display.string_of_thm ctxt thm)
-in
- Seq.single thm
-end *}
-
-ML LocalTheory.theory_result
-
-
-ML {* Binding.str_of @{binding foo} *}
-
ML {*
fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
let
(* generates typedef *)
- val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
+ val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
(* abs and rep functions *)
val abs_ty = #abs_type typedef_info
@@ -266,11 +231,6 @@
lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
||>> make_def (REP_name, NoSyn, REP_trm)
- (* REMOVE VARIFY *)
- val _ = tracing (Syntax.string_of_typ lthy' (type_of ABS_trm))
- val _ = tracing (Syntax.string_of_typ lthy' (type_of REP_trm))
- val _ = tracing (Syntax.string_of_typ lthy' (type_of rel))
-
(* quot_type theorem *)
val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
@@ -291,11 +251,10 @@
val exp = Morphism.thm exp_morphism;
val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
- ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))
- (*THEN print_tac "Hello"*))
+ ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
val mthdt = Method.Basic (fn _ => mthd)
val bymt = Proof.global_terminal_proof (mthdt, NONE)
- val exp_i = [(@{const_name QUOT_TYPE},((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+ val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
Expression.Named [
("R", rel),
("Abs", abs),
@@ -308,14 +267,13 @@
||> LocalTheory.theory (fn thy =>
let
val global_eqns = map exp_term [eqn2i, eqn1i];
+ (* Not sure if the following context should not be used *)
val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
-(* val _ = tracing (Syntax.string_of_typ lthy'''' (type_of (fst (Logic.dest_equals (exp_term eqn1i)))));*)
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
end
*}
-
section {* various tests for quotient types*}
datatype trm =
var "nat"
@@ -329,26 +287,9 @@
typedef_main
*}
-(*ML {*
- val lthy = @{context};
- val qty_name = @{binding "qtrm"}
- val rel = @{term "RR"}
- val ty = @{typ trm}
- val equiv_thm = @{thm r_eq}
-*}*)
-
local_setup {*
- fn lthy =>
- Toplevel.program (fn () =>
- exception_trace (
- fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy)
- )
- )
+ typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
*}
-print_theorems
-
-(*thm QUOT_TYPE_I_qtrm.thm11*)
-
term Rep_qtrm
term REP_qtrm
@@ -357,6 +298,9 @@
thm QUOT_TYPE_qtrm
thm QUOTIENT_qtrm
+(* Test interpretation *)
+thm QUOT_TYPE_I_qtrm.thm11
+
thm Rep_qtrm
text {* another test *}
@@ -376,9 +320,7 @@
local_setup {*
- fn lthy =>
- exception_trace
- (fn () => (typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd) lthy)
+ typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
*}
print_theorems
@@ -782,7 +724,7 @@
fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
| build_aux (f $ a) =
let
- val (f,args) = strip_comb (f $ a)
+ val (f, args) = strip_comb (f $ a)
val _ = writeln (Syntax.string_of_term @{context} f)
in
(if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
@@ -795,22 +737,20 @@
HOLogic.mk_eq ((build_aux concl), concl)
end *}
+ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
+ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
+ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
+ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
+ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
*}
-ML {* val emptyt = symmetric @{thm EMPTY_def} *}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
-
-ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
-ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *}
-
-(*theorem "(IN x EMPTY = False) = (x memb [] = False)"*)
-
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
apply(rule_tac f="(op =)" in arg_cong2)
unfolding IN_def EMPTY_def
apply (rule_tac mem_respects)
@@ -824,22 +764,17 @@
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
*}
-ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
-ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
-ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
-ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}
thm m2
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
*}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *}
-ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *}
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
apply(rule_tac f="(op =)" in arg_cong2)
unfolding IN_def
apply (rule_tac mem_respects)