106 in if member (op =) (permTs_of u) aT andalso aT <> bT then |
106 in if member (op =) (permTs_of u) aT andalso aT <> bT then |
107 let |
107 let |
108 val cp = cp_inst_of thy a b; |
108 val cp = cp_inst_of thy a b; |
109 val dj = dj_thm_of thy b a; |
109 val dj = dj_thm_of thy b a; |
110 val dj_cp' = [cp, dj] MRS dj_cp; |
110 val dj_cp' = [cp, dj] MRS dj_cp; |
111 val cert = SOME o Thm.cterm_of thy |
111 val cert = SOME o Thm.global_cterm_of thy |
112 in |
112 in |
113 SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.ctyp_of thy S)] |
113 SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.global_ctyp_of thy S)] |
114 [cert t, cert r, cert s] dj_cp')) |
114 [cert t, cert r, cert s] dj_cp')) |
115 end |
115 end |
116 else NONE |
116 else NONE |
117 end |
117 end |
118 | perm_simproc' _ _ = NONE; |
118 | perm_simproc' _ _ = NONE; |
775 in (thy', defs @ [def_thm], eqns @ [eqn]) end; |
775 in (thy', defs @ [def_thm], eqns @ [eqn]) end; |
776 |
776 |
777 fun dt_constr_defs ((((((_, (_, _, constrs)), |
777 fun dt_constr_defs ((((((_, (_, _, constrs)), |
778 (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) = |
778 (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) = |
779 let |
779 let |
780 val rep_const = Thm.cterm_of thy |
780 val rep_const = Thm.global_cterm_of thy |
781 (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T')); |
781 (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T')); |
782 val dist = |
782 val dist = |
783 Drule.export_without_context |
783 Drule.export_without_context |
784 (cterm_instantiate |
784 (cterm_instantiate |
785 [(Thm.cterm_of thy distinct_f, rep_const)] Old_Datatype.distinct_lemma); |
785 [(Thm.global_cterm_of thy distinct_f, rep_const)] Old_Datatype.distinct_lemma); |
786 val (thy', defs', eqns') = fold (make_constr_def tname T T') |
786 val (thy', defs', eqns') = fold (make_constr_def tname T T') |
787 (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, []) |
787 (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, []) |
788 in |
788 in |
789 (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) |
789 (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) |
790 end; |
790 end; |
1049 |
1049 |
1050 val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma))); |
1050 val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma))); |
1051 val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else |
1051 val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else |
1052 map (Free o apfst fst o dest_Var) Ps; |
1052 map (Free o apfst fst o dest_Var) Ps; |
1053 val indrule_lemma' = cterm_instantiate |
1053 val indrule_lemma' = cterm_instantiate |
1054 (map (Thm.cterm_of thy8) Ps ~~ map (Thm.cterm_of thy8) frees) indrule_lemma; |
1054 (map (Thm.global_cterm_of thy8) Ps ~~ map (Thm.global_cterm_of thy8) frees) indrule_lemma; |
1055 |
1055 |
1056 val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms; |
1056 val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms; |
1057 |
1057 |
1058 val dt_induct_prop = Old_Datatype_Prop.make_ind descr'; |
1058 val dt_induct_prop = Old_Datatype_Prop.make_ind descr'; |
1059 val dt_induct = Goal.prove_global_future thy8 [] |
1059 val dt_induct = Goal.prove_global_future thy8 [] |
1266 (case Thm.prop_of th of |
1266 (case Thm.prop_of th of |
1267 _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T |
1267 _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T |
1268 | _ => false)) perm_fresh_fresh |
1268 | _ => false)) perm_fresh_fresh |
1269 in |
1269 in |
1270 Drule.instantiate' [] |
1270 Drule.instantiate' [] |
1271 [SOME (Thm.cterm_of thy a), NONE, SOME (Thm.cterm_of thy b)] th |
1271 [SOME (Thm.global_cterm_of thy a), NONE, SOME (Thm.global_cterm_of thy b)] th |
1272 end; |
1272 end; |
1273 |
1273 |
1274 val fs_cp_sort = |
1274 val fs_cp_sort = |
1275 map (fs_class_of thy9) dt_atoms @ |
1275 map (fs_class_of thy9) dt_atoms @ |
1276 maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms; |
1276 maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms; |
1380 REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)] |
1380 REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)] |
1381 end); |
1381 end); |
1382 |
1382 |
1383 val induct_aux' = Thm.instantiate ([], |
1383 val induct_aux' = Thm.instantiate ([], |
1384 map (fn (s, v as Var (_, T)) => |
1384 map (fn (s, v as Var (_, T)) => |
1385 (Thm.cterm_of thy9 v, Thm.cterm_of thy9 (Free (s, T)))) |
1385 (Thm.global_cterm_of thy9 v, Thm.global_cterm_of thy9 (Free (s, T)))) |
1386 (pnames ~~ map head_of (HOLogic.dest_conj |
1386 (pnames ~~ map head_of (HOLogic.dest_conj |
1387 (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @ |
1387 (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @ |
1388 map (fn (_, f) => |
1388 map (fn (_, f) => |
1389 let val f' = Logic.varify_global f |
1389 let val f' = Logic.varify_global f |
1390 in (Thm.cterm_of thy9 f', |
1390 in (Thm.global_cterm_of thy9 f', |
1391 Thm.cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f'))) |
1391 Thm.global_cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f'))) |
1392 end) fresh_fs) induct_aux; |
1392 end) fresh_fs) induct_aux; |
1393 |
1393 |
1394 val induct = Goal.prove_global_future thy9 [] |
1394 val induct = Goal.prove_global_future thy9 [] |
1395 (map (augment_sort thy9 fs_cp_sort) ind_prems) |
1395 (map (augment_sort thy9 fs_cp_sort) ind_prems) |
1396 (augment_sort thy9 fs_cp_sort ind_concl) |
1396 (augment_sort thy9 fs_cp_sort ind_concl) |
1549 val ths' = map (fn ((P, Q), th) => |
1549 val ths' = map (fn ((P, Q), th) => |
1550 Goal.prove_global_future thy11 [] [] |
1550 Goal.prove_global_future thy11 [] [] |
1551 (augment_sort thy1 pt_cp_sort |
1551 (augment_sort thy1 pt_cp_sort |
1552 (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) |
1552 (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) |
1553 (fn {context = ctxt, ...} => dtac (Thm.instantiate ([], |
1553 (fn {context = ctxt, ...} => dtac (Thm.instantiate ([], |
1554 [(Thm.cterm_of thy11 (Var (("pi", 0), permT)), |
1554 [(Thm.global_cterm_of thy11 (Var (("pi", 0), permT)), |
1555 Thm.cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN |
1555 Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN |
1556 NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) |
1556 NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) |
1557 in (ths, ths') end) dt_atomTs); |
1557 in (ths, ths') end) dt_atomTs); |
1558 |
1558 |
1559 (** finite support **) |
1559 (** finite support **) |
1560 |
1560 |
1628 val unique = [unique_prem', unique_prem' RS sym] MRS trans; |
1628 val unique = [unique_prem', unique_prem' RS sym] MRS trans; |
1629 val _ $ (_ $ (_ $ S $ _)) $ _ = Thm.prop_of supports_fresh; |
1629 val _ $ (_ $ (_ $ S $ _)) $ _ = Thm.prop_of supports_fresh; |
1630 val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns') |
1630 val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns') |
1631 in EVERY |
1631 in EVERY |
1632 [rtac (Drule.cterm_instantiate |
1632 [rtac (Drule.cterm_instantiate |
1633 [(Thm.cterm_of thy11 S, |
1633 [(Thm.global_cterm_of thy11 S, |
1634 Thm.cterm_of thy11 (Const (@{const_name Nominal.supp}, |
1634 Thm.global_cterm_of thy11 (Const (@{const_name Nominal.supp}, |
1635 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] |
1635 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] |
1636 supports_fresh) 1, |
1636 supports_fresh) 1, |
1637 simp_tac (put_simpset HOL_basic_ss context addsimps |
1637 simp_tac (put_simpset HOL_basic_ss context addsimps |
1638 [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1, |
1638 [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1, |
1639 REPEAT_DETERM (resolve_tac context [allI, impI] 1), |
1639 REPEAT_DETERM (resolve_tac context [allI, impI] 1), |
1640 REPEAT_DETERM (etac conjE 1), |
1640 REPEAT_DETERM (etac conjE 1), |
1641 rtac unique 1, |
1641 rtac unique 1, |
1642 SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY |
1642 SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY |
1643 [cut_facts_tac [rec_prem] 1, |
1643 [cut_facts_tac [rec_prem] 1, |
1644 rtac (Thm.instantiate ([], |
1644 rtac (Thm.instantiate ([], |
1645 [(Thm.cterm_of thy11 (Var (("pi", 0), mk_permT aT)), |
1645 [(Thm.global_cterm_of thy11 (Var (("pi", 0), mk_permT aT)), |
1646 Thm.cterm_of thy11 |
1646 Thm.global_cterm_of thy11 |
1647 (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1, |
1647 (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1, |
1648 asm_simp_tac (put_simpset HOL_ss context addsimps |
1648 asm_simp_tac (put_simpset HOL_ss context addsimps |
1649 (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1, |
1649 (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1, |
1650 rtac rec_prem 1, |
1650 rtac rec_prem 1, |
1651 simp_tac (put_simpset HOL_ss context addsimps (fs_name :: |
1651 simp_tac (put_simpset HOL_ss context addsimps (fs_name :: |
1669 Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $ |
1669 Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $ |
1670 Abs ("y", U, R $ Free x $ Bound 0)) |
1670 Abs ("y", U, R $ Free x $ Bound 0)) |
1671 (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets); |
1671 (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets); |
1672 |
1672 |
1673 val induct_aux_rec = Drule.cterm_instantiate |
1673 val induct_aux_rec = Drule.cterm_instantiate |
1674 (map (apply2 (Thm.cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort)) |
1674 (map (apply2 (Thm.global_cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort)) |
1675 (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT, |
1675 (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT, |
1676 Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple))) |
1676 Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple))) |
1677 fresh_fs @ |
1677 fresh_fs @ |
1678 map (fn (((P, T), (x, U)), Q) => |
1678 map (fn (((P, T), (x, U)), Q) => |
1679 (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)), |
1679 (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)), |
1859 let |
1859 let |
1860 val U as Type (_, [Type (_, [T, _])]) = fastype_of p; |
1860 val U as Type (_, [Type (_, [T, _])]) = fastype_of p; |
1861 val l = find_index (equal T) dt_atomTs; |
1861 val l = find_index (equal T) dt_atomTs; |
1862 val th = nth (nth rec_equiv_thms' l) k; |
1862 val th = nth (nth rec_equiv_thms' l) k; |
1863 val th' = Thm.instantiate ([], |
1863 val th' = Thm.instantiate ([], |
1864 [(Thm.cterm_of thy11 (Var (("pi", 0), U)), |
1864 [(Thm.global_cterm_of thy11 (Var (("pi", 0), U)), |
1865 Thm.cterm_of thy11 p)]) th; |
1865 Thm.global_cterm_of thy11 p)]) th; |
1866 in rtac th' 1 end; |
1866 in rtac th' 1 end; |
1867 val th' = Goal.prove context'' [] [] |
1867 val th' = Goal.prove context'' [] [] |
1868 (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) |
1868 (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) |
1869 (fn _ => EVERY |
1869 (fn _ => EVERY |
1870 (map eqvt_tac pi @ |
1870 (map eqvt_tac pi @ |