--- a/QuotMain.thy Tue Aug 18 14:04:51 2009 +0200
+++ b/QuotMain.thy Thu Aug 20 10:31:44 2009 +0200
@@ -60,6 +60,12 @@
unfolding ABS_def
by (simp only: equiv[simplified EQUIV_def] lem7)
+lemma REP_ABS_rsp:
+ shows "R f g \<Longrightarrow> R f (REP (ABS g))"
+apply(subst thm11)
+apply(simp add: thm10 thm11)
+done
+
lemma QUOTIENT:
"QUOTIENT R ABS REP"
apply(unfold QUOTIENT_def)
@@ -74,6 +80,11 @@
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
@@ -88,6 +99,12 @@
*}
ML {*
+ typedef_term @{term R} @{typ "nat"} @{context}
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
val typedef_tac =
EVERY1 [rewrite_goal_tac @{thms mem_def},
rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
@@ -103,7 +120,7 @@
NONE typedef_tac) lthy
*}
-text {* proves the QUOTIENT theorem for the new type *}
+text {* proves the QUOT_TYPE theorem for the new type *}
ML {*
fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
let
@@ -125,6 +142,11 @@
end
*}
+term QUOT_TYPE
+ML {* HOLogic.mk_Trueprop *}
+ML {* Goal.prove *}
+ML {* Syntax.check_term *}
+
ML {*
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
let
@@ -225,16 +247,21 @@
consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
axioms r_eq: "EQUIV R"
+ML {*
+ typedef_main
+*}
+
local_setup {*
typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
*}
term Rep_qtrm
+term REP_qtrm
term Abs_qtrm
term ABS_qtrm
-term REP_qtrm
thm QUOT_TYPE_qtrm
thm QUOTIENT_qtrm
+
thm Rep_qtrm
text {* another test *}
@@ -300,6 +327,7 @@
#> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}})
*}
+
ML {* lookup (Context.Proof @{context}) @{type_name list} *}
ML {*
@@ -337,6 +365,14 @@
*}
ML {*
+ get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+
+ML {*
fun get_const_def nconst oconst rty qty lthy =
let
val ty = fastype_of nconst
@@ -378,6 +414,26 @@
end
*}
+local_setup {*
+ make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+*}
+
+local_setup {*
+ make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+*}
+
+local_setup {*
+ make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+*}
+
+thm VR_def
+thm AP_def
+thm LM_def
+term LM
+term VR
+term AP
+
+
text {* a test with functions *}
datatype 'a t' =
vr' "string"
@@ -391,6 +447,7 @@
typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
*}
+
local_setup {*
make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}
@@ -447,6 +504,8 @@
term Nil
term EMPTY
+thm EMPTY_def
+
local_setup {*
make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
@@ -454,6 +513,7 @@
term Cons
term INSERT
+thm INSERT_def
local_setup {*
make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
@@ -461,8 +521,9 @@
term append
term UNION
+thm UNION_def
+
thm QUOTIENT_fset
-thm Insert_def
fun
membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
@@ -470,6 +531,15 @@
m1: "(x memb []) = False"
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+lemma mem_respects:
+ fixes z::"nat"
+ assumes a: "list_eq x y"
+ shows "z memb x = z memb y"
+using a
+apply(induct)
+apply(auto)
+done
+
local_setup {*
make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
@@ -477,78 +547,39 @@
term membship
term IN
-
-lemma
- shows "IN x EMPTY = False"
-unfolding IN_def EMPTY_def
-apply(auto)
-thm Rep_fset_inverse
+thm IN_def
-
-
-
-
-
-
-
+lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
+thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
-
-text {* old stuff *}
-
-
-lemma QUOT_TYPE_qtrm_old:
- "QUOT_TYPE R Abs_qtrm Rep_qtrm"
-apply(rule QUOT_TYPE.intro)
-apply(rule r_eq)
-apply(rule Rep_qtrm[simplified mem_def])
-apply(rule Rep_qtrm_inverse)
-apply(rule Abs_qtrm_inverse[simplified mem_def])
-apply(rule exI)
-apply(rule refl)
-apply(rule Rep_qtrm_inject)
+lemma yy:
+ shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
+unfolding IN_def EMPTY_def
+apply(rule_tac f="(op =) False" in arg_cong)
+apply(rule mem_respects)
+apply(unfold REP_fset_def ABS_fset_def)
+apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(rule list_eq.intros)
done
-definition
- "ABS_qtrm_old \<equiv> QUOT_TYPE.ABS R Abs_qtrm"
-
-definition
- "REP_qtrm_old \<equiv> QUOT_TYPE.REP Rep_qtrm"
-
-lemma
- "QUOTIENT R (ABS_qtrm) (REP_qtrm)"
-apply(simp add: ABS_qtrm_def REP_qtrm_def)
-apply(rule QUOT_TYPE.QUOTIENT)
-apply(rule QUOT_TYPE_qtrm)
+lemma
+ shows "IN (x::nat) EMPTY = False"
+using m1
+apply -
+apply(rule yy[THEN iffD1, symmetric])
+apply(simp)
done
-term "var"
-term "app"
-term "lam"
-
-definition
- "VAR x \<equiv> ABS_qtrm (var x)"
-
-definition
- "APP t1 t2 \<equiv> ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))"
-
-definition
- "LAM x t \<equiv> ABS_qtrm (lam x (REP_qtrm t))"
-
-
-
+lemma
+ shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
+ ((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
+unfolding IN_def INSERT_def
+apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
+apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
+apply(rule mem_respects)
+apply(rule list_eq.intros(3))
+apply(unfold REP_fset_def ABS_fset_def)
+apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(rule list_eq_sym)
+done
-definition
- "VR x \<equiv> ABS_qt (vr x)"
-
-definition
- "AP ts \<equiv> ABS_qt (ap (map REP_qt ts))"
-
-definition
- "LM x t \<equiv> ABS_qt (lm x (REP_qt t))"
-
-(* for printing types *)
-ML {*
-fun setmp_show_all_types f =
- setmp show_all_types
- (! show_types orelse ! show_sorts orelse ! show_all_types) f
-*}
\ No newline at end of file