414 

   414 section {* ATOMIZE *}

   415 text {* finite set example *}

   416 print_syntax

   417 inductive

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

   419 where

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

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

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

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

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

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

   426 

   427 lemma list_eq_refl:

   428   shows "xs \<approx> xs"

   429   apply (induct xs)

   430    apply (auto intro: list_eq.intros)

   431   done

   432 

   433 lemma equiv_list_eq:

   434   shows "EQUIV list_eq"

   435   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

   436   apply(auto intro: list_eq.intros list_eq_refl)

   437   done

   438 

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

   440   apply(rule equiv_list_eq)

   441   done

   442 

   443 print_theorems

   444 

   445 typ "'a fset"

   446 thm "Rep_fset"

   447 

   448 local_setup {*

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

   450 *}

   451 

   452 term Nil

   453 term EMPTY

   454 thm EMPTY_def

   455 

   456 

   457 local_setup {*

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

   459 *}

   460 

   461 term Cons

   462 term INSERT

   463 thm INSERT_def

   464 

   465 local_setup {*

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

   467 *}

   468 

   469 term append

   470 term UNION

   471 thm UNION_def

   472 

   473 

   474 thm QUOTIENT_fset

   475 

   476 thm QUOT_TYPE_I_fset.thm11

   477 

   478 

   479 fun

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

   481 where

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

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

   484 

   485 lemma mem_respects:

   486   fixes z

   487   assumes a: "list_eq x y"

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

   489   using a by induct auto

   490 

   491 

   492 fun

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

   494 where

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

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

   497 

   498 local_setup {*

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

   500 *}

   501 

   502 term card1

   503 term card

   504 thm card_def

   505 

   506 (* text {*

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

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

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

   510 *}*)

   511 

   512 lemma card1_rsp:

   513   fixes a b :: "'a list"

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

   515   shows "card1 a = card1 b"

   516   using e apply induct

   517   apply (simp_all add:mem_respects)

   518   done

   519 

   520 lemma card1_0:

   521   fixes a :: "'a list"

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

   523   apply (induct a)

   524    apply (simp)

   525   apply (simp_all)

   526    apply meson

   527   apply (simp_all)

   528   done

   529 

   530 lemma not_mem_card1:

   531   fixes x :: "'a"

   532   fixes xs :: "'a list"

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

   534   by simp

   535 

   536 

   537 lemma mem_cons:

   538   fixes x :: "'a"

   539   fixes xs :: "'a list"

   540   assumes a : "x memb xs"

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

   542   using a

   543   apply (induct xs)

   544   apply (auto intro: list_eq.intros)

   545   done

   546 

   547 lemma card1_suc:

   548   fixes xs :: "'a list"

   549   fixes n :: "nat"

   550   assumes c: "card1 xs = Suc n"

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

   552   using c

   553 apply(induct xs)

   554 apply (metis Suc_neq_Zero card1_0)

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

   556 done

   557 

   558 primrec

   559   fold1

   560 where

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

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

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

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

   565      then (

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

   567      ) else z)"

   568 

   569 (* fold1_def is not usable, but: *)

   570 thm fold1.simps

   571 

   572 lemma cons_preserves:

   573   fixes z

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

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

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

   577 

   578 lemma fs1_strong_cases:

   579   fixes X :: "'a list"

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

   581   apply (induct X)

   582   apply (simp)

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

   584   done

   585 

   586 local_setup {*

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

   588 *}

   589 

   590 term membship

   591 term IN

   592 thm IN_def

   593 

   594 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]

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

   596 

   597 lemma yy:

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

   599 unfolding IN_def EMPTY_def

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

   601 apply(rule mem_respects)

   602 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   603 apply(rule list_eq.intros)

   604 done

   605 

   606 lemma

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

   608 using m1

   609 apply -

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

   611 apply(simp)

   612 done

   613 

   614 lemma

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

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

   617 unfolding IN_def INSERT_def

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

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

   620 apply(rule mem_respects)

   621 apply(rule list_eq.intros(3))

   622 apply(unfold REP_fset_def ABS_fset_def)

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

   624 apply(rule list_eq_refl)

   625 done

   626 

   627 lemma append_respects_fst:

   628   assumes a : "list_eq l1 l2"

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

   630   using a

   631   apply(induct)

   632   apply(auto intro: list_eq.intros)

   633   apply(simp add: list_eq_refl)

   634 done

   635 

   636 lemma yyy:

   637   shows "

   638     (

   639      (UNION EMPTY s = s) &

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

   641     ) = (

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

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

   644     )"

   645   unfolding UNION_def EMPTY_def INSERT_def

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

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

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

   649   apply(rule append_respects_fst)

   650   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   651   apply(rule list_eq_refl)

   652   apply(simp)

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

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

   655   apply(rule append_respects_fst)

   656   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   657   apply(rule list_eq_refl)

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

   659   apply(rule list_eq.intros(5))

   660   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   661   apply(rule list_eq_refl)

   662 done

   663 

   664 lemma

   665   shows "

   666      (UNION EMPTY s = s) &

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

   668   apply (simp add: yyy)

   669   apply (simp add: QUOT_TYPE_I_fset.thm10)

   670   done

   671 

   672 ML {*

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

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

   675   val consts = [@{const_name "Nil"}, @{const_name "Cons"},

   676                 @{const_name "membship"}, @{const_name "card1"},

   677                 @{const_name "append"}, @{const_name "fold1"}];

   678 *}

   679 

   680 ML {* val tm = @{term "x :: 'a list"} *}

   681 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}

   682 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}

   683 

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

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

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

   687 

   688 ML {*

   689 fun needs_lift (rty as Type (rty_s, _)) ty =

   690   case ty of

   691     Type (s, tys) =>

   692       (s = rty_s) orelse (exists (needs_lift rty) tys)

   693   | _ => false

   694 

   695 *}

   696 

   697 ML {*

   698 fun build_goal_term lthy thm constructors rty qty =

   699   let

   700     fun mk_rep tm =

   701       let

   702         val ty = exchange_ty rty qty (fastype_of tm)

   703       in fst (get_fun repF rty qty lthy ty) $ tm end

   704 

   705     fun mk_abs tm =

   706       let

   707         val _ = tracing (Syntax.string_of_term @{context} tm)

   708         val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))

   709         val ty = exchange_ty rty qty (fastype_of tm) in

   710       fst (get_fun absF rty qty lthy ty) $ tm end

   711 

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

   713       | is_constructor _ = false;

   714 

   715     fun build_aux lthy tm =

   716       case tm of

   717       Abs (a as (_, vty, _)) =>

   718       let

   719         val (vs, t) = Term.dest_abs a;

   720         val v = Free(vs, vty);

   721         val t' = lambda v (build_aux lthy t)

   722       in

   723       if (not (needs_lift rty (fastype_of tm))) then t'

   724       else mk_rep (mk_abs (

   725         if not (needs_lift rty vty) then t'

   726         else

   727           let

   728             val v' = mk_rep (mk_abs v);

   729             val t1 = Envir.beta_norm (t' $ v')

   730           in

   731             lambda v t1

   732           end

   733       ))

   734       end

   735     | x =>

   736       let

   737         val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)

   738         val (opp, tms0) = Term.strip_comb tm

   739         val tms = map (build_aux lthy) tms0

   740         val ty = fastype_of tm

   741       in

   742         if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)

   743           then (list_comb (opp, (hd tms0) :: (tl tms)))

   744       else if (is_constructor opp andalso needs_lift rty ty) then

   745           mk_rep (mk_abs (list_comb (opp,tms)))

   746         else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then

   747             mk_rep(mk_abs(list_comb(opp,tms)))

   748         else if tms = [] then opp

   749         else list_comb(opp, tms)

   750       end

   751   in

   752     build_aux lthy (Thm.prop_of thm)

   753   end

   754 

   755 *}

   756 

   757 ML {*

   758 fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =

   759   let

   760     fun mk_rep_abs x = mk_rep (mk_abs x);

   761 

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

   763       | is_constructor _ = false;

   764 

   765     fun maybe_mk_rep_abs t =

   766       let

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

   768       in

   769         if fastype_of t = rty then mk_rep_abs t else t

   770       end;

   771 

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

   773       | is_all _ = false;

   774 

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

   776       | is_ex _ = false;

   777 

   778     fun build_aux ctxt1 tm =

   779       let

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

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

   782       in

   783         (case head of

   784           Abs (x, T, t) =>

   785             if T = rty then let

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

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

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

   789               val rec_term = build_aux ctxt2 t';

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

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

   792             in

   793               Term.lambda_name (x, v) rec_term

   794             end else let

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

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

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

   798               val rec_term = build_aux ctxt2 t';

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

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

   801             if is_all head then

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

   803             else if is_ex head then

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

   805             else if is_constructor head then

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

   807             else

   808               maybe_mk_rep_abs (list_comb (head, args'))

   809         )

   810       end;

   811   in

   812     build_aux ctxt (Thm.prop_of thm)

   813   end

   814 *}

   815 

   816 ML {*

   817 fun build_goal ctxt thm cons rty qty =

   818   Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))

   819 *}

   820 

   821 ML {*

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

   823 *}

   824 

   825 ML {*

   826 cterm_of @{theory} (prop_of m1_novars);

   827 cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});

   828 cterm_of @{theory} (build_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)

   829 *}

   830 

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

   468 ML {*

   890 ML {*

   469 fun atomize_thm thm =

   891   fun transconv_fset_tac' ctxt =

   470 let

   892     (LocalDefs.unfold_tac @{context} fset_defs) THEN

   471   val thm' = forall_intr_vars thm

   893     ObjectLogic.full_atomize_tac 1 THEN

   472   val thm'' = ObjectLogic.atomize (cprop_of thm')

   894     REPEAT_ALL_NEW (FIRST' [

   473 in

   895       rtac @{thm list_eq_refl},

   474   Simplifier.rewrite_rule [thm''] thm'

   896       rtac @{thm cons_preserves},

   475 end

   897       rtac @{thm mem_respects},

   476 *}

   898       rtac @{thm card1_rsp},

   477 

   899       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

   478 

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

   479 section {* REGULARIZE *}

   901       Cong_Tac.cong_tac @{thm cong},

   902       rtac @{thm ext}

   903     ]) 1

   904 *}

   905 

   906 ML {*

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

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

   909   val cgoal = cterm_of @{theory} goal

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

   911 *}

   912 

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

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

   915 

   916 

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

   918   apply (tactic {* transconv_fset_tac' @{context} *})

   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"}

   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 {* transconv_fset_tac' @{context} *})

   930   sorry

   931 

   932 thm m2

   933 ML {*

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

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

   936   val cgoal = cterm_of @{theory} goal

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

   938 *}

   939 prove {* Thm.term_of cgoal2 *}

   940   apply (tactic {* transconv_fset_tac' @{context} *})

   941   done

   942 

   943 thm list_eq.intros(4)

   944 ML {*

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

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

   947   val cgoal = cterm_of @{theory} goal

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

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

   950 *}

   951 

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

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

   954   apply (tactic {* transconv_fset_tac' @{context} *})

   955   done

   956 

   957 (*lemma zzz' :

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

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

   960 

   961 thm QUOT_TYPE_I_fset.REPS_same

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

   963 *)

   964 

   965 thm list_eq.intros(5)

   966 ML {*

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

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

   969   val cgoal = cterm_of @{theory} goal

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

   971 *}

   972 prove {* Thm.term_of cgoal2 *}

   973   apply (tactic {* transconv_fset_tac' @{context} *})

   974   done

   975 

   976 section {* handling quantifiers - regularize *}

  1190 ML {*

   702 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)

  1191 fun atomize_thm thm =

   703   trm == new_trm

  1192 let

   704 *)

  1193   val thm' = forall_intr_vars thm

   705 

  1194   val thm'' = ObjectLogic.atomize (cprop_of thm')

   706 section {* TRANSCONV *}

  1195 in

   707 

  1196   Simplifier.rewrite_rule [thm''] thm'

   708 

  1197 end

   709 ML {*

  1198 *}

   710 fun build_goal_term lthy thm constructors rty qty =

   711   let

   712     fun mk_rep tm =

   713       let

   714         val ty = exchange_ty rty qty (fastype_of tm)

   715       in fst (get_fun repF rty qty lthy ty) $ tm end

   716 

   717     fun mk_abs tm =

   718       let

   719         val _ = tracing (Syntax.string_of_term @{context} tm)

   720         val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))

   721         val ty = exchange_ty rty qty (fastype_of tm) in

   722       fst (get_fun absF rty qty lthy ty) $ tm end

   723 

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

   725       | is_constructor _ = false;

   726 

   727     fun build_aux lthy tm =

   728       case tm of

   729       Abs (a as (_, vty, _)) =>

   730       let

   731         val (vs, t) = Term.dest_abs a;

   732         val v = Free(vs, vty);

   733         val t' = lambda v (build_aux lthy t)

   734       in

   735       if (not (needs_lift rty (fastype_of tm))) then t'

   736       else mk_rep (mk_abs (

   737         if not (needs_lift rty vty) then t'

   738         else

   739           let

   740             val v' = mk_rep (mk_abs v);

   741             val t1 = Envir.beta_norm (t' $ v')

   742           in

   743             lambda v t1

   744           end

   745       ))

   746       end

   747     | x =>

   748       let

   749         val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)

   750         val (opp, tms0) = Term.strip_comb tm

   751         val tms = map (build_aux lthy) tms0

   752         val ty = fastype_of tm

   753       in

   754         if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)

   755           then (list_comb (opp, (hd tms0) :: (tl tms)))

   756       else if (is_constructor opp andalso needs_lift rty ty) then

   757           mk_rep (mk_abs (list_comb (opp,tms)))

   758         else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then

   759             mk_rep(mk_abs(list_comb(opp,tms)))

   760         else if tms = [] then opp

   761         else list_comb(opp, tms)

   762       end

   763   in

   764     build_aux lthy (Thm.prop_of thm)

   765   end

   766 *}

   767 

   768 ML {*

   769 fun build_goal ctxt thm cons rty qty =

   770   Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))

   771 *}

   772 

   773 

   774 

   775 

   776 

   777 text {* finite set example *}

   778 print_syntax

   779 inductive

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

   781 where

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

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

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

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

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

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

   788 

   789 lemma list_eq_refl:

   790   shows "xs \<approx> xs"

   791   apply (induct xs)

   792    apply (auto intro: list_eq.intros)

   793   done

   794 

   795 lemma equiv_list_eq:

   796   shows "EQUIV list_eq"

   797   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

   798   apply(auto intro: list_eq.intros list_eq_refl)

   799   done

   800 

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

   802   apply(rule equiv_list_eq)

   803   done

   804 

   805 print_theorems

   806 

   807 typ "'a fset"

   808 thm "Rep_fset"

   809 

   810 local_setup {*

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

   812 *}

   813 

   814 term Nil

   815 term EMPTY

   816 thm EMPTY_def

   817 

   818 

   819 local_setup {*

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

   821 *}

   822 

   823 term Cons

   824 term INSERT

   825 thm INSERT_def

   826 

   827 local_setup {*

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

   829 *}

   830 

   831 term append

   832 term UNION

   833 thm UNION_def

   834 

   835 

   836 thm QUOTIENT_fset

   837 

   838 thm QUOT_TYPE_I_fset.thm11

   839 

   840 

   841 fun

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

   843 where

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

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

   846 

   847 lemma mem_respects:

   848   fixes z

   849   assumes a: "list_eq x y"

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

   851   using a by induct auto

   852 

   853 

   854 fun

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

   856 where

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

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

   859 

   860 local_setup {*

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

   862 *}

   863 

   864 term card1

   865 term card

   866 thm card_def

   867 

   868 (* text {*

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

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

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

   872 *}*)

   873 

   874 lemma card1_rsp:

   875   fixes a b :: "'a list"

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

   877   shows "card1 a = card1 b"

   878   using e apply induct

   879   apply (simp_all add:mem_respects)

   880   done

   881 

   882 lemma card1_0:

   883   fixes a :: "'a list"

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

   885   apply (induct a)

   886    apply (simp)

   887   apply (simp_all)

   888    apply meson

   889   apply (simp_all)

   890   done

   891 

   892 lemma not_mem_card1:

   893   fixes x :: "'a"

   894   fixes xs :: "'a list"

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

   896   by simp

   897 

   898 

   899 lemma mem_cons:

   900   fixes x :: "'a"

   901   fixes xs :: "'a list"

   902   assumes a : "x memb xs"

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

   904   using a

   905   apply (induct xs)

   906   apply (auto intro: list_eq.intros)

   907   done

   908 

   909 lemma card1_suc:

   910   fixes xs :: "'a list"

   911   fixes n :: "nat"

   912   assumes c: "card1 xs = Suc n"

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

   914   using c

   915 apply(induct xs)

   916 apply (metis Suc_neq_Zero card1_0)

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

   918 done

   919 

   920 primrec

   921   fold1

   922 where

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

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

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

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

   927      then (

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

   929      ) else z)"

   930 

   931 (* fold1_def is not usable, but: *)

   932 thm fold1.simps

   933 

   934 lemma cons_preserves:

   935   fixes z

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

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

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

   939 

   940 lemma fs1_strong_cases:

   941   fixes X :: "'a list"

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

   943   apply (induct X)

   944   apply (simp)

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

   946   done

   947 

   948 local_setup {*

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

   950 *}

   951 

   952 term membship

   953 term IN

   954 thm IN_def

   955 

   956 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]

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

   958 

   959 lemma yy:

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

   961 unfolding IN_def EMPTY_def

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

   963 apply(rule mem_respects)

   964 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

   965 apply(rule list_eq.intros)

   966 done

   967 

   968 lemma

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

   970 using m1

   971 apply -

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

   973 apply(simp)

   974 done

   975 

   976 lemma

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

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

   979 unfolding IN_def INSERT_def

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

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

   982 apply(rule mem_respects)

   983 apply(rule list_eq.intros(3))

   984 apply(unfold REP_fset_def ABS_fset_def)

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

   986 apply(rule list_eq_refl)

   987 done

   988 

   989 lemma append_respects_fst:

   990   assumes a : "list_eq l1 l2"

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

   992   using a

   993   apply(induct)

   994   apply(auto intro: list_eq.intros)

   995   apply(simp add: list_eq_refl)

   996 done

   997 

   998 lemma yyy:

   999   shows "

  1000     (

  1001      (UNION EMPTY s = s) &

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

  1003     ) = (

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

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

  1006     )"

  1007   unfolding UNION_def EMPTY_def INSERT_def

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

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

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

  1011   apply(rule append_respects_fst)

  1012   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1013   apply(rule list_eq_refl)

  1014   apply(simp)

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

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

  1017   apply(rule append_respects_fst)

  1018   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1019   apply(rule list_eq_refl)

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

  1021   apply(rule list_eq.intros(5))

  1022   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1023   apply(rule list_eq_refl)

  1024 done

  1025 

  1026 lemma

  1027   shows "

  1028      (UNION EMPTY s = s) &

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

  1030   apply (simp add: yyy)

  1031   apply (simp add: QUOT_TYPE_I_fset.thm10)

  1032   done

  1033 

  1034 ML {*

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

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

  1037   val consts = [@{const_name "Nil"}, @{const_name "Cons"},

  1038                 @{const_name "membship"}, @{const_name "card1"},

  1039                 @{const_name "append"}, @{const_name "fold1"}];

  1040 *}

  1041 

  1042 ML {* val tm = @{term "x :: 'a list"} *}

  1043 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}

  1044 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}

  1045 

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

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

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

  1049 

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

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

  1052 

  1053 

  1054 

  1055 ML {*

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

  1057 *}

  1058 

  1059 ML {*

  1060 cterm_of @{theory} (prop_of m1_novars);

  1061 cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});

  1062 *}

  1063 

  1064 

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

  1066 ML {*

  1067   fun transconv_fset_tac' ctxt =

  1068     (LocalDefs.unfold_tac @{context} fset_defs) THEN

  1069     ObjectLogic.full_atomize_tac 1 THEN

  1070     REPEAT_ALL_NEW (FIRST' [

  1071       rtac @{thm list_eq_refl},

  1072       rtac @{thm cons_preserves},

  1073       rtac @{thm mem_respects},

  1074       rtac @{thm card1_rsp},

  1075       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

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

  1077       Cong_Tac.cong_tac @{thm cong},

  1078       rtac @{thm ext}

  1079     ]) 1

  1080 *}

  1081 

  1082 ML {*

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

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

  1085   val cgoal = cterm_of @{theory} goal

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

  1087 *}

  1088 

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

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

  1091 

  1092 

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

  1094   apply (tactic {* transconv_fset_tac' @{context} *})

  1095   done

  1096 

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

  1098 ML {*

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

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

  1101   val cgoal = cterm_of @{theory} goal

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

  1103 *}

  1104 prove {* Thm.term_of cgoal2 *}

  1105   apply (tactic {* transconv_fset_tac' @{context} *})

  1106   sorry

  1107 

  1108 thm m2

  1109 ML {*

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

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

  1112   val cgoal = cterm_of @{theory} goal

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

  1114 *}

  1115 prove {* Thm.term_of cgoal2 *}

  1116   apply (tactic {* transconv_fset_tac' @{context} *})

  1117   done

  1118 

  1119 thm list_eq.intros(4)

  1120 ML {*

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

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

  1123   val cgoal = cterm_of @{theory} goal

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

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

  1126 *}

  1127 

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

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

  1130   apply (tactic {* transconv_fset_tac' @{context} *})

  1131   done

  1132 

  1133 (*lemma zzz' :

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

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

  1136 

  1137 thm QUOT_TYPE_I_fset.REPS_same

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

  1139 *)

  1140 

  1141 thm list_eq.intros(5)

  1142 ML {*

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

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

  1145   val cgoal = cterm_of @{theory} goal

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

  1147 *}

  1148 prove {* Thm.term_of cgoal2 *}

  1149   apply (tactic {* transconv_fset_tac' @{context} *})

  1150   done

  1151