
diff -r 8d0fad689dce -r e0b4bca46c6a QuotMain.thy
--- 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




