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 14 5f6ee943c697
parent 13 c13bb9e02eb7
child 15 f46eddb570a3
equal deleted inserted replaced
13:c13bb9e02eb7 14:5f6ee943c697 
   106     (HOLogic.mk_exists 
   106     (HOLogic.mk_exists 
   107        ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 
   107        ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 
   108 end
 
   108 end
 
   109 *}
 
   109 *}
 
   110 
   110 
   111 ML {*
 
   111 (*
 
   112  typedef_term @{term R} @{typ "nat"} @{context} 
   112 ML {*
 
       
   113  typedef_term @{term R} @{typ "nat"} @{context}
 
   113   |> Syntax.string_of_term @{context}
 
   114   |> Syntax.string_of_term @{context}
 
   114   |> writeln
 
   115   |> writeln
 
   115 *}
 
   116 *}*)
 
   116 
   117 
   117 ML {*
 
   118 ML {*
 
   118 val typedef_tac =  
   119 val typedef_tac =  
   119   EVERY1 [rewrite_goal_tac @{thms mem_def},
 
   120   EVERY1 [rewrite_goal_tac @{thms mem_def},
 
   120           rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
 
   121           rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
 
   197 in
 
   198 in
 
   198   ((trm, thm), lthy')
 
   199   ((trm, thm), lthy')
 
   199 end
 
   200 end
 
   200 *}
 
   201 *}
 
   201 
   202 
       
   203 (*
 
       
   204 locale foo = fixes x :: nat
 
       
   205 begin
 
       
   206 
       
   207 ML {* make_def (@{binding foo}, NoSyn, @{term "x + x"}) @{context} *}
 
       
   208 *)
 
       
   209 
   202 ML {*
 
   210 ML {*
 
   203 fun reg_thm (name, thm) lthy = 
   211 fun reg_thm (name, thm) lthy = 
   204 let
 
   212 let
 
   205   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
   213   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
   206 in
 
   214 in
 
   207   (thm',lthy')
 
   215   (thm',lthy')
 
   208 end
 
   216 end
 
   209 *}
 
   217 *}
 
   210 
   218 
   211 ML {* 
   219 ML {*
 
       
   220 val no_vars = Thm.rule_attribute (fn context => fn th =>
 
       
   221   let
 
       
   222     val ctxt = Variable.set_body false (Context.proof_of context);
 
       
   223     val ((_, [th']), _) = Variable.import true [th] ctxt;
 
       
   224   in th' end);
 
       
   225 *}
 
       
   226 
       
   227 ML ProofContext.theory_of
 
       
   228 
       
   229 ML Expression.interpretation
 
       
   230 
       
   231 ML {*
 
       
   232 fun my_print_tac ctxt thm =
 
       
   233 let
 
       
   234    val _ = tracing (Display.string_of_thm ctxt thm)
 
       
   235 in
 
       
   236    Seq.single thm
 
       
   237 end *}
 
       
   238 
       
   239 ML LocalTheory.theory_result
 
       
   240 
       
   241 
       
   242 ML {* Binding.str_of @{binding foo} *}
 
       
   243 
       
   244 ML {*
 
   212 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
 
   245 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
 
   213 let 
   246 let 
   214   (* generates typedef *)
 
   247   (* generates typedef *)
 
   215   val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
 
   248   val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
 
   216 
   249 
   231   val REP_name = Binding.prefix_name "REP_" qty_name  
   264   val REP_name = Binding.prefix_name "REP_" qty_name  
   232   val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 
   265   val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 
   233          lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
 
   266          lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
 
   234                ||>> make_def (REP_name, NoSyn, REP_trm)
 
   267                ||>> make_def (REP_name, NoSyn, REP_trm)
 
   235 
   268 
       
   269   (* REMOVE VARIFY *)
 
       
   270   val _ = tracing (Syntax.string_of_typ lthy' (type_of ABS_trm))
 
       
   271   val _ = tracing (Syntax.string_of_typ lthy' (type_of REP_trm))
 
       
   272   val _ = tracing (Syntax.string_of_typ lthy' (type_of rel))
 
       
   273 
   236   (* quot_type theorem *)
 
   274   (* quot_type theorem *)
 
   237   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
 
   275   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
 
   238   val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
 
   276   val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
 
   239 
   277 
   240   (* quotient theorem *)
 
   278   (* quotient theorem *)
 
   241   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
 
   279   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
 
   242   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   280   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   243 
   281 
   244 in
 
   282   (* interpretation *)
 
   245   lthy'' 
   283   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
 
   246   |> reg_thm (quot_thm_name, quot_thm)  
   284   val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
 
       
   285   val eqn1i = Thm.prop_of (symmetric eqn1pre)
 
       
   286   val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
 
       
   287   val eqn2i = Thm.prop_of (symmetric eqn2pre)
 
       
   288 
       
   289   val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
 
       
   290   val exp_term = Morphism.term exp_morphism;
 
       
   291   val exp = Morphism.thm exp_morphism;
 
       
   292 
       
   293   val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
 
       
   294     ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))
 
       
   295     (*THEN print_tac "Hello"*))
 
       
   296   val mthdt = Method.Basic (fn _ => mthd)
 
       
   297   val bymt = Proof.global_terminal_proof (mthdt, NONE)
 
       
   298   val exp_i = [(@{const_name QUOT_TYPE},((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
 
       
   299     Expression.Named [
 
       
   300      ("R", rel),
 
       
   301      ("Abs", abs),
 
       
   302      ("Rep", rep)
 
       
   303     ]))]
 
       
   304 in
 
       
   305   lthy''''
 
       
   306   |> reg_thm (quot_thm_name, quot_thm)
 
   247   ||>> reg_thm (quotient_thm_name, quotient_thm)
 
   307   ||>> reg_thm (quotient_thm_name, quotient_thm)
 
   248 end
 
   308   ||> LocalTheory.theory (fn thy =>
 
   249 *}
 
   309       let
 
       
   310         val global_eqns = map exp_term [eqn2i, eqn1i];
 
       
   311         val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
 
       
   312         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
 
       
   313 (*        val _ = tracing (Syntax.string_of_typ lthy'''' (type_of (fst (Logic.dest_equals (exp_term eqn1i)))));*)
 
       
   314       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 
       
   315 end
 
       
   316 *}
 
       
   317 
   250 
   318 
   251 section {* various tests for quotient types*}
 
   319 section {* various tests for quotient types*}
 
   252 datatype trm =
 
   320 datatype trm =
 
   253   var  "nat" 
   321   var  "nat" 
   254 | app  "trm" "trm"
 
   322 | app  "trm" "trm"
 
   255 | lam  "nat" "trm"
 
   323 | lam  "nat" "trm"
 
   256 
   324 
   257 axiomatization R :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
 
   325 axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
 
   258   r_eq: "EQUIV R"
 
   326   r_eq: "EQUIV RR"
 
   259 
   327 
   260 ML {*
 
   328 ML {*
 
   261   typedef_main 
   329   typedef_main 
   262 *}
 
   330 *}
 
   263 
   331 
   264 local_setup {*
 
   332 (*ML {*
 
   265   typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
 
   333   val lthy = @{context};
 
   266 *}
 
   334   val qty_name = @{binding "qtrm"}
 
       
   335   val rel = @{term "RR"}
 
       
   336   val ty = @{typ trm}
 
       
   337   val equiv_thm = @{thm r_eq}
 
       
   338 *}*)
 
       
   339 
       
   340 local_setup {*
 
       
   341   fn lthy =>
 
       
   342     Toplevel.program (fn () =>
 
       
   343     exception_trace (
 
       
   344       fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy)
 
       
   345     )
 
       
   346   )
 
       
   347 *}
 
       
   348 print_theorems
 
       
   349 
       
   350 (*thm QUOT_TYPE_I_qtrm.thm11*)
 
       
   351 
   267 
   352 
   268 term Rep_qtrm
 
   353 term Rep_qtrm
 
   269 term REP_qtrm
 
   354 term REP_qtrm
 
   270 term Abs_qtrm
 
   355 term Abs_qtrm
 
   271 term ABS_qtrm
 
   356 term ABS_qtrm
 
   287 | lam'  "'a" "'a trm'"
 
   372 | lam'  "'a" "'a trm'"
 
   288   
   373   
   289 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 
   374 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 
   290 axioms r_eq': "EQUIV R'"
 
   375 axioms r_eq': "EQUIV R'"
 
   291 
   376 
   292 local_setup {*
 
   377 
   293   typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
 
   378 local_setup {*
 
   294 *}
 
   379   fn lthy =>
 
       
   380     exception_trace
 
       
   381       (fn () => (typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd) lthy)
 
       
   382 *}
 
       
   383 
       
   384 print_theorems
 
   295 
   385 
   296 term ABS_qtrm'
 
   386 term ABS_qtrm'
 
   297 term REP_qtrm'
 
   387 term REP_qtrm'
 
   298 thm QUOT_TYPE_qtrm'
 
   388 thm QUOT_TYPE_qtrm'
 
   299 thm QUOTIENT_qtrm'
 
   389 thm QUOTIENT_qtrm'
 
   300 thm Rep_qtrm'
 
   390 thm Rep_qtrm'
 
       
   391 
   301 
   392 
   302 text {* a test with lists of terms *}
 
   393 text {* a test with lists of terms *}
 
   303 datatype t =
 
   394 datatype t =
 
   304   vr "string"
 
   395   vr "string"
 
   305 | ap "t list"
 
   396 | ap "t list"
 
   385 ML {*
 
   476 ML {*
 
   386 fun get_const_def nconst oconst rty qty lthy =
 
   477 fun get_const_def nconst oconst rty qty lthy =
 
   387 let
 
   478 let
 
   388   val ty = fastype_of nconst
 
   479   val ty = fastype_of nconst
 
   389   val (arg_tys, res_ty) = strip_type ty
 
   480   val (arg_tys, res_ty) = strip_type ty
 
   390  
   481 
   391   val fresh_args = arg_tys |> map (pair "x")
 
   482   val fresh_args = arg_tys |> map (pair "x")
 
   392                            |> Variable.variant_frees lthy [nconst, oconst] 
   483                            |> Variable.variant_frees lthy [nconst, oconst] 
   393                            |> map Free
 
   484                            |> map Free
 
   394 
   485 
   395   val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
 
   486   val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
 
   437 *}
 
   528 *}
 
   438 
   529 
   439 thm VR_def
 
   530 thm VR_def
 
   440 thm AP_def
 
   531 thm AP_def
 
   441 thm LM_def
 
   532 thm LM_def
 
   442 term LM 
   533 term LM
 
   443 term VR
 
   534 term VR
 
   444 term AP
 
   535 term AP
 
   445 
   536 
   446 
   537 
   447 text {* a test with functions *}
 
   538 text {* a test with functions *}
 
   451 | lm' "'a" "string \<Rightarrow> ('a t')"
 
   542 | lm' "'a" "string \<Rightarrow> ('a t')"
 
   452 
   543 
   453 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 
   544 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 
   454 axioms t_eq': "EQUIV Rt'"
 
   545 axioms t_eq': "EQUIV Rt'"
 
   455 
   546 
       
   547 
   456 local_setup {*
 
   548 local_setup {*
 
   457   typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 
   549   typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 
   458 *}
 
   550 *}
 
   459 
   551 
       
   552 print_theorems
 
   460 
   553 
   461 local_setup {*
 
   554 local_setup {*
 
   462   make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 
   555   make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 
   463 *}
 
   556 *}
 
   464 
   557 
   471 *}
 
   564 *}
 
   472 
   565 
   473 thm VR'_def
 
   566 thm VR'_def
 
   474 thm AP'_def
 
   567 thm AP'_def
 
   475 thm LM'_def
 
   568 thm LM'_def
 
   476 term LM' 
   569 term LM'
 
   477 term VR'
 
   570 term VR'
 
   478 term AP'
 
   571 term AP'
 
   479 
   572 
       
   573 
   480 text {* finite set example *}
 
   574 text {* finite set example *}
 
   481 print_syntax
 
   575 print_syntax
 
   482 inductive 
   576 inductive
 
   483   list_eq (infix "\<approx>" 50)
 
   577   list_eq (infix "\<approx>" 50)
 
   484 where
 
   578 where
 
   485   "a#b#xs \<approx> b#a#xs"
 
   579   "a#b#xs \<approx> b#a#xs"
 
   486 | "[] \<approx> []"
 
   580 | "[] \<approx> []"
 
   487 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
 
   581 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
 
   503 
   597 
   504 local_setup {*
 
   598 local_setup {*
 
   505   typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 
   599   typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 
   506 *}
 
   600 *}
 
   507 
   601 
       
   602 print_theorems
 
       
   603 
   508 typ "'a fset"
 
   604 typ "'a fset"
 
   509 thm "Rep_fset"
 
   605 thm "Rep_fset"
 
   510 
   606 
   511 local_setup {*
 
   607 local_setup {*
 
   512   make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   608   make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   513 *}
 
   609 *}
 
   514 
   610 
   515 term Nil 
   611 term Nil
 
   516 term EMPTY
 
   612 term EMPTY
 
   517 thm EMPTY_def
 
   613 thm EMPTY_def
 
   518 
   614 
   519 
   615 
   520 local_setup {*
 
   616 local_setup {*
 
   521   make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   617   make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   522 *}
 
   618 *}
 
   523 
   619 
   524 term Cons 
   620 term Cons
 
   525 term INSERT
 
   621 term INSERT
 
   526 thm INSERT_def
 
   622 thm INSERT_def
 
   527 
   623 
   528 local_setup {*
 
   624 local_setup {*
 
   529   make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   625   make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   541 term CARD
 
   637 term CARD
 
   542 thm CARD_def
 
   638 thm CARD_def
 
   543 
   639 
   544 thm QUOTIENT_fset
 
   640 thm QUOTIENT_fset
 
   545 
   641 
   546 (* This code builds the interpretation from ML level, currently only
 
   642 thm QUOT_TYPE_I_fset.thm11
 
   547    for fset *) 
       
   548 
       
   549 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN
 
       
   550   simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def [symmetric]}) 1 THEN
 
       
   551   simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def [symmetric]}) 1) *}
 
       
   552 ML {* val mthdt = Method.Basic (fn _ => mthd) *}
 
       
   553 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *}
 
       
   554 ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true),
 
       
   555   Expression.Named [
 
       
   556    ("R",@{term list_eq}),
 
       
   557    ("Abs",@{term Abs_fset}),
 
       
   558    ("Rep",@{term Rep_fset})
 
       
   559   ]))] *}
 
       
   560 ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *}
 
       
   561 ML {* val eqn1i = (bindd, @{prop "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"}) *}
 
       
   562 ML {* val eqn2i = (bindd, @{prop "QUOT_TYPE.REP Rep_fset = REP_fset"}) *}
 
       
   563 setup {* fn thy => ProofContext.theory_of
 
       
   564   (bymt (Expression.interpretation (exp_i, []) [eqn2i,eqn1i] thy)) *}
 
       
   565 
       
   566 (* It is eqivalent to the below:
 
       
   567 
       
   568 interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset
 
       
   569   where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"
 
       
   570     and "QUOT_TYPE.REP Rep_fset = REP_fset"
 
       
   571   unfolding ABS_fset_def REP_fset_def
 
       
   572   apply (rule QUOT_TYPE_fset)
 
       
   573   apply (simp only: ABS_fset_def[symmetric])
 
       
   574   apply (simp only: REP_fset_def[symmetric])
 
       
   575   done
 
       
   576 *)
 
       
   577 
       
   578 
   643 
   579 
   644 
   580 fun
 
   645 fun
 
   581   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 
   646   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 
   582 where
 
   647 where
 
   626 lemma yy:
 
   691 lemma yy:
 
   627   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
   692   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
   628 unfolding IN_def EMPTY_def
 
   693 unfolding IN_def EMPTY_def
 
   629 apply(rule_tac f="(op =) False" in arg_cong)
 
   694 apply(rule_tac f="(op =) False" in arg_cong)
 
   630 apply(rule mem_respects)
 
   695 apply(rule mem_respects)
 
   631 apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   696 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   632 apply(rule list_eq.intros)
 
   697 apply(rule list_eq.intros)
 
   633 done
 
   698 done
 
   634 
   699 
   635 lemma
 
   700 lemma
 
   636   shows "IN (x::nat) EMPTY = False"
 
   701   shows "IN (x::nat) EMPTY = False"
 
   652 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
   717 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
   653 apply(rule list_eq_sym)
 
   718 apply(rule list_eq_sym)
 
   654 done
 
   719 done
 
   655 
   720 
   656 lemma append_respects_fst:
 
   721 lemma append_respects_fst:
 
   657   assumes a : "list_eq l1 l2"  
   722   assumes a : "list_eq l1 l2"
 
   658   shows "list_eq (l1 @ s) (l2 @ s)"
 
   723   shows "list_eq (l1 @ s) (l2 @ s)"
 
   659   using a
 
   724   using a
 
   660   apply(induct)
 
   725   apply(induct)
 
   661   apply(auto intro: list_eq.intros)
 
   726   apply(auto intro: list_eq.intros)
 
   662   apply(simp add: list_eq_sym)
 
   727   apply(simp add: list_eq_sym)
 
   672      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
 
   737      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
 
   673     )"
 
   738     )"
 
   674   unfolding UNION_def EMPTY_def INSERT_def
 
   739   unfolding UNION_def EMPTY_def INSERT_def
 
   675   apply(rule_tac f="(op &)" in arg_cong2)
 
   740   apply(rule_tac f="(op &)" in arg_cong2)
 
   676   apply(rule_tac f="(op =)" in arg_cong2)
 
   741   apply(rule_tac f="(op =)" in arg_cong2)
 
   677   apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
 
   742   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
 
   678   apply(rule append_respects_fst)
 
   743   apply(rule append_respects_fst)
 
   679   apply(simp only:QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   744   apply(simp only:QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   680   apply(rule list_eq_sym)
 
   745   apply(rule list_eq_sym)
 
   681   apply(simp)
 
   746   apply(simp)
 
   682   apply(rule_tac f="(op =)" in arg_cong2)
 
   747   apply(rule_tac f="(op =)" in arg_cong2)
 
   683   apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
 
   748   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
 
   684   apply(rule append_respects_fst)
 
   749   apply(rule append_respects_fst)
 
   685   apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   750   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   686   apply(rule list_eq_sym)
 
   751   apply(rule list_eq_sym)
 
   687   apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
 
   752   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
 
   688   apply(rule list_eq.intros(5))
 
   753   apply(rule list_eq.intros(5))
 
   689   apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   754   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   690   apply(rule list_eq_sym)
 
   755   apply(rule list_eq_sym)
 
   691 done
 
   756 done
 
   692 
   757 
   693 lemma
 
   758 lemma
 
   694   shows "
 
   759   shows "
 
   695      (UNION EMPTY s = s) &
 
   760      (UNION EMPTY s = s) &
 
   696      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
 
   761      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
 
   697   apply (simp add: yyy)
 
   762   apply (simp add: yyy)
 
   698   apply (rule QUOT_TYPE_fset_i.thm10)
 
   763   apply (rule QUOT_TYPE_I_fset.thm10)
 
   699   done
 
   764   done
 
   700 
   765 
   701 ML {*
 
   766 ML {*
 
   702   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
 
   767   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
 
   703   val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
 
   768   val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
 
   728     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
 
   793     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
 
   729   in
 
   794   in
 
   730   HOLogic.mk_eq ((build_aux concl), concl)
 
   795   HOLogic.mk_eq ((build_aux concl), concl)
 
   731 end *}
 
   796 end *}
 
   732 
   797 
   733 ML {*
 
       
   734 val no_vars = Thm.rule_attribute (fn context => fn th =>
 
       
   735   let
 
       
   736     val ctxt = Variable.set_body false (Context.proof_of context);
 
       
   737     val ((_, [th']), _) = Variable.import true [th] ctxt;
 
       
   738   in th' end);
 
       
   739 *}
 
       
   740 
   798 
   741 ML {*
 
   799 ML {*
 
   742   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
 
   800   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
 
   743   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   801   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   744   val cgoal = cterm_of @{theory} goal
 
   802   val cgoal = cterm_of @{theory} goal
 
   754 
   812 
   755 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
 
   813 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
 
   756 apply(rule_tac f="(op =)" in arg_cong2)
 
   814 apply(rule_tac f="(op =)" in arg_cong2)
 
   757 unfolding IN_def EMPTY_def
 
   815 unfolding IN_def EMPTY_def
 
   758 apply (rule_tac mem_respects)
 
   816 apply (rule_tac mem_respects)
 
   759 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   817 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   760 apply (simp_all)
 
   818 apply (simp_all)
 
   761 apply (rule list_eq_sym)
 
   819 apply (rule list_eq_sym)
 
   762 done
 
   820 done
 
   763 
   821 
   764 thm length_append (* Not true but worth checking that the goal is correct *)
 
   822 thm length_append (* Not true but worth checking that the goal is correct *)
 
   784 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
 
   842 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
 
   785 apply(rule_tac f="(op =)" in arg_cong2)
 
   843 apply(rule_tac f="(op =)" in arg_cong2)
 
   786 unfolding IN_def
 
   844 unfolding IN_def
 
   787 apply (rule_tac mem_respects)
 
   845 apply (rule_tac mem_respects)
 
   788 unfolding INSERT_def
 
   846 unfolding INSERT_def
 
   789 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   847 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   790 apply (rule cons_preserves)
 
   848 apply (rule cons_preserves)
 
   791 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   849 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   792 apply (rule list_eq_sym)
 
   850 apply (rule list_eq_sym)
 
   793 apply(rule_tac f="(op \<or>)" in arg_cong2)
 
   851 apply(rule_tac f="(op \<or>)" in arg_cong2)
 
   794 apply (simp)
 
   852 apply (simp)
 
   795 apply (rule_tac mem_respects)
 
   853 apply (rule_tac mem_respects)
 
   796 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 
   854 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
   797 apply (rule list_eq_sym)
 
   855 apply (rule list_eq_sym)
 
   798 done
 
   856 done
nominal2