302 

   303 text {* produces the definition for a lifted constant *}

   304 

   305 ML {*

   306 fun get_const_def nconst oconst rty qty lthy =

   307 let

   308   val ty = fastype_of nconst

   309   val (arg_tys, res_ty) = strip_type ty

   310 

   311   val fresh_args = arg_tys |> map (pair "x")

   312                            |> Variable.variant_frees lthy [nconst, oconst]

   313                            |> map Free

   314 

   315   val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys

   316   val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty

   317 

   318 in

   319   map (op $) (rep_fns ~~ fresh_args)

   320   |> curry list_comb oconst

   321   |> curry (op $) abs_fn

   322   |> fold_rev lambda fresh_args

   323 end

   324 *}

   325 

   326 ML {*

   327 fun exchange_ty rty qty ty =

   328   if ty = rty

   329   then qty

   330   else

   331     (case ty of

   332        Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)

   333       | _ => ty

   334     )

   335 *}

   336 

   337 ML {*

   338 fun make_const_def nconst_bname oconst mx rty qty lthy =

   339 let

   340   val oconst_ty = fastype_of oconst

   341   val nconst_ty = exchange_ty rty qty oconst_ty

   342   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)

   343   val def_trm = get_const_def nconst oconst rty qty lthy

   344 in

   345   define (nconst_bname, mx, def_trm) lthy

   346 end

   347 *}

   348 

   349 local_setup {*

   350   make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   351   make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   352   make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd

   353 *}

   354 

   355 term vr

   356 term ap

   357 term lm

   358 thm VR_def AP_def LM_def

   359 term LM

   360 term VR

   361 term AP

   362 

   363 text {* a test with functions *}

   364 datatype 'a t' =

   365   vr' "string"

   366 | ap' "('a t') * ('a t')"

   367 | lm' "'a" "string \<Rightarrow> ('a t')"

   368 

   369 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"

   370 axioms t_eq': "EQUIV Rt'"

   371 

   372 quotient qt' = "'a t'" / "Rt'"

   373   apply(rule t_eq')

   374   done

   375 

   376 print_theorems

   377 

   378 local_setup {*

   379   make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   380   make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   381   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

   382 *}

   383 

   384 term vr'

   385 term ap'

   386 term ap'

   387 thm VR'_def AP'_def LM'_def

   388 term LM'

   389 term VR'

   390 term AP'

   391 

   392 

   393 text {* finite set example *}

   394 print_syntax

   395 inductive

   396   list_eq (infix "\<approx>" 50)

   397 where

   398   "a#b#xs \<approx> b#a#xs"

   399 | "[] \<approx> []"

   400 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

   401 | "a#a#xs \<approx> a#xs"

   402 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

   403 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

   404 

   405 lemma list_eq_refl:

   406   shows "xs \<approx> xs"

   407   apply (induct xs)

   408    apply (auto intro: list_eq.intros)

   409   done

   410 

   411 lemma equiv_list_eq:

   412   shows "EQUIV list_eq"

   413   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

   414   apply(auto intro: list_eq.intros list_eq_refl)

   415   done

   416 

   417 quotient fset = "'a list" / "list_eq"

   418   apply(rule equiv_list_eq)

   419   done

   420 

   421 print_theorems

   422 

   423 typ "'a fset"

   424 thm "Rep_fset"

   425 

   426 local_setup {*

   427   make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   428 *}

   429 

   430 term Nil

   431 term EMPTY

   432 thm EMPTY_def

   433 

   434 

   435 local_setup {*

   436   make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   437 *}

   438 

   439 term Cons

   440 term INSERT

   441 thm INSERT_def

   442 

   443 local_setup {*

   444   make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   445 *}

   446 

   447 term append

   448 term UNION

   449 thm UNION_def

   450 

   451 

   452 thm QUOTIENT_fset

   453 

   454 thm QUOT_TYPE_I_fset.thm11

   455 

   456 

   457 fun

   458   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)

   459 where

   460   m1: "(x memb []) = False"

   461 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"

   462 

   463 lemma mem_respects:

   464   fixes z

   465   assumes a: "list_eq x y"

   466   shows "(z memb x) = (z memb y)"

   467   using a by induct auto

   468 

   469 

   470 fun

   471   card1 :: "'a list \<Rightarrow> nat"

   472 where

   473   card1_nil: "(card1 []) = 0"

   474 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"

   475 

   476 local_setup {*

   477   make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   478 *}

   479 

   480 term card1

   481 term card

   482 thm card_def

   483 

   484 (* text {*

   485  Maybe make_const_def should require a theorem that says that the particular lifted function

   486  respects the relation. With it such a definition would be impossible:

   487  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   488 *}*)

   489 

   490 lemma card1_rsp:

   491   fixes a b :: "'a list"

   492   assumes e: "a \<approx> b"

   493   shows "card1 a = card1 b"

   494   using e apply induct

   495   apply (simp_all add:mem_respects)

   496   done

   497 

   498 lemma card1_0:

   499   fixes a :: "'a list"

   500   shows "(card1 a = 0) = (a = [])"

   501   apply (induct a)

   502    apply (simp)

   503   apply (simp_all)

   504    apply meson

   505   apply (simp_all)

   506   done

   507 

   508 lemma not_mem_card1:

   509   fixes x :: "'a"

   510   fixes xs :: "'a list"

   511   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"

   512   by simp

   513 

   514 

   515 lemma mem_cons:

   516   fixes x :: "'a"

   517   fixes xs :: "'a list"

   518   assumes a : "x memb xs"

   519   shows "x # xs \<approx> xs"

   520   using a

   521   apply (induct xs)

   522   apply (auto intro: list_eq.intros)

   523   done

   524 

   525 lemma card1_suc:

   526   fixes xs :: "'a list"

   527   fixes n :: "nat"

   528   assumes c: "card1 xs = Suc n"

   529   shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"

   530   using c

   531 apply(induct xs)

   532 apply (metis Suc_neq_Zero card1_0)

   533 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)

   534 done

   535 

   536 primrec

   537   fold1

   538 where

   539   "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"

   540 | "fold1 f g z (a # A) =

   541      (if ((!u v. (f u v = f v u))

   542       \<and> (!u v w. ((f u (f v w) = f (f u v) w))))

   543      then (

   544        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))

   545      ) else z)"

   546 

   547 thm fold1.simps

   548 

   549 lemma cons_preserves:

   550   fixes z

   551   assumes a: "xs \<approx> ys"

   552   shows "(z # xs) \<approx> (z # ys)"

   553   using a by (rule QuotMain.list_eq.intros(5))

   554 

   555 lemma fs1_strong_cases:

   556   fixes X :: "'a list"

   557   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"

   558   apply (induct X)

   559   apply (simp)

   560   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)

   561   done

   562 

   563 

   564 text {*

   565   Unabs_def converts a definition given as

   566 

   567     c \<equiv> %x. %y. f x y

   568 

   569   to a theorem of the form

   570 

   571     c x y \<equiv> f x y

   572 

   573   This function is needed to rewrite the right-hand

   574   side to the left-hand side.

   575 *}

   576 

   577 ML {*

   578 fun unabs_def ctxt def =

   579 let

   580   val (lhs, rhs) = Thm.dest_equals (cprop_of def)

   581   val xs = strip_abs_vars (term_of rhs)

   582   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt

   583   

   584   val thy = ProofContext.theory_of ctxt'

   585   val cxs = map (cterm_of thy o Free) xs

   586   val new_lhs = Drule.list_comb (lhs, cxs)

   587 

   588   fun get_conv [] = Conv.rewr_conv def

   589     | get_conv (x::xs) = Conv.fun_conv (get_conv xs)

   590 in

   591   get_conv xs new_lhs |>  

   592   singleton (ProofContext.export ctxt' ctxt)

   593 end

   594 *}

   595 

   596 local_setup {*

   597   make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   598 *}

   599 

   600 term membship

   601 term IN

   602 thm IN_def

   603 

   604 (* unabs_def tests *)

   605 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}

   606 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}

   607 ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}

   608 

   609 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]

   610 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]

   611 

   612 lemma yy:

   613   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"

   614 unfolding IN_def EMPTY_def

   615 apply(rule_tac f="(op =) False" in arg_cong)

   616 apply(rule mem_respects)

   617 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   618 apply(rule list_eq.intros)

   619 done

   620 

   621 lemma

   622   shows "IN (x::nat) EMPTY = False"

   623 using m1

   624 apply -

   625 apply(rule yy[THEN iffD1, symmetric])

   626 apply(simp)

   627 done

   628 

   629 lemma

   630   shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =

   631          ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"

   632 unfolding IN_def INSERT_def

   633 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)

   634 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)

   635 apply(rule mem_respects)

   636 apply(rule list_eq.intros(3))

   637 apply(unfold REP_fset_def ABS_fset_def)

   638 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

   639 apply(rule list_eq_refl)

   640 done

   641 

   642 lemma append_respects_fst:

   643   assumes a : "list_eq l1 l2"

   644   shows "list_eq (l1 @ s) (l2 @ s)"

   645   using a

   646   apply(induct)

   647   apply(auto intro: list_eq.intros)

   648   apply(simp add: list_eq_refl)

   649 done

   650 

   651 lemma yyy:

   652   shows "

   653     (

   654      (UNION EMPTY s = s) &

   655      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))

   656     ) = (

   657      ((ABS_fset ([] @ REP_fset s)) = s) &

   658      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))

   659     )"

   660   unfolding UNION_def EMPTY_def INSERT_def

   661   apply(rule_tac f="(op &)" in arg_cong2)

   662   apply(rule_tac f="(op =)" in arg_cong2)

   663   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   664   apply(rule append_respects_fst)

   665   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   666   apply(rule list_eq_refl)

   667   apply(simp)

   668   apply(rule_tac f="(op =)" in arg_cong2)

   669   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   670   apply(rule append_respects_fst)

   671   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   672   apply(rule list_eq_refl)

   673   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

   674   apply(rule list_eq.intros(5))

   675   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   676   apply(rule list_eq_refl)

   677 done

   678 

   679 lemma

   680   shows "

   681      (UNION EMPTY s = s) &

   682      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"

   683   apply (simp add: yyy)

   684   apply (simp add: QUOT_TYPE_I_fset.thm10)

   685   done

   686 

   687 ML {*

   688   fun mk_rep x = @{term REP_fset} $ x;

   689   fun mk_abs x = @{term ABS_fset} $ x;

   690   val consts = [@{const_name "Nil"}, @{const_name "append"},

   691                 @{const_name "Cons"}, @{const_name "membship"},

   692                 @{const_name "card1"}]

   693 *}

   694 

   695 ML {* val qty = @{typ "'a fset"} *}

   696 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}

   697 ML {* val fall = Const(@{const_name all}, dummyT) *}

   698 

   699 ML {*

   700 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =

   701   let

   702     fun mk_rep_abs x = mk_rep (mk_abs x);

   703 

   704     fun is_constructor (Const (x, _)) = member (op =) constructors x

   705       | is_constructor _ = false;

   706 

   707     fun maybe_mk_rep_abs t =

   708       let

   709         val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)

   710       in

   711         if fastype_of t = rty then mk_rep_abs t else t

   712       end;

   713 

   714     fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty

   715       | is_all _ = false;

   716 

   717     fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty

   718       | is_ex _ = false;

   719 

   720     fun build_aux ctxt1 tm =

   721       let

   722         val (head, args) = Term.strip_comb tm;

   723         val args' = map (build_aux ctxt1) args;

   724       in

   725         (case head of

   726           Abs (x, T, t) =>

   727             if T = rty then let

   728               val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;

   729               val v = Free (x', qty);

   730               val t' = subst_bound (mk_rep v, t);

   731               val rec_term = build_aux ctxt2 t';

   732               val _ = tracing (Syntax.string_of_term ctxt2 t')

   733               val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))

   734             in

   735               Term.lambda_name (x, v) rec_term

   736             end else let

   737               val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;

   738               val v = Free (x', T);

   739               val t' = subst_bound (v, t);

   740               val rec_term = build_aux ctxt2 t';

   741             in Term.lambda_name (x, v) rec_term end

   742         | _ =>  (* I assume that we never lift 'prop' since it is not of sort type *)

   743             if is_all head then

   744               list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1

   745             else if is_ex head then

   746               list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1

   747             else if is_constructor head then

   748               maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))

   749             else

   750               maybe_mk_rep_abs (list_comb (head, args'))

   751         )

   752       end;

   753   in

   754     build_aux ctxt (Thm.prop_of thm)

   755   end

   756 *}

   757 

   758 ML {*

   759 fun build_goal ctxt thm cons rty qty mk_rep mk_abs =

   760   Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))

   761 *}

   762 

   763 ML {*

   764   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))

   765 *}

   766   

   767 ML {*

   768 m1_novars |> prop_of

   769 |> Syntax.string_of_term @{context}

   770 |> writeln; 

   771 build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   772 |> Syntax.string_of_term @{context}

   773 |> writeln

   774 *}

   775 

   776 

   777 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}

   778 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}

   779 

   780 ML {*

   781   fun dest_cbinop t =

   782     let

   783       val (t2, rhs) = Thm.dest_comb t;

   784       val (bop, lhs) = Thm.dest_comb t2;

   785     in

   786       (bop, (lhs, rhs))

   787     end

   788 *}

   789 

   790 ML {*

   791   fun dest_ceq t =

   792     let

   793       val (bop, pair) = dest_cbinop t;

   794       val (bop_s, _) = Term.dest_Const (Thm.term_of bop);

   795     in

   796       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))

   797     end

   798 *}

   799 

   800 ML Thm.instantiate

   801 ML {*@{thm arg_cong2}*}

   802 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}

   803 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}

   804 ML {*

   805   Toplevel.program (fn () =>

   806     Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}

   807   )

   808 *}

   809 

   810 ML {*

   811   fun split_binop_conv t =

   812     let

   813       val (lhs, rhs) = dest_ceq t;

   814       val (bop, _) = dest_cbinop lhs;

   815       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

   816       val [cmT, crT] = Thm.dest_ctyp cr2;

   817     in

   818       Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}

   819     end

   820 *}

   821 

   822 ML {*

   823   fun split_arg_conv t =

   824     let

   825       val (lhs, rhs) = dest_ceq t;

   826       val (lop, larg) = Thm.dest_comb lhs;

   827       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

   828     in

   829       Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}

   830     end

   831 *}

   832 

   833 ML {*

   834   fun split_binop_tac n thm =

   835     let

   836       val concl = Thm.cprem_of thm n;

   837       val (_, cconcl) = Thm.dest_comb concl;

   838       val rewr = split_binop_conv cconcl;

   839     in

   840       rtac rewr n thm

   841     end

   842       handle CTERM _ => Seq.empty

   843 *}

   844 

   845 ML {*

   846   fun split_arg_tac n thm =

   847     let

   848       val concl = Thm.cprem_of thm n;

   849       val (_, cconcl) = Thm.dest_comb concl;

   850       val rewr = split_arg_conv cconcl;

   851     in

   852       rtac rewr n thm

   853     end

   854       handle CTERM _ => Seq.empty

   855 *}

   856 

   857 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)

   858 

   859 lemma trueprop_cong:

   860   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"

   861   by auto

   862 

   863 ML {*

   864   Cong_Tac.cong_tac

   865 *}

   866 

   867 thm QUOT_TYPE_I_fset.R_trans2

   868 ML {*

   869   fun foo_tac' ctxt =

   870     REPEAT_ALL_NEW (FIRST' [

   871 (*      rtac @{thm trueprop_cong},*)

   872       rtac @{thm list_eq_refl},

   873       rtac @{thm cons_preserves},

   874       rtac @{thm mem_respects},

   875       rtac @{thm card1_rsp},

   876       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

   877       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),

   878       Cong_Tac.cong_tac @{thm cong},

   879       rtac @{thm ext}

   880 (*      rtac @{thm eq_reflection},*)

   881 (*      CHANGED o (ObjectLogic.full_atomize_tac)*)

   882     ])

   883 *}

   884 

   885 ML {*

   886   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))

   887   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   888   val cgoal = cterm_of @{theory} goal

   889   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

   890 *}

   891 

   892 (*notation ( output) "prop" ("#_" [1000] 1000) *)

   893 notation ( output) "Trueprop" ("#_" [1000] 1000)

   894 

   895 lemma atomize_eqv[atomize]: 

   896   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 

   897 proof

   898   assume "A \<equiv> B" 

   899   then show "Trueprop A \<equiv> Trueprop B" by unfold

   900 next

   901   assume *: "Trueprop A \<equiv> Trueprop B"

   902   have "A = B"

   903   proof (cases A)

   904     case True

   905     have "A" by fact

   906     then show "A = B" using * by simp

   907   next

   908     case False

   909     have "\<not>A" by fact

   910     then show "A = B" using * by auto

   911   qed

   912   then show "A \<equiv> B" by (rule eq_reflection)

   913 qed

   914 

   915 prove {* (Thm.term_of cgoal2) *}

   916   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

   917   apply (atomize(full))

   918   apply (tactic {* foo_tac' @{context} 1 *})

   919   done

   920 

   921 thm length_append (* Not true but worth checking that the goal is correct *)

   922 ML {*

   923   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))

   924   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   925   val cgoal = cterm_of @{theory} goal

   926   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

   927 *}

   928 prove {* Thm.term_of cgoal2 *}

   929   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

   930   apply (atomize(full))

   931   apply (tactic {* foo_tac' @{context} 1 *})

   932   sorry

   933 

   934 thm m2

   935 ML {*

   936   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))

   937   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   938   val cgoal = cterm_of @{theory} goal

   939   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

   940 *}

   941 prove {* Thm.term_of cgoal2 *}

   942   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

   943   apply (atomize(full))

   944   apply (tactic {* foo_tac' @{context} 1 *})

   945   done

   946 

   947 thm list_eq.intros(4)

   948 ML {*

   949   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))

   950   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   951   val cgoal = cterm_of @{theory} goal

   952   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

   953   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)

   954 *}

   955 

   956 (* It is the same, but we need a name for it. *)

   957 prove zzz : {* Thm.term_of cgoal3 *}

   958   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

   959   apply (atomize(full))

   960   apply (tactic {* foo_tac' @{context} 1 *})

   961   done

   962 

   963 lemma zzz' :

   964   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"

   965   using list_eq.intros(4) by (simp only: zzz)

   966 

   967 thm QUOT_TYPE_I_fset.REPS_same

   968 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}

   969 

   970 

   971 thm list_eq.intros(5)

   972 ML {*

   973   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))

   974   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs

   975 *}

   976 ML {*

   977   val cgoal =

   978     Toplevel.program (fn () =>

   979       cterm_of @{theory} goal

   980     )

   981 *}

   982 ML {*

   983   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)

   984 *}

   985 prove {* Thm.term_of cgoal2 *}

   986   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

   987   apply (atomize(full))

   988   apply (tactic {* foo_tac' @{context} 1 *})

   989   done

   990 

   991 section {* handling quantifiers - regularize *}