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.
FSet.thy
changeset 479 24799397a3ce
parent 478 b0e572776612
child 480 7fbbb2690bc5
equal deleted inserted replaced
478:b0e572776612 479:24799397a3ce 
   307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   307 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   308 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
 
   308 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
 
   309 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 
   309 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 
   310 done
 
   310 done
 
   311 
   311 
   312 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 
       
   313 by (simp add: QUOT_TRUE_def)
 
       
   314 
       
   315 ML {*
 
       
   316 fun quot_true_tac' ctxt fnctn =
 
       
   317   CSUBGOAL (fn (cgl, i) =>
 
       
   318   let
 
       
   319     val gl = term_of cgl;
 
       
   320     val thy = ProofContext.theory_of ctxt;
 
       
   321     fun find_fun trm =
 
       
   322       case trm of
 
       
   323         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
 
       
   324       | _ => false
 
       
   325   in
 
       
   326     case find_first find_fun (Logic.strip_assums_hyp gl) of
 
       
   327       SOME (asm as (_ $ (_ $ x))) =>
 
       
   328         let
 
       
   329           val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
 
       
   330           val _ = tracing (Syntax.string_of_term @{context} (prop_of (thm')))
 
       
   331           val ps = Logic.strip_params (Thm.concl_of thm');
 
       
   332           val fx = fnctn x;
 
       
   333           val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
 
       
   334             val insts = [(fx', fx)]
 
       
   335             |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
 
       
   336           val thm_i = Drule.cterm_instantiate insts thm'
 
       
   337           val thm_j = Thm.forall_elim_vars 0 thm_i
 
       
   338         in
 
       
   339           dtac thm_j i
 
       
   340         end
 
       
   341     | NONE => error "quot_true_tac!"
 
       
   342     | _ => error "quot_true_tac!!"
 
       
   343   end)
 
       
   344 *}
 
       
   345 
       
   346 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   347 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   313 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   348 
   314 
   349 lemma "INSERT a (INSERT a x) = INSERT a x"
 
   315 lemma "INSERT a (INSERT a x) = INSERT a x"
 
   350 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
 
   316 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
 
   359 done
 
   325 done
 
   360 
   326 
   361 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 
   327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 
   362 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 
   328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 
   363 done
 
   329 done
 
   364 
       
   365 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
       
   366 
   330 
   367 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   331 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   368   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   332   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   369 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   333 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   370 done
 
   334 done
 
   377 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 
   341 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 
   378 done
 
   342 done
 
   379 
   343 
   380 lemma cheat: "P" sorry
 
   344 lemma cheat: "P" sorry
 
   381 
   345 
       
   346 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
   382 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
 
   347 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
 
   383 
       
   384 ML {*
 
       
   385 fun quot_true_conv1 ctxt fnctn ctrm =
 
       
   386   case (term_of ctrm) of
 
       
   387     (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ x)) =>
 
       
   388     let
 
       
   389       val _ = tracing "A";
 
       
   390       val fx = fnctn x;
 
       
   391       val thy = ProofContext.theory_of ctxt;
 
       
   392       val cx = cterm_of thy x;
 
       
   393       val cfx = cterm_of thy fx;
 
       
   394       val cxt = ctyp_of thy (fastype_of x);
 
       
   395       val cfxt = ctyp_of thy (fastype_of fx);
 
       
   396       val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
 
       
   397       val _ = tracing (Syntax.string_of_term @{context} (prop_of thm));
 
       
   398     in
 
       
   399       Conv.rewr_conv thm ctrm
 
       
   400     end
 
       
   401 *}
 
       
   402 
       
   403 ML {*
 
       
   404 fun quot_true_conv ctxt fnctn ctrm =
 
       
   405   case (term_of ctrm) of
 
       
   406     (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) =>
 
       
   407       quot_true_conv1 ctxt fnctn ctrm
 
       
   408   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
 
       
   409   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
 
       
   410   | _ => Conv.all_conv ctrm
 
       
   411 *}
 
       
   412 
       
   413 ML CONVERSION
 
       
   414 ML {*
 
       
   415 fun quot_true_tac ctxt fnctn = CONVERSION (
 
       
   416   fn ctrm => 
       
   417     let
 
       
   418       val _ = tracing "B";
 
       
   419       val t = quot_true_conv ctxt fnctn ctrm;
 
       
   420       val _ = tracing "C";
 
       
   421     in
 
       
   422       t
 
       
   423     end)
 
       
   424 *}
 
       
   425 
   348 
   426 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   427 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   350 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   428 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   351 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   429 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   352 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   430 prefer 2
 
   353 prefer 2
 
   431 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 
   354 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 
   432 apply (tactic {* quot_true_tac @{context} (fst o dest_comb) 1 *}) apply(assumption)
 
       
   433 
       
   434 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   355 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   435 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   356 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   436 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   357 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   437 apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption)
 
       
   438 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   358 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   439 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   359 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   440 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   360 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   441 apply (drule QT_lam)
 
   361 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   442 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   362 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   443 apply (tactic {* quot_true_tac' @{context} (fst o dest_comb) 1 *})
 
   363 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   444 apply (assumption)
 
   364 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   445 apply (assumption)
 
   365 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   446 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
 
   366 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
 
   447 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   367 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   448 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   368 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* D *) (* reflexivity of basic relations *)
 
   449 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   369 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   450 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   370 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   451 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   371 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   452 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   372 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   453 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
 
   373 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   454 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   374 
   455 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   375 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
 
   456 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   376 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   457 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   377 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   458 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   378 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   459 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
 
   379 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   460 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   380 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 
   461 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   381 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   462 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   382 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   463 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
       
   464 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
       
   465 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
       
   466 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
       
   467 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   468 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   469 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   470 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   471 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
nominal2