(* GDC.ML *) val general_connectives = true ; (* val () = qed_goal_spec_mp "subf_size" GDC.thy "subf sfml fml --> size sfml < size fml" (fn _ => [(case_tac "fml" 1), Auto_tac]) ; val () = qed_goal "subf_irrefl" GDC.thy "~ subf fml fml" (fn _ => [(rtac notI 1), dtac subf_size 1, etac less_irrefl 1]) ; *) AddIffs ipsubfml.intrs ; val ipsubfml_FCE :: nosubfmls = map ipsubfml.mk_cases ["(P, FC conn Ps) : ipsubfml", "(P, FV str) : ipsubfml", "(P, PP str) : ipsubfml"] ; val ipsubfml_simps = tacsthm [(etac ipsubfml_FCE 1), atac 1, Fast_tac 1] iffI :: Seq.list_of (eresolve_tac nosubfmls 1 notI) ; Addsimps ipsubfml_simps ; val () = qed_goalw "child_fmls_simps" GDC.thy [child_fmls_def] "child_fmls (FC conn fmls) = set fmls & \ \ child_fmls (FV str) = {} & child_fmls (PP str) = {}" (fn _ => [ (fast_tac (ces ipsubfml.elims) 1) ]) ; Addsimps [child_fmls_simps] ; val () = qed_goal_spec_mp "ipsubfml_size" GDC.thy "(sfml, fml) : ipsubfml --> size sfml < size fml" (fn _ => [strip_tac 1, (etac ipsubfml.elim 1), Asm_full_simp_tac 1, (etac thin_rl 1), (etac rev_mp 1), (induct_tac "Ps" 1), Auto_tac]) ; val () = qed_goal "wfp_ipsubfml'" GDC.thy "fml : wfp ipsubfml & set fmls <= wfp ipsubfml" (fn _ => [ (induct_tac "fml fmls" 1), (TRYALL (rtac wfp.wfpI)), Auto_tac ]) ; val _ = bind_thm ("wf_ipsubfml", wfp_ipsubfml' RS conjunct1 RS wfp_wfI) ; val () = bind_thm ("ipsubfml_irrefl", wf_ipsubfml RS wf_not_refl) ; AddIffs [wf_ipsubfml, ipsubfml_irrefl] ; (* induction on formulae *) val () = bind_thm ("formula_induct_all", tacthm (eatac Ball_set_ConsI 1 5 THEN Simp_tac 4) formula.induct RS conjunct1) ; val () = bind_thm ("formula_induct_subfml", (hd o msc) (prove_goal GDC.thy "(ALL f. (ALL sf. (sf, f) : ipsubfml --> P sf) --> P f) --> \ \ P f & Ball (set fs) P" (fn _ => [ (rtac impI 1), (induct_tac "f fs" 1), (ALLGOALS Simp_tac), (TRYALL (fast_tac (claset () addSEs ipsubfml.elims)))]))) ;