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.
QuotMain.thy
changeset 101 4f93c5a026d2
parent 100 09f4d69f7b66
child 102 9d41f680d755
child 103 4aef3882b436
equal deleted inserted replaced
100:09f4d69f7b66 101:4f93c5a026d2 
   772 ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
 
   772 ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
 
   773 
   773 
   774 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 
   774 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 
   775 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
   775 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
   776 
   776 
   777 ML {*
 
       
   778   fun dest_cbinop t =
 
       
   779     let
 
       
   780       val (t2, rhs) = Thm.dest_comb t;
 
       
   781       val (bop, lhs) = Thm.dest_comb t2;
 
       
   782     in
 
       
   783       (bop, (lhs, rhs))
 
       
   784     end
 
       
   785 *}
 
       
   786 
       
   787 ML {*
 
       
   788   fun dest_ceq t =
 
       
   789     let
 
       
   790       val (bop, pair) = dest_cbinop t;
 
       
   791       val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
 
       
   792     in
 
       
   793       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
 
       
   794     end
 
       
   795 *}
 
       
   796 
       
   797 ML Thm.instantiate
 
       
   798 ML {*@{thm arg_cong2}*}
 
       
   799 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
 
       
   800 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
 
       
   801 ML {*
 
       
   802   Toplevel.program (fn () =>
 
       
   803     Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
 
       
   804   )
 
       
   805 *}
 
       
   806 
       
   807 ML {*
 
       
   808   fun split_binop_conv t =
 
       
   809     let
 
       
   810       val (lhs, rhs) = dest_ceq t;
 
       
   811       val (bop, _) = dest_cbinop lhs;
 
       
   812       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
 
       
   813       val [cmT, crT] = Thm.dest_ctyp cr2;
 
       
   814     in
 
       
   815       Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
 
       
   816     end
 
       
   817 *}
 
       
   818 
       
   819 ML {*
 
       
   820   fun split_arg_conv t =
 
       
   821     let
 
       
   822       val (lhs, rhs) = dest_ceq t;
 
       
   823       val (lop, larg) = Thm.dest_comb lhs;
 
       
   824       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
 
       
   825     in
 
       
   826       Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
 
       
   827     end
 
       
   828 *}
 
       
   829 
       
   830 ML {*
 
       
   831   fun split_binop_tac n thm =
 
       
   832     let
 
       
   833       val concl = Thm.cprem_of thm n;
 
       
   834       val (_, cconcl) = Thm.dest_comb concl;
 
       
   835       val rewr = split_binop_conv cconcl;
 
       
   836     in
 
       
   837       rtac rewr n thm
 
       
   838     end
 
       
   839       handle CTERM _ => Seq.empty
 
       
   840 *}
 
       
   841 
       
   842 ML {*
 
       
   843   fun split_arg_tac n thm =
 
       
   844     let
 
       
   845       val concl = Thm.cprem_of thm n;
 
       
   846       val (_, cconcl) = Thm.dest_comb concl;
 
       
   847       val rewr = split_arg_conv cconcl;
 
       
   848     in
 
       
   849       rtac rewr n thm
 
       
   850     end
 
       
   851       handle CTERM _ => Seq.empty
 
       
   852 *}
 
       
   853 
       
   854 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 
   777 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 
   855 
   778 ML {*
 
   856 lemma trueprop_cong:
 
   779   fun transconv_fset_tac' ctxt =
 
   857   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
 
       
   858   by auto
 
       
   859 
       
   860 ML {*
 
       
   861   Cong_Tac.cong_tac
 
       
   862 *}
 
       
   863 
       
   864 thm QUOT_TYPE_I_fset.R_trans2
 
       
   865 ML {*
 
       
   866   fun foo_tac' ctxt =
 
       
   867     REPEAT_ALL_NEW (FIRST' [
 
   780     REPEAT_ALL_NEW (FIRST' [
 
   868 (*      rtac @{thm trueprop_cong},*)
 
       
   869       rtac @{thm list_eq_refl},
 
   781       rtac @{thm list_eq_refl},
 
   870       rtac @{thm cons_preserves},
 
   782       rtac @{thm cons_preserves},
 
   871       rtac @{thm mem_respects},
 
   783       rtac @{thm mem_respects},
 
   872       rtac @{thm card1_rsp},
 
   784       rtac @{thm card1_rsp},
 
   873       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
 
   785       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
 
   874       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
 
   786       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
 
   875       Cong_Tac.cong_tac @{thm cong},
 
   787       Cong_Tac.cong_tac @{thm cong},
 
   876       rtac @{thm ext}
 
   788       rtac @{thm ext}
 
   877 (*      rtac @{thm eq_reflection},*)
 
       
   878 (*      CHANGED o (ObjectLogic.full_atomize_tac)*)
 
       
   879     ])
 
   789     ])
 
   880 *}
 
   790 *}
 
   881 
   791 
   882 ML {*
 
   792 ML {*
 
   883   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 
   793   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 
   910 qed
 
   820 qed
 
   911 
   821 
   912 prove {* (Thm.term_of cgoal2) *}
 
   822 prove {* (Thm.term_of cgoal2) *}
 
   913   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   823   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   914   apply (atomize(full))
 
   824   apply (atomize(full))
 
   915   apply (tactic {* foo_tac' @{context} 1 *})
 
   825   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
   916   done
 
   826   done
 
   917 
   827 
   918 thm length_append (* Not true but worth checking that the goal is correct *)
 
   828 thm length_append (* Not true but worth checking that the goal is correct *)
 
   919 ML {*
 
   829 ML {*
 
   920   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
 
   830   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
 
   923   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   833   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   924 *}
 
   834 *}
 
   925 prove {* Thm.term_of cgoal2 *}
 
   835 prove {* Thm.term_of cgoal2 *}
 
   926   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   836   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   927   apply (atomize(full))
 
   837   apply (atomize(full))
 
   928   apply (tactic {* foo_tac' @{context} 1 *})
 
   838   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
   929   sorry
 
   839   sorry
 
   930 
   840 
   931 thm m2
 
   841 thm m2
 
   932 ML {*
 
   842 ML {*
 
   933   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   843   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   936   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   846   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   937 *}
 
   847 *}
 
   938 prove {* Thm.term_of cgoal2 *}
 
   848 prove {* Thm.term_of cgoal2 *}
 
   939   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   849   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   940   apply (atomize(full))
 
   850   apply (atomize(full))
 
   941   apply (tactic {* foo_tac' @{context} 1 *})
 
   851   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
   942   done
 
   852   done
 
   943 
   853 
   944 thm list_eq.intros(4)
 
   854 thm list_eq.intros(4)
 
   945 ML {*
 
   855 ML {*
 
   946   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
 
   856   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
 
   952 
   862 
   953 (* It is the same, but we need a name for it. *)
 
   863 (* It is the same, but we need a name for it. *)
 
   954 prove zzz : {* Thm.term_of cgoal3 *}
 
   864 prove zzz : {* Thm.term_of cgoal3 *}
 
   955   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   865   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   956   apply (atomize(full))
 
   866   apply (atomize(full))
 
   957   apply (tactic {* foo_tac' @{context} 1 *})
 
   867   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
   958   done
 
   868   done
 
   959 
   869 
   960 lemma zzz' :
 
   870 lemma zzz' :
 
   961   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
 
   871   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
 
   962   using list_eq.intros(4) by (simp only: zzz)
 
   872   using list_eq.intros(4) by (simp only: zzz)
 
   980   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
   890   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
   981 *}
 
   891 *}
 
   982 prove {* Thm.term_of cgoal2 *}
 
   892 prove {* Thm.term_of cgoal2 *}
 
   983   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   893   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   984   apply (atomize(full))
 
   894   apply (atomize(full))
 
   985   apply (tactic {* foo_tac' @{context} 1 *})
 
   895   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
   986   done
 
   896   done
 
   987 
   897 
   988 section {* handling quantifiers - regularize *}
 
   898 section {* handling quantifiers - regularize *}
 
   989 
   899 
   990 text {* tyRel takes a type and builds a relation that a quantifier over this
 
   900 text {* tyRel takes a type and builds a relation that a quantifier over this
 
  1213 *}
 
  1123 *}
 
  1214 
  1124 
  1215 prove {* (Thm.term_of cgoal2) *}
 
  1125 prove {* (Thm.term_of cgoal2) *}
 
  1216   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
  1126   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
  1217   apply (atomize(full))
 
  1127   apply (atomize(full))
 
  1218   apply (tactic {* foo_tac' @{context} 1 *})
 
  1128   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
  1219   sorry
 
  1129   sorry
 
  1220 
  1130 
  1221 ML {*
 
  1131 ML {*
 
  1222   fun lift_theorem_fset_aux thm lthy =
 
  1132   fun lift_theorem_fset_aux thm lthy =
 
  1223     let
 
  1133     let
 
  1224       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
 
  1134       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
 
  1225       val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
 
  1135       val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
 
  1226       val cgoal = cterm_of @{theory} goal;
 
  1136       val cgoal = cterm_of @{theory} goal;
 
  1227       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
 
  1137       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
 
  1228       val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1;
 
  1138       val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (transconv_fset_tac' @{context}) 1;
 
  1229       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
 
  1139       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
 
  1230       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
 
  1140       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
 
  1231       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
 
  1141       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
 
  1232       val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
 
  1142       val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
 
  1233     in
 
  1143     in
 
  1378 
  1288 
  1379 
  1289 
  1380 (*prove aaa: {* (Thm.term_of cgoal2) *}
 
  1290 (*prove aaa: {* (Thm.term_of cgoal2) *}
 
  1381   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
  1291   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
  1382   apply (atomize(full))
 
  1292   apply (atomize(full))
 
  1383   apply (tactic {* foo_tac' @{context} 1 *})
 
  1293   apply (tactic {* transconv_fset_tac' @{context} 1 *})
 
  1384   done*)
 
  1294   done*)
 
  1385 
  1295 
  1386 (*
 
  1296 (*
 
  1387 datatype obj1 =
 
  1297 datatype obj1 =
 
  1388   OVAR1 "string"
 
  1298   OVAR1 "string"
nominal2