nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:55b646c6c4cd
+:ce522150c1f7
 term append
 term UNION
 thm UNION_def
+(* Maybe the infrastructure should not allow this kind of definition, without showing that
+the relation respects lenght... *)
 local_setup {*
 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 term length
 *}
 term membship
 term IN
 thm IN_def
+ML {* unlam_def @{context} @{context} @{thm IN_def} *}
 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
 lemma yy:
 apply(induct)
 apply(auto intro: list_eq.intros)
 apply(simp add: list_eq_sym)
 done
-lemma yyy :
+lemma yyy:
 shows "
 (
 (UNION EMPTY s = s) &
 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
 ) = (
 unfolding UNION_def EMPTY_def INSERT_def
 apply(rule_tac f="(op &)" in arg_cong2)
 apply(rule_tac f="(op =)" in arg_cong2)
 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
 apply(rule append_respects_fst)
-apply(simp only:QUOT_TYPE_I_fset.REP_ABS_rsp)
+apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply(rule list_eq_sym)
 apply(simp)
 apply(rule_tac f="(op =)" in arg_cong2)
 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
 apply(rule append_respects_fst)
 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
+thm m1
 ML {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 val cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 apply(rule_tac f="(op =)" in arg_cong2)
 unfolding IN_def EMPTY_def
 apply (rule_tac mem_respects)
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (simp_all)
 apply (rule list_eq_sym)
 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 cgoal = cterm_of @{theory} goal
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
 *}
+(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+unfolding CARD_def UNION_def
+apply(rule_tac f="(op =)" in arg_cong2)*)
 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
 unfolding INSERT_def
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule cons_preserves)
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
-apply(rule_tac f="(op \<or>)" in arg_cong2)
+apply (rule_tac f="(op \<or>)" in arg_cong2)
 apply (simp)
 apply (rule_tac mem_respects)
 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
 done
+notation ( output) "prop" ("#_" [1000] 1000)
+ML {* @{thm arg_cong2} *}
+ML {* rtac *}
+ML {* Term.dest_Const @{term "op ="} *}
+ML {*
+fun dest_cbinop t =
+let
+val (t2, rhs) = Thm.dest_comb t;
+val (bop, lhs) = Thm.dest_comb t2;
+in
+(bop, (lhs, rhs))
+end
+*}
+ML {*
+fun dest_ceq t =
+let
+val (bop, pair) = dest_cbinop t;
+val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+in
+if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
+end
+*}
+ML {*
+fun foo_conv ctxt t =
+let
+val (lhs, rhs) = dest_ceq t;
+val (bop, _) = dest_cbinop lhs;
+(*      val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of lhs))*)
+in
+@{thm arg_cong2}
+end
+*}
+ML {*
+fun foo_tac ctxt thm =
+let
+val concl = Thm.concl_of thm;
+val (_, cconcl) = Thm.dest_comb (Thm.cterm_of @{theory} concl);
+val (_, cconcl) = Thm.dest_comb cconcl;
+val rewr = foo_conv ctxt cconcl;
+val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of cconcl))
+in
+Seq.single thm
+end
+*}
+ML {* Thm.assume @{cprop "0 = 0"} *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+apply (tactic {* foo_tac @{context} *})
+(*
+datatype obj1 =
+OVAR1 "string"
+| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
+| INVOKE1 "obj1 \<Rightarrow> string"
+| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
+*)

changeset 18	ce522150c1f7
parent 17	55b646c6c4cd
child 19	55aefc2d524a