diff -r 000000000000 -r ebe0ea8fe247 QuotMain.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotMain.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,559 @@
+theory QuotMain
+imports QuotScript QuotList
+begin
+
+locale QUOT_TYPE =
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+  assumes equiv: "EQUIV R"
+  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
+  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+begin 
+
+definition
+  "ABS x \<equiv> Abs (R x)"
+
+definition
+  "REP a = Eps (Rep a)"
+
+lemma lem9: 
+  shows "R (Eps (R x)) = R x"
+proof -
+  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+  then have "R x (Eps (R x))" by (rule someI)
+  then show "R (Eps (R x)) = R x" 
+    using equiv unfolding EQUIV_def by simp
+qed
+
+theorem thm10:
+  shows "ABS (REP a) = a"
+unfolding ABS_def REP_def
+proof -
+  from rep_prop 
+  obtain x where eq: "Rep a = R x" by auto
+  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+  also have "\<dots> = Abs (R x)" using lem9 by simp
+  also have "\<dots> = Abs (Rep a)" using eq by simp
+  also have "\<dots> = a" using rep_inverse by simp
+  finally
+  show "Abs (R (Eps (Rep a))) = a" by simp
+qed
+
+lemma REP_refl: 
+  shows "R (REP a) (REP a)"
+unfolding REP_def
+by (simp add: equiv[simplified EQUIV_def])
+
+lemma lem7:
+  "(R x = R y) = (Abs (R x) = Abs (R y))"
+apply(rule iffI)
+apply(simp)
+apply(drule rep_inject[THEN iffD2])
+apply(simp add: abs_inverse)
+done
+  
+theorem thm11:
+  shows "R r r' = (ABS r = ABS r')"
+unfolding ABS_def
+by (simp only: equiv[simplified EQUIV_def] lem7)
+
+lemma QUOTIENT:
+  "QUOTIENT R ABS REP"
+apply(unfold QUOTIENT_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equiv[simplified EQUIV_def])
+done
+
+end
+
+ML {*
+  Variable.variant_frees
+*}
+
+
+section {* type definition for the quotient type *}
+
+ML {*
+(* constructs the term \<lambda>(c::ty\<Rightarrow>bool). \<exists>x. c = rel x *)
+fun typedef_term rel ty lthy =
+let 
+  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] 
+               |> Variable.variant_frees lthy [rel]
+               |> map Free
+in
+  lambda c  
+    ((HOLogic.exists_const ty) $ 
+      (lambda x (HOLogic.mk_eq (c, (rel $ x)))))
+end
+*}
+
+ML {*
+val typedef_tac =  
+  EVERY1 [rewrite_goal_tac @{thms mem_def},
+          rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
+*}
+
+ML {*
+(* makes the new type definitions *)
+fun typedef_make (qty_name, rel, ty) lthy =
+  LocalTheory.theory_result
+  (TypedefPackage.add_typedef false NONE 
+     (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
+       (typedef_term rel ty lthy)
+         NONE typedef_tac) lthy
+*}
+
+text {* proves the QUOTIENT theorem for the new type *}
+ML {*
+fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = 
+let
+  val rep_thm = #Rep typedef_info
+  val rep_inv = #Rep_inverse typedef_info
+  val abs_inv = #Abs_inverse typedef_info
+  val rep_inj = #Rep_inject typedef_info
+
+  val ss = HOL_basic_ss addsimps @{thms mem_def}
+  val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
+  val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
+in
+  EVERY1 [rtac @{thm QUOT_TYPE.intro},
+          rtac equiv_thm, 
+          rtac rep_thm_simpd, 
+          rtac rep_inv, 
+          rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
+          rtac rep_inj]
+end
+*}
+
+ML {* 
+fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
+let
+  val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
+  val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+             |> Syntax.check_term lthy
+in
+  Goal.prove lthy [] [] goal
+    (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
+end
+*}
+
+ML {*
+fun typedef_quotient_thm_tac defs quot_type_thm =
+  EVERY1 [K (rewrite_goals_tac defs), 
+          rtac @{thm QUOT_TYPE.QUOTIENT}, 
+          rtac quot_type_thm]
+*}
+
+ML {* 
+fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
+let
+  val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
+  val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
+             |> Syntax.check_term lthy
+in
+  Goal.prove lthy [] [] goal
+    (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
+end
+*}
+
+text {* two wrappers for define and note *}
+ML {* 
+fun make_def (name, mx, trm) lthy =
+let   
+  val ((trm, (_ , thm)), lthy') = 
+     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
+in
+  ((trm, thm), lthy')
+end
+*}
+
+ML {*
+fun reg_thm (name, thm) lthy = 
+let
+  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
+in
+  (thm',lthy')
+end
+*}
+
+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
+
+  (* abs and rep functions *)
+  val abs_ty = #abs_type typedef_info
+  val rep_ty = #rep_type typedef_info
+  val abs_name = #Abs_name typedef_info
+  val rep_name = #Rep_name typedef_info
+  val abs = Const (abs_name, rep_ty --> abs_ty)
+  val rep = Const (rep_name, abs_ty --> rep_ty)
+
+  (* ABS and REP definitions *)
+  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
+  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
+  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) 
+  val REP_trm = Syntax.check_term lthy' (REP_const $ rep) 
+  val ABS_name = Binding.prefix_name "ABS_" qty_name
+  val REP_name = Binding.prefix_name "REP_" qty_name  
+  val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 
+         lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
+               ||>> make_def (REP_name, NoSyn, REP_trm)
+
+  (* 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
+
+  (* quotient theorem *)
+  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
+
+in
+  lthy'' 
+  |> reg_thm (quot_thm_name, quot_thm)  
+  ||>> reg_thm (quotient_thm_name, quotient_thm)
+end
+*}
+
+section {* various tests for quotient types*}
+datatype trm =
+  var  "nat" 
+| app  "trm" "trm"
+| lam  "nat" "trm"
+  
+consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+axioms r_eq: "EQUIV R"
+
+local_setup {*
+  typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
+*}
+
+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 *}
+datatype 'a my = foo
+consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
+axioms rmy_eq: "EQUIV Rmy"
+
+term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
+
+datatype 'a trm' =
+  var'  "'a" 
+| app'  "'a trm'" "'a trm'"
+| lam'  "'a" "'a trm'"
+  
+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
+*}
+
+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"
+| ap "t list"
+| lm "string" "t"
+
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
+axioms t_eq: "EQUIV Rt"
+
+local_setup {*
+  typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
+*}
+
+section {* lifting of constants *}
+
+text {* information about map-functions for type-constructor *}
+ML {*
+type typ_info = {mapfun: string}
+
+local
+  structure Data = GenericDataFun
+  (type T = typ_info Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   fun merge _ = Symtab.merge (K true))
+in
+ val lookup = Symtab.lookup o Data.get
+ fun update k v = Data.map (Symtab.update (k, v)) 
+end
+*}
+
+(* mapfuns for some standard types *)
+setup {*
+    Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
+ #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
+ #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
+*}
+
+ML {* lookup (Context.Proof @{context}) @{type_name list} *}
+
+ML {*
+datatype abs_or_rep = abs | rep
+
+fun get_fun abs_or_rep rty qty lthy ty = 
+let
+  val qty_name = Long_Name.base_name (fst (dest_Type qty))
+  
+  fun get_fun_aux s fs_tys =
+  let
+    val (fs, tys) = split_list fs_tys
+    val (otys, ntys) = split_list tys 
+    val oty = Type (s, otys)
+    val nty = Type (s, ntys)
+    val ftys = map (op -->) tys
+  in
+   (case (lookup (Context.Proof lthy) s) of 
+      SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
+    | NONE => raise ERROR ("no map association for type " ^ s))
+  end
+
+  fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
+    | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
+in
+  if ty = qty
+  then (get_const abs_or_rep)
+  else (case ty of
+          TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))
+        | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))
+        | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)  
+        | _ => raise ERROR ("no variables")
+       )
+end
+*}
+
+ML {*
+fun get_const_def nconst oconst rty qty lthy =
+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
+
+  val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
+  val abs_fn  = (fst o get_fun abs rty qty lthy) res_ty
+
+in
+  map (op $) (rep_fns ~~ fresh_args)
+  |> curry list_comb oconst
+  |> curry (op $) abs_fn
+  |> fold_rev lambda fresh_args
+end
+*}
+
+ML {*
+fun exchange_ty rty qty ty = 
+  if ty = rty then qty
+  else 
+    (case ty of
+       Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
+      | _ => ty)
+*}
+
+ML {*
+fun make_const_def nconst_name oconst mx rty qty lthy = 
+let
+  val oconst_ty = fastype_of oconst
+  val nconst_ty = exchange_ty rty qty oconst_ty
+  val nconst = Const (nconst_name, nconst_ty)
+  val def_trm = get_const_def nconst oconst rty qty lthy
+in
+  make_def (Binding.name nconst_name, mx, def_trm) lthy
+end  
+*}
+
+text {* a test with functions *}
+datatype 'a t' =
+  vr' "string"
+| ap' "('a t') * ('a t')"
+| lm' "'a" "string \<Rightarrow> ('a t')"
+
+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
+*}
+
+local_setup {*
+  make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+  make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+  make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+thm VR'_def
+thm AP'_def
+thm LM'_def
+term LM' 
+term VR'
+term AP'
+
+text {* finite set example *}
+
+inductive 
+  list_eq ("_ \<approx> _")
+where
+  "a#b#xs \<approx> b#a#xs"
+| "[] \<approx> []"
+| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
+| "a#a#xs \<approx> a#xs"
+| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
+| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
+
+lemma list_eq_sym:
+  shows "xs \<approx> xs"
+apply(induct xs)
+apply(auto intro: list_eq.intros)
+done
+
+lemma equiv_list_eq:
+  shows "EQUIV list_eq"
+unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+apply(auto intro: list_eq.intros list_eq_sym)
+done
+
+local_setup {*
+  typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
+*}
+
+typ "'a fset"
+thm "Rep_fset"
+
+local_setup {*
+  make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Nil 
+term EMPTY
+
+local_setup {*
+  make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Cons 
+term INSERT
+
+local_setup {*
+  make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term append 
+term UNION
+thm QUOTIENT_fset
+thm Insert_def
+
+fun 
+  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
+where
+  m1: "(x memb []) = False"
+| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+
+
+local_setup {*
+  make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term membship
+term IN
+
+lemma
+  shows "IN x EMPTY = False"
+unfolding IN_def EMPTY_def
+apply(auto)
+thm Rep_fset_inverse
+
+
+
+
+
+
+
+
+
+
+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)
+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)
+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))"
+
+
+
+
+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