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.
Nominal/Fv.thy
changeset 1656 c9d3dda79fe3
parent 1653 a2142526bb01
child 1658 aacab5f67333
equal deleted inserted replaced
1655:9cec4269b7f9 1656:c9d3dda79fe3 
   142 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 
   142 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
 
   143   | is_atom_set thy _ = false;
 
   143   | is_atom_set thy _ = false;
 
   144 
   144 
   145 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
 
   145 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
 
   146   | is_atom_fset thy _ = false;
 
   146   | is_atom_fset thy _ = false;
 
   147 
   147 *}
 
   148 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 
       
   149 *}
 
       
   150 
       
   151 
       
   152 
   148 
   153 
   149 
   154 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 
   150 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 
   155 ML {*
 
   151 ML {*
 
   156 fun map2i _ [] [] = []
 
   152 fun map2i _ [] [] = []
 
   213   fun mk_atom_fset t =
 
   209   fun mk_atom_fset t =
 
   214     let
 
   210     let
 
   215       val ty = fastype_of t;
 
   211       val ty = fastype_of t;
 
   216       val atom_ty = dest_fsetT ty --> @{typ atom};
 
   212       val atom_ty = dest_fsetT ty --> @{typ atom};
 
   217       val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
 
   213       val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
 
       
   214       val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 
   218     in
 
   215     in
 
   219       fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
 
   216       fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
 
   220     end;
 
   217     end;
 
   221   (* Similar to one in USyntax *)
 
   218   (* Similar to one in USyntax *)
 
   222   fun mk_pair (fst, snd) =
 
   219   fun mk_pair (fst, snd) =
 
   239 in
 
   236 in
 
   240   fold fold_fun tys (Abs ("", tyh, fvs_union))
 
   237   fold fold_fun tys (Abs ("", tyh, fvs_union))
 
   241 end;
 
   238 end;
 
   242 *}
 
   239 *}
 
   243 
   240 
   244 ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}
 
       
   245 
       
   246 (* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
 
   241 (* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
 
   247 ML {*
 
   242 ML {*
 
   248 fun mk_compound_alpha Rs =
 
   243 fun mk_compound_alpha Rs =
 
   249 let
 
   244 let
 
   250   val nos = (length Rs - 1) downto 0;
 
   245   val nos = (length Rs - 1) downto 0;
 
   256   val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
 
   251   val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
 
   257 in
 
   252 in
 
   258   fold fold_fun tys (Abs ("", tyh, abs_rhs))
 
   253   fold fold_fun tys (Abs ("", tyh, abs_rhs))
 
   259 end;
 
   254 end;
 
   260 *}
 
   255 *}
 
   261 
       
   262 ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}
 
       
   263 
   256 
   264 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
   257 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
   265 
   258 
   266 ML {*
 
   259 ML {*
 
   267 fun non_rec_binds l =
 
   260 fun non_rec_binds l =
 
   643 *}
 
   636 *}
 
   644 
   637 
   645 ML {*
 
   638 ML {*
 
   646 fun reflp_tac induct eq_iff ctxt =
 
   639 fun reflp_tac induct eq_iff ctxt =
 
   647   rtac induct THEN_ALL_NEW
 
   640   rtac induct THEN_ALL_NEW
 
   648   simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
 
   641   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
 
   649   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   642   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   650   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   643   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   651      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   644      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   652        add_0_left supp_zero_perm Int_empty_left split_conv})
 
   645        add_0_left supp_zero_perm Int_empty_left split_conv})
 
   653 *}
 
   646 *}
 
   660 in
 
   653 in
 
   661   HOLogic.conj_elims refl_conj
 
   654   HOLogic.conj_elims refl_conj
 
   662 end
 
   655 end
 
   663 *}
 
   656 *}
 
   664 
   657 
   665 ML {*
 
       
   666 fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt  =
 
       
   667 let
 
       
   668   val (fvs_alphas, ls) = split_list fv_alphas_lst;
 
       
   669   val (_, alpha_ts) = split_list fvs_alphas;
 
       
   670   val tys = map (domain_type o fastype_of) alpha_ts;
 
       
   671   val names = Datatype_Prop.make_tnames tys;
 
       
   672   val names2 = Name.variant_list names names;
 
       
   673   val args = map Free (names ~~ tys);
 
       
   674   val args2 = map Free (names2 ~~ tys);
 
       
   675   fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) =
 
       
   676     if l = [] then [] else
 
       
   677     let
 
       
   678       val alpha_bns = map snd l;
 
       
   679       val lhs = alpha $ arg $ arg2;
 
       
   680       val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns);
 
       
   681       val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs);
 
       
   682       fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI}
 
       
   683         THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1
 
       
   684       val th = Goal.prove ctxt (names @ names2) [] gl tac;
 
       
   685     in
 
       
   686       Project_Rule.projects ctxt (1 upto length l) th
 
       
   687     end;
 
       
   688   val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls));
 
       
   689 in
 
       
   690   flat eqs
 
       
   691 end
 
       
   692 *}
 
       
   693 
       
   694 
       
   695 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 
   658 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 
   696 apply (erule exE)
 
   659 apply (erule exE)
 
   697 apply (rule_tac x="-pi" in exI)
 
   660 apply (rule_tac x="-pi" in exI)
 
   698 by auto
 
   661 by auto
 
   699 
   662 
   700 ML {*
 
   663 ML {*
 
   701 fun symp_tac induct inj eqvt ctxt =
 
   664 fun symp_tac induct inj eqvt ctxt =
 
   702   rel_indtac induct THEN_ALL_NEW
 
   665   rel_indtac induct THEN_ALL_NEW
 
   703   simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac
 
   666   simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
 
   704   THEN_ALL_NEW
 
   667   THEN_ALL_NEW
 
   705   REPEAT o etac @{thm exi_neg}
 
   668   REPEAT o etac @{thm exi_neg}
 
   706   THEN_ALL_NEW
 
   669   THEN_ALL_NEW
 
   707   split_conj_tac THEN_ALL_NEW
 
   670   split_conj_tac THEN_ALL_NEW
 
   708   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
 
   671   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
 
   709   TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
 
   672   TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
 
   710   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 
   673   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 
   711 *}
 
   674 *}
 
   712 
   675 
   713 ML {*
 
       
   714 fun imp_elim_tac case_rules =
 
       
   715   Subgoal.FOCUS (fn {concl, context, ...} =>
 
       
   716     case term_of concl of
 
       
   717       _ $ (_ $ asm $ _) =>
 
       
   718         let
 
       
   719           fun filter_fn case_rule = (
 
       
   720             case Logic.strip_assums_hyp (prop_of case_rule) of
 
       
   721               ((_ $ asmc) :: _) =>
 
       
   722                 let
 
       
   723                   val thy = ProofContext.theory_of context
 
       
   724                 in
 
       
   725                   Pattern.matches thy (asmc, asm)
 
       
   726                 end
 
       
   727             | _ => false)
 
       
   728           val matching_rules = filter filter_fn case_rules
 
       
   729         in
 
       
   730          (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
 
       
   731         end
 
       
   732     | _ => no_tac
 
       
   733   )
 
       
   734 *}
 
       
   735 
       
   736 
   676 
   737 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
 
   677 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
 
   738 apply (erule exE)+
 
   678 apply (erule exE)+
 
   739 apply (rule_tac x="pia + pi" in exI)
 
   679 apply (rule_tac x="pia + pi" in exI)
 
   740 by auto
 
   680 by auto
 
   741 
   681 
   742 ML {*
 
   682 
   743 fun is_ex (Const ("Ex", _) $ Abs _) = true
 
   683 ML {*
 
   744   | is_ex _ = false;
 
   684 fun eetac rule = 
   745 *}
 
   685   Subgoal.FOCUS_PARAMS (fn focus =>
 
   746 
   686     let
 
   747 ML {*
 
   687       val concl = #concl focus
 
   748 fun eetac rule = Subgoal.FOCUS_PARAMS 
   688       val prems = Logic.strip_imp_prems (term_of concl)
 
   749   (fn (focus) =>
 
   689       val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
 
   750      let
 
   690       val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
 
   751        val concl = #concl focus
 
   691       val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
 
   752        val prems = Logic.strip_imp_prems (term_of concl)
 
   692     in
 
   753        val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
 
   693       (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
 
   754        val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
 
   694     end
 
   755        val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
 
       
   756      in
 
       
   757      (etac rule THEN' RANGE[
 
       
   758         atac,
 
       
   759         eresolve_tac thins
 
       
   760      ]) 1
 
       
   761      end
 
       
   762   )
 
   695   )
 
   763 *}
 
   696 *}
 
   764 
   697 
   765 ML {*
 
   698 ML {*
 
   766 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
 
   699 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
 
   767   rel_indtac induct THEN_ALL_NEW
 
   700   rel_indtac induct THEN_ALL_NEW
 
   768   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
 
   701   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
 
   769   asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW
 
   702   asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
 
   770   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
 
   703   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
 
   771   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
 
   704   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
 
   772   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
 
   705   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
 
   773   TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
 
   706   TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
 
   774   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 
   707   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 
   811       Goal.prove ctxt [] [] goal tac
 
   744       Goal.prove ctxt [] [] goal tac
 
   812     end
 
   745     end
 
   813 in
 
   746 in
 
   814   map equivp alphas
 
   747   map equivp alphas
 
   815 end
 
   748 end
 
   816 *}
 
       
   817 
       
   818 (*
 
       
   819 Tests:
 
       
   820 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 
       
   821 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
 
       
   822 
       
   823 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 
       
   824 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
 
       
   825 
       
   826 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 
       
   827 by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
 
       
   828 
       
   829 lemma alpha1_equivp:
 
       
   830   "equivp alpha_rtrm1"
 
       
   831   "equivp alpha_bp"
 
       
   832 apply (tactic {*
 
       
   833   (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
 
       
   834   THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
 
       
   835   resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
 
       
   836   THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
 
       
   837   resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
 
       
   838   THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
 
       
   839 )
 
       
   840 1 *})
 
       
   841 done*)
 
       
   842 
       
   843 ML {*
 
       
   844 fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
 
       
   845   | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
 
       
   846   | dtyp_no_of_typ dts (Type (tname, Ts)) =
 
       
   847       case try (find_index (curry op = tname o fst)) dts of
 
       
   848         NONE => error "dtyp_no_of_typ: Illegal recursion"
 
       
   849       | SOME i => i
 
       
   850 *}
 
   749 *}
 
   851 
   750 
   852 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 
   751 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
 
   853 by auto
 
   752 by auto
 
   854 
   753 
  1023 in
 
   922 in
 
  1024   (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
 
   923   (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
 
  1025 end
 
   924 end
 
  1026 *}
 
   925 *}
 
  1027 
   926 
  1028 ML {*
 
   927 end
 
  1029 fun build_rsp_gl alphas fnctn ctxt =
 
       
  1030 let
 
       
  1031   val typ = domain_type (fastype_of fnctn);
 
       
  1032   val (argl, argr) = the (AList.lookup (op=) alphas typ);
 
       
  1033 in
 
       
  1034   ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
 
       
  1035 end
 
       
  1036 *}
 
       
  1037 
       
  1038 ML {*
 
       
  1039 fun fvbv_rsp_tac' simps ctxt =
 
       
  1040   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
 
       
  1041   asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
 
       
  1042   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
 
       
  1043   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
 
       
  1044   TRY o blast_tac (claset_of ctxt)
 
       
  1045 *}
 
       
  1046 
       
  1047 ML {*
 
       
  1048 fun build_fvbv_rsps alphas ind simps fnctns ctxt =
 
       
  1049   prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
 
       
  1050 *}
 
       
  1051 
       
  1052 end
nominal2