nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:f078dbf557b7
+:d98224cafb86
 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
 |> Variable.variant_frees lthy [rel]
 |> map Free
 in
 lambda c
 (HOLogic.exists_const ty $
 lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
 let
 val typedef_tac =
 EVERY1 [rewrite_goal_tac @{thms mem_def},
 rtac @{thm exI},
 rtac @{thm exI},
 rtac @{thm refl}]
 in
 LocalTheory.theory_result
 (Typedef.add_typedef false NONE
 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
 val typedef_quotient_thm_tac =
 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
 rtac @{thm QUOT_TYPE.QUOTIENT},
 rtac quot_type_thm]
 in
 Goal.prove lthy [] [] goal
 (K typedef_quotient_thm_tac)
 end
 *}
 text {* two wrappers for define and note *}
 datatype trm =
 var  "nat"
 | app  "trm" "trm"
 | lam  "nat" "trm"
 axiomatization
 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 where
 r_eq: "EQUIV RR"
 local_setup {*
 typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 end
 *}
 ML {*
 fun exchange_ty rty qty ty =
 if ty = rty
 then qty
 else
 (case ty of
 Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
 | _ => ty
 lemma mem_cons:
 fixes x :: "'a"
 fixes xs :: "'a list"
 assumes a : "x memb xs"
 shows "x # xs \<approx> xs"
 using a
 apply (induct xs)
 apply (auto intro: list_eq.intros)
 done
 lemma card1_suc:
 fixes xs :: "'a list"
 fixes n :: "nat"
 assumes c: "card1 xs = Suc n"
 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
 using c
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
-apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
 done
 lemma cons_preserves:
 fixes z
 assumes a: "xs \<approx> ys"
 shows "(z # xs) \<approx> (z # ys)"
 using a by (rule QuotMain.list_eq.intros(5))
 text {*
 Unlam_def converts a definition given as
 c \<equiv> %x. %y. f x y
 to a theorem of the form
 c x y \<equiv> f x y
 This function is needed to rewrite the right-hand
 side to the left-hand side.
 *}
 apply (simp add: QUOT_TYPE_I_fset.thm10)
 done
 ML {*
 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
 val consts = [@{const_name "Nil"}, @{const_name "append"},
 @{const_name "Cons"}, @{const_name "membship"},
 @{const_name "card1"}]
 *}
 ML {*
 fun build_goal ctxt thm constructors lifted_type mk_rep_abs =
 ML {*
 fun build_goal' ctxt thm constructors lifted_type mk_rep_abs =
 let
 fun is_const (Const (x, t)) = member (op =) constructors x
 | is_const _ = false
 fun maybe_mk_rep_abs t =
 let
 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
 in
 if type_of t = lifted_type then mk_rep_abs t else t
 (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args)))
 else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args)
 end
 | build_aux _ x =
 if is_const x then maybe_mk_rep_abs x else x
 val concl2 = term_of (#prop (crep_thm thm))
 in
 Logic.mk_equals (build_aux ctxt concl2, concl2)
 end *}
 CHANGED o (ObjectLogic.full_atomize_tac)
 ])
 *}
 ML {*
-<<<<<<< variant A
 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
->>>>>>> variant B
-val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
-val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
-####### Ancestor
-val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-======= end
 val cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 qed
 prove {* (Thm.term_of cgoal2) *}
 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-apply (atomize (full))
-apply (rule trueprop_cong)
 apply (tactic {* foo_tac' @{context} 1 *})
-thm eq_reflection
 done
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
-val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 val cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 sorry
 thm m2
 ML {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 val cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 done
 thm list_eq.intros(4)
 ML {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
-val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 val cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
 *}
 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
 thm list_eq.intros(5)
 ML {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
-val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
 val cgoal =
 Toplevel.program (fn () =>
 cterm_of @{theory} goal
 ML {*
 fun lift_theorem_fset_aux thm lthy =
 let
 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
-val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs;
+val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_abs;
 val cgoal = cterm_of @{theory} goal;
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML {* @{term "\<exists>x. P x"} *}
 ML {*  Thm.bicompose *}
 prove {* (Thm.term_of cgoal2) *}
 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 apply (tactic {* foo_tac' @{context} 1 *})
 (*
 datatype obj1 =

changeset 45	d98224cafb86
parent 44	f078dbf557b7
child 46	e801b929216b