--- a/QuotMain.thy Fri Aug 28 17:12:19 2009 +0200
+++ b/QuotMain.thy Tue Sep 15 09:59:56 2009 +0200
@@ -108,11 +108,12 @@
end
*}
+(*
ML {*
- typedef_term @{term R} @{typ "nat"} @{context}
+ typedef_term @{term R} @{typ "nat"} @{context}
|> Syntax.string_of_term @{context}
|> writeln
-*}
+*}*)
ML {*
val typedef_tac =
@@ -199,6 +200,13 @@
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
@@ -208,7 +216,32 @@
end
*}
-ML {*
+ML {*
+val no_vars = Thm.rule_attribute (fn context => fn th =>
+ let
+ val ctxt = Variable.set_body false (Context.proof_of context);
+ val ((_, [th']), _) = Variable.import true [th] ctxt;
+ 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 *)
@@ -233,6 +266,11 @@
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
@@ -241,29 +279,76 @@
val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+ (* interpretation *)
+ val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+ val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
+ val eqn1i = Thm.prop_of (symmetric eqn1pre)
+ val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
+ val eqn2i = Thm.prop_of (symmetric eqn2pre)
+
+ val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
+ val exp_term = Morphism.term exp_morphism;
+ 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"*))
+ 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),
+ Expression.Named [
+ ("R", rel),
+ ("Abs", abs),
+ ("Rep", rep)
+ ]))]
in
- lthy''
- |> reg_thm (quot_thm_name, quot_thm)
+ lthy''''
+ |> reg_thm (quot_thm_name, quot_thm)
||>> reg_thm (quotient_thm_name, quotient_thm)
+ ||> LocalTheory.theory (fn thy =>
+ let
+ val global_eqns = map exp_term [eqn2i, eqn1i];
+ 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"
| app "trm" "trm"
| lam "nat" "trm"
-axiomatization R :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
- r_eq: "EQUIV R"
+axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
+ r_eq: "EQUIV RR"
ML {*
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 {*
- typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
+ fn lthy =>
+ Toplevel.program (fn () =>
+ exception_trace (
+ fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy)
+ )
+ )
*}
+print_theorems
+
+(*thm QUOT_TYPE_I_qtrm.thm11*)
+
term Rep_qtrm
term REP_qtrm
@@ -289,16 +374,22 @@
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
axioms r_eq': "EQUIV R'"
+
local_setup {*
- typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
+ fn lthy =>
+ exception_trace
+ (fn () => (typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd) lthy)
*}
+print_theorems
+
term ABS_qtrm'
term REP_qtrm'
thm QUOT_TYPE_qtrm'
thm QUOTIENT_qtrm'
thm Rep_qtrm'
+
text {* a test with lists of terms *}
datatype t =
vr "string"
@@ -387,7 +478,7 @@
let
val ty = fastype_of nconst
val (arg_tys, res_ty) = strip_type ty
-
+
val fresh_args = arg_tys |> map (pair "x")
|> Variable.variant_frees lthy [nconst, oconst]
|> map Free
@@ -439,7 +530,7 @@
thm VR_def
thm AP_def
thm LM_def
-term LM
+term LM
term VR
term AP
@@ -453,10 +544,12 @@
consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
axioms t_eq': "EQUIV Rt'"
+
local_setup {*
typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
*}
+print_theorems
local_setup {*
make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
@@ -473,13 +566,14 @@
thm VR'_def
thm AP'_def
thm LM'_def
-term LM'
+term LM'
term VR'
term AP'
+
text {* finite set example *}
print_syntax
-inductive
+inductive
list_eq (infix "\<approx>" 50)
where
"a#b#xs \<approx> b#a#xs"
@@ -505,6 +599,8 @@
typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
*}
+print_theorems
+
typ "'a fset"
thm "Rep_fset"
@@ -512,7 +608,7 @@
make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
-term Nil
+term Nil
term EMPTY
thm EMPTY_def
@@ -521,7 +617,7 @@
make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
-term Cons
+term Cons
term INSERT
thm INSERT_def
@@ -543,38 +639,7 @@
thm QUOTIENT_fset
-(* This code builds the interpretation from ML level, currently only
- for fset *)
-
-ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN
- simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def [symmetric]}) 1 THEN
- simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def [symmetric]}) 1) *}
-ML {* val mthdt = Method.Basic (fn _ => mthd) *}
-ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *}
-ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true),
- Expression.Named [
- ("R",@{term list_eq}),
- ("Abs",@{term Abs_fset}),
- ("Rep",@{term Rep_fset})
- ]))] *}
-ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *}
-ML {* val eqn1i = (bindd, @{prop "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"}) *}
-ML {* val eqn2i = (bindd, @{prop "QUOT_TYPE.REP Rep_fset = REP_fset"}) *}
-setup {* fn thy => ProofContext.theory_of
- (bymt (Expression.interpretation (exp_i, []) [eqn2i,eqn1i] thy)) *}
-
-(* It is eqivalent to the below:
-
-interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset
- where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"
- and "QUOT_TYPE.REP Rep_fset = REP_fset"
- unfolding ABS_fset_def REP_fset_def
- apply (rule QUOT_TYPE_fset)
- apply (simp only: ABS_fset_def[symmetric])
- apply (simp only: REP_fset_def[symmetric])
- done
-*)
-
+thm QUOT_TYPE_I_fset.thm11
fun
@@ -628,7 +693,7 @@
unfolding IN_def EMPTY_def
apply(rule_tac f="(op =) False" in arg_cong)
apply(rule mem_respects)
-apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply(rule list_eq.intros)
done
@@ -654,7 +719,7 @@
done
lemma append_respects_fst:
- assumes a : "list_eq l1 l2"
+ assumes a : "list_eq l1 l2"
shows "list_eq (l1 @ s) (l2 @ s)"
using a
apply(induct)
@@ -674,19 +739,19 @@
unfolding UNION_def EMPTY_def INSERT_def
apply(rule_tac f="(op &)" in arg_cong2)
apply(rule_tac f="(op =)" in arg_cong2)
- apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+ apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
apply(rule append_respects_fst)
- apply(simp only:QUOT_TYPE_fset_i.REP_ABS_rsp)
+ apply(simp only:QUOT_TYPE_I_fset.REP_ABS_rsp)
apply(rule list_eq_sym)
apply(simp)
apply(rule_tac f="(op =)" in arg_cong2)
- apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+ apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
apply(rule append_respects_fst)
- apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+ apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply(rule list_eq_sym)
- apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+ apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
apply(rule list_eq.intros(5))
- apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+ apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply(rule list_eq_sym)
done
@@ -695,7 +760,7 @@
(UNION EMPTY s = s) &
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
apply (simp add: yyy)
- apply (rule QUOT_TYPE_fset_i.thm10)
+ apply (rule QUOT_TYPE_I_fset.thm10)
done
ML {*
@@ -730,13 +795,6 @@
HOLogic.mk_eq ((build_aux concl), concl)
end *}
-ML {*
-val no_vars = Thm.rule_attribute (fn context => fn th =>
- let
- val ctxt = Variable.set_body false (Context.proof_of context);
- val ((_, [th']), _) = Variable.import true [th] ctxt;
- in th' end);
-*}
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
@@ -756,7 +814,7 @@
apply(rule_tac f="(op =)" in arg_cong2)
unfolding IN_def EMPTY_def
apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (simp_all)
apply (rule list_eq_sym)
done
@@ -786,13 +844,13 @@
unfolding IN_def
apply (rule_tac mem_respects)
unfolding INSERT_def
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule cons_preserves)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule list_eq_sym)
apply(rule_tac f="(op \<or>)" in arg_cong2)
apply (simp)
apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule list_eq_sym)
done