# HG changeset patch # User berghofe # Date 1161346428 -7200 # Node ID be0a17371ba6eaf9b8f84f906a4324302e4c0976 # Parent ede39342debfc1e25b13b5fc2f6af3893eace64d Proof of "bs # fK bs us vs" no longer depends on FCBs. diff -r ede39342debf -r be0a17371ba6 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Oct 20 11:07:45 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri Oct 20 14:13:48 2006 +0200 @@ -1711,6 +1711,7 @@ val pi1 = map perm_of_pair (boundsl ~~ freshs1); val rpi1 = rev pi1; val pi2 = map perm_of_pair (boundsr ~~ freshs1); + val rpi2 = rev pi2; fun mk_not_sym ths = List.concat (map (fn th => case prop_of th of @@ -1804,42 +1805,38 @@ val ihs = filter (fn th => case prop_of th of _ $ (Const ("All", _) $ _) => true | _ => false) prems'; - (** pi1 o rs = p2 o vs , rs = pi1^-1 o pi2 o vs **) - val _ = warning "step 7: pi1 o rs = p2 o vs , rs = pi1^-1 o pi2 o vs"; - val (rec_eqns1, rec_eqns2) = ListPair.unzip (map (fn (th, ih) => + (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **) + val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs"; + val rec_eqns = map (fn (th, ih) => let val th' = th RS (ih RS spec RS mp) RS sym; val _ $ (_ $ lhs $ rhs) = prop_of th'; fun strip_perm (_ $ _ $ t) = strip_perm t | strip_perm t = t; in - (Goal.prove context'' [] [] + Goal.prove context'' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (foldr (mk_perm []) lhs pi1, foldr (mk_perm []) (strip_perm rhs) pi2))) (fn _ => simp_tac (HOL_basic_ss addsimps - (th' :: perm_swap)) 1), - th') - end) (rec_prems' ~~ ihs)); + (th' :: perm_swap)) 1) + end) (rec_prems' ~~ ihs); - (** as # rs , bs # vs **) - val _ = warning "step 8: as # rs , bs # vs"; - val (rec_freshs1, rec_freshs2) = ListPair.unzip (List.concat - (map (fn (((rec_prem, rec_prem'), eqn), ih) => + (** as # rs **) + val _ = warning "step 8: as # rs"; + val rec_freshs = List.concat + (map (fn (rec_prem, ih) => let val _ $ (S $ x $ (y as Free (_, T))) = prop_of rec_prem; - val _ $ (_ $ _ $ y') = prop_of rec_prem'; val k = find_index (equal S) rec_sets; - val atoms = List.concat (List.mapPartial - (fn ((bs, z), (bs', _)) => - if z = x then NONE else SOME (bs ~~ bs')) - (cargsl' ~~ cargsr')) + val atoms = List.concat (List.mapPartial (fn (bs, z) => + if z = x then NONE else SOME bs) cargsl') in - map (fn (a as Free (_, aT), b) => - let - val l = find_index (equal aT) dt_atomTs; - val th = Goal.prove context'' [] [] + map (fn a as Free (_, aT) => + let val l = find_index (equal aT) dt_atomTs; + in + Goal.prove context'' [] [] (HOLogic.mk_Trueprop (Const ("Nominal.fresh", aT --> T --> HOLogic.boolT) $ a $ y)) (fn _ => EVERY @@ -1847,35 +1844,49 @@ map (fn th => rtac th 1) (snd (List.nth (finite_thss, l))) @ [rtac rec_prem 1, rtac ih 1, - REPEAT_DETERM (resolve_tac fresh_prems 1)])); - val th' = Goal.prove context'' [] [] - (HOLogic.mk_Trueprop (Const ("Nominal.fresh", - aT --> T --> HOLogic.boolT) $ b $ y')) - (fn _ => cut_facts_tac [th] 1 THEN - asm_full_simp_tac (HOL_ss addsimps (eqn :: - fresh_left @ fresh_prems' @ freshs2' @ - rev_simps @ app_simps @ calc_atm)) 1) - in (th, th') end) atoms - end) (rec_prems1 ~~ rec_prems2 ~~ rec_eqns2 ~~ ihs))); + REPEAT_DETERM (resolve_tac fresh_prems 1)])) + end) atoms + end) (rec_prems1 ~~ ihs)); (** as # fK as ts rs , bs # fK bs us vs **) val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs"; - fun prove_fresh_result t (a as Free (_, aT)) = + fun prove_fresh_result (a as Free (_, aT)) = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (Const ("Nominal.fresh", - aT --> rT --> HOLogic.boolT) $ a $ t)) + aT --> rT --> HOLogic.boolT) $ a $ rhs')) (fn _ => EVERY [resolve_tac fcbs 1, REPEAT_DETERM (resolve_tac - (fresh_prems @ rec_freshs1 @ rec_freshs2) 1), + (fresh_prems @ rec_freshs) 1), REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1 THEN resolve_tac rec_prems 1), resolve_tac P_ind_ths 1, REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]); - val fresh_results = - map (prove_fresh_result rhs') (List.concat (map fst cargsl')) @ - map (prove_fresh_result lhs') (List.concat (map fst cargsr')); + val fresh_results'' = map prove_fresh_result boundsl; + + fun prove_fresh_result'' ((a as Free (_, aT), b), th) = + let val th' = Goal.prove context'' [] [] + (HOLogic.mk_Trueprop (Const ("Nominal.fresh", + aT --> rT --> HOLogic.boolT) $ + foldr (mk_perm []) a (rpi2 @ pi1) $ + foldr (mk_perm []) rhs' (rpi2 @ pi1))) + (fn _ => simp_tac (HOL_ss addsimps fresh_bij) 1 THEN + rtac th 1) + in + Goal.prove context'' [] [] + (HOLogic.mk_Trueprop (Const ("Nominal.fresh", + aT --> rT --> HOLogic.boolT) $ b $ lhs')) + (fn _ => EVERY + [cut_facts_tac [th'] 1, + NominalPermeq.perm_simp_tac (HOL_ss addsimps + (rec_eqns @ pi1_pi2_eqs @ perm_swap)) 1, + full_simp_tac (HOL_ss addsimps (calc_atm @ + fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1]) + end; + + val fresh_results = fresh_results'' @ map prove_fresh_result'' + (boundsl ~~ boundsr ~~ fresh_results''); (** cs # fK as ts rs , cs # fK bs us vs **) val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs"; @@ -1902,7 +1913,7 @@ (HOLogic.mk_Trueprop (HOLogic.mk_eq (foldr (mk_perm []) rhs' pi1, foldr (mk_perm []) lhs' pi2))) (fn _ => NominalPermeq.perm_simp_tac (HOL_ss addsimps - pi1_pi2_eqs @ rec_eqns1) 1 THEN + pi1_pi2_eqs @ rec_eqns) 1 THEN TRY (simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));