Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 277 37636f2b1c19
parent 275 34ad627ac5d5
child 282 e9212a4a44be
equal deleted inserted replaced
275:34ad627ac5d5 277:37636f2b1c19 
     1 theory QuotMain
 
     1 theory QuotMain
 
     2 imports QuotScript QuotList Prove
 
     2 imports QuotScript QuotList Prove
 
     3 uses ("quotient_info.ML") 
     3 uses ("quotient_info.ML") 
     4      ("quotient.ML")
 
     4      ("quotient.ML")
 
       
     5      ("quotient_def.ML")
 
     5 begin
 
     6 begin
 
     6 
       
     7 ML {* Attrib.empty_binding *}
 
       
     8 
     7 
     9 locale QUOT_TYPE =
 
     8 locale QUOT_TYPE =
 
    10   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
     9   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
    11   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
 
    10   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
 
    12   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
 
    11   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
 
   141 section {* type definition for the quotient type *}
 
   140 section {* type definition for the quotient type *}
 
   142 
   141 
   143 (* the auxiliary data for the quotient types *)
 
   142 (* the auxiliary data for the quotient types *)
 
   144 use "quotient_info.ML"
 
   143 use "quotient_info.ML"
 
   145 
   144 
   146 
       
   147 declare [[map list = (map, LIST_REL)]]
 
   145 declare [[map list = (map, LIST_REL)]]
 
   148 declare [[map * = (prod_fun, prod_rel)]]
 
   146 declare [[map * = (prod_fun, prod_rel)]]
 
   149 declare [[map "fun" = (fun_map, FUN_REL)]]
 
   147 declare [[map "fun" = (fun_map, FUN_REL)]]
 
   150 
   148 
   151 ML {* maps_lookup @{theory} "List.list" *}
 
   149 ML {* maps_lookup @{theory} "List.list" *}
 
   152 ML {* maps_lookup @{theory} "*" *}
 
   150 ML {* maps_lookup @{theory} "*" *}
 
   153 ML {* maps_lookup @{theory} "fun" *}
 
   151 ML {* maps_lookup @{theory} "fun" *}
 
   154 
   152 
   155 
   153 
   156 (* definition of the quotient types *)
 
   154 (* definition of the quotient types *)
 
       
   155 (* FIXME: should be called quotient_typ.ML *)
 
   157 use "quotient.ML"
 
   156 use "quotient.ML"
 
       
   157 
       
   158 
       
   159 (* lifting of constants *)
 
       
   160 use "quotient_def.ML"
 
   158 
   161 
   159 
   162 
   160 text {* FIXME: auxiliary function *}
 
   163 text {* FIXME: auxiliary function *}
 
   161 ML {*
 
   164 ML {*
 
   162 val no_vars = Thm.rule_attribute (fn context => fn th =>
 
   165 val no_vars = Thm.rule_attribute (fn context => fn th =>
 
   163   let
 
   166   let
 
   164     val ctxt = Variable.set_body false (Context.proof_of context);
 
   167     val ctxt = Variable.set_body false (Context.proof_of context);
 
   165     val ((_, [th']), _) = Variable.import true [th] ctxt;
 
   168     val ((_, [th']), _) = Variable.import true [th] ctxt;
 
   166   in th' end);
 
   169   in th' end);
 
   167 *}
 
       
   168 
       
   169 section {* lifting of constants *}
 
       
   170 
       
   171 ML {*
 
       
   172 
       
   173 fun lookup_qenv qenv qty =
 
       
   174   (case (AList.lookup (op=) qenv qty) of
 
       
   175     SOME rty => SOME (qty, rty)
 
       
   176   | NONE => NONE)
 
       
   177 *}
 
       
   178 
       
   179 ML {*
 
       
   180 (* calculates the aggregate abs and rep functions for a given type; 
       
   181    repF is for constants' arguments; absF is for constants;
 
       
   182    function types need to be treated specially, since repF and absF
 
       
   183    change
 
       
   184 *)
 
       
   185 datatype flag = absF | repF
 
       
   186 
       
   187 fun negF absF = repF
 
       
   188   | negF repF = absF
 
       
   189 
       
   190 fun get_fun flag qenv lthy ty =
 
       
   191 let
 
       
   192   
       
   193   fun get_fun_aux s fs_tys =
 
       
   194   let
 
       
   195     val (fs, tys) = split_list fs_tys
 
       
   196     val (otys, ntys) = split_list tys
 
       
   197     val oty = Type (s, otys)
 
       
   198     val nty = Type (s, ntys)
 
       
   199     val ftys = map (op -->) tys
 
       
   200   in
 
       
   201    (case (maps_lookup (ProofContext.theory_of lthy) s) of
 
       
   202       SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
 
       
   203     | NONE      => error ("no map association for type " ^ s))
 
       
   204   end
 
       
   205 
       
   206   fun get_fun_fun fs_tys =
 
       
   207   let
 
       
   208     val (fs, tys) = split_list fs_tys
 
       
   209     val ([oty1, oty2], [nty1, nty2]) = split_list tys
 
       
   210     val oty = nty1 --> oty2
 
       
   211     val nty = oty1 --> nty2
 
       
   212     val ftys = map (op -->) tys
 
       
   213   in
 
       
   214     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
 
       
   215   end
 
       
   216 
       
   217   fun get_const flag (qty, rty) =
 
       
   218   let 
       
   219     val thy = ProofContext.theory_of lthy
 
       
   220     val qty_name = Long_Name.base_name (fst (dest_Type qty))
 
       
   221   in
 
       
   222     case flag of
 
       
   223       absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
 
       
   224     | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
 
       
   225   end
 
       
   226 
       
   227   fun mk_identity ty = Abs ("", ty, Bound 0)
 
       
   228 
       
   229 in
 
       
   230   if (AList.defined (op=) qenv ty)
 
       
   231   then (get_const flag (the (lookup_qenv qenv ty)))
 
       
   232   else (case ty of
 
       
   233           TFree _ => (mk_identity ty, (ty, ty))
 
       
   234         | Type (_, []) => (mk_identity ty, (ty, ty)) 
       
   235         | Type ("fun" , [ty1, ty2]) => 
       
   236                  get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
 
       
   237         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
 
       
   238         | _ => raise ERROR ("no type variables")
 
       
   239        )
 
       
   240 end
 
       
   241 *}
 
       
   242 
       
   243 ML {*
 
       
   244 fun make_def nconst_bname rhs qty mx qenv lthy =
 
       
   245 let
 
       
   246   val (arg_tys, res_ty) = strip_type qty
 
       
   247 
       
   248   val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
 
       
   249   val abs_fn  = (fst o get_fun absF qenv lthy) res_ty
 
       
   250 
       
   251   fun mk_fun_map t s = 
       
   252         Const (@{const_name "fun_map"}, dummyT) $ t $ s
 
       
   253 
       
   254   val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
 
       
   255                   |> Syntax.check_term lthy 
       
   256 in
 
       
   257   define (nconst_bname, mx, absrep_fn $ rhs) lthy
 
       
   258 end
 
       
   259 *}
 
       
   260 
       
   261 ML {*
 
       
   262 (* returns all subterms where two types differ *)
 
       
   263 fun diff (T, S) Ds =
 
       
   264   case (T, S) of
 
       
   265     (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
       
   266   | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
 
       
   267   | (Type (a, Ts), Type (b, Us)) => 
       
   268       if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
 
       
   269   | _ => (T, S)::Ds
 
       
   270 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
 
       
   271   | diffs ([], []) Ds = Ds
 
       
   272   | diffs _ _ = error "Unequal length of type arguments"
 
       
   273 *}
 
       
   274 
       
   275 ML {*
 
       
   276 fun error_msg lthy (qty, rty) =
 
       
   277 let 
       
   278   val qtystr = quote (Syntax.string_of_typ lthy qty)
 
       
   279   val rtystr = quote (Syntax.string_of_typ lthy rty)
 
       
   280 in
 
       
   281   error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
 
       
   282 end
 
       
   283 
       
   284 
       
   285 fun sanity_chk lthy qenv =
 
       
   286 let
 
       
   287    val qenv' = Quotient_Info.mk_qenv lthy
 
       
   288    val thy = ProofContext.theory_of lthy
 
       
   289 
       
   290    fun is_inst thy (qty, rty) (qty', rty') =
 
       
   291    if Sign.typ_instance thy (qty, qty')
 
       
   292    then let
 
       
   293           val inst = Sign.typ_match thy (qty', qty) Vartab.empty
 
       
   294         in
 
       
   295           rty = Envir.subst_type inst rty'
 
       
   296         end
 
       
   297    else false
 
       
   298 
       
   299    fun chk_inst (qty, rty) = 
       
   300      if exists (is_inst thy (qty, rty)) qenv' then true
 
       
   301      else error_msg lthy (qty, rty)
 
       
   302 in
 
       
   303   forall chk_inst qenv
 
       
   304 end
 
       
   305 *}
 
       
   306 
       
   307 ML {*
 
       
   308 fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
 
       
   309 let   
       
   310   val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
 
       
   311   val (_, rhs) = PrimitiveDefs.abs_def prop'
 
       
   312 
       
   313   val rty = fastype_of rhs
 
       
   314   val qenv = distinct (op=) (diff (qty, rty) [])
 
       
   315  
       
   316 in
 
       
   317   sanity_chk lthy qenv;
 
       
   318   make_def bind rhs qty mx qenv lthy 
       
   319 end
 
       
   320 *}
 
       
   321 
       
   322 ML {*
 
       
   323 val quotdef_parser =
 
       
   324   (OuterParse.binding --
 
       
   325     (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
       
   326       OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
       
   327        (SpecParse.opt_thm_name ":" -- OuterParse.prop)
 
       
   328 *}
 
       
   329 
       
   330 ML {*
 
       
   331 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
       
   332 let
 
       
   333   val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
 
       
   334   val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
 
       
   335 in
 
       
   336   quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 
       
   337 end
 
       
   338 *}
 
       
   339 
       
   340 ML {*
 
       
   341 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
 
       
   342   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
       
   343 *}
 
   170 *}
 
   344 
   171 
   345 section {* ATOMIZE *}
 
   172 section {* ATOMIZE *}
 
   346 
   173 
   347 text {*
 
   174 text {*
 
   520      Logic.mk_implies
 
   347      Logic.mk_implies
 
   521        ((prop_of thm),
 
   348        ((prop_of thm),
 
   522        (my_reg lthy rel rty (prop_of thm)))
 
   349        (my_reg lthy rel rty (prop_of thm)))
 
   523 *}
 
   350 *}
 
   524 
   351 
   525 lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
 
   352 lemma universal_twice: 
       
   353   "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
 
   526 by auto
 
   354 by auto
 
   527 
   355 
   528 lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
   356 lemma implication_twice: 
       
   357   "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
   529 by auto
 
   358 by auto
 
   530 
   359 
   531 (*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
 
   360 (*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
 
   532 by auto*)
 
   361 by auto*)
 
   533 
   362 
   571         Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
 
   400         Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
 
   572       | _ => ty
 
   401       | _ => ty
 
   573      )
 
   402      )
 
   574 *}
 
   403 *}
 
   575 
   404 
       
   405 
   576 ML {*
 
   406 ML {*
 
   577 fun old_get_fun flag rty qty lthy ty =
 
   407 fun old_get_fun flag rty qty lthy ty =
 
   578   get_fun flag [(qty, rty)] lthy ty 
   408   get_fun flag [(qty, rty)] lthy ty 
   579 
   409 
   580 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
 
   410 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
 
   581   make_def nconst_bname otrm qty mx [(qty, rty)] lthy
 
   411   make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy
 
   582 *}
 
   412 *}
 
   583 
   413 
   584 text {* Does the same as 'subst' in a given prop or theorem *}
 
   414 text {* Does the same as 'subst' in a given prop or theorem *}
 
   585 ML {*
 
   415 ML {*
 
   586 fun eqsubst_prop ctxt thms t =
 
   416 fun eqsubst_prop ctxt thms t =
nominal2