(* note - this file also in some other directories *)
(* stuff relating new rulefs (based on type classes) to old one *)
(* rules like the original rules, calculated from the type class ones *)
(*
set show_sorts ;
reset show_sorts ;
*)
(* following ensures that type structr sequent is seen as in class seqsub
when this theorem is used, eg in seqSubst_in_all RSN (2, derR_sub_a) *)
val seqSubst_in_all = transfer GSub2.thy seqSubst_in_all ;
(* want to get rules about rulefs here, from rules about rulefsc,
and eliminate them from GSub.ML ;
similarly get results from GDT.ML from previous results, and delete them *)
(* now we declare rulefs in GSub1.thy, as the type class version,
so don't want results re rulefsc *)
(*
to get rulefs intrs and elims as previously,
just change the intrs and elim rules as below,
*)
structure rulefs_a = drtsub.rulefs ;
structure rulefs = struct
val note = "structure rulefs redefined in GSub2.ML" ;
val intrs as [iisubI] = [zero_var_indexes (fold_rule [ruleSubst_psc]
(seqSubst_in_all RSN (2, rulefs_a.iisubIa)))] ;
val elims as [elim] =
[tacsthm [(dtac (all_seq_subs_alt RS def_imp_eq RS equalityD1') 2),
clarify_tac set_cs 2, fold_goals_tac [ruleSubst_psc],
prune_params_tac, chop_last (etac thin_rl 2) ] rulefs_a.elim] ;
val elim' = tacthm (dtac sym 2) elim ;
end ;
(* following from GSub.ML *)
(* temporary *)
structure GSub = struct val thy = GSub2.thy end ;
val () = qed_goal_spec_mp "esrmi" GSub.thy
"ruleSubst I_pfs rule : S --> rule : S" (fn _ => [Simp_tac 1]) ;
val () = bind_thm ("rulefs_subI", rulefs.iisubI) ;
val () = bind_thm ("rulefs_invI", rulefs.iisubI) ;
AddSEs [rulefs.iisubI] ;
val () = qed_goal_spec_mp "rulefs_pairI" GSub.thy
"(ps, c) : rls --> (map (seqSubst f) ps, seqSubst f c) : rulefs rls"
(fn _ => [ (rtac impI 1), (dtac rulefs.iisubI 1), Force_tac 1 ]) ;
AddSEs [rulefs_pairI] ;
(* following may be needed in proofs, since the simplifier
sometimes does these automatically *)
val () = qed_goalw_spec_mp "rulefs_sub" GSub.thy [ruleSubst_psc]
"r : rulefs x --> ruleSubst fs r : rulefs x"
(fn _ => [ (rtac impI 1), (etac rulefs_sub_a 1), Simp_tac 1 ]) ;
val () = qed_goal "im_rulefs_sub" GSub.thy
"(ALL sub. ruleSubst sub ` rulefs rules <= rulefs rules)"
(fn _ => [ Safe_tac, (dtac rulefs_sub 1),
(Clarsimp_tac 1), atac 1]) ;
val _ = bind_thm ("im_rulefs_sub'",
rewrite_rule [mk_eq ruleSubst_psc] im_rulefs_sub) ;
val () = qed_goal_spec_mp "rulefs_sub_inv" GSub.thy
"(ALL sub. ruleSubst sub ` rules <= rules) --> rulefs rules = rules"
(fn _ => [ (fast_tac (ces rulefs.elims) 1) ]) ;
val () = qed_goalw "rulefs_mdef" GSub2.thy [meta_eq_def]
"ruleUsed : rulefs {ruleGiven} == (? fs. ruleSubst fs ruleGiven = ruleUsed)"
(fn _ => [(fast_tac (ces rulefs.elims addSIs rulefs.intrs) 1)]) ;